G
plain-language theorem explainer
The definition supplies the RS-native expression for Newton's gravitational constant as G = λ_rec² c³ / (π ħ) with λ_rec the recognition length and ħ = φ^{-5}. Researchers deriving all constants from the Recognition Composition Law and T5-T8 forcing chain cite this form. It is obtained by direct algebraic inversion of the lambda_rec relation in Bridge.DataCore.
Claim. $G = λ_{rec}^2 c^3 / (π ħ)$ in RS-native units where $c=1$ and $ħ=φ^{-5}$.
background
The Constants module expresses all constants in RS-native units with the fundamental tick τ₀ = 1. Here λ_rec is defined locally as ell0 (the base length from the eight-tick cycle) while the upstream Bridge.DataCore.lambda_rec records the physical identity λ_rec = √(ħ G / c³). The reduced Planck constant is given by hbar := cLagLock * tau0, which the module doc identifies with E_coh · τ₀ = φ^{-5}. The module imports Cost.FunctionalEquation to place these constants inside the J-cost framework.
proof idea
One-line definition that substitutes the local lambda_rec and hbar into the inverted form of the lambda_rec identity from Bridge.DataCore.
why it matters
This supplies the G value required by the cost-algebra uniqueness theorems (cost_algebra_unique and cost_algebra_unique_aczel) that establish T5 J-uniqueness, and by the zero-parameter certificate ml_zero_parameter_certificate together with the scaffold H_RSZeroParameterStatus. It realizes the framework relation G = φ^5 / π once λ_rec and ħ are inserted, completing one link in the constant-derivation chain from the Meta-Principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.