Local Validity Checker

A computable, pure-ℚ checker that verifies whether a decision-tree row satisfies the preconditions of the rational local theorem. Everything here is computable — no noncomputable keyword.

@[reducible, inline]

abbrev Noperthedron.Solution.sqrt_twoℚ : ℚ

Equations

• Noperthedron.Solution.sqrt_twoℚ = 142 / 100

@[reducible, inline]

abbrev Noperthedron.Solution.Row.Pi (r : Row) : Fin 3 → VertexIndex

Equations

• r.Pi = ![r.P1_index, r.P2_index, r.P3_index]

@[reducible, inline]

abbrev Noperthedron.Solution.Row.Qi (r : Row) : Fin 3 → VertexIndex

Equations

• r.Qi = ![r.Q1_index, r.Q2_index, r.Q3_index]

@[reducible, inline]

abbrev Noperthedron.Solution.Row.X₁ (r : Row) : Fin 3 → ℚ

Equations

• r.X₁ = RationalApprox.vecXℚ r.θ₁ r.φ₁

@[reducible, inline]

abbrev Noperthedron.Solution.Row.X₂ (r : Row) : Fin 3 → ℚ

Equations

• r.X₂ = RationalApprox.vecXℚ r.θ₂ r.φ₂

@[reducible, inline]

abbrev Noperthedron.Solution.rot90 : Matrix (Fin 2) (Fin 2) ℚ

Equations

• Noperthedron.Solution.rot90 = !![0, -1; 1, 0]

@[reducible, inline]

abbrev Noperthedron.Solution.Row.r (row : Row) : ℚ

Equations

• row.r = ↑row.r' / 1000

Spanning condition: hoisted trig, scalarized applied vectors

def Noperthedron.Solution.Spanningℚ (θ φ ε : ℚ) (T : Fin 3 → Fin 3 → ℚ) : Prop

The rational matrix form of the ε-κ-spanning condition on the triangle T for angles (θ, φ) (cf. Local.Triangle.κSpanning). Named so that its Decidable instance (via Spanningℚ.check) can hoist the trig entries of rotMℚ_mat θ φ out of the i-loop and bind the applied vectors' components as scalars; the generic mulVec/dotProduct instances would re-evaluate the trig partial sums on every component access.

Equations

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

def Noperthedron.Solution.Spanningℚ.check (θ φ ε : ℚ) (T : Fin 3 → Fin 3 → ℚ) : Bool

Bool-valued Spanningℚ check: trig partial sums are evaluated once per pose and everything the i-loop touches is bound as a scalar.

Equations

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

theorem Noperthedron.Solution.Spanningℚ.check_iff (θ φ ε : ℚ) (T : Fin 3 → Fin 3 → ℚ) : check θ φ ε T = true ↔ Spanningℚ θ φ ε T

@[instance_reducible]

instance Noperthedron.Solution.Spanningℚ.instDecidable (θ φ ε : ℚ) (T : Fin 3 → Fin 3 → ℚ) : Decidable (Spanningℚ θ φ ε T)

Equations

• Noperthedron.Solution.Spanningℚ.instDecidable θ φ ε T = decidable_of_iff (Noperthedron.Solution.Spanningℚ.check θ φ ε T = true) ⋯

Row.δ: max over per-i BoundDeltaℚi values, hoisting trig once

structure Noperthedron.Solution.Row.δ.PoseTrigQ : Type

The ten sin/cos values (of θ₁ φ₁ α θ₂ φ₂) of a rational pose, evaluated once per pose.

• st1 : ℚ
• ct1 : ℚ
• sp1 : ℚ
• cp1 : ℚ
• sa : ℚ
• ca : ℚ
• st2 : ℚ
• ct2 : ℚ
• sp2 : ℚ
• cp2 : ℚ

@[inline]

def Noperthedron.Solution.Row.δ.PoseTrigQ.ofPose (p : Pose ℚ) : PoseTrigQ

Equations

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

@[inline]

def Noperthedron.Solution.Row.δ.boundDelta_at (t : PoseTrigQ) (P Q : Fin 3 → ℚ) : ℚ

BoundDeltaℚi for a single i, with the 10 trig values used by M₁, R, M₂ passed in already evaluated.

Equations

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

