The contact-sensitive exclusion checker (computable part)

All data are integer polynomials in one real parameter x (the offset s - lo of the covering parameter from the left end of a certificate interval), lowest degree first. A point P : IPoint denotes the real point (1/den) • (P.1(x), P.2(x)). A Cap records a contact constraint: the real point p/den is a full ray endpoint with exit direction dv (strict = false) or a forbidden point on a positive ray from a mandatory point (strict = true).

excluded Ps den caps ord a b d fuel depth decides, for the parameter piece [a/d, b/d], whether no equilateral triangle of side < 1 can contain all points of Ps while satisfying the caps and (for ord = some i) the non-overfull condition of side owner i. Its structure mirrors tools/proto_checker.py (the untrusted Python reference model):

• ordinaryExclusion: segments between mandatory points cross the two boundary rays of vertex i and give lower bounds whose sum reaches 1;
• a pair of mandatory points at distance ≥ 1;
• fanCheck: the closed 120-degree cone from east = (1, 0) to rot east = (-1, 1) (which contains one of the three outward edge directions of every triangle) is cut by a list of candidate directions into consecutive cones; every node and every cone is certified either by a support triple (side ≥ 1) or by the impossibility of every cap on all three faces;
• on failure the parameter piece is split at a rational knot and both halves are checked.

Only the leaf tests (nonnegOn, posOn) and the chain structure are used by the soundness proofs in CheckerSound.lean; everything else (choice of nodes, triples, knots) is untrusted search executed inside the checker.

@[reducible, inline]

abbrev ConwaySoifer.Certificates.IPoint : Type

A point whose two coordinates are integer polynomials in the interval parameter.

Equations

• ConwaySoifer.Certificates.IPoint = (ConwaySoifer.Certificates.IPoly × ConwaySoifer.Certificates.IPoly)

@[reducible, inline]

abbrev ConwaySoifer.Certificates.Triple : Type

Indices of the three mandatory points used by a support bound.

Equations

• ConwaySoifer.Certificates.Triple = (ℕ × ℕ × ℕ)

structure ConwaySoifer.Certificates.Cap : Type

An endpoint or forbidden-point constraint, with an exit direction and strictness flag.

• p : IPoint

  The polynomial contact point.

• dv : IPoint

  The positive exit direction at the contact point.

• strict : Bool

  Whether the contact point is forbidden rather than a closed endpoint.

def ConwaySoifer.Certificates.instReprCap.repr : Cap → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ConwaySoifer.Certificates.instReprCap : Repr Cap

Equations

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

def ConwaySoifer.Certificates.instDecidableEqCap.decEq (x✝ x✝¹ : Cap) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance ConwaySoifer.Certificates.instDecidableEqCap : DecidableEq Cap

Equations

• ConwaySoifer.Certificates.instDecidableEqCap = ConwaySoifer.Certificates.instDecidableEqCap.decEq

Polynomial geometry

def ConwaySoifer.Certificates.detP (u v : IPoint) : IPoly

The determinant polynomial of two polynomial points.

Equations

• ConwaySoifer.Certificates.detP u v = (u.1.mul v.2).sub (u.2.mul v.1)

def ConwaySoifer.Certificates.normP (u : IPoint) : IPoly

The squared Euclidean norm polynomial in triangular coordinates.

Equations

• ConwaySoifer.Certificates.normP u = ((u.1.mul u.1).add (u.1.mul u.2)).add (u.2.mul u.2)

def ConwaySoifer.Certificates.rotP (u : IPoint) : IPoint

Rotation through 120 degrees in polynomial triangular coordinates.

Equations

• ConwaySoifer.Certificates.rotP u = ((ConwaySoifer.Certificates.IPoly.smul (-1) u.1).sub u.2, u.1)

def ConwaySoifer.Certificates.negP (u : IPoint) : IPoint

Negation of both polynomial coordinates.

Equations

• ConwaySoifer.Certificates.negP u = (ConwaySoifer.Certificates.IPoly.smul (-1) u.1, ConwaySoifer.Certificates.IPoly.smul (-1) u.2)

def ConwaySoifer.Certificates.psub (p q : IPoint) : IPoint

Coordinatewise subtraction of polynomial points.

Equations

• ConwaySoifer.Certificates.psub p q = (p.1.sub q.1, p.2.sub q.2)

def ConwaySoifer.Certificates.padd (p q : IPoint) : IPoint

Coordinatewise addition of polynomial points.

Equations

• ConwaySoifer.Certificates.padd p q = (p.1.add q.1, p.2.add q.2)

def ConwaySoifer.Certificates.eastP : IPoint

The constant east direction in polynomial coordinates.

Equations

• ConwaySoifer.Certificates.eastP = ([1], [0])

def ConwaySoifer.Certificates.rotEastP : IPoint

The constant direction obtained by rotating east through 120 degrees.

Equations

• ConwaySoifer.Certificates.rotEastP = ([-1], [1])

def ConwaySoifer.Certificates.supportNumP (u P₀ P₁ P₂ : IPoint) : IPoly

The sum of support determinants for three successive orientation normals.

Equations

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

def ConwaySoifer.Certificates.gapP (den : ℤ) (u P₀ P₁ P₂ : IPoint) : IPoly

N² - den² |u|²: nonnegative together with N ≥ 0 iff the side bound is at least one.

Equations

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

def ConwaySoifer.Certificates.nth {α : Type} : List α → ℕ → Option α

A structural, optional lookup used by the verified support checker.

Equations

• ConwaySoifer.Certificates.nth [] x✝ = none
• ConwaySoifer.Certificates.nth (a :: tail) 0 = some a
• ConwaySoifer.Certificates.nth (head :: l) n.succ = ConwaySoifer.Certificates.nth l n

Trusted leaf tests

def ConwaySoifer.Certificates.supportOK (Ps : List IPoint) (den : ℤ) (u : IPoint) (T : Triple) (a b d : ℤ) (fuel : ℕ) : Bool

Check a supplied support triple over the complete rational parameter interval.

Equations

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

def ConwaySoifer.Certificates.badFace (Ps : List IPoint) (e : IPoint) (c : Cap) (a b d : ℤ) (fuel : ℕ) : Bool

Face e cannot be the contact face of cap c anywhere on the piece.

Equations

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

def ConwaySoifer.Certificates.badFaceCone (Ps : List IPoint) (eu ev : IPoint) (c : Cap) (a b d : ℤ) (fuel : ℕ) : Bool

Faces a • eu + b • ev (a, b > 0) cannot be the contact face of cap c.

Equations

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

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

Check that one cap rejects all three contact faces at one orientation direction.

Equations

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

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

Check that one cap rejects all contact faces throughout a positive orientation cone.

Equations

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

Untrusted search helpers

def ConwaySoifer.Certificates.maxLen : List IPoint → ℕ

The maximum coefficient-list length among all polynomial point coordinates.

Equations

• ConwaySoifer.Certificates.maxLen [] = 0
• ConwaySoifer.Certificates.maxLen (P :: Ps) = max (max (List.length P.1) (List.length P.2)) (ConwaySoifer.Certificates.maxLen Ps)

def ConwaySoifer.Certificates.argmaxAux : List ℤ → ℕ → ℕ → ℤ → ℕ

Track the first largest value while scanning values with their indices.

Equations

• ConwaySoifer.Certificates.argmaxAux [] x✝² x✝¹ x✝ = x✝¹
• ConwaySoifer.Certificates.argmaxAux (v :: vs) x✝² x✝¹ x✝ = if x✝ < v then ConwaySoifer.Certificates.argmaxAux vs (x✝² + 1) x✝² v else ConwaySoifer.Certificates.argmaxAux vs (x✝² + 1) x✝¹ x✝

def ConwaySoifer.Certificates.argmax : List ℤ → ℕ

The first index attaining the largest value, or zero for an empty list.

Equations

• ConwaySoifer.Certificates.argmax [] = 0
• ConwaySoifer.Certificates.argmax (v :: vs) = ConwaySoifer.Certificates.argmaxAux vs 1 0 v

def ConwaySoifer.Certificates.maxIndex (Ps : List IPoint) (l : IPoint) (num den : ℤ) (N2 : ℕ) : ℕ

Select a point with the largest exact support determinant at a rational parameter.

Equations

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

def ConwaySoifer.Certificates.tripleAt (Ps : List IPoint) (N : ℕ) (u : IPoint) (num den : ℤ) : Triple

The maximising triple for direction u at the parameter num/den.

Equations

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

def ConwaySoifer.Certificates.supportNode (Ps : List IPoint) (den : ℤ) (N : ℕ) (u : IPoint) (a b d : ℤ) (fuel : ℕ) : Bool

Try support triples selected at the midpoint and endpoints of one interval.

Equations

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

def ConwaySoifer.Certificates.supportCone (Ps : List IPoint) (den : ℤ) (N : ℕ) (u v : IPoint) (a b d : ℤ) (fuel : ℕ) : Bool

Try one common support triple at both endpoints of an orientation cone.

Equations

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

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

Reject a direction using either a support bound or a cap.

Equations

• ConwaySoifer.Certificates.nodeCheck Ps den caps N u a b d fuel = (ConwaySoifer.Certificates.supportNode Ps den N u a b d fuel || ConwaySoifer.Certificates.capNode Ps caps u a b d fuel)

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

Reject a positive orientation cone using a common support triple or a cap.

Equations

• ConwaySoifer.Certificates.coneCheck Ps den caps N u v a b d fuel = (ConwaySoifer.Certificates.supportCone Ps den N u v a b d fuel || ConwaySoifer.Certificates.capCone Ps caps u v a b d fuel)

def ConwaySoifer.Certificates.nodeCond (u : IPoint) (a b d : ℤ) (fuel : ℕ) : Bool

A node must be nonzero and lie in the closed cone from east to rot east on the piece.

Equations

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

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

nodesOK … u ns: the consecutive cones (u, v₁), (v₁, v₂), … up to rot east all pass, consecutive determinants are nonnegative on the piece, and every intermediate node satisfies nodeCond.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.nodesOK Ps den caps N a b d fuel x✝ [] = false

Candidate nodes (untrusted)

def ConwaySoifer.Certificates.sixDirs (e : IPoint) : List IPoint

The six rotations and opposite rays generated by a polynomial direction.

Equations

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

def ConwaySoifer.Certificates.pairDirs : List IPoint → List IPoint

Differences of every unordered pair of mandatory polynomial points.

Equations

• ConwaySoifer.Certificates.pairDirs [] = []
• ConwaySoifer.Certificates.pairDirs (P :: Ps) = List.map (fun (Q : ConwaySoifer.Certificates.IPoint) => ConwaySoifer.Certificates.psub Q P) Ps ++ ConwaySoifer.Certificates.pairDirs Ps

def ConwaySoifer.Certificates.candidateDirs (Ps : List IPoint) (caps : List Cap) : List IPoint

Candidate fan directions obtained from point differences and cap constraints.

Equations

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

@[reducible, inline]

abbrev ConwaySoifer.Certificates.RayV : Type

A polynomial direction paired with its exact integer evaluation.

Equations

• ConwaySoifer.Certificates.RayV = (ConwaySoifer.Certificates.IPoint × ℤ × ℤ)

def ConwaySoifer.Certificates.evalRay (num den : ℤ) (N : ℕ) (r : IPoint) : RayV

Pair a polynomial ray with its scaled rational-coordinate evaluation.

Equations

• ConwaySoifer.Certificates.evalRay num den N r = (r, ConwaySoifer.Certificates.evalScaledN r.1 num den N, ConwaySoifer.Certificates.evalScaledN r.2 num den N)

def ConwaySoifer.Certificates.det2 (u v : ℤ × ℤ) : ℤ

The determinant of two integer coordinate vectors.

Equations

• ConwaySoifer.Certificates.det2 u v = u.1 * v.2 - u.2 * v.1

def ConwaySoifer.Certificates.merge {α : Type} (lt : α → α → Bool) : ℕ → List α → List α → List α

Fuel-bounded merge of two lists using a Boolean ordering test.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.merge lt 0 x✝¹ x✝ = x✝¹ ++ x✝
• ConwaySoifer.Certificates.merge lt n.succ [] x✝ = x✝
• ConwaySoifer.Certificates.merge lt n.succ x✝ [] = x✝

def ConwaySoifer.Certificates.msort {α : Type} (lt : α → α → Bool) : ℕ → List α → List α

Fuel-bounded merge sort used only to propose certificate data.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.msort lt 0 x✝ = x✝
• ConwaySoifer.Certificates.msort lt fuel.succ [] = []
• ConwaySoifer.Certificates.msort lt fuel.succ [x_2] = [x_2]

def ConwaySoifer.Certificates.dedupe (prev : ℤ × ℤ) : List RayV → List RayV

Remove consecutive parallel evaluated directions.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.dedupe prev [] = []

def ConwaySoifer.Certificates.robustFilter (a b d : ℤ) (fuel : ℕ) : IPoint → List IPoint → List IPoint

Keep a node only when the trusted conditions with the previously kept node hold.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.robustFilter a b d fuel x✝ [] = []

def ConwaySoifer.Certificates.quadNodes (Ps : List IPoint) (caps : List Cap) (N : ℕ) (a b d : ℤ) (fuel : ℕ) : List IPoint

Propose ordered fan nodes from exact midpoint evaluations and interval tests.

Equations

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

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

Check the proposed fan across the closed 120-degree orientation arc.

Equations

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

Non-overfull owners

def ConwaySoifer.Certificates.vertexP (den : ℤ) : Fin 6 → IPoint

den • vertex i.

Equations

• ConwaySoifer.Certificates.vertexP den = ![([den], [0]), ([0], [den]), ([-den], [den]), ([-den], [0]), ([0], [-den]), ([den], [-den])]

def ConwaySoifer.Certificates.crossesRay (v dvec A B : IPoint) (a b d : ℤ) (fuel : ℕ) : Bool

The segment [A, B] crosses the ray from v in direction dvec (all conditions on the piece): dd > 0, 0 ≤ mu ≤ dd (crossing parameter inside the segment) and nm ≥ 0 (nonnegative ray parameter nm/dd).

Equations

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

def ConwaySoifer.Certificates.rayBounds (Ps : List IPoint) (v dvec : IPoint) (a b d : ℤ) (fuel : ℕ) : List (IPoint × IPoint)

Candidate crossing pairs (untrusted pruning; everything is re-verified in rayBoundsSum).

Equations

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

def ConwaySoifer.Certificates.rayBoundsSum (Ps : List IPoint) (v dv₁ dv₂ : IPoint) (L R : List (IPoint × IPoint)) (a b d : ℤ) (fuel : ℕ) : Bool

Trusted: two crossing pairs (points of Ps) whose lower bounds nm₁/dd₁ + nm₂/dd₂ reach 1 on the whole piece.

Equations

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

def ConwaySoifer.Certificates.bestBounds (v dvec : IPoint) (bs : List (IPoint × IPoint)) (num dd : ℤ) (N2 : ℕ) : List (IPoint × IPoint)

Best four pairs by the value of the bound at the midpoint (untrusted pruning).

Equations

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

def ConwaySoifer.Certificates.ordinaryExclusion (Ps : List IPoint) (den : ℤ) (i : Fin 6) (a b d : ℤ) (fuel : ℕ) : Bool

Check an exclusion using the side-owner non-overfull condition.

Equations

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

def ConwaySoifer.Certificates.ordinaryCheck (Ps : List IPoint) (den : ℤ) (ord : Option (Fin 6)) (a b d : ℤ) (fuel : ℕ) : Bool

Apply the non-overfull exclusion when an owner flag is present.

Equations

• ConwaySoifer.Certificates.ordinaryCheck Ps den none a b d fuel = false
• ConwaySoifer.Certificates.ordinaryCheck Ps den (some i) a b d fuel = ConwaySoifer.Certificates.ordinaryExclusion Ps den i a b d fuel

Diameter

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

Search for a pair whose certified separation excludes a subunit triangle.

Equations

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

Rational split points (untrusted)

def ConwaySoifer.Certificates.mkIRat (n m : ℤ) : IRat

A rational as a pair with positive denominator.

Equations

• ConwaySoifer.Certificates.mkIRat n m = if m < 0 then (-n, -m) else (n, m)

def ConwaySoifer.Certificates.trimP : IPoly → IPoly

Remove trailing zero coefficients from an integer polynomial.

Equations

• ConwaySoifer.Certificates.trimP [] = []
• ConwaySoifer.Certificates.trimP (c :: p) = match ConwaySoifer.Certificates.trimP p with | [] => if c = 0 then [] else [c] | q => c :: q

def ConwaySoifer.Certificates.derivAux : ℕ → IPoly → IPoly

Differentiate successive coefficients starting at a specified degree.

Equations

• ConwaySoifer.Certificates.derivAux x✝ [] = []
• ConwaySoifer.Certificates.derivAux x✝ (c :: p) = ↑x✝ * c :: ConwaySoifer.Certificates.derivAux (x✝ + 1) p

def ConwaySoifer.Certificates.derivP : IPoly → IPoly

Differentiate an integer coefficient list.

Equations

• ConwaySoifer.Certificates.derivP [] = []
• ConwaySoifer.Certificates.derivP (c :: p) = ConwaySoifer.Certificates.derivAux 1 p

def ConwaySoifer.Certificates.qtrim : List ℚ → List ℚ

Remove trailing zeros from a rational coefficient list.

Equations

• ConwaySoifer.Certificates.qtrim [] = []
• ConwaySoifer.Certificates.qtrim (c :: p) = match ConwaySoifer.Certificates.qtrim p with | [] => if c = 0 then [] else [c] | q => c :: q

def ConwaySoifer.Certificates.qstep (a b : List ℚ) : List ℚ

One Euclidean step a - c x ^ k b where c = lead a / lead b, k = deg a - deg b.

Equations

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

def ConwaySoifer.Certificates.qremAux : ℕ → List ℚ → List ℚ → List ℚ

Fuel-bounded polynomial remainder calculation over rational coefficients.

Equations

• ConwaySoifer.Certificates.qremAux 0 x✝¹ x✝ = x✝¹
• ConwaySoifer.Certificates.qremAux k.succ x✝¹ x✝ = if x✝¹.length < x✝.length then x✝¹ else ConwaySoifer.Certificates.qremAux k (ConwaySoifer.Certificates.qstep x✝¹ x✝) x✝

def ConwaySoifer.Certificates.qrem (a b : List ℚ) : List ℚ

A proposed rational polynomial remainder, with a degree-based fuel bound.

Equations

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

def ConwaySoifer.Certificates.qgcd : ℕ → List ℚ → List ℚ → List ℚ

Fuel-bounded rational polynomial Euclidean algorithm used by the untrusted search.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.qgcd 0 x✝¹ x✝ = x✝¹

def ConwaySoifer.Certificates.ratRootsAux : ℕ → IPoly → List IRat

