G_derived
plain-language theorem explainer
G_derived defines the gravitational constant via the Planck gate identity as G = π c³ λ_rec² / ℏ. Researchers closing the Recognition Science constant chain from φ to G cite this definition when expressing G in terms of c, ℏ and the recognition wavelength. It is a direct one-line algebraic rearrangement of the identity (c³ λ_rec²) / (ℏ G) = 1/π.
Claim. $G = π c^3 λ_{rec}^2 / ℏ$, where λ_rec is the recognition wavelength satisfying the Planck gate identity $(c^3 λ_{rec}^2) / (ℏ G) = 1/π$.
background
In the RRF Foundation module all constants derive from φ through gate identities rather than being postulated. The chain is φ → E_coh → τ₀ → c → ℏ → G → α^{-1}. The Planck gate identity states that (c³ λ_rec²) / (ℏ G) = 1/π, with λ_rec the recognition wavelength. Upstream, the Bridge.DataCore definition gives λ_rec = √(ℏ G / c³) together with the explicit identity (c^3 · λ_rec^2) / (ħ G) = 1/π. hbar is defined as E_coh · τ₀ = φ^{-5} in native units and K as φ^{1/2}.
proof idea
This is a one-line definition that directly encodes the algebraic solution of the Planck gate identity for G. It applies the rearrangement G = π c³ λ_rec² / ℏ with no additional lemmas or tactics.
why it matters
This definition supplies the explicit expression for G required by the constant derivation chain in the RRF framework. It feeds the parent results G_derived_pos and G_relation_satisfied in Constants.Derivation, which establish positivity and equality to the CODATA value. It realizes the Planck gate identity quoted in the module doc-comment and supports the eight-tick octave structure through λ_rec.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.