proofs
Provedalphaalpha-core-v0erasuresemantic-refinement

Alpha Core v0: erasure refines the fixture's semantics (source and runtime agree, no effects)

Evaluates⁡ fixture⁡ successor⁡(zero⁡)∧erase⁡([],fixture⁡)=some⁡(runtimeFixture⁡)∧RuntimeEvaluates⁡ runtimeFixture⁡ value⁡(fixtureOutcome⁡)∧effects⁡(fixtureOutcome⁡)=[]\begin{aligned} & \htmlData{mx=6}{\htmlData{mx=1}{\operatorname{Evaluates}}\,\htmlData{mx=2}{\operatorname{fixture}}\,\htmlData{mx=5}{\htmlData{mx=3}{\operatorname{successor}}(\htmlData{mx=4}{\operatorname{zero}})}} \\ & \htmlData{mx=0}{\land} \htmlData{mx=10}{\htmlData{mx=7}{\operatorname{erase}}(\htmlData{mx=8}{\left[ \right]}, \htmlData{mx=9}{\operatorname{fixture}})} \mathrel{\htmlData{mx=14}{=}} \htmlData{mx=13}{\htmlData{mx=11}{\operatorname{some}}(\htmlData{mx=12}{\operatorname{runtimeFixture}})} \\ & \htmlData{mx=0}{\land} \htmlData{mx=20}{\htmlData{mx=15}{\operatorname{RuntimeEvaluates}}\,\htmlData{mx=16}{\operatorname{runtimeFixture}}\,\htmlData{mx=19}{\operatorname{value}\left(\htmlData{mx=18}{\operatorname{fixtureOutcome}}\right)}} \\ & \htmlData{mx=0}{\land} \htmlData{mx=23}{\operatorname{effects}\left(\htmlData{mx=22}{\operatorname{fixtureOutcome}}\right)} \mathrel{\htmlData{mx=25}{=}} \htmlData{mx=24}{\left[ \right]} \end{aligned}
What the notation means · or point at any symbol
Evaluates
Evaluates: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Evaluates)
fixture
fixture: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (fixture)
successor
Term.successor: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Term.successor)
f(x)Function application
Term.successor applied to zero. Lean writes f x; papers write f(x). (Term.successor Term.zero)
zero
Term.zero: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Term.zero)
erase
erase: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (erase)
=Equality
erase([], fixture) and some(runtimeFixture) are the same. (erase [] fixture = some runtimeFixture)
[a, b]List
The list of , in order. ([])
some
some: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (some)
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)
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)
∧And
Both hold: RuntimeEvaluates(runtimeFixture, fixtureOutcome.value), and fixtureOutcome.effects = []. (RuntimeEvaluates runtimeFixture fixture…)
fixtureOutcome
fixtureOutcome: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (fixtureOutcome)
e.fvalue
value of fixtureOutcome: Lean's dot notation e.value means value applied to e. (fixtureOutcome.value)
e.feffects
effects of fixtureOutcome: Lean's dot notation e.effects means effects applied to e. (fixtureOutcome.effects)

The fixture evaluates to 1; erasing it gives the runtime fixture; the runtime fixture evaluates to the recorded outcome's value (1); and that outcome's effect trace is empty — the source and erased programs agree on the frozen fixture.

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
28 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements