Geometry Discrete Bianchi

The discrete Bianchi identity

The contracted Bianchi identity, ∇_μG^μν = 0, is a fundamental constraint in general relativity: it says the Einstein tensor has zero divergence, which is required for the Einstein field equations to be consistent. In Regge calculus, a discrete approach to general relativity where spacetime is approximated by flat simplices, this identity takes a discrete form. The module DiscreteBianchi.lean in the Recognition Science library establishes a structural theorem about this discrete identity.

The key result is that the contracted discrete Bianchi identity at a vertex is equivalent to the Schläfli identity, a kinematic identity in simplicial geometry. The Schläfli identity states that for each interior vertex v of a triangulation, the sum over bones b incident to v of the deficit angle ε_b times the derivative of the bone area A_b with respect to the vertex position x_v equals zero: Σ_b∋v ε_b · ∂A_b/∂x_v = 0. This is a purely geometric statement about how areas change when a vertex moves.

The module defines abstract Regge data, states the Schläfli identity at a vertex as a named property, and proves the equivalence with the contracted discrete Bianchi. It also provides a canonical witness: the flat substrate, where all deficit angles are zero, satisfies the identity by construction. This ensures the result is non-vacuous. The proof is machine-checked with zero sorry and zero RS-specific axioms.

In Recognition Science, this structural theorem is part of a larger quantum-gravity master plan. The module closes Track 1.C, establishing the discrete Bianchi identity at the structural level. However, the general Schläfli identity for arbitrary triangulations remains future work, requiring a full proof of the simplex volume-area relation. The current result is a scaffold, not the complete geometric proof.

What this means in plain language: the framework has verified that a key constraint in discrete gravity is equivalent to a known geometric identity. This is a necessary step, but not the final one, in building a fully verified discrete gravity theory.

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

/-- The hypothesis space of Schläfli-satisfying Regge triangulations is
nonempty (witnessed by `flatSchlafliReggeData`). -/
theorem SchlafliReggeData_inhabited (V B : Type) [Fintype B] :
    Nonempty (SchlafliReggeData V B) :=
  ⟨flatSchlafliReggeData V B⟩

/-- **Track 1.C structural theorem**: in any Schläfli-satisfying Regge
triangulation, the contracted discrete Bianchi holds at every vertex.

This is the conditional form of `discrete_bianchi_contracted` from the
master theorem template, awaiting the unconditional Schläfli identity
proof (multi-session geometry work). -/
theorem discrete_bianchi_contracted_from_schlafli {V B : Type} [Fintype B]
    (R : SchlafliReggeData V B) (v : V) :
    DiscreteBianchiContractedAtVertex R.toReggeData v :=
  R.schlafli v

What this page does not claim

The general Schläfli identity for arbitrary Regge triangulations is not proved. The module does not establish the continuum limit of Regge calculus. The result does not derive the Einstein field equations from discrete 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: