module module high

`IndisputableMonolith.Geometry.DiscreteBianchi`

Abstract Regge triangulation data: deficit angles as bone holonomies and bone-area gradients with respect to incident vertices. Supplies the discrete contracted Bianchi identity via the Schläfli relation at each vertex, plus flat and certificate witnesses. Gravity Track 1.B/1.C imports it as the structural half of the Regge–Einstein–Hilbert continuum plus discrete Bianchi package. The development is definitional scaffolding plus algebraic identification of the contracted Bianchi sum with the Schläfli identity.

claimOver abstract vertex and bone index types, Regge data assign to each bone a deficit angle $\varepsilon_b$ (holonomy of parallel transport around the bone) and bone-area gradients $\partial A_b/\partial x_v$ (zero unless $v$ is incident on $b$). The contracted discrete Bianchi identity at a vertex is the vanishing of $\sum_b \varepsilon_b\,\partial A_b/\partial x_v$, and equals the Schläfli identity on the same data.

background

Regge calculus replaces smooth curvature by deficit angles on the bones (codimension-2 hinges) of a triangulation. The deficit is the holonomy of parallel transport around a bone; the Einstein–Hilbert action becomes a sum of deficit times bone area. Variation with respect to vertex positions yields a discrete Einstein equation once the Schläfli identity is used to cancel pure area variations.

This module packages that combinatorial skeleton without committing to a concrete mesh: vertex and bone index types, deficit angles, and bone-area gradients that vanish for non-incident vertices. The contracted discrete Bianchi identity at a vertex is the weighted sum of deficits by those gradients. In the continuum the (contracted) Bianchi identity is $\nabla^a G_{ab}=0$; here the discrete analogue is identified with the classical Schläfli relation on the same Regge data.

Flat configurations (vanishing deficits) inhabit the structure and supply trivial witnesses. A certificate type records that the contracted Bianchi sum equals the Schläfli form, ready for import by gravity-track structural theorems.

proof idea

Definition module with a thin algebraic layer. Regge data and the two vertex-wise propositions (Schläfli identity; contracted discrete Bianchi) are introduced as structures and Props. The key lemma is an equality of those two Props on any Regge data: the contracted Bianchi sum is definitionally the Schläfli sum, so one holds iff the other does. Flat Regge data (zero deficits) discharge both identities by direct substitution. Inhabited instances and a certificate wrapper package the equality for downstream structural witnesses. No analytic estimates or continuum limits live here.

why it matters in Recognition Science

Feeds Gravity.Track1BCStructural, the structural witness for the master Track 1.B/1.C theorem (Regge–EH continuum plus discrete Bianchi; status: structural theorem, 0 sorry, closure 2026-05-22). That parent module needs a clean, Mathlib-only discrete Bianchi side so the continuum matching can sit on a named algebraic identity rather than an ad-hoc sum. Within Recognition Science geometry, this is the discrete conservation law dual to the continuum contracted Bianchi identity, ensuring the Regge skeleton used for gravity tracks is variationally consistent at each vertex. It does not itself force $D=3$ or the eight-tick octave; those enter elsewhere in the forcing chain. It closes the combinatorial half of the Track 1 structural package.

scope and limits

Does not construct a concrete triangulation or embed bones in $\mathbb{R}^n$.
Does not prove a continuum limit to $\nabla^a G_{ab}=0$.
Does not derive Einstein equations from a variational principle here.
Does not force spatial dimension $D=3$ or link to the eight-tick octave.
Does not address curvature bounds, convergence rates, or numerical stability.

used by (1)

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

IndisputableMonolith.Gravity.Track1BCStructural module_import

declarations in this module (14)

structure ReggeData L95
def SchlafliIdentityAtVertex L120
def DiscreteBianchiContractedAtVertex L130
theorem discreteBianchi_eq_schlafli L137
structure SchlafliReggeData L148
theorem discrete_bianchi_contracted_from_schlafli L157
def flatReggeData L168
theorem flatReggeData_schlafli L179
def flatSchlafliReggeData L187
theorem SchlafliReggeData_inhabited L194
structure DiscreteBianchiContractedCert L203
def discreteBianchiContractedCert L219
theorem discreteBianchiContractedCert_inhabited L225
theorem discrete_bianchi_contracted_one_statement L239