Pith. sign in
module module high

IndisputableMonolith.Geometry.DiscreteBianchi

show as:
view Lean formalization →

Defines abstract Regge triangulation data (vertices, bones, deficit angles as holonomies, bone-area gradients) and proves the contracted discrete Bianchi identity equals the Schläfli identity at each vertex. Gravity Track 1.B/1.C imports it as the discrete-curvature half of the structural witness. The argument is algebraic: equate the contracted Bianchi sum to the Schläfli sum on any ReggeData, then specialize to flat data.

claimOn abstract Regge data $(V,B,\varepsilon,\partial A)$ with deficit angles $\varepsilon_b$ (holonomy around bone $b$) and bone-area gradients $\partial_v A_b$, the contracted discrete Bianchi identity at each vertex $v$ is identical to the Schläfli identity $\sum_b \varepsilon_b\,\partial_v A_b = 0$. Flat configurations satisfy both identities, and a certificate packages the equality for downstream use.

background

Regge calculus replaces smooth spacetime by a piecewise-flat simplicial complex. Curvature concentrates on codimension-2 hinges ("bones"): the deficit angle $\varepsilon_b$ is the holonomy of parallel transport around bone $b$. The Einstein–Hilbert action becomes a sum of $\varepsilon_b A_b$, so stationarity and Bianchi identities reduce to combinatorial relations among deficits and areas.

This module axiomatizes that data over arbitrary vertex and bone index types: a record ReggeData carries deficits and the partials $\partial_v A_b$ (zero when $v$ is not incident on $b$). The classical Schläfli identity states that the first variation of the action vanishes identically under pure vertex motion when the metric is held edge-length consistent; its discrete form is $\sum_b \varepsilon_b,\partial_v A_b = 0$ at each vertex.

The contracted discrete Bianchi identity is the same linear combination, re-interpreted as the discrete analogue of $\nabla^\mu G_{\mu\nu}=0$. The module therefore treats Bianchi and Schläfli as two names for one algebraic constraint on Regge data.

proof idea

Definition layer first: ReggeData and the two vertex-wise propositions SchlafliIdentityAtVertex and DiscreteBianchiContractedAtVertex. The core lemma discreteBianchi_eq_schlafli is a direct propositional equality of those two sums, so any structure satisfying one satisfies the other (discrete_bianchi_contracted_from_schlafli).

Flat data (flatReggeData) set all deficits to zero; the Schläfli sum vanishes trivially, yielding flatSchlafliReggeData and an inhabited instance. A small certificate type DiscreteBianchiContractedCert packages the equality for import by gravity modules. No analytic estimates or continuum limits appear; the module is pure finite-sum algebra over the abstract index types.

why it matters in Recognition Science

Track 1.B/1.C of the gravity program needs a discrete Bianchi identity that matches the Regge–Einstein–Hilbert variation. Downstream module Gravity.Track1BCStructural imports this file as the "Discrete Bianchi" half of its structural witness (status: 0 sorry, closure 2026-05-22).

Within Recognition Science geometry, the result supplies the combinatorial conservation law that continuum GR obtains from $\nabla\cdot G=0$. It does not yet force $D=3$ or the eight-tick structure (those live in the T0–T8 forcing chain); it only guarantees that whatever Regge skeleton is later coupled to the recognition ladder already obeys the correct contracted Bianchi/Schläfli identity. The certificate is the hook used by the master structural theorem.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (14)