jcost_to_regge_factor_eq
plain-language theorem explainer
The normalization constant equating the J-cost action on simplicial ledgers to the Regge action equals 8φ⁵. Researchers deriving Einstein field equations from discrete J-cost stationarity cite this to fix the coupling in the continuum limit. The proof is a one-line reflexivity that follows directly from the explicit definition of the factor.
Claim. The normalization factor κ relating the J-cost functional to the Regge action satisfies κ = 8φ⁵.
background
In the ContinuumBridge module the J-cost functional on the simplicial ledger is identified with the Regge action up to normalization. J-cost sums J(ψ_i/ψ_j) over neighboring simplices where J(x) = cosh(log x) - 1, which expands quadratically as ε²/2 for small log deviations ε. This structure matches the Regge action Σ δ_h A_h whose quadratic form arises from deficit angles in metric perturbations.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of jcost_to_regge_factor, which is constructed as 8 * phi ^ 5 from the calibration J''(1) = 1 and the Regge normalization 1/κ.
why it matters
This equality supplies the κ value instantiated in the JCostToEFE chain and the ContinuumBridgeCert. It completes the normalization step from J_global to the Einstein field equations, aligning with Recognition Science constants where G = φ⁵/π and κ = 8φ⁵. The result is invoked in the cubic field curvature certificate and the kappa-Einstein identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.