Geometry Discrete Bianchi Discrete Bianchi Contracted Cert Inhabited

The flat witness

In general relativity, the Einstein tensor G satisfies a conservation law: its divergence vanishes. This is the contracted Bianchi identity, written ∇_μG^μν = 0. It is not an extra assumption; it follows from the geometry of spacetime itself. Regge calculus is a discrete approximation to general relativity, replacing smooth spacetime with a triangulated network of flat simplices. On such a network, the identity takes a discrete form: at each interior vertex, a weighted sum over the surrounding bones (the shared faces of the simplices) must equal zero.

The Schläfli identity is a classical result in simplicial geometry: for a simplex, the sum over its faces of the deficit angle times the variation of the face area with respect to a vertex position vanishes. In Regge calculus, this identity is exactly the discrete contracted Bianchi identity. The framework's machine-checked library of formal theorems states this equivalence as a named property, SchlafliIdentityAtVertex, and proves that the two formulations are logically equivalent for abstract Regge data.

The declaration discreteBianchiContractedCert_inhabited proves that a certificate bundling these facts exists. The certificate contains three components: the equivalence between the discrete Bianchi and the Schläfli identity, the derivation of the Bianchi from the Schläfli hypothesis, and a witness showing the hypothesis space is nonempty. That witness is the flat substrate: Regge data where every deficit angle, bone area, and vertex gradient is zero. In plain language, the theorem establishes that the structural scaffold of discrete gravity is consistent, because empty flat space satisfies the discrete Einstein constraint trivially.

In Recognition Science, this result is a structural theorem, not a physical prediction. It proves that the abstract framework for discrete gravity has a model, but it does not prove that the full Schläfli identity holds for arbitrary triangulations. The general proof, requiring the simplex volume-area relation and its kinematic consequences, remains future work. The theorem also does not address the continuum limit, which is a separate track in the framework's master plan. What the declaration does establish is that the discrete Bianchi identity is not vacuous: there is at least one concrete configuration, flat space, where it holds.

/-- **Structural equivalence**: the contracted discrete Bianchi at a
vertex equals the Schläfli identity at that vertex. This is the
definitional identification in Regge calculus. -/
theorem discreteBianchi_eq_schlafli {V B : Type} [Fintype B]
    (R : ReggeData V B) (v : V) :
    DiscreteBianchiContractedAtVertex R v ↔ SchlafliIdentityAtVertex R v :=
  Iff.rfl

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

The general Schläfli identity for arbitrary triangulations is not proved here. The continuum limit of Regge calculus is not established by this declaration. No physical prediction about gravity in our universe follows from this structural theorem.

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: