Geometry Triangulation3 Dconsistency Incidence Consistent

Incidence consistency

A triangulation of three-dimensional space is a way of chopping space into tetrahedra, the simplest solid shapes, that meet only along whole faces, edges, or vertices. A triangulation is incidence-consistent when the local data attached to each tetrahedron agrees with the global data of the whole complex wherever they overlap. Specifically, if a global edge is identified with a local edge slot inside a particular tetrahedron, then the squared length recorded in that local slot must equal the squared length recorded in the global chart. This is a bookkeeping condition: it ensures that the same physical edge is not assigned two different lengths depending on which tetrahedron you ask.

The framework's machine-checked library of formal theorems proves two consequences of this consistency. First, the length of any edge, computed locally inside a tetrahedron, equals the length computed from the global chart. Second, and more substantially, incidence consistency is enough to construct a global Schläfli data package, a structure that carries the derivative data needed for Schläfli cancellation, a technique for summing angle defects across a triangulation. The theorem global_schlaefli_from_incidence shows that from the incidence mixin, which includes a local closed-form proof, one can build the global package without the caller having to supply any additional data. A further theorem states that such a package is always available, that is, nonempty, for any incidence-consistent triangulation.

The declaration also separates two levels of assumption. The structure IncidenceConsistent stores both the incidence fields and the local Schläfli proof as data. A second structure, IncidenceGeometry, keeps only the pure geometric incidence consistency, without storing any local proofs. The library then shows that once the local closed-form Schläfli theorem is proved globally, pure incidence geometry alone suffices to construct the local Schläfli data on every tetrahedron, and from that the global package. This factorization means the heavy local theorem can be proved once and reused, rather than being restated as a field in every geometric structure.

What this declaration does not claim is just as important. It does not assert that any particular triangulation of space exists or that space is in fact triangulated; it only states a condition on triangulations that are already given. It does not prove the local closed-form Schläfli theorem itself; that theorem is an assumption, named SchlaefliTetrahedronClosedFormTarget, which the incidence structure may carry or which must be supplied separately. Finally, it makes no claim about the physical content of three-dimensional space, such as why space has three dimensions. The declaration is a piece of pure geometry, a consistency condition and its consequences, not a statement about the physical world.

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

/-- The local edge length at any incident tetrahedral edge equals the global
edge length determined by the consistency chart. -/
theorem localEdgeLength_eq_globalEdgeLength
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (e : Fin K.nE) (τ : Fin K.nT) (f : Fin 6)
    (h : K.edgeInTet e τ = some f) :
    Real.sqrt ((K.tet τ).sqEdge f) = globalEdgeLength K hK e := by
  unfold globalEdgeLength
  rw [localSqEdge_eq_globalSqEdge K hK e τ f h]

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

/-- Incidence consistency constructs the global Schläfli data package. -/
theorem nonempty_triangulationSchlaefliData_of_incidence
    (K : Triangulation3D) (hK : IncidenceConsistent K) :
    Nonempty (TriangulationSchlaefliData K) :=
  ⟨triangulationSchlaefliData_of_incidence K hK⟩

What this page does not claim

The declaration does not assert that any particular triangulation of space exists. The declaration does not prove the local closed-form Schläfli theorem, which remains an assumption. The declaration makes no claim about why space has three dimensions.

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: