kappa_G_product
plain-language theorem explainer
The product of the Einstein coupling κ and Newton's constant G equals 8 φ^{10}/π in RS-native units. Researchers closing the quantum-gravity duality relations would cite this to complete the triad of pairwise products among κ, G, and ℏ. The proof is a direct algebraic reduction that substitutes the explicit forms for κ and G then simplifies via ring and real-power addition.
Claim. $κ_{Einstein} · G = 8 φ^{10} / π$ in RS-native units, where $κ_{Einstein}$ is the coefficient in the Einstein field equations and $G$ is Newton's gravitational constant.
background
The Quantum-Gravity Octave Duality module derives all constants from the single J-cost functional equation. The Einstein coupling is defined as κ = 8πG/c^4, which reduces to 8φ^5 when c=1 and ℏ=φ^{-5}. Newton's constant takes the form G = φ^5/π from the recognition scale λ_rec. Upstream results include the lemma kappa_einstein_eq stating κ = 8 φ^5 and the definition of G as (λ_rec^2 c^3)/(π ℏ) in native units.
proof idea
The tactic proof rewrites using kappa_einstein_eq and G_eq_phi_fifth_over_pi to insert the explicit expressions. A calc block then applies ring to obtain 8 φ^5 · (φ^5/π), followed by rw [← Real.rpow_add phi_pos] to add the exponents and norm_num to reach the final form.
why it matters
This supplies the third leg of the three_products theorem, which packages the complete set of pairwise products κ·ℏ=8, G·ℏ=1/π, and κ·G=8φ^{10}/π. It fills the gravitational self-product slot in the QG duality development forced by the J-cost equation and the eight-tick octave (T7). No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.