Geometry Triangulation3 Dconsistency Local Sq Edge Eq Global Sq Edge

The local-global edge agreement

In computational geometry, a three-dimensional shape is often built from simpler pieces, like a geodesic dome is built from triangles. The Recognition Science framework's library of formal theorems works with such a construction, called a triangulation, where the pieces are tetrahedra, the three-dimensional analog of triangles. A central question is whether the local geometry of each tetrahedron agrees with the global geometry of the whole triangulation. The declaration localSqEdge_eq_globalSqEdge establishes exactly this agreement: it proves that the squared length of an edge, as measured within a single tetrahedron, equals the squared length of the same edge as recorded in the global chart of the entire triangulation.

The theorem, proved in the machine-checked library IndisputableMonolith/Geometry/Triangulation3DConsistency.lean, is a formal statement about a structure called IncidenceConsistent. This structure packages the assumption that the local edge slots of each tetrahedron correctly correspond to the global edge endpoints, up to orientation. The theorem's statement is precise: for any edge e in the triangulation, any tetrahedron τ, and any local edge slot f, if the incidence map says that edge e is in tetrahedron τ at slot f, then the squared edge length stored locally, (K.tet τ).sqEdge f, is equal to the global squared edge length, hK.globalSqEdge e. The proof is a direct rewrite using the field local_sqEdge_eq_global from the consistency structure.

This agreement is not an isolated fact. The same library derives a companion theorem, localEdgeLength_eq_globalEdgeLength, which states the same equality for the actual edge lengths (the square roots of the squared lengths). More importantly, this local-global consistency is a stepping stone. The library uses it to construct, from the incidence data alone, a package of local Schläfli data (a geometric quantity related to the derivative of a tetrahedron's volume with respect to its edge lengths) on every tetrahedron. From that, a further theorem, global_schlaefli_from_incidence, derives the global Schläfli identity, a key relation in the framework's treatment of Regge calculus, a discrete approach to general relativity. The chain shows that a consistent local geometry automatically yields a consistent global one.

What the theorem does not claim is just as important. It does not assert that any particular triangulation exists, or that any specific set of edge lengths is physically realizable. The theorem is conditional: it says if you have a triangulation satisfying the IncidenceConsistent structure, then the local and global squared edge lengths agree. It also does not claim that the local Schläfli data can be computed without a separate closed-form proof; the structure IncidenceConsistent includes a field for that local proof, and the later theorem global_schlaefli_from_geometry shows how to proceed when that local proof is available as a separate hypothesis. The theorem is a consistency guarantee within a formal framework, not a statement about the physical universe.

For the Recognition Science framework, this theorem is a load-bearing piece of infrastructure. It ensures that when the framework builds a global geometric object from local pieces, the edge lengths do not silently disagree, which would make any subsequent global calculation meaningless. By proving this agreement once in a machine-checked library, the framework can rely on it in any future construction, from discrete gravity to other geometric applications. The practical consequence is that a researcher or a downstream theorem can safely use the global edge length chart without re-checking each local tetrahedron, because the consistency is guaranteed by the formal proof.

/-- Local tetrahedral squared-edge slots agree with the global squared-edge
chart whenever the incidence map identifies them. -/
theorem localSqEdge_eq_globalSqEdge
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (e : Fin K.nE) (τ : Fin K.nT) (f : Fin 6)
    (h : K.edgeInTet e τ = some f) :
    (K.tet τ).sqEdge f = hK.globalSqEdge e :=
  hK.local_sqEdge_eq_global e τ f h

/-- Local tetrahedral squared-edge slots agree with the global squared-edge
chart whenever the incidence map identifies them. -/
theorem localSqEdge_eq_globalSqEdge
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (e : Fin K.nE) (τ : Fin K.nT) (f : Fin 6)
    (h : K.edgeInTet e τ = some f) :
    (K.tet τ).sqEdge f = hK.globalSqEdge e :=
  hK.local_sqEdge_eq_global e τ f h

/-- Construct local Schläfli data on every tetrahedron from the incidence
mixin's closed-form local Schläfli proof. -/
def triangulationSchlaefliData_of_incidence
    (K : Triangulation3D) (hK : IncidenceConsistent K) :
    TriangulationSchlaefliData K where
  tetData := fun τ =>
    tetraSchlaefliDerivativeData_closedForm (K.tet τ) (hK.local_schlaefli τ)

/-- Strong incidence plus local closed-form Schläfli gives global Schläfli. -/
theorem global_schlaefli_from_incidence
    (K : Triangulation3D) (hK : IncidenceConsistent K) (e' : Fin 6) :
    globalSchlaefliLHS K (triangulationSchlaefliData_of_incidence K hK) e' =
      globalSchlaefliRHS K (triangulationSchlaefliData_of_incidence K hK) e' :=
  global_schlaefli_of_local K (triangulationSchlaefliData_of_incidence K hK) e'

What this page does not claim

The theorem does not assert that any particular triangulation exists or that any specific set of edge lengths is physically realizable. The theorem does not claim that the local Schläfli data can be computed without a separate closed-form proof. The theorem is a consistency guarantee within a formal framework, not a statement about the physical universe.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/Triangulation3DConsistency.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: