hbar_over_G
plain-language theorem explainer
The ratio of the reduced Planck constant to Newton's gravitational constant equals π over φ to the tenth in RS-native units. Researchers deriving Planck-scale relations or gravitational couplings from the J-cost functional would cite this identity. The proof is a direct algebraic reduction that substitutes the explicit forms ħ = φ^{-5} and G = φ^5/π then simplifies the resulting expression via field arithmetic and exponent rules.
Claim. In RS-native units the ratio of the reduced Planck constant to Newton's gravitational constant satisfies $ħ/G = π/φ^{10}$.
background
The module establishes quantum-gravity octave duality from the single J-cost functional. J-cost is defined as the AM-GM gap: for x > 0, Jcost x = (x − 1)² / (2x), which equals AM(x, x^{-1}) − GM(x, x^{-1}) and yields J ≥ 0 with equality iff x = 1. Upstream results supply the constants: hbar_eq_phi_inv_fifth states ħ = φ^{-5}, while Constants.G gives G = λ_rec² c³ / (π ħ) which simplifies to φ^5/π in RS units. The module doc notes that G · ħ = 1/π follows as Gauss-Bonnet closure for the curvature quantum of Q₃.
proof idea
The tactic proof opens with rw [div_eq_iff (ne_of_gt G_pos)] to clear the denominator using G_pos. It then substitutes G_eq_phi_fifth_over_pi and hbar_eq_phi_inv_fifth. The resulting goal is verified by a symmetric calc block: field_simp reduces the product, div_eq_mul_inv rewrites the division, Real.rpow_neg and Real.rpow_add handle the exponents, and norm_num collapses the final power to φ^{-5}.
why it matters
This identity fills QG-003 in the module doc, confirming G · ħ = 1/π directly from the phi-ladder constants forced by the J-cost equation (T5). It anchors the gravitational coupling inside the eight-tick octave (T7) and supports the central duality κ ħ = 8. The result closes one link in the unification chain without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.