IndisputableMonolith.Gravity.DiscreteBianchi
The DiscreteBianchi module supplies the hinge-rotation and discrete Bianchi machinery for Regge calculus on the RS lattice. Gravity modelers cite it when replacing linearized deficit assumptions with exact nonlinear identities. The module consists of definitions for SO(3) rotations by deficit angles together with lemmas that derive loop holonomy closure and conservation statements from those rotations.
claimHingeRotation($\theta$) denotes the SO(3) rotation in the plane normal to a 3D edge by the deficit angle $\theta$. The discrete Bianchi identity asserts that the composition of such rotations around any closed loop yields the identity element in SO(3).
background
The module imports Constants, which fixes the RS time quantum $\tau_0 = 1$ tick, and ReggeCalculus, whose doc-comment states that it replaces the linearized deficit-angle ansatz (Assumption A2) with the full nonlinear Regge framework on the RS lattice. In this setting the hinge is a 1-dimensional edge and the deficit angle measures the failure of parallel transport to close after one circuit.
HingeRotation is defined as the element of SO(3) whose rotation angle equals the deficit; compose_same_axis and loop_holonomy then build the group product of these rotations. The module therefore operates entirely within the D = 3 sector of the eight-tick octave lattice.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the discrete Bianchi identity and the derived conservation_from_bianchi lemma that feed the continuum-limit statement H_bianchi_continuum_limit. It therefore occupies the step that converts the Regge-calculus replacement of the linearized ansatz into a closed set of identities from which the Einstein tensor can be recovered in the long-wavelength limit.
scope and limits
- Does not treat dimensions other than D = 3.
- Does not include matter sources or stress-energy tensors.
- Does not derive the continuum Einstein equations.
- Does not address quantum fluctuations beyond the classical Regge lattice.
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