The initial model follows from the canonical case hypotheses

initModel_holds: if Canonical c T r s (and, when hi ≤ 1/14, SmallStrengthening), then the model rebuilt by initModel for the interval (lo, hi] ∋ s holds for T at x = s - lo. Together with CertData.check_sound this turns every checked certificate into the exclusion of its parameter interval in its contact case.

Evaluation of the constructed points

theorem ConwaySoifer.Certificates.evalR_trimP (p : IPoly) (x : ℝ) : evalR (trimP p) x = evalR p x

theorem ConwaySoifer.Certificates.evalR_trimKeep (p : IPoly) (x : ℝ) : evalR (trimKeep p) x = evalR p x

theorem ConwaySoifer.Certificates.Rat.cast_num_of_den_eq_one {q : ℚ} (h : q.den = 1) : ↑q.num = ↑q

theorem ConwaySoifer.Certificates.realPt_mkPt {denI : ℤ} {lo a b c d : ℚ} {P : IPoint} (h : mkPt denI lo a b c d = some P) (hden : 0 < denI) (x : ℝ) : realPt (↑denI) P x = (↑a + ↑c * (↑lo + x), ↑b + ↑d * (↑lo + x))

The real point represented by mkPt.

theorem ConwaySoifer.Certificates.evalF_mkPt_const {denI : ℤ} {lo a b : ℚ} {P : IPoint} (h : mkPt denI lo a b 0 0 = some P) (x : ℝ) : evalF P x = ↑denI • (↑a, ↑b)

Rational data versus real data

theorem ConwaySoifer.Certificates.vQ_cast (i : Fin 6) : (↑(vQ i).1, ↑(vQ i).2) = vertex i

theorem ConwaySoifer.Certificates.wQ_cast (j : Fin 3) : (↑(wQ j).1, ↑(wQ j).2) = corner j

theorem ConwaySoifer.Certificates.kQ_cast (j : Fin 6) : (↑(kQ j).1, ↑(kQ j).2) = coreDir j

theorem ConwaySoifer.Certificates.recvIdx_eq (c : Case) (cc : ContactCase) : (c = Case.Sext ↔ cc = ContactCase.Sext) → (c = Case.Sint ↔ cc = ContactCase.Sint) → (c = Case.Aown ↔ cc = ContactCase.Aown) → (c = Case.Across ↔ cc = ContactCase.Across) → recvIdx c = neighbor 0 cc.right

def ConwaySoifer.Certificates.Case.toContact : Case → ContactCase

The correspondence between the checker's Case and the geometric ContactCase.

Equations

• ConwaySoifer.Certificates.Case.Sext.toContact = ConwaySoifer.ContactCase.Sext
• ConwaySoifer.Certificates.Case.Sint.toContact = ConwaySoifer.ContactCase.Sint
• ConwaySoifer.Certificates.Case.Aown.toContact = ConwaySoifer.ContactCase.Aown
• ConwaySoifer.Certificates.Case.Across.toContact = ConwaySoifer.ContactCase.Across

theorem ConwaySoifer.Certificates.recvIdx_toContact (c : Case) : recvIdx c = neighbor 0 c.toContact.right

Membership in the raw lists

theorem ConwaySoifer.Certificates.mem_filterMap_id {P : IPoint} {l : List (Option IPoint)} (h : P ∈ List.filterMap id l) : some P ∈ l

theorem ConwaySoifer.Certificates.mem_corePts {lo hi : ℚ} {denI : ℤ} {P : IPoint} (h : some P ∈ corePts lo hi denI) : ∃ (j : Fin 6), mkPt denI lo 0 0 ((1 - hi) * (kQ j).1 / 3) ((1 - hi) * (kQ j).2 / 3) = some P

theorem ConwaySoifer.Certificates.mem_sidePts {lo : ℚ} {denI : ℤ} {i : Fin 6} {P : IPoint} (h : some P ∈ sidePts lo denI i) : mkPt denI lo (vQ i).1 (vQ i).2 0 0 = some P ∨ mkPt denI lo (vQ i).1 (vQ i).2 ((vQ (i + 5)).1 - (vQ i).1) ((vQ (i + 5)).2 - (vQ i).2) = some P ∨ mkPt denI lo (vQ i).1 (vQ i).2 ((vQ (i + 1)).1 - (vQ i).1) ((vQ (i + 1)).2 - (vQ i).2) = some P

