kappa_pos
plain-language theorem explainer
The theorem establishes positivity of the RS-derived Einstein coupling constant 8φ^5. Researchers formalizing the continuum limit of ledger curvature cite it to fix the sign of the gravitational constant in the derived field equations. The proof is a direct term reduction that unfolds the definition and invokes standard positivity of multiplication by 8 together with the fifth power of the positive golden-ratio fixed point.
Claim. $0 < 8φ^5$, where $φ$ is the golden-ratio self-similar fixed point and $κ = 8φ^5$ is the derived Einstein gravitational coupling.
background
The Zero-Parameter Gravity module derives gravity as large-scale curvature of the ledger lattice induced by defect distributions. The Einstein field equations appear as the continuum limit with coupling $κ = 8φ^5$, where $φ$ is the self-similar fixed point forced by the T0–T8 chain. The definition kappa_rs supplies the explicit RS prediction for this coupling, obtained rather than postulated.
proof idea
The term proof unfolds kappa_rs to the expression 8 * phi^5, applies mul_pos to the positive constant 8 (via norm_num), and closes with pow_pos using the upstream fact phi_pos.
why it matters
The result is invoked by ContinuumBridgeCert and ContinuumFieldCurvatureCert to certify that J-cost stationarity yields the Einstein equations with the derived positive coupling. It completes the G-002 registry item in the module and anchors the sign of κ inside the eight-tick octave and phi-ladder structure of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.