jcost_to_regge_factor
plain-language theorem explainer
The declaration defines the normalization constant κ = 8φ⁵ that equates the J-cost action on a simplicial ledger to the Regge action. Researchers closing the discrete-to-continuum gap in Recognition Science would cite this factor when matching J-cost stationarity to curvature equations. The definition is a direct assignment justified by the calibration J''(1) = 1 together with the standard Regge prefactor 1/(8πG).
Claim. The normalization factor relating J-cost action to Regge action is given by κ = 8φ⁵, where φ denotes the golden-ratio fixed point of the Recognition Science forcing chain.
background
The Continuum Bridge module identifies the J-cost functional on the simplicial ledger with the Regge action up to normalization. In log coordinates ε = ln ψ the expansion J(e^ε) = cosh(ε) − 1 = ε²/2 + O(ε⁴) produces a discrete Laplacian whose quadratic structure matches the linearized Regge action Σ_h δ_h A_h. Upstream, the cost function is supplied by MultiplicativeRecognizerL4.cost as derivedCost m.comparator and by ObserverForcing.cost as Cost.Jcost e.state; both rest on the Recognition Composition Law and the J-uniqueness property T5.
proof idea
One-line definition that directly assigns the constant 8 * phi ^ 5. The assignment is pinned by the calibration axiom J''(1) = 1 (axiom A3) and the Regge normalization 1/κ with κ drawn from Constants.
why it matters
The definition supplies the coupling used throughout the module, appearing in ContinuumBridgeCert, induced_regge_action, JCostToEFE, and jcost_stationarity_implies_regge. It completes the normalization step in the derivation chain SimplicialLedger.J_global → quadratic expansion → discrete Laplacian → Regge identification → κ = 8φ⁵ → continuum limit = EFE. It instantiates the framework landmark that φ is the self-similar fixed point (T6) and that the Regge-to-EFE convergence (Cheeger–Müller–Schrader) is recovered once the discrete action is correctly scaled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.