G_rs_pos
plain-language theorem explainer
Newton's constant in RS-native units, G = φ⁵/π, is strictly positive. Cosmology and constants modules cite this to keep Friedmann and certificate constructions well-defined. The proof unfolds the definition and multiplies the positivity of φ⁵ by the positivity of π.
Claim. In RS-native units, Newton's gravitational constant $G = \varphi^5/\pi$ satisfies $0 < G$.
background
The electroweak phase-transition module is an RS-native scaffold for $T_{\mathrm{EW}}$ on the φ-ladder and the radiation-era Hubble rate $H(T_{\mathrm{EW}})$. In that setting the Friedmann combination is written $H^2 = \mathrm{friedmann_coeff}\cdot G\cdot g_\star\cdot T^4$ with the $T^4$ factor kept explicit.
RS-native $G$ is the Family-A value $G=\varphi^5/\pi$. Upstream, Constants.GravitationalConstant records the same formula from $G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$ with $\lambda_{\mathrm{rec}}=c=1$ and $\hbar=\varphi^{-5}$. The local G_rs is that same quotient, re-exported so the EW scaffold does not import the full constants stack for a one-line positivity fact.
Positivity of $G$ is the only arithmetic input needed before multiplying by the positive Friedmann coefficient, $g_\star^{\mathrm{EW}}$, and $T_{\mathrm{EW}}^4$.
proof idea
Term-mode proof. Unfold the local definition $G=\varphi^5/\pi$. Apply div_pos to the pair of facts pow_pos phi_pos 5 (powers of a positive base stay positive) and Real.pi_pos. No further lemmas are required.
why it matters
Keeps the radiation-era Hubble square positive at the electroweak scale: hubble_sq_at_ew_pos multiplies this fact with positivity of the Friedmann coefficient, $g_\star^{\mathrm{EW}}$, and $T_{\mathrm{EW}}^4$. The EW transition certificate ew_transition_cert packages it as the G_positive field.
On the constants side it is the positivity half of gravitational_constant_derived (C-002): $G=\varphi^5/\pi$ with no free parameters, matching the primer landmark $G=\varphi^5/\pi$. The module itself remains a MODEL scaffold; this lemma only discharges the $G>0$ obligation inside that scaffold and does not close the separate Boltzmann-transport path to $\eta_B$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.