Provedalphaalpha-core-v0evaluationerasure

Alpha Core v0: the erased runtime fixture evaluates to 1

\htmlData{mx=5}{\htmlData{mx=0}{\operatorname{RuntimeEvaluates}}\,\htmlData{mx=1}{\operatorname{runtimeFixture}}\,\htmlData{mx=4}{\htmlData{mx=2}{\operatorname{successor}}(\htmlData{mx=3}{\operatorname{zero}})}}

What the notation means · or point at any symbol

RuntimeEvaluates: RuntimeEvaluates: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (RuntimeEvaluates)
runtimeFixture: runtimeFixture: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (runtimeFixture)
successor: RuntimeTerm.successor: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (RuntimeTerm.successor)
f(x)Function application: RuntimeTerm.successor applied to zero. Lean writes f x; papers write f(x). (RuntimeTerm.successor RuntimeTerm.zero)
zero: RuntimeTerm.zero: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (RuntimeTerm.zero)

theorem alpha-core-v0-runtime-fixture-evaluates :
    RuntimeEvaluates runtimeFixture (RuntimeTerm.successor RuntimeTerm.zero)

The runtime calculus evaluates the erased fixture (λ¹ value. value) (successor zero) to successor zero.

How it was proved

Proved: 21 October 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 10 lines of Lean