IndisputableMonolith.Gravity.WeakFieldConformalRegge
The WeakFieldConformalRegge module supplies the exact identity ℓ_{ij}(ξ)² = ℓ_0² exp(ξ_i + ξ_j) that expresses squared edge lengths via a conformal factor in the weak-field Regge setting. Discrete-gravity researchers linking the J-cost functional to the Regge action would cite this identity when linearizing the simplicial ledger. The module assembles the identity through a chain of auxiliary definitions that decompose the length expression using the imported continuum bridge and Schläfli results.
claim\(\ell_{ij}(\xi)^2 = \ell_0^2 \exp(\xi_i + \xi_j)\)
background
The module sits inside Recognition Science gravity, where the J-cost functional on the simplicial ledger equals the Regge action (normalized by κ = 8φ⁵) as shown in the ContinuumBridge import. The EdgeLengthFromPsi import supplies the identification of the recognition potential ψ on 3-simplices with the ten edge lengths per 4-simplex needed for that action. Schlaefli supplies the differential identities for piecewise-flat complexes, while Constants fixes the RS time quantum τ₀ = 1 tick. The central object is the conformal length-squared field built from the exponential of the potential ξ.
proof idea
This is a definition module, no proofs. It introduces the exact conformal length identity together with remainder, Taylor, and quadratic-form auxiliaries that decompose the edge-length expression for later use in the Regge linearization.
why it matters in Recognition Science
The module supplies the weak-field conformal factor required to pass from J-cost stationarity on the ledger to the linearized Einstein equations inside the Regge framework. It directly supports the parent results in the ContinuumBridge module that close the discrete-to-continuum gap between the simplicial ledger and the Einstein field equations. The supplied identity fills the conformal step in the gravity-from-recognition draft.
scope and limits
- Does not treat strong-field or nonlinear Regge regimes.
- Does not incorporate matter sources or the stress-energy tensor.
- Does not derive the full curvature tensors beyond the weak-field limit.
- Does not establish the continuum limit without further hypotheses.
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