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.rotRℚ (r : Row) : Matrix (Fin 2) (Fin 2) ℚ

Equations

• r.rotRℚ = RationalApprox.rotRℚ_mat r.α

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• r.X₂ = RationalApprox.vecXℚ_mat 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

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 ℚ
• exists_symmetry : ∃ (s : TriangleSymmetry), s.applicable row.Qi ∧ ∀ (i : Fin 3), row.Pi i = s.apply (row.Qi i)
• X₁_inner_gt (i : Fin 3) : sqrt_twoℚ * row.epsilon + 3 * κQ < row.X₁.transpose.mulVec (pythonVertex (row.Pi i)) 0
• X₂_inner_gt (i : Fin 3) : sqrt_twoℚ * row.epsilon + 3 * κQ < (-1) ^ ↑row.sigma_Q * row.X₂.transpose.mulVec (pythonVertex (row.Qi i)) 0
• P_spanning (i : Fin 3) : 2 * row.epsilon * (sqrt_twoℚ + row.epsilon) + 6 * κQ < 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 * κQ < rot90.mulVec (row.M₂_.mulVec (pythonVertex (row.Qi i))) ⬝ᵥ row.M₂_.mulVec (pythonVertex (row.Qi (i + 1)))

theorem Noperthedron.Solution.Row.validLocal_iff (row : Row) : row.ValidLocal ↔ row.nodeType = 2 ∧ row.interval.centerPose ∈ fourInterval ℚ ∧ (∃ (s : TriangleSymmetry), s.applicable row.Qi ∧ ∀ (i : Fin 3), row.Pi i = s.apply (row.Qi i)) ∧ (∀ (i : Fin 3), sqrt_twoℚ * row.epsilon + 3 * κQ < row.X₁.transpose.mulVec (pythonVertex (row.Pi i)) 0) ∧ (∀ (i : Fin 3), sqrt_twoℚ * row.epsilon + 3 * κQ < (-1) ^ ↑row.sigma_Q * row.X₂.transpose.mulVec (pythonVertex (row.Qi i)) 0) ∧ (∀ (i : Fin 3), 2 * row.epsilon * (sqrt_twoℚ + row.epsilon) + 6 * κQ < 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 * κQ < rot90.mulVec (row.M₂_.mulVec (pythonVertex (row.Qi i))) ⬝ᵥ row.M₂_.mulVec (pythonVertex (row.Qi (i + 1)))

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