IndisputableMonolith.Gravity.DiscreteBianchi
DiscreteBianchi module supplies the discrete Bianchi identity and supporting structures inside the Regge calculus treatment of RS gravity. It defines hinge rotations by deficit angles together with composition, holonomy, and conservation statements. Gravity modelers cite it when moving from linearized deficit assumptions to the full nonlinear Regge setting on the RS lattice. The module consists of a chain of definitions and lemmas imported from ReggeCalculus.
claimThe module defines hinge rotation $R_h$ as the element of $SO(D)$ acting by the deficit angle in the 2-plane normal to a $(D-2)$-dimensional hinge; it states the discrete Bianchi identity on closed loops and derives the associated conservation law.
background
The module belongs to the Gravity domain and imports Constants (where the RS time quantum satisfies τ₀ = 1 tick) together with ReggeCalculus. The upstream ReggeCalculus module states that it “Formalizes the exact (nonlinear) Regge calculus framework for the RS discrete gravity programme. This replaces the linearized deficit-angle ansatz (Assumption A2 in the paper) with the full Regge machinery.”
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the discrete Bianchi identity, loop holonomy, and conservation_from_bianchi that feed the continuum-limit statement H_bianchi_continuum_limit and the overall discrete gravity programme. It completes the exact Regge treatment required to reach the classical limit without Assumption A2 and supports the forcing-chain step that fixes D = 3.
scope and limits
- Does not linearize deficit angles.
- Does not specify a concrete lattice triangulation.
- Does not derive the Einstein tensor explicitly.
- Does not include quantum corrections.
depends on (2)
declarations in this module (12)
-
structure
HingeRotation -
def
compose_same_axis -
def
loop_holonomy -
def
discrete_bianchi_identity -
def
linearized_bianchi -
theorem
linearized_implies_general -
theorem
flat_bianchi -
def
discrete_conservation -
theorem
conservation_from_bianchi -
def
H_bianchi_continuum_limit -
structure
DiscreteBianchiCert -
theorem
discrete_bianchi_cert