Provedalphaalpha-core-v0validity

Alpha Core v0: the fixture is valid (well typed at Nat and evaluates)

\htmlData{mx=3}{\htmlData{mx=0}{\operatorname{ValidV0}}\,\htmlData{mx=1}{\operatorname{fixture}}\,\htmlData{mx=2}{\operatorname{fixtureType}}}

What the notation means · or point at any symbol

ValidV0: ValidV0: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (ValidV0)
f(x)Function application: ValidV0 applied to fixture, fixtureType. Lean writes f x; papers write f(x). (ValidV0 fixture fixtureType)
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)
fixtureType: fixtureType: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (fixtureType)

theorem alpha-core-v0-fixture-valid :
    ValidV0 fixture fixtureType

ValidV0 fixture Nat: the fixture infers Nat in the empty context and evaluates to some value.

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: 20 lines of Lean