kappa_einstein_eq
plain-language theorem explainer
kappa_einstein evaluates to 8 phi^5 in RS-native units with c=1. Researchers completing the G derivation chain or certifying continuum curvature from the simplicial ledger cite the identity to normalize J-cost against the Regge action. The term-mode proof unfolds the constant definitions then cancels via field_simp and rpow_neg.
Claim. In RS-native units the Einstein coupling satisfies $k_E = 8 phi^5$.
background
The Constants module defines tau0 as the fundamental tick equal to 1. cLagLock is phi^{-5}, so hbar equals cLagLock times tau0. G is constructed as lambda_rec^2 times c^3 over pi times hbar, where lambda_rec is the recognition length whose dimensionless identity states that c^3 lambda_rec^2 over hbar G equals 1 over pi. kappa_einstein is the prefactor that appears in the linearized Einstein equations and is expressed through these constants.
proof idea
The term proof unfolds kappa_einstein, G, hbar, cLagLock, lambda_rec, ell0, c, tau0 and tick. It applies simp only on one_pow, mul_one and div_one, asserts Real.pi ≠ 0, runs field_simp on that fact, rewrites the negative exponent with Real.rpow_neg using phi_pos.le, and finishes with field_simp on phi_ne_zero.
why it matters
The lemma supplies the kappa value required by continuumFieldCurvatureCert and bridge_chain_complete to certify that J-cost Dirichlet energy equals the scaled Regge sum. It also feeds G_derivation_chain_complete and jcost_to_regge_factor_eq_kappa_einstein. The result closes the constants block after J-uniqueness and phi forcing, confirming that G = phi^5 / pi produces the Einstein prefactor 8 phi^5 and enables the full bridge chain from the Recognition Composition Law to the simplicial ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.