Geometry Discrete Bianchi Discrete Bianchi Eq Schlafli

The discrete Bianchi identity

In Regge calculus, spacetime is approximated by a network of flat simplices, and curvature lives only along the shared edges, called bones. The theory's central constraint is that the Einstein tensor's divergence vanishes, a condition that guarantees the action is unchanged by moving a vertex. In the discrete setting, this constraint takes the form: 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.

This discrete Bianchi identity is not a new condition. It is exactly the Schläfli identity, a kinematic fact about simplicial geometry that follows from the volume-area relation of a simplex. The machine-checked library of formal theorems records this as an equivalence: the property named DiscreteBianchiContractedAtVertex holds if and only if SchlafliIdentityAtVertex holds. The proof is immediate, since one is defined as the other, but the content is the identification of two apparently different statements.

The library also provides a witness that the condition is not vacuous: the flat substrate, where all deficit angles are zero, satisfies the identity by construction. This establishes that the discrete Bianchi constraint is consistent and has at least one model. The certificate bundles the equivalence, the implication from the Schläfli hypothesis, and the existence of the flat witness into a single object.

In Recognition Science, this declaration is a structural theorem: it proves the equivalence of two named properties within the framework's formal system, with no unproved assumptions in the library's own axioms. It does not prove the general Schläfli identity for arbitrary triangulations, which requires substantial infrastructure in simplex geometry and remains future work. It also does not claim that the discrete Bianchi identity holds for all Regge data; it only states the equivalence and provides a flat example where it holds.

What this changes is the status of the discrete Bianchi identity in the framework's development. It is no longer an open conjecture but a structural fact, conditional on the Schläfli hypothesis being satisfied. The next step is to prove that hypothesis for general triangulations, which would complete the discrete side of the gravity track.

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

noncomputable def discreteBianchiContractedCert
    (V B : Type) [Fintype B] : DiscreteBianchiContractedCert V B where
  discrete_bianchi_at_every_vertex := discrete_bianchi_contracted_from_schlafli
  schlafli_iff_bianchi := discreteBianchi_eq_schlafli
  hypothesis_space_inhabited := SchlafliReggeData_inhabited V B

What this page does not claim

The general Schläfli identity for arbitrary Regge triangulations is not proved here. The discrete Bianchi identity does not hold for all Regge data, only for those satisfying the Schläfli hypothesis. This declaration does not establish the full Track 1 closure, which also requires the continuum convergence result.

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: