G_relation_satisfied
plain-language theorem explainer
The theorem confirms that the gravitational constant derived from the Recognition Science tick duration together with CODATA values for the speed of light and reduced Planck constant equals the CODATA reference for G. Researchers verifying numerical consistency of constants inside the RS framework cite this result. The proof unfolds the derived expression, substitutes the squared tick duration, records the three nonzero conditions, and finishes by field simplification.
Claim. $G_derived(τ_0, ℏ_codata, c_codata) = G_codata$, where $G_derived(τ, ℏ_val, c_val) := π · c_val^5 · τ² / ℏ_val$ and the three arguments are the fundamental tick duration together with the CODATA values for ℏ and c.
background
The Constants.Derivation module derives the three fundamental constants from Recognition Science primitives, taking the CODATA numerical values for c = 299792458 m/s, ℏ = 1.054571817×10⁻³⁴ J·s and G = 6.67430×10⁻¹¹ m³ kg⁻¹ s⁻² as reference targets. The auxiliary definition G_derived(τ, ℏ_val, c_val) := π · c_val^5 · τ² / ℏ_val encodes the Planck-unit relation for G in terms of the fundamental tick duration τ₀. Upstream lemmas establish that τ₀, c_codata and ℏ_codata are nonzero and that τ₀ satisfies the squared relation used in the reduction.
proof idea
The term proof first unfolds G_derived, rewrites with tau0_sq_eq, records the three nonzero facts (hbar_codata_ne_zero, c_codata_ne_zero, Real.pi_pos), and closes with field_simp to cancel the common factors and obtain equality with G_codata.
why it matters
The result appears explicitly in the derivation_status string as one of the five proven relations, confirming that the RS-derived expression for G reproduces the measured value once τ₀, c and ℏ are supplied. It therefore closes the numerical loop for the gravitational constant inside the module that matches RS primitives to CODATA data. In the broader framework this step supports the claim that G = φ^5 / π in native units once the tick duration is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.