Geometry Discrete Bianchi Discrete Bianchi Contracted Cert

The contracted Bianchi identity

In the simplicial geometry used to discretize general relativity, the contracted Bianchi identity is a local conservation law. It states that a certain weighted sum of area changes vanishes at each vertex of a triangulation. This identity is the discrete analogue of the statement that the divergence of the Einstein tensor is zero, which in the continuum is a direct consequence of the field equations. The classical Schläfli identity is the geometric fact that 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 equals zero.

The formal library's DiscreteBianchiContractedCert establishes a structural theorem: it defines the abstract data of a Regge triangulation (vertices, bones, deficit angles, areas), and proves that the contracted discrete Bianchi identity at a vertex is equivalent to the Schläfli identity at that vertex. This is a machine-checked proof, with zero axioms beyond the standard logical ones. The certificate also provides a canonical witness: the flat substrate, where all deficit angles are zero, satisfies the identity non-vacuously, so the statement is not empty.

What the certificate does not claim is the general Schläfli identity for arbitrary triangulations. That remains open, requiring a full proof of the simplex volume-area relation. The certificate is a structural scaffold: it fixes the statement and proves the equivalence under a named hypothesis, but the unconditional geometric proof is future work. In the framework's own terms, this is a theorem under a hypothesis, not an unconditional law.

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

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

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

What this page does not claim

The general Schläfli identity for arbitrary triangulations is not proved; only the structural equivalence under the named hypothesis is established. The certificate does not prove the continuum limit or the full Regge action covariance; that requires the Track 1.B convergence result. The flat substrate witness does not demonstrate the identity for curved or non-trivial geometries.

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: