flat_bianchi
plain-language theorem explainer
For a flat lattice where every deficit angle vanishes, the linearized discrete Bianchi identity holds by direct reduction of the summed deficits. Discrete gravity researchers working in Regge calculus within the Recognition Science framework cite this as the trivial base case that initiates the discrete conservation law. The proof is a straightforward induction on the input list that repeatedly applies the zero hypothesis and the zero_add lemma to collapse the sum.
Claim. Let $D = (d_1, d_2, ..., d_k)$ be a finite list of real numbers. If $d_i = 0$ for every index $i$, then the linearized discrete Bianchi identity holds for $D$.
background
The DiscreteBianchi module formalizes the exact discrete Bianchi identity for Regge calculus following Hamber and Kagel (2004). This is the lattice analog of the contracted Bianchi identity nabla^mu G_mu_nu = 0; when combined with the Regge equations it forces a discrete conservation law for the stress-energy. Deficit angles measure curvature at hinges, and the linearized version approximates the identity for small angles. The local setting treats the product of holonomy matrices around contractible loops as the identity, with the flat case serving as the starting point for the full constraint on neighboring deficits.
proof idea
The proof unfolds the definition of the linearized Bianchi identity and proceeds by induction on the list of deficits. The nil case collapses immediately by simplification. In the cons case the hypothesis forces the head entry to zero, the sum is rewritten via sum_cons and zero_add, and the inductive hypothesis is applied to the tail under the restricted membership predicate.
why it matters
This result supplies the flat_ok field of the DiscreteBianchiCert theorem, which packages flat_bianchi together with linearized_implies_general and conservation_from_bianchi. It therefore anchors the discrete analog of the Bianchi identity that, together with the Regge equations, yields conservation_from_bianchi. In the broader Recognition framework it supports the passage from lattice geometry to the eight-tick octave and the emergence of three spatial dimensions by ensuring consistency of the discrete curvature constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.