IndisputableMonolith.Gravity.WeakFieldConformalRegge
The module establishes the exact identity ℓ_{ij}(ξ)² = ℓ_0² exp(ξ_i + ξ_j) for edge lengths in the weak-field conformal Regge setting. Researchers bridging discrete J-cost functionals to continuum gravity would cite it when justifying conformal approximations to the Regge action. The module imports the psi-to-edge-length map and applies algebraic identities to reach the exponential form directly.
claimThe module proves the identity $ℓ_{ij}(ξ)^2 = ℓ_0^2 · exp(ξ_i + ξ_j)$, where $ℓ_{ij}$ is the length of the edge between vertices i and j, ξ is the recognition potential on vertices, and $ℓ_0$ is a reference length scale.
background
The module operates in the Gravity domain and imports Constants (τ₀ = 1 tick), Schlaefli (Schläfli's identity for piecewise-flat simplicial complexes), ContinuumBridge (J-cost functional on the simplicial ledger equals the Regge action up to normalization by κ = 8φ⁵; stationarity δJ = 0 yields the Regge equations), and EdgeLengthFromPsi (scalar recognition potential ψ on 3-simplices determines the full set of edge lengths required for the Regge action). It supplies the weak-field conformal specialization of the Field-Curvature Identity.
proof idea
The module consists of a sequence of definitions (conformal_length_sq_exact, conformal_remainder, edgeSqFirstOrder, etc.) followed by lemmas that establish the exact identity, its second-order Taylor expansion, and the vanishing of the remainder term. It applies the edge-length construction from the psi field together with direct algebraic expansion and the recognition composition law.
why it matters in Recognition Science
The module supplies the conformal length relation required for the weak-field limit when deriving Einstein's equations from J-cost stationarity in the Gravity from Recognition draft. It supports the parent equivalence between the discrete ledger and the Regge action stated in ContinuumBridge. It contributes to Phase C3 by providing the explicit length map needed for deficit linearization on general complexes.
scope and limits
- Does not treat strong-field or non-conformal metrics.
- Does not derive the full Einstein field equations.
- Does not compute numerical values or run simulations.
- Does not address higher-order curvature corrections beyond the second-order remainder.
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