theorem ConwaySoifer.Certificates.mem_cornerPts {lo : ℚ} {denI : ℤ} {j : Fin 3} {P : IPoint} (h : some P ∈ cornerPts lo denI j) : mkPt denI lo (wQ j).1 (wQ j).2 0 0 = some P ∨ mkPt denI lo (wQ j).1 (wQ j).2 ((vQ ⟨2 * ↑j, ⋯⟩).1 - (wQ j).1) ((vQ ⟨2 * ↑j, ⋯⟩).2 - (wQ j).2) = some P ∨ mkPt denI lo (wQ j).1 (wQ j).2 ((vQ ⟨2 * ↑j + 1, ⋯⟩).1 - (wQ j).1) ((vQ ⟨2 * ↑j + 1, ⋯⟩).2 - (wQ j).2) = some P

theorem ConwaySoifer.Certificates.mem_cornerMids {lo : ℚ} {denI : ℤ} {j : Fin 3} {P : IPoint} (h : some P ∈ cornerMids lo denI j) : mkPt denI lo (((wQ j).1 + (vQ ⟨2 * ↑j, ⋯⟩).1) / 2) (((wQ j).2 + (vQ ⟨2 * ↑j, ⋯⟩).2) / 2) 0 0 = some P ∨ mkPt denI lo (((wQ j).1 + (vQ ⟨2 * ↑j + 1, ⋯⟩).1) / 2) (((wQ j).2 + (vQ ⟨2 * ↑j + 1, ⋯⟩).2) / 2) 0 0 = some P

theorem ConwaySoifer.Certificates.mem_rawB {c : Case} {lo hi : ℚ} {denI : ℤ} {j : Fin 10} {P : IPoint} (h : some P ∈ rawB c lo hi denI j) : j = 0 ∧ some P ∈ corePts lo hi denI ∨ (∃ (i : Fin 6), j = sideIndex i ∧ (some P ∈ sidePts lo denI i ∨ c.isS = true ∧ i = recvIdx c ∧ some P = endpointPt c lo denI ∨ c = Case.Aown ∧ i = 0 ∧ some P = mid0Pt lo denI ∨ c = Case.Across ∧ i = 1 ∧ some P = mid0Pt lo denI)) ∨ ∃ (k : Fin 3), j = cornerIndex k ∧ (some P ∈ cornerPts lo denI k ∨ c.isS = false ∧ k = 0 ∧ some P = endpointPt c lo denI ∨ c.isS = true ∧ smallHi hi = true ∧ ↑k ≠ ↑(recvIdx c) / 2 ∧ some P ∈ cornerMids lo denI k ∨ c = Case.Aown ∧ smallHi hi = true ∧ k ≠ 0 ∧ some P ∈ cornerMids lo denI k)

Geometric meaning of the constructed points

theorem ConwaySoifer.Certificates.mem_of_le_rayLen' (U : EquilateralTriangle) {v d : Point} (hv : v ∈ U.carrier) (hd : sqDist d (0, 0) = 1) {t : ℝ} (ht : 0 ≤ t) (hle : t ≤ rayLen U v d) : linePoint v d t ∈ U.carrier

theorem ConwaySoifer.Certificates.linePoint_eq_add (v d : Point) (t : ℝ) : linePoint v d t = v + t • d

theorem ConwaySoifer.Certificates.sidePts_mem {T : Configuration} {r s : ℝ} {c : ContactCase} (H : Canonical c T r s) {lo : ℚ} {denI : ℤ} (hden : 0 < denI) {i : Fin 6} {P : IPoint} (h : some P ∈ sidePts lo denI i) : realPt (↑denI) P (s - ↑lo) ∈ (T (sideIndex i)).carrier

The real point of a side list entry.

theorem ConwaySoifer.Certificates.cornerPts_mem {T : Configuration} {r s : ℝ} {c : ContactCase} (H : Canonical c T r s) {lo : ℚ} {denI : ℤ} (hden : 0 < denI) {k : Fin 3} {P : IPoint} (h : some P ∈ cornerPts lo denI k) : realPt (↑denI) P (s - ↑lo) ∈ (T (cornerIndex k)).carrier

theorem ConwaySoifer.Certificates.corePts_mem {T : Configuration} {r s : ℝ} {c : ContactCase} (H : Canonical c T r s) {lo hi : ℚ} {denI : ℤ} (hden : 0 < denI) (hhi : s ≤ ↑hi) (hhi1 : ↑hi ≤ 1) {P : IPoint} (h : some P ∈ corePts lo hi denI) : realPt (↑denI) P (s - ↑lo) ∈ (T 0).carrier

theorem ConwaySoifer.Certificates.endpointPt_real {c : Case} {lo : ℚ} {denI : ℤ} (hden : 0 < denI) {P : IPoint} (h : endpointPt c lo denI = some P) (s : ℝ) : realPt (↑denI) P (s - ↑lo) = minEndpoint c.toContact s

theorem ConwaySoifer.Certificates.mid0Pt_real {lo : ℚ} {denI : ℤ} (hden : 0 < denI) {P : IPoint} (h : mid0Pt lo denI = some P) (x : ℝ) : realPt (↑denI) P x = extMid0

