discrete_conservation
plain-language theorem explainer
Discrete conservation asserts that Regge equations holding for a list of hinges together with the linearized Bianchi identity on their deficit angles forces the discrete stress-energy to be conserved. Researchers working on Regge-calculus discretizations of gravity cite it to recover the continuum implication nabla^mu T_mu_nu = 0 from nabla^mu G_mu_nu = 0. The definition encodes the implication directly as a Prop by mapping hinges to deficit angles and invoking the sum-zero condition.
Claim. Let $H$ be a list of hinge data. If the Regge equations hold for every hinge in $H$ and the sum of deficit angles over $H$ is zero, then the discrete stress-energy tensor is conserved: $H : List HingeData, (Regge eqs satisfied) → (sum deficit angles = 0) → conservation.
background
HingeData is the structure recording the area and list of dihedral angles at a codimension-2 face in a Regge triangulation; deficit_angle extracts the curvature measure 2π minus the sum of those dihedral angles. linearized_bianchi is the predicate that the sum of deficit angles over a list vanishes exactly, which is the small-curvature reduction of the full discrete Bianchi identity. The module sets the local setting as the discrete analog of the contracted Bianchi identity nabla^mu G_mu_nu = 0 in Regge calculus, following Hamber-Kagel, so that the Einstein-Regge equations plus this identity imply conservation of the discrete stress-energy.
proof idea
One-line wrapper that directly assembles the universal quantifier over hinge lists, applies the map operation to extract deficit angles, and composes the linearized_bianchi predicate with the placeholder Regge-equation hypothesis to yield the conservation Prop.
why it matters
The definition supplies the Prop consumed by conservation_from_bianchi and by the DiscreteBianchiCert structure, closing the discrete version of the continuum argument that Bianchi plus Einstein equations force nabla^mu T_mu_nu = 0. It anchors the gravity sector of the Recognition framework by ensuring structural consistency between curvature constraints and matter sources, parallel to the T5-T8 forcing chain that fixes dimension and self-similarity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.