Explicit arithmetic witnesses avoid re-running proposal searches in the kernel.

def ConwaySoifer.Certificates.pairCheck (Ps : List IPoint) (den : ℤ) (i j : ℕ) (a b d : ℤ) (fuel : ℕ) : Bool

Check the distance obstruction for two supplied indices, without searching other pairs.

Equations

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

theorem ConwaySoifer.Certificates.pairCheck_sound {U : EquilateralTriangle} {den x : ℝ} {Ps : List IPoint} {caps : List Cap} {ord : Option (Fin 6)} (C : Ctx U den x Ps caps ord) {denI : ℤ} (hden : ↑denI = den) (hdpos : 0 < denI) {i j : ℕ} {a b d : ℤ} (hd : 0 < d) {fuel : ℕ} (h : pairCheck Ps denI i j a b d fuel = true) (hlo : ↑a / ↑d ≤ x) (hhi : x ≤ ↑b / ↑d) : False

@[reducible, inline]

abbrev ConwaySoifer.Certificates.BoundWitness : Type

A support triple, or a request to use the cap checker.

Equations

• ConwaySoifer.Certificates.BoundWitness = Option ConwaySoifer.Certificates.Triple

def ConwaySoifer.Certificates.nodeWitnessCheck (Ps : List IPoint) (den : ℤ) (caps : List Cap) (witness : BoundWitness) (u : IPoint) (a b d : ℤ) (fuel : ℕ) : Bool

Check a supplied support triple or cap obstruction at a single direction.

Equations

• ConwaySoifer.Certificates.nodeWitnessCheck Ps den caps (some T) u a b d fuel = ConwaySoifer.Certificates.supportOK Ps den u T a b d fuel
• ConwaySoifer.Certificates.nodeWitnessCheck Ps den caps none u a b d fuel = ConwaySoifer.Certificates.capNode Ps caps u a b d fuel

def ConwaySoifer.Certificates.coneWitnessCheck (Ps : List IPoint) (den : ℤ) (caps : List Cap) (witness : BoundWitness) (u v : IPoint) (a b d : ℤ) (fuel : ℕ) : Bool

Check one supplied triple at both cone endpoints, or use a cap obstruction.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.coneWitnessCheck Ps den caps none u v a b d fuel = ConwaySoifer.Certificates.capCone Ps caps u v a b d fuel

theorem ConwaySoifer.Certificates.nodeWitnessCheck_sound {U : EquilateralTriangle} {den x : ℝ} {Ps : List IPoint} {caps : List Cap} {ord : Option (Fin 6)} (C : Ctx U den x Ps caps ord) {denI : ℤ} (hden : ↑denI = den) (hdpos : 0 < denI) {witness : BoundWitness} {u : IPoint} {a b d : ℤ} (hd : 0 < d) {fuel : ℕ} (h : nodeWitnessCheck Ps denI caps witness u a b d fuel = true) (hx : 0 < x) (hlo : ↑a / ↑d ≤ x) (hhi : x ≤ ↑b / ↑d) (O : Orientation U) {t : ℝ} (ht : 0 < t) (hdir : O.dir = t • evalF u x) : False

theorem ConwaySoifer.Certificates.coneWitnessCheck_sound {U : EquilateralTriangle} {den x : ℝ} {Ps : List IPoint} {caps : List Cap} {ord : Option (Fin 6)} (C : Ctx U den x Ps caps ord) {denI : ℤ} (hden : ↑denI = den) (hdpos : 0 < denI) {witness : BoundWitness} {u v : IPoint} {a b d : ℤ} (hd : 0 < d) {fuel : ℕ} (h : coneWitnessCheck Ps denI caps witness u v a b d fuel = true) (hx : 0 < x) (hlo : ↑a / ↑d ≤ x) (hhi : x ≤ ↑b / ↑d) (O : Orientation U) {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) (hdir : O.dir = α • evalF u x + β • evalF v x) : False

theorem ConwaySoifer.Certificates.reject_closed_cone {U : EquilateralTriangle} (O : Orientation U) {u v : Point} (hu : ∀ (t : ℝ), 0 < t → O.dir = t • u → False) (hv : ∀ (t : ℝ), 0 < t → O.dir = t • v → False) (huv : ∀ (α β : ℝ), 0 < α → 0 < β → O.dir = α • u + β • v → False) (hdet : 0 ≤ cross u v) (hu' : InArc u) (hu0 : u ≠ 0) (hv' : InArc v) (hv0 : v ≠ 0) (hO : InArc O.dir) (h1 : 0 ≤ cross u O.dir) (h2 : 0 ≤ cross O.dir v) : False

Semantic rejection at both boundary rays and inside a cone covers its closed directions.

inductive ConwaySoifer.Certificates.FanWitness : Type

A finite fan terminating at the fixed 120-degree endpoint, with explicit arithmetic bounds.

• terminal (nodeLeft nodeRight cone : BoundWitness) : FanWitness
• next (direction : IPoint) (node cone : BoundWitness) (rest : FanWitness) : FanWitness

def ConwaySoifer.Certificates.FanWitness.first : FanWitness → BoundWitness

The arithmetic witness at the left boundary of a fan.

Equations

• (ConwaySoifer.Certificates.FanWitness.terminal nodeLeft nodeRight cone).first = nodeLeft
• (ConwaySoifer.Certificates.FanWitness.next direction node cone rest).first = node

def ConwaySoifer.Certificates.FanWitness.check (Ps : List IPoint) (den : ℤ) (caps : List Cap) (a b d : ℤ) (fuel : ℕ) : FanWitness → IPoint → Bool

Verify every fan cone, boundary ray, ordering determinant and intermediate arc condition.

Equations

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

theorem ConwaySoifer.Certificates.FanWitness.first_checked {Ps : List IPoint} {caps : List Cap} {w : FanWitness} {denI a b d : ℤ} {fuel : ℕ} {u : IPoint} (h : check Ps denI caps a b d fuel w u = true) : nodeWitnessCheck Ps denI caps w.first u a b d fuel = true

theorem ConwaySoifer.Certificates.FanWitness.sound {U : EquilateralTriangle} {den x : ℝ} {Ps : List IPoint} {caps : List Cap} {ord : Option (Fin 6)} (C : Ctx U den x Ps caps ord) {denI : ℤ} (hden : ↑denI = den) (hdpos : 0 < denI) {a b d : ℤ} (hd : 0 < d) {fuel : ℕ} (hx : 0 < x) (hlo : ↑a / ↑d ≤ x) (hhi : x ≤ ↑b / ↑d) (O : Orientation U) (hO : InArc O.dir) (w : FanWitness) (u : IPoint) : check Ps denI caps a b d fuel w u = true → InArc (evalF u x) → evalF u x ≠ 0 → 0 ≤ cross (evalF u x) O.dir → 0 ≤ cross O.dir (rot eastDir) → False

theorem ConwaySoifer.Certificates.FanWitness.rejects {U : EquilateralTriangle} {den x : ℝ} {Ps : List IPoint} {caps : List Cap} {ord : Option (Fin 6)} (w : FanWitness) (C : Ctx U den x Ps caps ord) {denI : ℤ} (hden : ↑denI = den) (hdpos : 0 < denI) {a b d : ℤ} (hd : 0 < d) {fuel : ℕ} (h : check Ps denI caps a b d fuel w eastP = true) (hx : 0 < x) (hlo : ↑a / ↑d ≤ x) (hhi : x ≤ ↑b / ↑d) : False