G_pi_eq_phi5
plain-language theorem explainer
In RS-native units the gravitational constant satisfies G·π = φ⁵. Anyone citing the canonical φ-ladder values for G, or the quantum-gravity octave duality that equates G·π with 1/ℏ, needs this identity. The proof is a one-line cancellation after unfolding the definition G = φ⁵/π.
Claim. In RS-native units, $G_{\mathrm{rs}}\cdot\pi=\varphi^{5}$, where $G_{\mathrm{rs}}=\varphi^{5}/\pi$ is the recognition-geometry gravitational constant and $\varphi$ is the golden ratio.
background
The module derives $c$, $\hbar$, $G$, and $\alpha$ from the RS foundation rather than treating them as free parameters. After the composition law forces the unique cost $J$ and the self-similar fixed point $\varphi$, the gravitational constant emerges as a curvature extremum. With $\lambda_{\mathrm{rec}}=c=1$ and $\hbar=\varphi^{-5}$, the formula $G=\lambda_{\mathrm{rec}}^{2}c^{3}/(\pi\hbar)$ collapses to $G=\varphi^{5}/\pi$.
$G_{\mathrm{rs}}$ is the in-module Family-A canonical value of that constant. Bare $G$ is not itself a pure power of $\varphi$ because of the geometric factor $\pi$; the honest algebraic claim is that the product $G\cdot\pi$ clears the denominator and yields $\varphi^{5}$. Upstream definitions of $G$ in Constants and GravitationalConstant state the same RS-native projection.
proof idea
Unfold the definition $G_{\mathrm{rs}}:=\varphi^{5}/\pi$. The goal becomes $(\varphi^{5}/\pi)\cdot\pi=\varphi^{5}$. Discharge it by div_mul_cancel₀ with the side condition $\pi\neq 0$ (Real.pi_ne_zero). That is the entire term proof: definitional cancellation, no further lemmas.
why it matters
This identity is the $G$ half of the canonical $\varphi$-constants bridge used by t6_to_phi_constants_canonical_bridge_holds in the unified forcing chain: T6 forces $\varphi$, and the bridge packages $c=1$, $\hbar=\varphi^{-5}$, and $G\cdot\pi=\varphi^{5}$ as fixed exponents rather than existential claims.
Downstream, QuantumGravityOctaveDuality reuses it to prove $G\cdot\pi=1/\hbar=\varphi^{5}$ and the double appearance of $\varphi^{5}$ in both quantum and gravitational couplings (phi5_is_both_quantum_and_gravitational). That double appearance is the formal content of zero free parameters for the gravitational and Planck sectors. It also feeds the sibling claim that $G\cdot\pi$ is algebraic in $\varphi$. Framework landmarks: T6 ($\varphi$ forced) and the RS-native constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.