Geometry Discrete Bianchi Flat Regge Data Schlafli

The Flat Substrate Witness

Regge calculus is a discrete approach to general relativity where spacetime is approximated by a network of flat simplices, like a curved surface built from flat triangles. The curvature is concentrated along the "bones" (edges in 2D, triangles in 3D) where the simplices meet, measured by a deficit angle. A central identity in this framework is the contracted discrete Bianchi identity, the discrete analog of the statement that the divergence of the Einstein tensor vanishes, which ensures the action is invariant under moving vertices. In this discrete setting, this identity is equivalent to the Schläfli identity: for each interior vertex, the sum over incident bones of the deficit angle times the derivative of the bone area with respect to the vertex position equals zero.

The theorem flatReggeData_schlafli establishes that the simplest possible configuration, the flat substrate where all deficit angles and areas are zero, satisfies the Schläfli identity at every vertex. This is proven in the machine-checked library of formal theorems with no unproven assumptions (0 sorry, 0 RS-internal axiom). The proof is a direct simplification: with all terms zero, the sum is trivially zero. This provides a canonical witness, a concrete example showing that the condition is not vacuous, and it allows the framework to construct a certificate bundling the equivalence between the Schläfli identity and the contracted discrete Bianchi for this flat case.

In Recognition Science, this result is a structural scaffold, not a physical derivation. It does not prove the general Schläfli identity for arbitrary triangulations, which requires a full proof of the simplex volume-area relation and its kinematic consequences, work that remains open. The theorem also does not claim that the flat substrate represents a physical spacetime; it is a starting point for the discrete geometry, ensuring the formalism is consistent before moving to curved configurations. The framework's library uses this to establish that the discrete Bianchi identity holds non-vacuously, a necessary check for the broader quantum-gravity program, but it is not a statement about the physics of curved space itself.

/-- The flat Regge data satisfies the Schläfli identity at every
vertex by construction (zero deficits → zero sum). -/
theorem flatReggeData_schlafli {V B : Type} [Fintype B] :
    ∀ v : V,
      SchlafliIdentityAtVertex (flatReggeData V B) v := by
  intro v i
  simp [flatReggeData]

/-- The flat Regge data satisfies the Schläfli identity at every
vertex by construction (zero deficits → zero sum). -/
theorem flatReggeData_schlafli {V B : Type} [Fintype B] :
    ∀ v : V,
      SchlafliIdentityAtVertex (flatReggeData V B) v := by
  intro v i
  simp [flatReggeData]

theorem discreteBianchiContractedCert_inhabited
    (V B : Type) [Fintype B] :
    Nonempty (DiscreteBianchiContractedCert V B) :=
  ⟨discreteBianchiContractedCert V B⟩

What this page does not claim

This does not prove the general Schläfli identity for arbitrary triangulations. This does not claim the flat substrate represents a physical spacetime. This does not derive any empirical prediction about quantum gravity.

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