All rational roots of a polynomial of degree at most two (integer square root test), and the rational roots of gcd(p, p') for higher degrees (double roots). Fuel-bounded.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.ratRootsAux 0 x✝ = []

def ConwaySoifer.Certificates.ratRoots (p : IPoly) : List IRat

Propose rational roots using a degree-based recursion budget.

Equations

• ConwaySoifer.Certificates.ratRoots p = ConwaySoifer.Certificates.ratRootsAux (List.length p) p

def ConwaySoifer.Certificates.iratLt (x y : IRat) : Bool

Rational comparison n₁/m₁ < n₂/m₂ for positive denominators.

Equations

• ConwaySoifer.Certificates.iratLt x y = decide (x.1 * y.2 < y.1 * x.2)

def ConwaySoifer.Certificates.iratEq (x y : IRat) : Bool

Compare rational pairs by cross multiplication; denominators are assumed positive.

Equations

• ConwaySoifer.Certificates.iratEq x y = decide (x.1 * y.2 = y.1 * x.2)

def ConwaySoifer.Certificates.rootsInside (p : IPoly) (a b d : ℤ) : List IRat

Roots strictly inside (a/d, b/d).

Equations

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

def ConwaySoifer.Certificates.dedupeRats (l : List IRat) : List IRat

Keep the first occurrence of each cross-multiplication equivalence class.

Equations

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

def ConwaySoifer.Certificates.knots (Ps : List IPoint) (caps : List Cap) (a b d : ℤ) : List IRat

Candidate knots: switch parameters of support values, sign changes of contact polynomials and crossings of candidate directions.

Equations

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

def ConwaySoifer.Certificates.splitPoint (Ps : List IPoint) (caps : List Cap) (a b d : ℤ) : IRat

Split point: the knot closest to the midpoint, else the midpoint.

Equations

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

The exclusion decision

def ConwaySoifer.Certificates.splitPieces (a b d : ℤ) (r : IRat) : List (ℤ × ℤ × ℤ)

Split [a/d, b/d] at n/m (with a/d < n/m < b/d) into two pieces.

Equations

• ConwaySoifer.Certificates.splitPieces a b d r = ConwaySoifer.Certificates.piecesOf a b d [r]

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

Try geometric exclusions and recursively proposed rational interval splits.

Equations

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

Point sets: the ordered-field thinning of the reference verifier

def ConwaySoifer.Certificates.firstSign : IPoly → ℤ

The sign of the first nonzero coefficient, or zero for a zero coefficient list.

Equations

• ConwaySoifer.Certificates.firstSign [] = 0
• ConwaySoifer.Certificates.firstSign (c :: p) = if 0 < c then 1 else if c < 0 then -1 else ConwaySoifer.Certificates.firstSign p

def ConwaySoifer.Certificates.cmpPt (x y : IPoint) : ℤ

Compare polynomial points lexicographically by the first nonzero coefficient difference.

Equations

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

def ConwaySoifer.Certificates.sortPts (Ps : List IPoint) : List IPoint

Sort polynomial points using their coefficient comparison.

Equations

• ConwaySoifer.Certificates.sortPts Ps = ConwaySoifer.Certificates.msort (fun (x y : ConwaySoifer.Certificates.IPoint) => decide (ConwaySoifer.Certificates.cmpPt x y < 0)) (Ps.length + 1) Ps

def ConwaySoifer.Certificates.dedupePts (l : List IPoint) : List IPoint

Retain the first point in each coefficient-comparison equivalence class.

Equations

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

def ConwaySoifer.Certificates.halfHullAux : ℕ → List IPoint → List IPoint → List IPoint

Stack scan with a structural recursion budget. Each transition decreases out.length + 2 * rest.length, so that measure suffices for the complete scan.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.halfHullAux 0 x✝¹ x✝ = x✝¹
• ConwaySoifer.Certificates.halfHullAux n.succ x✝ [] = x✝
• ConwaySoifer.Certificates.halfHullAux fuel.succ x✝ (q :: rest) = ConwaySoifer.Certificates.halfHullAux fuel (q :: x✝) rest

def ConwaySoifer.Certificates.halfHull (out rest : List IPoint) : List IPoint

Complete half-hull scan; the budget bounds stack transitions, not input size.

Equations

• ConwaySoifer.Certificates.halfHull out rest = ConwaySoifer.Certificates.halfHullAux (out.length + 2 * rest.length) out rest

def ConwaySoifer.Certificates.thinHull (Ps : List IPoint) : List IPoint

The subset selection of exact_polynomials.thin_hull (a weakening; never a hull claim).

Equations

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

Certificate replay

structure ConwaySoifer.Certificates.Step : Type

One forced step: point q (scaled by the common denominator) is forced into owner owner.

• owner : Fin 10

  The owner forced to contain the new point.

• q : IPoint

  The newly assigned polynomial point.

@[instance_reducible]

instance ConwaySoifer.Certificates.instReprStep : Repr Step

Equations

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

def ConwaySoifer.Certificates.instReprStep.repr : Step → ℕ → Std.Format

Equations

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

structure ConwaySoifer.Certificates.Model : Type

The replay state: mandatory point lists, caps and ordinary flags per owner.

• B : Fin 10 → List IPoint

  The mandatory polynomial points for each owner.

• caps : Fin 10 → List Cap

  The contact constraints for each owner.

• ord : Fin 10 → Option (Fin 6)

  Optional non-overfull side-owner indices.

def ConwaySoifer.Certificates.inTarget (q : IPoint) (den a b d : ℤ) (fuel : ℕ) : Bool

q lies in the target triangle a ≤ 1, b ≤ 1, -1 ≤ a + b (scaled by den).

Equations

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

def ConwaySoifer.Certificates.stepCheck (M : Model) (den : ℤ) (st : Step) (a b d : ℤ) (fuel depth : ℕ) : Bool

Check target membership and exclusion from every owner except the proposed owner.

Equations

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

def ConwaySoifer.Certificates.thinHullChecked (L : List IPoint) : List IPoint

The thinned list, filtered to elements of the original list (so that membership is a syntactic fact and no property of the hull heuristic is needed).

Equations

• ConwaySoifer.Certificates.thinHullChecked L = List.filter (fun (P : ConwaySoifer.Certificates.IPoint) => decide (P ∈ L)) (ConwaySoifer.Certificates.thinHull L)

def ConwaySoifer.Certificates.Model.insert (M : Model) (st : Step) : Model

Insert a forced point into its owner set and retain only a checked hull subset.

Equations

• M.insert st = { B := fun (j : Fin 10) => if j = st.owner then ConwaySoifer.Certificates.thinHullChecked (M.B j ++ [st.q]) else M.B j, caps := M.caps, ord := M.ord }

def ConwaySoifer.Certificates.replay (M : Model) (den a b d : ℤ) (fuel depth : ℕ) : List Step → Fin 10 → Bool

Check the forced assignments in order and a final owner contradiction.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.replay M den a b d fuel depth [] x✝ = ConwaySoifer.Certificates.excluded (M.B x✝) den (M.caps x✝) (M.ord x✝) fuel depth a b d