IndisputableMonolith.Gravity.WeakFieldConformalRegge
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
- Does not treat non-conformal metric perturbations.
- Does not include matter sources or cosmological terms.
- Does not establish convergence of the discrete action to the Einstein-Hilbert functional.
- Does not fix the overall normalization constant κ.
depends on (4)
declarations in this module (40)
-
theorem
conformal_length_sq_exact -
def
conformal_remainder -
theorem
conformal_length_sq_taylor2 -
theorem
conformal_remainder_zero -
def
edgeSqFirstOrder -
def
edgeSqSecondOrder -
theorem
conformal_length_sq_decomposition -
def
dirichletForm -
def
quadraticForm -
lemma
sum_const_mul_right -
lemma
inner_sum_const -
theorem
dirichlet_eq_neg_quadratic -
theorem
dirichlet_form_eq_neg_quadratic -
structure
WeakFieldReggeData -
def
bilinearCoefficient -
theorem
bilinearCoefficient_symm -
def
SchlaefliRowSum -
def
secondOrderReggeAction -
def
edgeArea -
theorem
edgeArea_symm -
theorem
dirichletForm_neg -
theorem
dirichletForm_edgeArea -
theorem
weak_field_conformal_reduction -
theorem
weak_field_conformal_reduction_kappa -
theorem
secondOrderReggeAction_flat -
theorem
dirichletForm_flat -
def
edgeAreaGraph -
theorem
secondOrder_eq_half_laplacian_action -
def
laplacianCoefficient -
theorem
laplacianCoefficient_symm -
theorem
laplacianCoefficient_row_sum -
def
laplacianReggeData -
theorem
bilinearCoefficient_laplacianReggeData -
theorem
schlaefliRowSum_laplacianReggeData -
theorem
dirichletForm_diag_irrelevant -
theorem
dirichletForm_edgeArea_laplacianReggeData -
theorem
weak_field_conformal_reduction_laplacianData -
theorem
weak_field_conformal_reduction_laplacianData_kappa -
structure
WeakFieldConformalReggeCert -
theorem
weakFieldConformalReggeCert