Extensional checkpoint lemmas for kernel-checked certificate replay. Concrete checkpoints are untrusted data; every transition is proved in Lean.

theorem ConwaySoifer.Certificates.Model.ext_fields (M N : Model) (hB : ∀ (j : Fin 10), M.B j = N.B j) (hc : ∀ (j : Fin 10), M.caps j = N.caps j) (ho : ∀ (j : Fin 10), M.ord j = N.ord j) : M = N

Two replay models agree when all owner fields agree.

theorem ConwaySoifer.Certificates.initial_checkpoint (o : Option Model) (M : Model) (hs : o.isSome = true) (hB : ∀ (j : Fin 10), (o.getD { B := fun (x : Fin 10) => [], caps := fun (x : Fin 10) => [], ord := fun (x : Fin 10) => none }).B j = M.B j) (hc : ∀ (j : Fin 10), (o.getD { B := fun (x : Fin 10) => [], caps := fun (x : Fin 10) => [], ord := fun (x : Fin 10) => none }).caps j = M.caps j) (ho : ∀ (j : Fin 10), (o.getD { B := fun (x : Fin 10) => [], caps := fun (x : Fin 10) => [], ord := fun (x : Fin 10) => none }).ord j = M.ord j) : o = some M

A concrete model is the initial model if initialization succeeds and each field agrees.

def ConwaySoifer.Certificates.ExcludedOn (Ps : List IPoint) (den : ℤ) (caps : List Cap) (ord : Option (Fin 6)) (a b d : ℤ) : Prop

An exclusion holds for every triangle and parameter in a closed interval.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Certificates.StepValid (M : Model) (den : ℤ) (st : Step) (a b d : ℤ) : Prop

A forced-point step preserves the semantic model throughout the interval.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Certificates.ModelImpossible (M : Model) (den a b d : ℤ) : Prop

A model cannot hold at any positive parameter in the interval.

Equations

• ConwaySoifer.Certificates.ModelImpossible M den a b d = ∀ (T : ConwaySoifer.Configuration) (x : ℝ), 0 < x → ↑a / ↑d ≤ x → x ≤ ↑b / ↑d → ConwaySoifer.Certificates.ModelHolds M T (↑den) x → False

def ConwaySoifer.Certificates.CertData.Valid (C : CertData) : Prop

The same semantic certificate contract as CertData.check_sound.

Equations

• One or more equations did not get rendered due to their size.

theorem ConwaySoifer.Certificates.step_checkpoint (M : Model) (den : ℤ) (st : Step) (a b d : ℤ) (fuel : ℕ) (hden : 0 < den) (hd : 0 < d) (hq : inTarget st.q den a b d fuel = true) (he : ∀ (j : Fin 10), j ≠ st.owner → ExcludedOn (M.B j ++ [st.q]) den (M.caps j) (M.ord j) a b d) : StepValid M den st a b d

Ownership follows from target membership and the rejection of every other owner.

theorem ConwaySoifer.Certificates.replay_checkpoint (M N : Model) (den a b d : ℤ) (st : Step) (hn : M.insert st = N) (hs : StepValid M den st a b d) (ht : ModelImpossible N den a b d) : ModelImpossible M den a b d

Compose a forced step, a checked state equality, and the remaining contradiction.

theorem ConwaySoifer.Certificates.final_checkpoint (M : Model) (den a b d : ℤ) (last : Fin 10) (h : ExcludedOn (M.B last) den (M.caps last) (M.ord last) a b d) : ModelImpossible M den a b d

Excluding the last owner's mandatory points contradicts the final model.

theorem ConwaySoifer.Certificates.certificate_checkpoint (C : CertData) (M : Model) (den b d : ℤ) (hd : 0 < C.den) (hlo : 0 ≤ C.lo) (hlt : C.lo < C.hi) (hhi : C.hi ≤ 11 / 25) (hm : initModel C.case C.lo C.hi C.den = some M) (hden : C.den = den) (hb : (C.hi - C.lo).num = b) (hwidth : ↑(C.hi - C.lo).den = d) (hr : ModelImpossible M den 0 b d) : C.Valid

Assemble the exact original interval contract from the checked initial model.