G_pos
plain-language theorem explainer
Newton's gravitational constant is positive in RS-native units. Researchers deriving the Einstein coupling constant or Planck length cite this result to satisfy the positivity hypotheses in the Physical structure. The term-mode proof unfolds the definition of G and applies div_pos to a numerator built from mul_pos on lambda_rec and c powers together with a denominator built from mul_pos on pi and hbar.
Claim. In RS-native units, Newton's gravitational constant satisfies $0 < G$ where $G = λ_{rec}^2 c^3 / (π ħ)$.
background
The Constants module defines Newton's gravitational constant by the RS-native expression $G = λ_{rec}^2 c^3 / (π ħ)$. The local setting fixes the fundamental time quantum to one tick, $τ_0 = 1$. Upstream lemmas supply the required positivity facts: c_pos states $0 < c$, hbar_pos states $0 < ħ$ with the explicit identity ħ = φ^{-5} (quoted from its doc-comment as THEOREM C-004.1), and lambda_rec_pos states $0 < λ_{rec}$.
proof idea
The proof is a one-line wrapper that unfolds G then applies div_pos. Numerator positivity is obtained by mul_pos on pow_pos lambda_rec_pos 2 and pow_pos c_pos 3. Denominator positivity is obtained by mul_pos on Real.pi_pos and hbar_pos.
why it matters
This lemma supplies the G_pos hypothesis required by the Physical structure in Bridge.DataCore and by kappa_einstein_pos. It closes the positivity chain for the RS-native form G = φ^5 / π, which yields the Einstein coupling κ = 8φ^5. The result therefore supports the eight-tick octave and the derivation of D = 3 through the constants layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.