theorem Noperthedron.Solution.Row.δ.boundDelta_at_eq (p : Pose ℚ) (P Q : Fin 3 → ℚ) : boundDelta_at (PoseTrigQ.ofPose p) P Q = RationalApprox.sqrtApprox16.upper_sqrt.norm (p.rotRℚ (p.rotM₁ℚ P) - p.rotM₂ℚ Q) / 2 + 3 * RationalApprox.κℚ

Integer core

The norm² is assembled exactly at scale 10¹¹⁰ (difference vector at 10⁵⁵) and the upper square root becomes one integer ceiling division plus Nat.sqrt (sqrtNum110, output scale 10¹⁶), so the whole per-i value is (sqrtNum110 … + 6·10⁶) / (2·10¹⁶). The ℚ helpers above stay as the proof-side bridge to BoundDeltaℚi.

def Noperthedron.Solution.Row.δ.sqrtNum110 (S : ℤ) : ℤ

Integer form of sqrtℚUp16 on inputs S/10¹¹⁰: the inner ceiling ⌈S/10⁷⁸⌉ is -((-S)/10⁷⁸) (floor division). Output scale 10¹⁶.

Equations

• Noperthedron.Solution.Row.δ.sqrtNum110 S = if S ≤ 0 then 0 else ↑((-(-S / 10 ^ 78)).toNat.sqrt + 1)

structure Noperthedron.Solution.Row.δ.PoseTrigN : Type

The ten trig numerators (scale 10¹³) of a rational pose.

• st1 : ℤ
• ct1 : ℤ
• sp1 : ℤ
• cp1 : ℤ
• sa : ℤ
• ca : ℤ
• st2 : ℤ
• ct2 : ℤ
• sp2 : ℤ
• cp2 : ℤ

@[inline]

def Noperthedron.Solution.Row.δ.PoseTrigN.ofPose (p : Pose ℚ) : PoseTrigN

Equations

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

@[inline]

def Noperthedron.Solution.Row.δ.boundDeltaN (t : PoseTrigN) (P0 P1 P2 Q0 Q1 Q2 : ℤ) : ℤ

Integer core of boundDelta_at (up to the final (·+6·10⁶)/(2·10¹⁶)): M₁-rows lifted to scale 10²⁶, dots at 10⁴², the R-rotated and M₂-lifted difference at 10⁵⁵, norm² at 10¹¹⁰.

Equations

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

theorem Noperthedron.Solution.Row.δ.boundDeltaN_div_eq (p : Pose ℚ) (a b : VertexIndex) : ↑(boundDeltaN (PoseTrigN.ofPose p) (pythonVertexNumCurried a.ℓ a.i a.k 0) (pythonVertexNumCurried a.ℓ a.i a.k 1) (pythonVertexNumCurried a.ℓ a.i a.k 2) (pythonVertexNumCurried b.ℓ b.i b.k 0) (pythonVertexNumCurried b.ℓ b.i b.k 1) (pythonVertexNumCurried b.ℓ b.i b.k 2) + 6 * 10 ^ 6) / (2 * 10 ^ 16) = boundDelta_at (PoseTrigQ.ofPose p) (pythonVertex a) (pythonVertex b)

def Noperthedron.Solution.Row.δ (row : Row) : ℚ

The δ bound for a row: max_i ‖R·M₁·P_i − M₂·Q_i‖ / 2 + 3κ. Equivalent to Finset.max' (Finset.image BoundDeltaℚi univ) _ (see Row.δ_eq_max'_BoundDeltaℚi), but the trig partial sums are hoisted once per pose for a ~6× runtime speedup.

Equations

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

theorem Noperthedron.Solution.Row.δ_eq_max'_BoundDeltaℚi (row : Row) : row.δ = (Finset.image (RationalApprox.LocalTheorem.BoundDeltaℚi row.interval.centerPose (pythonVertex ∘ row.Pi) (pythonVertex ∘ row.Qi) RationalApprox.sqrtApprox16) Finset.univ).max' ⋯

Precomputed pairwise vertex-difference norms for Bεℚ

The n_dv term of the Bεℚ predicate — sqrtApprox16.upper_sqrt.norm (Q_i − v_k) — is pose-independent, but costs a sqrtℚUp16 call on a denominator-10³² input for each of the 270 (i, k) pairs of every local row. sqrtDv reads all 90 × 90 pairs from the source-literal table sqrtDvCurried (generated, see Checker/SqrtDvLiterals.lean), and BεℚPy.check is the pythonVertexA/sqrtApprox16 checker of Bεℚ that reads it (the Bεℚ predicate itself is unchanged). The curried-literal form keeps the table cheap for the kernel too: an access walks a few dozen Fin.cons cells, where reducing an equivalent 8100-entry Array.ofFn push chain made a single high-index access cost tens of gigabytes under decide +kernel.

def Noperthedron.Solution.ofFlat (m : ℕ) (h : m < 90) : VertexIndex

Decode the flat index 45·ℓ + 15·i + k (see rowDotsGet).

Equations

• Noperthedron.Solution.ofFlat m h = { k := ⟨m % 15, ⋯⟩, ℓ := ⟨m / 45, ⋯⟩, i := ⟨m / 15 % 3, ⋯⟩ }

def Noperthedron.Solution.sqrtDv (a b : VertexIndex) : ℚ

Table-backed pairwise vertex-difference norm: equal to sqrtApprox16.upper_sqrt.norm (pythonVertexA a - pythonVertexA b) by sqrtDv_eq.

Equations

• Noperthedron.Solution.sqrtDv a b = Noperthedron.Solution.sqrtDvCurried a.ℓ a.i a.k b.ℓ b.i b.k

theorem Noperthedron.Solution.sqrtDv_eq (a b : VertexIndex) : sqrtDv a b = RationalApprox.sqrtApprox16.upper_sqrt.norm (pythonVertexA a - pythonVertexA b)

def Noperthedron.Solution.sqrtDvTable : Array ℚ

Runtime lookup table for sqrtDv, built once per process from the sqrtDvCurried literals; indexed by the flat pair index flat a * 90 + flat b with flat ⟨k, ℓ, i⟩ = 45·ℓ + 15·i + k.

Equations

• Noperthedron.Solution.sqrtDvTable = Array.ofFn fun (j : Fin 8100) => Noperthedron.Solution.sqrtDv (Noperthedron.Solution.ofFlat (↑j / 90) ⋯) (Noperthedron.Solution.ofFlat (↑j % 90) ⋯)

def Noperthedron.Solution.sqrtDvImpl (a b : VertexIndex) : ℚ

Array-backed implementation of sqrtDv: a per-pair curried lookup costs ~40 Fin.cons dispatches plus a Rat renormalization, which measurably slows the compiled hot loop, so sqrtDv_eq_sqrtDvImpl (@[csimp]) substitutes this O(1) array read in compiled code. The kernel keeps reducing the curried-literal sqrtDv itself.

Equations

• Noperthedron.Solution.sqrtDvImpl a b = Noperthedron.Solution.sqrtDvTable[(45 * ↑a.ℓ + 15 * ↑a.i + ↑a.k) * 90 + (45 * ↑b.ℓ + 15 * ↑b.i + ↑b.k)]

@[csimp]

theorem Noperthedron.Solution.sqrtDv_eq_sqrtDvImpl : sqrtDv = sqrtDvImpl

def Noperthedron.Solution.BεℚPy.rowDots (e : Local.TriangleQ.Bεℚ.MatEntries) : List (ℚ × ℚ)

Per-pose table of the row dot products ((M₂ vⱼ)₀, (M₂ vⱼ)₁) (unrounded) for all 90 vertices, indexed by flat ⟨k, ℓ, i⟩ = 45·ℓ + 15·i + k. check computes it once per pose; by linearity M₂(v₁ - v₂) = M₂v₁ - M₂v₂, each (i, k) dot then costs one lookup and one subtraction instead of three products.

Equations

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

def Noperthedron.Solution.BεℚPy.rowDotsGet (dots : List (ℚ × ℚ)) (a : VertexIndex) : ℚ × ℚ

Read a rowDots table at a vertex index.

Equations

• Noperthedron.Solution.BεℚPy.rowDotsGet dots a = dots[45 * ↑a.ℓ + 15 * ↑a.i + ↑a.k]!

theorem Noperthedron.Solution.BεℚPy.rowDots_fst (e : Local.TriangleQ.Bεℚ.MatEntries) (a : VertexIndex) : (rowDotsGet (rowDots e) a).1 = e.m₀₀ * pythonVertexA a 0 + e.m₀₁ * pythonVertexA a 1 + e.m₀₂ * pythonVertexA a 2

theorem Noperthedron.Solution.BεℚPy.rowDots_snd (e : Local.TriangleQ.Bεℚ.MatEntries) (a : VertexIndex) : (rowDotsGet (rowDots e) a).2 = e.m₁₀ * pythonVertexA a 0 + e.m₁₁ * pythonVertexA a 1 + e.m₁₂ * pythonVertexA a 2

def Noperthedron.Solution.BεℚPy.check (Qi : Fin 3 → VertexIndex) (p : Pose ℚ) (ε δ r : ℚ) : Bool

Bool-valued checker for Bεℚ at pythonVertexA and sqrtApprox16, with the per-pose work hoisted out of the k-loop:

• the pose-independent n_dv norms come from the sqrtDvCurried literals;
• the unrounded row dots M₂vⱼ come from the per-pose rowDots table, so a pair's d-vector is one lookup and one subtraction (M₂(v₁-v₂) = M₂v₁-M₂v₂);
• the scalars F2, cD, eterm, tenκ, twoκ, bd are loop-invariant.

Each (i, k) pair first tries a cheap sufficient test (the left disjunct) that avoids the per-pair upper_sqrt.f call on the denominator-10²⁶ input d0² + d1²: by Cauchy–Schwarz, d0² + d1² ≤ (F·n_dv + 2·10⁻¹³)² where F is a per-pose Frobenius-norm bound (one sqrt call per pose), so the fixed-point accuracy bound sqrtℚUp16 x ≤ Y + 2·10⁻¹⁶ caps the exact denom2 by F·n_dv + 2·10⁻¹³ + 2·10⁻¹⁶ + 2·√⁺2·ε + 6κ (see cheap_sufficient). Only pairs that fail the cheap test — binding or near-binding k — fall back to the exact test in the right disjunct; the Or/And Decidable instances are macro_inline, so evaluation short-circuits.

Equations

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

theorem Noperthedron.Solution.BεℚPy.check_iff (Qi : Fin 3 → VertexIndex) (p : Pose ℚ) (ε δ r : ℚ) : check Qi p ε δ r = true ↔ Local.TriangleQ.Bεℚ Qi pythonVertexA p ε δ r RationalApprox.sqrtApprox16

@[instance_reducible, instance 10000]

instance Noperthedron.Solution.BεℚPy.instDecidablePy (Qi : Fin 3 → VertexIndex) (p : Pose ℚ) (ε δ r : ℚ) : Decidable (Local.TriangleQ.Bεℚ Qi pythonVertexA p ε δ r RationalApprox.sqrtApprox16)

Decision procedure for the Bεℚ conjunct of Row.ValidLocal (the only one — the generic-ι checker layer was retired in favor of this specialization).

Equations

• Noperthedron.Solution.BεℚPy.instDecidablePy Qi p ε δ r = decidable_of_iff (Noperthedron.Solution.BεℚPy.check Qi p ε δ r = true) ⋯

Kernel-path vertex reads for the remaining Row.ValidLocal conjuncts

The Aεℚσ/Spanningℚ/BoundRℚ conjuncts read vertices through pythonVertexA; under decide +kernel its backing Array.ofFn push chain re-reduces as a quadratic List.concat walk (~150k list-step unfoldings per local row — the dominant cost, per kernel diagnostics). These instances transport each conjunct to the curried pythonVertex, whose lookups cost the kernel a few dozen Fin.cons steps; compiled code still gets O(1) array reads via pythonVertex's @[csimp].

@[instance_reducible, instance 10000]

instance Noperthedron.Solution.Aεℚσ.instDecidablePyV (X : Fin 3 → ℚ) (idx : Fin 3 → VertexIndex) (ε : ℚ) (σ : ℕ) (approx : RationalApprox.Approx) : Decidable (Local.TriangleQ.Aεℚσ X (pythonVertexA ∘ idx) ε σ approx)

Equations

• Noperthedron.Solution.Aεℚσ.instDecidablePyV X idx ε σ approx = decidable_of_iff (Local.TriangleQ.Aεℚσ X (Noperthedron.pythonVertex ∘ idx) ε σ approx) ⋯

@[instance_reducible, instance 10000]

instance Noperthedron.Solution.Spanningℚ.instDecidablePyV (θ φ ε : ℚ) (idx : Fin 3 → VertexIndex) : Decidable (Spanningℚ θ φ ε (pythonVertexA ∘ idx))

Equations

• Noperthedron.Solution.Spanningℚ.instDecidablePyV θ φ ε idx = decidable_of_iff (Noperthedron.Solution.Spanningℚ θ φ ε (Noperthedron.pythonVertex ∘ idx)) ⋯

@[instance_reducible, instance 10000]

instance Noperthedron.Solution.BoundRℚ.instDecidablePyV (r ε : ℚ) (p : Pose ℚ) (idx : Fin 3 → VertexIndex) (approx : RationalApprox.Approx) : Decidable (RationalApprox.LocalTheorem.BoundRℚ r ε p (pythonVertexA ∘ idx) approx)

Equations

• Noperthedron.Solution.BoundRℚ.instDecidablePyV r ε p idx approx = decidable_of_iff (RationalApprox.LocalTheorem.BoundRℚ r ε p (Noperthedron.pythonVertex ∘ idx) approx) ⋯

structure Noperthedron.Solution.Row.ValidLocal (row : Row) : Prop

Assertion that a row constitutes a valid application of the rational global theorem.

The vertex functions are the table-backed pythonVertexA (equal to pythonVertex by pythonVertexA_eq), so the hot loops of the Decidable instance read precomputed coordinates instead of re-dividing on every access.

• nodeType_eq : row.nodeType = 2
• center_in_fourQ : row.interval.centerPose ∈ fourInterval ℚ
• epsilon_pos : 0 < row.epsilon
• exists_symmetry : ∃ (s : TriangleSymmetry), s.applicable row.Qi ∧ ∀ (i : Fin 3), row.Pi i = s.apply (row.Qi i)
• X₁_inner_gt : Local.TriangleQ.Aεℚσ row.X₁ (pythonVertexA ∘ row.Pi) row.epsilon 0 RationalApprox.sqrtApprox16
• X₂_inner_gt : Local.TriangleQ.Aεℚσ row.X₂ (pythonVertexA ∘ row.Qi) row.epsilon (↑row.sigma_Q) RationalApprox.sqrtApprox16
• P_spanning : Spanningℚ row.θ₁ row.φ₁ row.epsilon (pythonVertexA ∘ row.Pi)
• Q_spanning : Spanningℚ row.θ₂ row.φ₂ row.epsilon (pythonVertexA ∘ row.Qi)
• rpos : 0 < row.r
• r_valid : RationalApprox.LocalTheorem.BoundRℚ row.r row.epsilon row.interval.centerPose (pythonVertexA ∘ row.Qi) RationalApprox.sqrtApprox16
• Bεℚ : Local.TriangleQ.Bεℚ row.Qi pythonVertexA row.interval.centerPose row.epsilon row.δ row.r RationalApprox.sqrtApprox16

theorem Noperthedron.Solution.Row.validLocal_iff (row : Row) : row.ValidLocal ↔ row.nodeType = 2 ∧ row.interval.centerPose ∈ fourInterval ℚ ∧ 0 < row.epsilon ∧ (∃ (s : TriangleSymmetry), s.applicable row.Qi ∧ ∀ (i : Fin 3), row.Pi i = s.apply (row.Qi i)) ∧ Local.TriangleQ.Aεℚσ row.X₁ (pythonVertexA ∘ row.Pi) row.epsilon 0 RationalApprox.sqrtApprox16 ∧ Local.TriangleQ.Aεℚσ row.X₂ (pythonVertexA ∘ row.Qi) row.epsilon (↑row.sigma_Q) RationalApprox.sqrtApprox16 ∧ Spanningℚ row.θ₁ row.φ₁ row.epsilon (pythonVertexA ∘ row.Pi) ∧ Spanningℚ row.θ₂ row.φ₂ row.epsilon (pythonVertexA ∘ row.Qi) ∧ 0 < row.r ∧ RationalApprox.LocalTheorem.BoundRℚ row.r row.epsilon row.interval.centerPose (pythonVertexA ∘ row.Qi) RationalApprox.sqrtApprox16 ∧ Local.TriangleQ.Bεℚ row.Qi pythonVertexA row.interval.centerPose row.epsilon row.δ row.r RationalApprox.sqrtApprox16

@[instance_reducible]

instance Noperthedron.Solution.instDecidableValidLocal (row : Row) : Decidable row.ValidLocal

Equations

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

Smoke test

def Noperthedron.Solution.testLocalRow : Row

Row 245 from data/solution_tree_300.csv — the first local leaf.

Equations

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

def Noperthedron.Solution.testLocalRowReflection : Row

Equations

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