Geometry Triangulation3 Dconsistency Incidence Geometry

Incidence geometry in triangulations

In three-dimensional geometry, a triangulation is a way of filling a shape with tetrahedra, the simplest solid with four triangular faces. The edges of those tetrahedra must match up: an edge that belongs to two neighboring tetrahedra is the same physical line segment, so its length must be the same whether measured from either side. The IncidenceGeometry structure formalizes exactly this matching condition, which mathematicians call incidence consistency. It states that whenever the triangulation's bookkeeping says a global edge appears inside a particular tetrahedron, the squared length recorded in that tetrahedron's local data equals the squared length recorded in the global chart.

This is a pure geometric consistency condition, and it does not by itself prove anything about the famous Schläfli formula, which describes how the volume of a tetrahedron changes when its edge lengths change. The framework's library proves two separate results. First, if the incidence condition is strengthened to also carry a local closed-form proof of the tetrahedral Schläfli identity, then the global Schläfli cancellation follows as a theorem: the contributions from all tetrahedra cancel in the required way. Second, with only the pure incidence geometry plus a separate assumption that the local Schläfli theorem holds, the same global conclusion follows. The second version stores no local proof data as fields, which is the right input once the tetrahedral theorem is available globally.

What this means in practice is a division of labor. The incidence structure guarantees that local and global edge measurements agree, so a computation performed on one tetrahedron's edge can be trusted as a computation about the whole triangulation. The Schläfli identity, which relates edge lengths to volume derivatives, is a separate mathematical fact that must be supplied either as stored data or as an assumed local theorem. The library shows that once both ingredients are present, the global Schläfli data package exists and the cancellation theorem holds.

The declaration does not claim that any particular triangulation exists, that any physical space is actually triangulated, or that the Schläfli identity itself is proved here. It establishes a consistency condition and shows what follows from it, leaving the local tetrahedral theorem as a target for separate proof.

/-- Pure geometric incidence consistency, without storing local Schläfli
proofs as fields.  This is the right input once the tetrahedral Schläfli
theorem is available globally. -/
structure IncidenceGeometry (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

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

/-- Pure incidence geometry plus the local theorem gives global Schläfli. -/
theorem global_schlaefli_from_geometry
    (K : Triangulation3D) (hK : IncidenceGeometry K)
    (hLocal : SchlaefliTetrahedronClosedFormTarget) (e' : Fin 6) :
    globalSchlaefliLHS K (triangulationSchlaefliData_of_geometry K hK hLocal) e' =
      globalSchlaefliRHS K (triangulationSchlaefliData_of_geometry K hK hLocal) e' :=
  global_schlaefli_of_local K (triangulationSchlaefliData_of_geometry K hK hLocal) e'

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

What this page does not claim

No particular triangulation of any shape or space is asserted to exist. The tetrahedral Schläfli identity itself is not proved by this module. No claim is made about physical space being triangulated.

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: