kappa_calibration_positive
plain-language theorem explainer
The identification shows that the Einstein coupling κ equals the positive Regge conversion factor obtained from the J-cost bridge. Researchers deriving discrete gravity from recognition potentials cite this to confirm that the coupling in the linearized Regge action is fixed by the recognition functional rather than inserted by hand. The proof is a one-line term-mode substitution that applies the equality lemma to the already-proved positivity of the factor.
Claim. $0 < 8φ^5$, where $8φ^5$ is the Einstein coupling κ obtained by equating the J-cost Dirichlet energy on simplices to the linearized Regge action under the bridge normalization.
background
The J-cost functional on a recognition potential ψ is defined via J(x) = (x + x^{-1})/2 - 1 and supplies the Dirichlet energy whose linearization yields deficit angles. The module builds an edge-length field L_e from ψ on 3-simplices and introduces the ReggeDeficitLinearizationHypothesis that converts log-potential differences into first-order changes in edge lengths. The ContinuumBridge supplies both the positivity of the conversion factor and the algebraic equality that identifies this factor with kappa_einstein.
proof idea
The proof is a one-line term-mode wrapper that applies the equality jcost_to_regge_factor_eq_kappa_einstein to the positivity result jcost_to_regge_factor_pos.
why it matters
This corollary discharges the paper claim that κ is derived from the recognition bridge (Gravity from Recognition, §5). It supplies the positive coupling required by the parent field-curvature identity and aligns with the phi fixed point (T6) that fixes the numerical value 8φ^5 in RS units. The result leaves open the discharge of the linearization hypothesis via explicit Cayley-Menger computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.