Geometry Discrete Bianchi Discrete Bianchi Contracted From Schlafli

The contracted Bianchi identity

In the simplicial geometry of Regge calculus, spacetime is built from flat triangular or tetrahedral pieces joined at shared faces. The curvature of such a piecewise-flat space is concentrated along the lower-dimensional hinges, called bones, where the pieces meet. The contracted Bianchi identity is a kinematic constraint on this curvature: it says that a certain weighted sum of the changes in bone areas, when one vertex of the triangulation is moved, vanishes exactly. This is the discrete analogue of the statement that the divergence of the Einstein tensor is zero in the continuum theory of general relativity.

The identity is equivalent to a classical result in simplex geometry, the Schläfli identity. For each interior vertex v, the sum over the bones b meeting at v of the deficit angle ε_b times the derivative of the bone area A_b with respect to the vertex position x_v is zero. The deficit angle is the amount by which the flat pieces around a bone fail to close flat, a measure of curvature there. The Schläfli identity is not an equation of motion; it is a purely geometric fact about how the volumes and angles of a simplex change under a variation of its vertices.

In Recognition Science, the machine-checked library of formal theorems contains a module that makes this structural relationship precise. It defines abstract data for a Regge triangulation: the vertices, the bones, the deficit angles, the bone areas, and the gradients of those areas with respect to vertex positions. It then states two named properties at a vertex: the Schläfli identity and the contracted discrete Bianchi identity. The declaration discrete_bianchi_contracted_from_schlafli proves, as a theorem, that any Regge data satisfying the Schläfli identity at every vertex also satisfies the contracted discrete Bianchi identity there. The proof is a one-line unfolding of definitions: the Bianchi property is defined to be exactly the Schläfli property.

The module also proves the converse direction, so the two identities are formally equivalent, and it provides a non-vacuous witness: the flat substrate, where all deficit angles and gradients are zero, satisfies the Schläfli identity by construction. This shows the statement is not empty, though it is the trivial case. The certificate bundles these results: the implication, the equivalence, and the existence of the flat witness.

What this declaration does not establish is the general Schläfli identity for arbitrary triangulations. The module takes the Schläfli identity as a named structural hypothesis. Proving that the identity holds for any actual geometric triangulation, from the simplex volume-area relation, remains future work in the library. The theorem here is conditional: if the geometry satisfies the Schläfli identity, then the contracted discrete Bianchi identity follows. The unconditional geometric proof is an open target.

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

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

What this page does not claim

The general Schläfli identity for arbitrary triangulations is not proved here; it is a named structural hypothesis. The declaration does not prove that any physical spacetime satisfies the Schläfli identity. The flat substrate witness is the trivial case; it does not demonstrate the identity for curved 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: