Untrusted exclusion hints with kernel-checked local arithmetic. The producer chooses a method, fan, or split; soundness does not trust the search.

inductive ConwaySoifer.Certificates.ExclusionHint : Type

A proposed exclusion proof; a split supplies its exact common denominator.

• ordinary : ExclusionHint
• diameter : ExclusionHint
• pair (i j : ℕ) : ExclusionHint
• witnessedFan (witness : FanWitness) : ExclusionHint
• fan (nodes : List IPoint) : ExclusionHint
• split (a mid b den : ℤ) (left right : ExclusionHint) : ExclusionHint

def ConwaySoifer.Certificates.ExclusionHint.check (Ps : List IPoint) (den : ℤ) (caps : List Cap) (ord : Option (Fin 6)) (fuel : ℕ) : ExclusionHint → ℤ → ℤ → ℤ → Bool

Verify a supplied hint without searching for fan directions or split points.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.ExclusionHint.check Ps den caps ord fuel ConwaySoifer.Certificates.ExclusionHint.diameter x✝² x✝¹ x✝ = ConwaySoifer.Certificates.diamCheck Ps den x✝² x✝¹ x✝ fuel
• ConwaySoifer.Certificates.ExclusionHint.check Ps den caps ord fuel (ConwaySoifer.Certificates.ExclusionHint.pair i j) x✝² x✝¹ x✝ = ConwaySoifer.Certificates.pairCheck Ps den i j x✝² x✝¹ x✝ fuel

theorem ConwaySoifer.Certificates.ExclusionHint.sound (hint : ExclusionHint) {Ps : List IPoint} {den : ℤ} {caps : List Cap} {ord : Option (Fin 6)} {fuel : ℕ} (hden : 0 < den) (a b d : ℤ) : 0 < d → check Ps den caps ord fuel hint a b d = true → ∀ (U : EquilateralTriangle) (x : ℝ), 0 < x → ↑a / ↑d ≤ x → x ≤ ↑b / ↑d → Ctx U (↑den) x Ps caps ord → False

Every accepted hint excludes every geometric context on the whole input interval.