jcost_to_regge_factor_ne_zero
plain-language theorem explainer
The normalization constant κ = 8φ⁵ equating J-cost action on the simplicial ledger to the Regge action is nonzero. Researchers deriving discrete-to-continuum limits in quantum gravity cite it to guarantee the field-curvature identity remains well-defined. The proof is a one-line wrapper that invokes the positivity result for the identical factor.
Claim. The normalization factor κ = 8φ⁵ relating the J-cost Dirichlet energy to the Regge action is nonzero.
background
This module proves the continuum bridge: J-cost stationarity on the simplicial ledger equals the Regge equations up to κ = 8φ⁵, with the Regge equations converging to the Einstein field equations. The J-cost functional expands as J(e^ε) = ε²/2 + O(ε⁴) in log coordinates ε = ln ψ, yielding a discrete Laplacian whose quadratic structure matches the Regge sum Σ_h δ_h A_h. The factor itself is defined upstream as 8 * phi ^ 5, calibrated by J''(1) = 1 and the Regge normalization 1/(8πG).
proof idea
One-line wrapper that applies the positivity theorem jcost_to_regge_factor_pos via ne_of_gt.
why it matters
This result removes a potential singularity from the field-curvature identity used in FieldCurvatureBridge and the nonlinear theorems jcost_stationarity_to_regge_nonlinear and nonlinear_field_curvature_identity. It completes the derivation chain SimplicialLedger.J_global → log expansion → Regge identification with κ = 8φ⁵ drawn from RS-native constants (T5 J-uniqueness, phi fixed point). The non-vanishing supports the claim that J-cost stationarity reproduces the Einstein equations in the continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.