Geometry Discrete Bianchi Discrete Bianchi Contracted One Statement

The discrete Bianchi identity

The contracted Bianchi identity is a core consistency condition in general relativity. In the continuum, it states that the divergence of the Einstein tensor vanishes, which is a kinematic constraint that must hold for the field equations to be self-consistent. In Regge calculus, a discrete approximation to spacetime built from flat simplices, the analogous condition is that a certain sum over the bones (the lower-dimensional faces) incident to each interior vertex vanishes. This discrete condition is equivalent to the Schläfli identity, a kinematic identity in simplicial geometry that relates the variation of deficit angles to the variation of bone areas.

The machine-checked library of formal theorems now contains a structural proof of this equivalence. The declaration discrete_bianchi_contracted_one_statement establishes three things: first, that any Regge data satisfying the Schläfli identity at every vertex also satisfies the contracted discrete Bianchi identity at every vertex; second, that the two conditions are equivalent for any Regge data; and third, that there exists at least one non-vacuous example, namely the flat substrate where all deficit angles and areas are zero. This last point matters because it shows the statement is not empty: there is a concrete model in which the discrete Bianchi identity holds.

The proof is structural rather than geometric. It does not derive the Schläfli identity from the simplex volume-area relation; that full derivation remains future work. Instead, the library defines the abstract data needed to state the identity, names the Schläfli condition as a property, and proves the equivalence by definition. The flat-substrate example is a witness that the hypothesis space is inhabited, not a demonstration of the identity for arbitrary triangulations.

In Recognition Science, this declaration is part of a larger track toward quantum gravity. It supplies the discrete Bianchi identity as a named structural hypothesis, which is a load-bearing component of the master theorem. The declaration does not close the general Schläfli identity for arbitrary Regge triangulations, nor does it prove the continuum convergence of Regge calculus. Those remain open targets.

/-- **TRACK 1.C ONE-STATEMENT** (structural form). For any Regge
triangulation `R` satisfying the Schläfli identity at every vertex,
the contracted discrete Bianchi identity holds at every vertex.
Together with the equivalence
`DiscreteBianchiContractedAtVertex R v ↔ SchlafliIdentityAtVertex R v`,
this gives the structural form of the master theorem clause
`discrete_bianchi_contracted` (Track 1.C of the master plan). -/
theorem discrete_bianchi_contracted_one_statement
    (V B : Type) [Fintype B] :
    (∀ (R : SchlafliReggeData V B) (v : V),
        DiscreteBianchiContractedAtVertex R.toReggeData v) ∧
    (∀ (R : ReggeData V B) (v : V),
        DiscreteBianchiContractedAtVertex R v ↔ SchlafliIdentityAtVertex R v) ∧
    Nonempty (SchlafliReggeData V B) :=
  ⟨discrete_bianchi_contracted_from_schlafli,
   discreteBianchi_eq_schlafli,
   SchlafliReggeData_inhabited V B⟩

/-- **TRACK 1.C ONE-STATEMENT** (structural form). For any Regge
triangulation `R` satisfying the Schläfli identity at every vertex,
the contracted discrete Bianchi identity holds at every vertex.
Together with the equivalence
`DiscreteBianchiContractedAtVertex R v ↔ SchlafliIdentityAtVertex R v`,
this gives the structural form of the master theorem clause
`discrete_bianchi_contracted` (Track 1.C of the master plan). -/
theorem discrete_bianchi_contracted_one_statement
    (V B : Type) [Fintype B] :
    (∀ (R : SchlafliReggeData V B) (v : V),
        DiscreteBianchiContractedAtVertex R.toReggeData v) ∧
    (∀ (R : ReggeData V B) (v : V),
        DiscreteBianchiContractedAtVertex R v ↔ SchlafliIdentityAtVertex R v) ∧
    Nonempty (SchlafliReggeData V B) :=
  ⟨discrete_bianchi_contracted_from_schlafli,
   discreteBianchi_eq_schlafli,
   SchlafliReggeData_inhabited V B⟩

/-- **TRACK 1.C ONE-STATEMENT** (structural form). For any Regge
triangulation `R` satisfying the Schläfli identity at every vertex,
the contracted discrete Bianchi identity holds at every vertex.
Together with the equivalence
`DiscreteBianchiContractedAtVertex R v ↔ SchlafliIdentityAtVertex R v`,
this gives the structural form of the master theorem clause
`discrete_bianchi_contracted` (Track 1.C of the master plan). -/
theorem discrete_bianchi_contracted_one_statement
    (V B : Type) [Fintype B] :
    (∀ (R : SchlafliReggeData V B) (v : V),
        DiscreteBianchiContractedAtVertex R.toReggeData v) ∧
    (∀ (R : ReggeData V B) (v : V),
        DiscreteBianchiContractedAtVertex R v ↔ SchlafliIdentityAtVertex R v) ∧
    Nonempty (SchlafliReggeData V B) :=
  ⟨discrete_bianchi_contracted_from_schlafli,
   discreteBianchi_eq_schlafli,
   SchlafliReggeData_inhabited V B⟩

What this page does not claim

The general Schläfli identity for arbitrary Regge triangulations is proved. The continuum limit of Regge calculus is established. The declaration provides a physical derivation of the discrete Bianchi identity from geometry.

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: