discreteBianchi_eq_schlafli
plain-language theorem explainer
In abstract Regge data, the contracted discrete Bianchi identity at a vertex is definitionally the same proposition as the Schläfli identity at that vertex. Anyone citing Track 1.C (discrete Bianchi on the Regge substrate) uses this as the structural identification. The proof is a one-line reflexivity of iff, since the Bianchi predicate is defined to be the Schläfli sum.
Claim. For any finite bone index set and any abstract Regge triangulation $R$ on vertices $V$ and bones $B$, and for every vertex $v\in V$, the contracted discrete Bianchi identity at $v$ holds if and only if the Schläfli identity at $v$ holds: $\sum_b \varepsilon_b\,\partial A_b/\partial x_v = 0$ componentwise in $\mathbb{R}^4$.
background
Track 1.C of the quantum-gravity master plan asks for the contracted discrete Bianchi identity $\nabla_\mu G^{\mu\nu}=0$ on a Regge triangulation. In continuum GR that identity is kinematic; in Regge calculus its discrete avatar is the Schläfli identity at each interior vertex.
Abstract Regge data packages vertex positions in $\mathbb{R}^4$, an incidence relation between bones and vertices, deficit angles $\varepsilon_b$ (holonomy around each bone), bone areas $A_b$, and the vertex-area gradients $\partial A_b/\partial x_v$ (zero off the star of $v$). The Schläfli identity at $v$ is the componentwise vanishing sum $\sum_b \varepsilon_b,(\partial A_b/\partial x_v)_i=0$ for $i\in{0,1,2,3}$.
The contracted discrete Bianchi at $v$ is introduced in this module as the discrete analog of $\nabla_\mu G^{\mu\nu}=0$ evaluated at $v$. By design in Regge calculus the two propositions express the same kinematic constraint: covariance of the Regge action under vertex variations.
proof idea
One-line term proof: Iff.rfl. The predicate DiscreteBianchiContractedAtVertex R v is defined to be exactly SchlafliIdentityAtVertex R v, so the biconditional is definitional equality of propositions and holds by reflexivity of ↔. No algebraic lemmas or summation identities are invoked.
why it matters
This is the structural hinge of Track 1.C. The module doc states the goal explicitly: prove that in Regge calculus the Schläfli identity IS the contracted discrete Bianchi at the structural level. Downstream, discrete_bianchi_contracted_one_statement packages the equivalence together with the implication from global Schläfli data, and discreteBianchiContractedCert records both facts in the Track 1.C certificate.
Gravity's physicalReggeEHBianchiInterface_of_localCorrespondence consumes the same interface when assembling the combined Track 1B-PHY / 1.C physical residual. The identification does not yet prove Schläfli from simplex geometry; it freezes the definitional bridge so that later geometric work can discharge the named structural hypothesis without renaming the Bianchi side.
Relative to the forcing chain, this sits on the gravity/geometry side rather than T5–T8, but it is the discrete kinematic counterpart of diffeomorphism covariance that continuum GR inherits once $D=3$ and the eight-tick octave are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.