Geometry Triangulation3 Dconsistency

Consistent 3D triangulations

A triangulation of three-dimensional space breaks a volume into tetrahedra, the simplest solid shapes, which meet along shared faces, edges, and vertices. A triangulation is incidence-consistent when the local description of each tetrahedron agrees with the global description of the whole complex. In plain terms, if two tetrahedra share an edge, that edge has the same length and the same squared length in both local records, up to a consistent orientation. The structure IncidenceConsistent formalizes that agreement with fields stating that local tetrahedral edge slots match global edge endpoints.

The classical setting for this work is Regge calculus, a discrete approach to general relativity where space is approximated by a triangulation and curvature lives on the edges. A central identity in this setting is the Schläfli identity, which relates small changes in edge lengths to changes in the volume of a tetrahedron. The main theorem, global_schlaefli_from_incidence, proves that if a triangulation is incidence-consistent, then the global Schläfli identity holds: the sum over all tetrahedra of the local Schläfli terms equals the global expression. This is a machine-checked result in the framework's library of formal proofs, not a paper derivation.

The structure IncidenceConsistent stores, for each tetrahedron, a proof that its local squared-edge data agrees with the global chart, plus a closed-form proof of the local Schläfli identity. From this, the module constructs a TriangulationSchlaefliData package, which supplies the per-tetrahedron derivative data needed for the global identity. This removes the need for a caller to provide such data by hand, because the consistency conditions themselves generate it. A second structure, IncidenceGeometry, drops the stored local proofs and instead takes the local Schläfli theorem as a global hypothesis, showing that pure geometric consistency plus the local theorem suffices for the global result.

The practical consequence is a clean separation of concerns. A triangulation can be checked for incidence consistency once, and that single check guarantees that the global Schläfli identity holds, without further per-tetrahedron bookkeeping. This is a step toward building global geometric identities from local data in a way that a machine can verify, which matters for any framework that wants to reason rigorously about discrete models of spacetime.

/-- 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'

/-- Strong incidence consistency for the current 3D Regge scaffold.

The first fields state that local tetrahedral edge slots agree with global
edge endpoints up to orientation.  The last field is the local closed-form
Schläfli proof required to build global Schläfli without caller-supplied
`TriangulationSchlaefliData`. -/
structure IncidenceConsistent (K : Triangulation3D) where
  globalSqEdge : Fin K.nE → ℝ
  edgeInTet_vertices :
    ∀ e τ f, K.edgeInTet e τ = some f →
      let ev := K.edgeVerts e
      let tv := ReggeRigorousFoundation.edgeVertices f
      (K.tetVerts τ tv.1 = ev.1 ∧ K.tetVerts τ tv.2 = ev.2) ∨
        (K.tetVerts τ tv.1 = ev.2 ∧ K.tetVerts τ tv.2 = ev.1)
  local_sqEdge_eq_global :
    ∀ e τ f, K.edgeInTet e τ = some f →
      (K.tet τ).sqEdge f = globalSqEdge e
  localEdge_complete :
    ∀ τ f, ∃ e : Fin K.nE, K.edgeInTet e τ = some f
  local_schlaefli :
    ∀ τ : Fin K.nT, TetraSchlaefliClosedEquation (K.tet τ)

/-- 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 τ)

What this page does not claim

This module does not prove the local closed-form Schläfli theorem; it assumes it as a hypothesis in the geometry variant. This module does not construct a specific triangulation of physical space; it establishes a consistency condition for any triangulation. This module does not derive the number of spatial dimensions; it works within a given three-dimensional scaffold.

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: