Soundness of the contact-sensitive checker #
The semantic context of one exclusion problem at a real parameter x is Ctx: a triangle U
of positive side < 1 containing the real mandatory points, satisfying the contact condition of
every cap for every orientation of U, and (when ord = some i) the non-overfull condition of
side owner i. The main results are excluded_sound (the checker never accepts a satisfiable
problem) and replay_sound (a checked forced-point trace excludes every configuration whose
initial model holds). Everything is proved from the leaf-test semantics of IntPoly.lean, the
support and contact lemmas of Support.lean, the ray lemmas of Rays.lean and convexity.
Evaluation #
Evaluate both integer-polynomial coordinates at a real interval parameter.
Equations
Instances For
The real point represented by a scaled integer point.
Equations
- ConwaySoifer.Certificates.realPt den P x = den⁻¹ • ConwaySoifer.Certificates.evalF P x
Instances For
The semantic context #
The contact condition of a cap on the face with outward direction n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
ConwaySoifer.Certificates.Ctx
(U : EquilateralTriangle)
(den x : ℝ)
(Ps : List IPoint)
(caps : List Cap)
(ord : Option (Fin 6))
:
The geometric hypotheses of one exclusion problem at parameter x.
Instances For
Support certificates #
theorem
ConwaySoifer.Certificates.HasBound.false
{U : EquilateralTriangle}
{den x : ℝ}
{Ps : List IPoint}
{caps : List Cap}
{ord : Option (Fin 6)}
(C : Ctx U den x Ps caps ord)
(O : Orientation U)
(h : HasBound den Ps x O.dir)
:
A support bound for the real points at the orientation direction is impossible.
theorem
ConwaySoifer.Certificates.supportOK_cone
{x : ℝ}
{Ps : List IPoint}
{denI : ℤ}
(hden : 0 < denI)
{u v : IPoint}
{T : Triple}
{a b d : ℤ}
(hd : 0 < d)
{fuel : ℕ}
(hu : supportOK Ps denI u T a b d fuel = true)
(hv : supportOK Ps denI v T a b d fuel = true)
(hlo : ↑a / ↑d ≤ x)
(hhi : x ≤ ↑b / ↑d)
{α β : ℝ}
(hα : 0 ≤ α)
(hβ : 0 ≤ β)
:
Two support bounds with a common triple propagate to positive combinations.
Contact certificates #
theorem
ConwaySoifer.Certificates.badFace_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)
{e : IPoint}
{c : Cap}
{a b d : ℤ}
(hd : 0 < d)
{fuel : ℕ}
(h : badFace Ps e c a b d fuel = true)
(hx : 0 < x)
(hlo : ↑a / ↑d ≤ x)
(hhi : x ≤ ↑b / ↑d)
{t : ℝ}
(ht : 0 < t)
(hF : FaceOK U den x (t • evalF e x) c)
:
theorem
ConwaySoifer.Certificates.badFaceCone_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)
{eu ev : IPoint}
{c : Cap}
{a b d : ℤ}
(hd : 0 < d)
{fuel : ℕ}
(h : badFaceCone Ps eu ev c a b d fuel = true)
(hx : 0 < x)
(hlo : ↑a / ↑d ≤ x)
(hhi : x ≤ ↑b / ↑d)
{α β : ℝ}
(hα : 0 < α)
(hβ : 0 < β)
(hF : FaceOK U den x (α • evalF eu x + β • evalF ev x) c)
:
theorem
ConwaySoifer.Certificates.capNode_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)
{u : IPoint}
{a b d : ℤ}
(hd : 0 < d)
{fuel : ℕ}
(h : capNode Ps caps 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)
:
theorem
ConwaySoifer.Certificates.capCone_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)
{u v : IPoint}
{a b d : ℤ}
(hd : 0 < d)
{fuel : ℕ}
(h : capCone Ps caps 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)
:
Nodes and cones #
theorem
ConwaySoifer.Certificates.nodeCheck_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)
{N : ℕ}
{u : IPoint}
{a b d : ℤ}
(hd : 0 < d)
{fuel : ℕ}
(h : nodeCheck Ps denI caps N 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)
:
theorem
ConwaySoifer.Certificates.coneCheck_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)
{N : ℕ}
{u v : IPoint}
{a b d : ℤ}
(hd : 0 < d)
{fuel : ℕ}
(h : coneCheck Ps denI caps N 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)
:
The direction of a node lies in the first cone and is nonzero (from nodeCond).
Equations
Instances For
theorem
ConwaySoifer.Certificates.cone_rejects
{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)
{N : ℕ}
{u v : IPoint}
{a b d : ℤ}
(hd : 0 < d)
{fuel : ℕ}
(hx : 0 < x)
(hlo : ↑a / ↑d ≤ x)
(hhi : x ≤ ↑b / ↑d)
(hu : nodeCheck Ps denI caps N u a b d fuel = true)
(hv : nodeCheck Ps denI caps N v a b d fuel = true)
(huv : coneCheck Ps denI caps N u v a b d fuel = true)
(hdet : 0 ≤ cross (evalF u x) (evalF v x))
(hu' : InArc (evalF u x))
(hu0 : evalF u x ≠ 0)
(hv' : InArc (evalF v x))
(hv0 : evalF v x ≠ 0)
(O : Orientation U)
(hO : InArc O.dir)
(h1 : 0 ≤ cross (evalF u x) O.dir)
(h2 : 0 ≤ cross O.dir (evalF v x))
:
Every direction of the closed cone (u, v) is rejected, given that u and v satisfy the
node conditions and the node/cone checks hold.
theorem
ConwaySoifer.Certificates.nodesOK_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)
{N : ℕ}
{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)
(ns : List IPoint)
(u : IPoint)
:
theorem
ConwaySoifer.Certificates.fanCheck_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 : ℕ}
(h : fanCheck Ps denI caps a b d fuel = true)
(hx : 0 < x)
(hlo : ↑a / ↑d ≤ x)
(hhi : x ≤ ↑b / ↑d)
:
Diameter #
theorem
ConwaySoifer.Certificates.diamCheck_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 : ℕ}
(h : diamCheck Ps denI a b d fuel = true)
(hlo : ↑a / ↑d ≤ x)
(hhi : x ≤ ↑b / ↑d)
:
Non-overfull owners #
theorem
ConwaySoifer.Certificates.crossesRay_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 : Fin 6}
{right : Bool}
{A B : IPoint}
(hA : A ∈ Ps)
(hB : B ∈ Ps)
(hv : vertex i ∈ U.carrier)
{a b d : ℤ}
(hd : 0 < d)
{fuel : ℕ}
(h : crossesRay (vertexP denI i) (psub (vertexP denI (neighbor i right)) (vertexP denI i)) A B a b d fuel = true)
(hx : 0 < x)
(hlo : ↑a / ↑d ≤ x)
(hhi : x ≤ ↑b / ↑d)
:
0 < evalR (detP (psub B A) (psub (vertexP denI (neighbor i right)) (vertexP denI i))) x ∧ 0 ≤ evalR (detP (psub B A) (psub A (vertexP denI i))) x ∧ evalR (detP (psub B A) (psub A (vertexP denI i))) x / evalR (detP (psub B A) (psub (vertexP denI (neighbor i right)) (vertexP denI i))) x ≤ rayLen U (vertex i) (sideDirection i right)
A verified crossing pair gives a lower bound for the full ray length.
theorem
ConwaySoifer.Certificates.ordinaryExclusion_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 : Fin 6}
(hi : ord = some i)
{a b d : ℤ}
(hd : 0 < d)
{fuel : ℕ}
(h : ordinaryExclusion Ps denI i a b d fuel = true)
(hx : 0 < x)
(hlo : ↑a / ↑d ≤ x)
(hhi : x ≤ ↑b / ↑d)
:
theorem
ConwaySoifer.Certificates.ordinaryCheck_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 : ℕ}
(h : ordinaryCheck Ps denI ord a b d fuel = true)
(hx : 0 < x)
(hlo : ↑a / ↑d ≤ x)
(hhi : x ≤ ↑b / ↑d)
:
The exclusion decision #
Replay of a forced-point trace #
theorem
ConwaySoifer.Certificates.ModelHolds.ctx
{M : Model}
{T : Configuration}
{den x : ℝ}
(H : ModelHolds M T den x)
(j : Fin 10)
:
theorem
ConwaySoifer.Certificates.mem_thinHullChecked
{L : List IPoint}
{P : IPoint}
(h : P ∈ thinHullChecked L)
:
theorem
ConwaySoifer.Certificates.stepCheck_sound
{M : Model}
{T : Configuration}
{den x : ℝ}
{denI : ℤ}
(hden : ↑denI = den)
(hdpos : 0 < denI)
{st : Step}
{a b d : ℤ}
(hd : 0 < d)
{fuel depth : ℕ}
(h : stepCheck M denI st a b d fuel depth = true)
(hx : 0 < x)
(hlo : ↑a / ↑d ≤ x)
(hhi : x ≤ ↑b / ↑d)
(H : ModelHolds M T den x)
:
ModelHolds (M.insert st) T den x
theorem
ConwaySoifer.Certificates.replay_sound
{T : Configuration}
{den x : ℝ}
{denI : ℤ}
(hden : ↑denI = den)
(hdpos : 0 < denI)
{a b d : ℤ}
(hd : 0 < d)
{fuel depth : ℕ}
(hx : 0 < x)
(hlo : ↑a / ↑d ≤ x)
(hhi : x ≤ ↑b / ↑d)
(steps : List Step)
(M : Model)
(last : Fin 10)
:
replay M denI a b d fuel depth steps last = true → ModelHolds M T den x → False