kappa_bounds
plain-language theorem explainer
The theorem proves that the RS gravitational coupling κ = 8φ⁵ satisfies 85.6 < κ < 90.4 in RS-native units. Researchers deriving gravity from the J-cost ledger lattice cite these bounds to fix the Einstein constant without free parameters. The proof is a term-mode wrapper that unfolds the definition of κ and scales the known interval on φ⁵ via linear arithmetic.
Claim. The RS gravitational coupling satisfies $85.6 < 8φ^5 < 90.4$.
background
The Zero-Parameter Gravity module derives gravity as lattice curvature induced by defect distributions, with the Einstein equations as the continuum limit. The coupling is defined by kappa_rs := 8 * phi^5, where the factor 8 arises from the eight vertices of the cubic lattice cell. This rests on phi_fifth_bounds, which states 10.7 < φ^5 < 11.3 from the self-similar fixed point of φ.
proof idea
The proof unfolds kappa_rs to 8 * phi^5, obtains the two-sided bounds on phi^5 from phi_fifth_bounds, and applies constructor followed by nlinarith to scale the interval by 8.
why it matters
This supplies the numerical interval consumed by NumericalPredictionsCert and the kappa_bounds theorem in the Masses module. It closes the numerical content of G-002, confirming that the Einstein coupling is fixed by the phi-ladder (T5-T6) without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.