theorem ConwaySoifer.Certificates.cornerMids_real {lo : ℚ} {denI : ℤ} (hden : 0 < denI) {k : Fin 3} {P : IPoint} (h : some P ∈ cornerMids lo denI k) (x : ℝ) : realPt (↑denI) P x = cornerMid k 0 ∨ realPt (↑denI) P x = cornerMid k 1

theorem ConwaySoifer.Certificates.exitDirPt_eval {c : Case} {lo : ℚ} {denI : ℤ} {P : IPoint} (h : exitDirPt c lo denI = some P) (x : ℝ) : evalF P x = ↑denI • sideDirection 0 c.toContact.right

theorem ConwaySoifer.Certificates.backDirPt_eval {lo : ℚ} {denI : ℤ} {P : IPoint} (h : backDirPt lo denI = some P) (x : ℝ) : evalF P x = ↑denI • sideDirection 1 false

theorem ConwaySoifer.Certificates.toContact_isS (c : Case) : c.isS = true ↔ c.toContact.isS

theorem ConwaySoifer.Certificates.sext_k_ne {k : Fin 3} (hk : ↑k ≠ ↑(recvIdx Case.Sext) / 2) : k ≠ 2

theorem ConwaySoifer.Certificates.sint_k_ne {k : Fin 3} (hk : ↑k ≠ ↑(recvIdx Case.Sint) / 2) : k ≠ 0

theorem ConwaySoifer.Certificates.sext_i_ne {i : Fin 6} (h : ¬i = recvIdx Case.Sext) : i ≠ 5

theorem ConwaySoifer.Certificates.sint_i_ne {i : Fin 6} (h : ¬i = recvIdx Case.Sint) : i ≠ 1

theorem ConwaySoifer.Certificates.smallMids_sext {T : Configuration} {r : ℝ} (hs : SmallStrengthening ContactCase.Sext T r) {k : Fin 3} (hk : k ≠ 2) (m : Fin 2) : cornerMid k m ∈ (T (cornerIndex k)).carrier

theorem ConwaySoifer.Certificates.smallMids_sint {T : Configuration} {r : ℝ} (hs : SmallStrengthening ContactCase.Sint T r) {k : Fin 3} (hk : k ≠ 0) (m : Fin 2) : cornerMid k m ∈ (T (cornerIndex k)).carrier

theorem ConwaySoifer.Certificates.smallMids_aown {T : Configuration} {r : ℝ} (hs : SmallStrengthening ContactCase.Aown T r) {k : Fin 3} (hk : k ≠ 0) (m : Fin 2) : cornerMid k m ∈ (T (cornerIndex k)).carrier

theorem ConwaySoifer.Certificates.smallOrd_sext {T : Configuration} {r : ℝ} (hs : SmallStrengthening ContactCase.Sext T r) {i : Fin 6} (hi : i ≠ 5) : rayLen (T (sideIndex i)) (vertex i) (sideDirection i false) + rayLen (T (sideIndex i)) (vertex i) (sideDirection i true) ≤ r

theorem ConwaySoifer.Certificates.smallOrd_sint {T : Configuration} {r : ℝ} (hs : SmallStrengthening ContactCase.Sint T r) {i : Fin 6} (hi : i ≠ 1) : rayLen (T (sideIndex i)) (vertex i) (sideDirection i false) + rayLen (T (sideIndex i)) (vertex i) (sideDirection i true) ≤ r

theorem ConwaySoifer.Certificates.smallOrd_aown {T : Configuration} {r : ℝ} (hs : SmallStrengthening ContactCase.Aown T r) {i : Fin 6} (hi : i ≠ 0) : rayLen (T (sideIndex i)) (vertex i) (sideDirection i false) + rayLen (T (sideIndex i)) (vertex i) (sideDirection i true) ≤ r

theorem ConwaySoifer.Certificates.ordOf_some {c : Case} {hi : ℚ} {j : Fin 10} {i : Fin 6} (h : ordOf c hi j = some i) : smallHi hi = true ∧ j = sideIndex i ∧ (c = Case.Sext → i ≠ 5) ∧ (c = Case.Sint → i ≠ 1) ∧ (c = Case.Aown → i ≠ 0) ∧ c ≠ Case.Across

The main theorem

theorem ConwaySoifer.Certificates.initModel_holds {T : Configuration} {r s : ℝ} {c : Case} {lo hi : ℚ} {denI : ℤ} {M : Model} (hM : initModel c lo hi denI = some M) (hden : 0 < denI) (hhi1 : ↑hi ≤ 1) (H : Canonical c.toContact T r s) (hhi : s ≤ ↑hi) (hsmall : smallHi hi = true → SmallStrengthening c.toContact T r) : ModelHolds M T (↑denI) (s - ↑lo)