pith. sign in
module module high

IndisputableMonolith.Gravity.WeakFieldConformalRegge

show as:
view Lean formalization →

The module supplies the exact identity relating squared edge lengths to the sum of vertex potentials ξ in the conformal weak-field regime. Workers linearizing the Regge action from the J-cost functional cite it when passing from the simplicial ledger to continuum gravity. The development consists of the exact statement, its second-order Taylor expansion, and explicit remainder estimates that vanish under the weak-field scaling.

claim$\ell_{ij}(\xi)^2 = \ell_0^2 \exp(\xi_i + \xi_j)$

background

The module sits inside the Recognition Science derivation of gravity. ContinuumBridge identifies the J-cost functional on the simplicial ledger with the Regge action (up to normalization by κ = 8φ⁵) and shows that stationarity δJ = 0 recovers the Regge equations. EdgeLengthFromPsi supplies the map from the recognition-potential field ψ on 3-simplices to the full set of edge lengths required by that action. Schläfli supplies the differential identities for piecewise-flat complexes, while Constants fixes the RS time quantum τ₀ = 1 tick.

proof idea

The module opens with the exact identity conformal_length_sq_exact. It then records the second-order Taylor expansion conformal_length_sq_taylor2 together with the remainder term conformal_remainder. The lemma conformal_remainder_zero shows the remainder vanishes to the order needed for the quadratic action. Supporting lemmas decompose the squared lengths, introduce the Dirichlet and quadratic forms, and verify the first- and second-order edge contributions.

why it matters in Recognition Science

The module supplies the conformal weak-field expansion required to linearize the Regge action inside ContinuumBridge. It thereby supports the passage from J-cost stationarity to the Einstein field equations in the Gravity from Recognition draft (Theorem 5.1, Field-Curvature Identity). Without this expansion the discrete-to-continuum limit in the weak-field sector remains formal.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (40)