Geometry Schlaefli Triangulation3 D Global Schlaefli Lhs

The global identity

The global Schläfli identity is a statement about any finite triangulation of a three-dimensional space: a triangulation built from tetrahedra glued face to face. The declaration globalSchlaefliLHS defines the left-hand side of that identity. It is a sum over every tetrahedron in the triangulation, and for each tetrahedron, a sum over its six edges. Each term multiplies the edge length (the square root of the squared edge length) by a number that records how that edge's dihedral angle changes as the tetrahedron deforms. The right-hand side, globalSchlaefliRHS, is simply zero.

The theorem global_schlaefli_of_local proves that this global sum equals zero. The proof is short: it applies the local tetrahedral Schläfli identity to each tetrahedron individually, and then sums the results. The local identity, a classical result in differential geometry, says that for a single tetrahedron, the sum over edges of edge length times dihedral angle variation vanishes. Summing these local cancellations over the whole triangulation gives the global cancellation. This is a theorem in the machine-checked library of formal theorems, meaning the proof is verified by a computer.

In Recognition Science, this identity appears as part of the framework's geometric foundation. The framework models physical structure through discrete recognition events, and this triangulation identity is a piece of the discrete geometry it uses. The declaration does not claim that any particular triangulation is physically realized, nor does it say that the edge lengths or dihedral angles come from a specific physical system. It is a purely combinatorial and geometric statement: given any finite triangulation and any assignment of derivative data to its tetrahedra, the sum cancels.

The practical consequence is a consistency check. Any computation that uses local Schläfli identities on a 3D triangulation can rely on the global sum vanishing, without needing to check each tetrahedron separately. The identity also illustrates a broader pattern: local geometric relations can assemble into global ones, a theme that recurs throughout the framework's treatment of discrete space.

/-- Summing local tetrahedral Schläfli identities gives the global finite
triangulation identity. -/
theorem global_schlaefli_of_local
    (K : Triangulation3D) (D : TriangulationSchlaefliData K) (e' : Fin 6) :
    globalSchlaefliLHS K D e' = globalSchlaefliRHS K D e' := by
  unfold globalSchlaefliLHS globalSchlaefliRHS
  have hlocal : ∀ τ : Fin K.nT,
      (∑ e : Fin 6,
        Real.sqrt ((K.tet τ).sqEdge e) * (D.tetData τ).dihedralDeriv e e')
        = 0 := by
    intro τ
    exact (D.tetData τ).schlaefli e'
  simp_rw [hlocal]
  simp

/-- The global Schläfli left-hand side, summed over tetrahedra and local
tetrahedral edges. -/
def globalSchlaefliLHS (K : Triangulation3D)
    (D : TriangulationSchlaefliData K) (e' : Fin 6) : ℝ :=
  ∑ τ : Fin K.nT,
    ∑ e : Fin 6,
      Real.sqrt ((K.tet τ).sqEdge e) * (D.tetData τ).dihedralDeriv e e'

/-- The global Schläfli right-hand side: the Euclidean angle-variation term
vanishes. -/
def globalSchlaefliRHS (K : Triangulation3D)
    (_D : TriangulationSchlaefliData K) (_e' : Fin 6) : ℝ :=
  0

What this page does not claim

The identity does not claim that any specific triangulation is physically realized. It does not assign physical meaning to the edge lengths or dihedral angle variations. It does not claim the local Schläfli identity holds without the derivative data structure.

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/SchlaefliTriangulation3D.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: