Certificate data and the initial necessary model

CertData is the content of one certificate file (proof/certificates/*.json): the contact case, the interval (lo, hi], the common denominator den, the forced steps and the owner whose final mandatory set is contradictory. initModel rebuilds the initial mandatory sets, caps and non-overfull flags inside Lean, exactly as proof/geometry_model.py does; nothing about them is read from the certificate. Owner indices: 0 = centre, 1..6 = side owners S₀..S₅, 7..9 = corner owners A₀..A₂.

Every initial point is mkPt den lo a b c d, the scaled integer form of the real parametric point (a + c s, b + d s) with s = lo + x; the lists are given explicitly per owner (rawB) so that their geometric meaning can be established by case analysis in ModelSound.lean.

inductive ConwaySoifer.Certificates.Case : Type

The four contact cases used by the rational certificate model.

• Sext : Case
• Sint : Case
• Aown : Case
• Across : Case

@[instance_reducible]

instance ConwaySoifer.Certificates.instDecidableEqCase : DecidableEq Case

Equations

• ConwaySoifer.Certificates.instDecidableEqCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ConwaySoifer.Certificates.instReprCase.repr : Case → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ConwaySoifer.Certificates.instReprCase : Repr Case

Equations

• ConwaySoifer.Certificates.instReprCase = { reprPrec := ConwaySoifer.Certificates.instReprCase.repr }

structure ConwaySoifer.Certificates.CertData : Type

Proposed interval and forced-assignment data; validity is proved separately.

• case : Case

  The normalized contact case covered by the trace.

• lo : ℚ

  The left endpoint of the closed parameter interval.

• hi : ℚ

  The right endpoint of the closed parameter interval.

• den : ℤ

  The positive common scale for integer polynomial coordinates.

• steps : List Step

  The proposed forced-point assignments, in replay order.

• last : Fin 10

  The proposed final obstructed owner; validity checks every owner.

@[instance_reducible]

instance ConwaySoifer.Certificates.instReprCertData : Repr CertData

Equations

• ConwaySoifer.Certificates.instReprCertData = { reprPrec := ConwaySoifer.Certificates.instReprCertData.repr }

def ConwaySoifer.Certificates.instReprCertData.repr : CertData → ℕ → Std.Format

Equations

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

def ConwaySoifer.Certificates.trimKeep (p : IPoly) : IPoly

Trim trailing zero coefficients but keep one coefficient, as exact_polynomials.trim.

Equations

• ConwaySoifer.Certificates.trimKeep p = match ConwaySoifer.Certificates.trimP p with | [] => [0] | q => q

def ConwaySoifer.Certificates.mkPt (den : ℤ) (lo a b c d : ℚ) : Option IPoint

The scaled parametric point ((a + c s), (b + d s)), s = lo + x, as integer polynomials in x; none if a coefficient is not integral.

Equations

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

def ConwaySoifer.Certificates.vQ : Fin 6 → ℚ × ℚ

The six hexagon vertices, three corners and six core directions as rationals.

Equations

• ConwaySoifer.Certificates.vQ = ![(1, 0), (0, 1), (-1, 1), (-1, 0), (0, -1), (1, -1)]

def ConwaySoifer.Certificates.wQ : Fin 3 → ℚ × ℚ

The three target corners as rational coordinate pairs.

Equations

• ConwaySoifer.Certificates.wQ = ![(1, 1), (-2, 1), (1, -2)]

def ConwaySoifer.Certificates.kQ : Fin 6 → ℚ × ℚ

The six adaptive-core directions as rational coordinate pairs.

Equations

• ConwaySoifer.Certificates.kQ = ![(1, 1), (-1, 2), (-2, 1), (-1, -1), (1, -2), (2, -1)]

def ConwaySoifer.Certificates.recvIdx (c : Case) : Fin 6

The side owner index whose section receives the minimal endpoint: 5 (v₅) for Sext, 1 (v₁) otherwise.

Equations

• ConwaySoifer.Certificates.recvIdx c = if c = ConwaySoifer.Certificates.Case.Sext then 5 else 1

def ConwaySoifer.Certificates.Case.isS (c : Case) : Bool

Whether the certificate case has a side-owner receiver.

Equations

• c.isS = (decide (c = ConwaySoifer.Certificates.Case.Sext) || decide (c = ConwaySoifer.Certificates.Case.Sint))

def ConwaySoifer.Certificates.corePts (lo hi : ℚ) (den : ℤ) : List (Option IPoint)

Core vertices ((1-hi) s / 3) K_j.

Equations

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

def ConwaySoifer.Certificates.sidePts (lo : ℚ) (den : ℤ) (i : Fin 6) : List (Option IPoint)

v_i, v_i + s (v_{i-1} - v_i), v_i + s (v_{i+1} - v_i).

Equations

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

def ConwaySoifer.Certificates.cornerPts (lo : ℚ) (den : ℤ) (j : Fin 3) : List (Option IPoint)

w_j, w_j + s (v_{2j} - w_j), w_j + s (v_{2j+1} - w_j).

Equations

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

def ConwaySoifer.Certificates.endpointPt (c : Case) (lo : ℚ) (den : ℤ) : Option IPoint

The minimal endpoint v₀ + s (v_jj - v₀).

Equations

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

def ConwaySoifer.Certificates.exitDirPt (c : Case) (lo : ℚ) (den : ℤ) : Option IPoint

The exit direction v_jj - v₀ (constant).

Equations

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

def ConwaySoifer.Certificates.backDirPt (lo : ℚ) (den : ℤ) : Option IPoint

The direction v₀ - v₁ (constant).

Equations

• ConwaySoifer.Certificates.backDirPt lo den = ConwaySoifer.Certificates.mkPt den lo 1 (-1) 0 0

def ConwaySoifer.Certificates.mid0Pt (lo : ℚ) (den : ℤ) : Option IPoint

The external midpoint M₀ = (1, 1/2).

Equations

• ConwaySoifer.Certificates.mid0Pt lo den = ConwaySoifer.Certificates.mkPt den lo 1 (1 / 2) 0 0

def ConwaySoifer.Certificates.cornerMids (lo : ℚ) (den : ℤ) (j : Fin 3) : List (Option IPoint)

The two external midpoints (w_j + v_{2j}) / 2, (w_j + v_{2j+1}) / 2 of corner cell j.

Equations

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

def ConwaySoifer.Certificates.smallHi (hi : ℚ) : Bool

Whether the small-parameter strengthenings of the model are active.

Equations

• ConwaySoifer.Certificates.smallHi hi = decide (hi ≤ 1 / 14)

def ConwaySoifer.Certificates.rawB (c : Case) (lo hi : ℚ) (den : ℤ) (j : Fin 10) : List (Option IPoint)

The initial mandatory list of owner j, before thinning.

Equations

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

def ConwaySoifer.Certificates.capsOf (c : Case) (e dv bd : IPoint) (j : Fin 10) : List Cap

The caps of owner j: the full endpoint of S₀ (owner 1) and, in the corner cases, the strict exclusion of the endpoint from S₁ (owner 2).

Equations

• ConwaySoifer.Certificates.capsOf c e dv bd j = if ↑j = 1 then [{ p := e, dv := dv, strict := false }] else if ↑j = 2 ∧ (!c.isS) = true then [{ p := e, dv := bd, strict := true }] else []

def ConwaySoifer.Certificates.ordOf (c : Case) (hi : ℚ) (j : Fin 10) : Option (Fin 6)

The non-overfull flags: side owners other than the receiver in the S cases and S₁..S₅ in Aown, only when hi ≤ 1/14.

Equations

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

def ConwaySoifer.Certificates.initModel (c : Case) (lo hi : ℚ) (den : ℤ) : Option Model

Rebuild necessary owner sets, cap constraints and non-overfull flags from a case.

Equations

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

def ConwaySoifer.Certificates.CertData.check (C : CertData) (fuel depth : ℕ) : Bool

The complete check of one certificate: the interval (lo, hi] is encoded as the piece [0, w] with w = hi - lo (the parameter x = s - lo), the model is rebuilt, every forced step is validated and the final mandatory set of last is contradictory.

Equations

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