jcost_to_regge_factor_eq_kappa_einstein
plain-language theorem explainer
The theorem identifies the normalization factor converting J-cost Dirichlet energy to Regge action with the Einstein gravitational coupling in RS-native units, both equal to 8 φ^5. Researchers deriving the field-curvature identity from recognition principles cite this to show the coupling is computed rather than adjusted. The proof is a term-mode algebraic reduction that rewrites each side from its defining equation and equates the powers via the natural-to-real cast.
Claim. The normalization factor from the J-cost Dirichlet energy to the Regge action equals the Einstein gravitational coupling constant $κ = 8 φ^5$ in RS-native units.
background
The Edge-Length Field from the Recognition Potential module supplies the map from a log-potential field on simplices to edge lengths and the linearization that turns deficit angles into differences of log-potentials. In this setting the J-cost Dirichlet energy on a weighted ledger graph is related to the Regge action by a single scalar factor. Upstream, the equality lemma for the J-cost to Regge factor and the lemma for the Einstein coupling both evaluate to 8 φ^5; the present result equates the two expressions.
proof idea
The term proof first rewrites the left side via the J-cost to Regge factor equality and the right side via the Einstein coupling equality. It then applies congr to reduce the goal to an identity on the common expression 8 φ^5. The final step casts the exponent 5 from ℕ to ℝ and invokes the natural-number power lemma to finish the equality.
why it matters
This identification feeds the Einstein-coupling form of the field-curvature identity and the simplicial versions that follow. It realizes the claim in the Gravity from Recognition draft that κ is derived from the Recognition Science constants rather than fitted, linking the J-cost action directly to the coefficient in G_{μν} + Λ g_{μν} = κ T_{μν}. The result closes one link in the bridge from discrete recognition cost to continuum gravity while leaving the linearization hypothesis open for later discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.