Pith. sign in
module module moderate

IndisputableMonolith.Gravity.DiscreteBianchi

show as:
view Lean formalization →

The DiscreteBianchi module formalizes hinge rotations and the discrete Bianchi identity inside the Regge calculus treatment of Recognition Science gravity. Researchers deriving conservation from curvature on the RS lattice would cite these results. The module builds the identity by composing SO(D) rotations around loops, using the nonlinear machinery imported from ReggeCalculus.

claimA hinge rotation is the element of SO(D) acting in the 2-plane normal to a (D-2)-dimensional hinge with rotation angle equal to the deficit angle. The discrete Bianchi identity asserts that the product of such rotations around any closed loop equals the identity: $\prod_i R(\delta_i) = I$.

background

The module sits inside the discrete gravity programme on the RS lattice. Its direct import ReggeCalculus supplies the exact nonlinear Regge framework that replaces the linearized deficit-angle ansatz (Assumption A2 in the paper) with full Regge machinery. Constants supplies the base time quantum $\tau_0 = 1$ tick. The central definition is HingeRotation: an SO(D) rotation in the plane perpendicular to the hinge whose angle equals the deficit; in three dimensions the hinge is an edge and the rotation lies in the orthogonal plane.

proof idea

The module first defines HingeRotation and auxiliary operations compose_same_axis and loop_holonomy. It then establishes discrete_bianchi_identity by showing that the total holonomy around any closed loop is the identity. Linearized_bianchi and flat_bianchi are obtained as special cases; H_bianchi_continuum_limit extracts the classical identity under refinement.

why it matters in Recognition Science

DiscreteBianchi supplies the curvature constraint that feeds discrete_conservation and conservation_from_bianchi. It realizes the discrete version of the Bianchi identity required by the Regge calculus replacement of Assumption A2, linking directly to the D = 3 spatial dimensions fixed by the forcing chain (T8). No downstream declarations are recorded, yet the module closes the discrete-to-continuum bridge inside the gravity domain.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (12)