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]

noncomputable abbrev Noperthedron.Solution.Row.P (r : Row) : Local.Triangle

Equations

• r.P = ![Noperthedron.exactVertex r.P1_index, Noperthedron.exactVertex r.P2_index, Noperthedron.exactVertex r.P3_index]

@[reducible, inline]

noncomputable abbrev Noperthedron.Solution.Row.Q (r : Row) : Local.Triangle

Equations

• r.Q = ![Noperthedron.exactVertex r.Q1_index, Noperthedron.exactVertex r.Q2_index, Noperthedron.exactVertex 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

@[implicit_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.κℚ

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 Bεℚ.check — 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 specialization of Bεℚ.check 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

Bεℚ.check specialized to 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

@[implicit_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)

Specialized decision procedure for the Bεℚ conjunct of Row.ValidLocal; the priority bump makes Row.ValidLocal's Decidable instance pick it over the generic Bεℚ.instDecidable.

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].

@[implicit_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) ⋯

@[implicit_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)) ⋯

@[implicit_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

@[implicit_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.