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.M₁_ (r : Row) : Matrix (Fin 2) (Fin 3) ℚ

Equations

• r.M₁_ = RationalApprox.rotMℚ_mat r.θ₁ r.φ₁

@[reducible, inline]

abbrev Noperthedron.Solution.Row.M₂_ (r : Row) : Matrix (Fin 2) (Fin 3) ℚ

Equations

• r.M₂_ = RationalApprox.rotMℚ_mat 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.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

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

theorem Noperthedron.Solution.Row.δ.boundDelta_at_eq (p : Pose ℚ) (P Q : Fin 3 → ℚ) : Noperthedron.Solution.Row.δ.boundDelta_at✝ (RationalApprox.sinℚ p.θ₁) (RationalApprox.cosℚ p.θ₁) (RationalApprox.sinℚ p.φ₁) (RationalApprox.cosℚ p.φ₁) (RationalApprox.sinℚ p.α) (RationalApprox.cosℚ p.α) (RationalApprox.sinℚ p.θ₂) (RationalApprox.cosℚ p.θ₂) (RationalApprox.sinℚ p.φ₂) (RationalApprox.cosℚ p.φ₂) P Q = RationalApprox.sqrtApprox.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.sqrtApprox) Finset.univ).max' ⋯

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

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

• 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₁ (pythonVertex ∘ row.Pi) row.epsilon 0 RationalApprox.sqrtApprox
• X₂_inner_gt : Local.TriangleQ.Aεℚσ row.X₂ (pythonVertex ∘ row.Qi) row.epsilon (↑row.sigma_Q) RationalApprox.sqrtApprox
• P_spanning (i : Fin 3) : 2 * row.epsilon * (sqrt_twoℚ + row.epsilon) + 6 * RationalApprox.κℚ < rot90.mulVec (row.M₁_.mulVec (pythonVertex (row.Pi i))) ⬝ᵥ row.M₁_.mulVec (pythonVertex (row.Pi (i + 1)))
• Q_spanning (i : Fin 3) : 2 * row.epsilon * (sqrt_twoℚ + row.epsilon) + 6 * RationalApprox.κℚ < rot90.mulVec (row.M₂_.mulVec (pythonVertex (row.Qi i))) ⬝ᵥ row.M₂_.mulVec (pythonVertex (row.Qi (i + 1)))
• rpos : 0 < row.r
• r_valid : RationalApprox.LocalTheorem.BoundRℚ row.r row.epsilon row.interval.centerPose (pythonVertex ∘ row.Qi) RationalApprox.sqrtApprox
• Bεℚ : Local.TriangleQ.Bεℚ (pythonVertex ∘ row.Qi) row.Qi pythonVertex row.interval.centerPose row.epsilon row.δ row.r RationalApprox.sqrtApprox

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₁ (pythonVertex ∘ row.Pi) row.epsilon 0 RationalApprox.sqrtApprox ∧ Local.TriangleQ.Aεℚσ row.X₂ (pythonVertex ∘ row.Qi) row.epsilon (↑row.sigma_Q) RationalApprox.sqrtApprox ∧ (∀ (i : Fin 3), 2 * row.epsilon * (sqrt_twoℚ + row.epsilon) + 6 * RationalApprox.κℚ < rot90.mulVec (row.M₁_.mulVec (pythonVertex (row.Pi i))) ⬝ᵥ row.M₁_.mulVec (pythonVertex (row.Pi (i + 1)))) ∧ (∀ (i : Fin 3), 2 * row.epsilon * (sqrt_twoℚ + row.epsilon) + 6 * RationalApprox.κℚ < rot90.mulVec (row.M₂_.mulVec (pythonVertex (row.Qi i))) ⬝ᵥ row.M₂_.mulVec (pythonVertex (row.Qi (i + 1)))) ∧ 0 < row.r ∧ RationalApprox.LocalTheorem.BoundRℚ row.r row.epsilon row.interval.centerPose (pythonVertex ∘ row.Qi) RationalApprox.sqrtApprox ∧ Local.TriangleQ.Bεℚ (pythonVertex ∘ row.Qi) row.Qi pythonVertex row.interval.centerPose row.epsilon row.δ row.r RationalApprox.sqrtApprox

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