jcost_to_regge_factor_pos
plain-language theorem explainer
The normalization factor κ = 8 φ^5 relating J-cost on the simplicial ledger to the Regge action is strictly positive. Researchers deriving the Einstein equations from discrete RS structures cite this to guarantee a positive gravitational coupling constant. The proof is a one-line term-mode reduction that unfolds the definition and applies multiplication and power positivity.
Claim. The J-cost to Regge normalization factor satisfies $0 < 8 φ^5$.
background
The ContinuumBridge module identifies the J-cost functional on the simplicial ledger with the Regge action up to normalization by κ = 8 φ^5. This factor is fixed by the calibration axiom that J''(1) = 1 together with the Regge normalization 1/κ = 1/(8πG). The upstream definition states: 'The J-cost normalization factor relating J-cost action to Regge action. Since J''(1) = 1 (the calibration axiom A3), and the Regge action has normalization 1/(8πG) = 1/κ, the factor is exactly κ = 8φ⁵.'
proof idea
The term proof unfolds jcost_to_regge_factor to 8 * phi^5, then applies mul_pos to the product of a positive constant (via norm_num) and phi^5 (via pow_pos using phi_pos).
why it matters
This result supplies the kappa_pos field in both continuum_bridge_cert and jcost_to_efe_chain, completing the chain from J-cost stationarity through the discrete Laplacian to the Einstein field equations. It anchors the claim that κ is derived from the phi-ladder rather than fitted, consistent with the module's derivation chain that runs from J_global through quadratic expansion to Regge identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.