G_derived
plain-language theorem explainer
This definition supplies the gravitational constant as G = π c^5 τ² / ℏ, with τ the recognition timescale. Researchers deriving constants from Recognition Science primitives cite it to connect the Planck gate identity to CODATA G. It is realized as a direct algebraic expression obtained by substituting λ_rec = c τ into the upstream rearrangement.
Claim. The derived gravitational constant is expressed by the formula $G = 3.14159... c^5 τ^2 / ℏ$, where $τ$ is the recognition timescale, $c$ the speed of light, and $ℏ$ the reduced Planck constant.
background
The module derives physical constants from Recognition Science primitives, referencing CODATA values c = 299792458 m/s, ℏ = 1.054571817×10⁻³⁴ J·s, and G = 6.67430×10⁻¹¹ m³/(kg·s²). The upstream G_derived in RRF.Foundation.Constants implements the Planck gate identity (c³ · λ_rec²) / (ℏ · G) = 1/π and solves for G = π c³ λ_rec² / ℏ. The present definition adapts that identity by the substitution λ_rec = c τ, producing the c^5 τ² form while preserving the 1/π factor.
proof idea
This is a direct definition that performs the algebraic substitution λ_rec = c τ inside the Planck gate rearrangement. No lemmas or tactics are invoked; the expression is written out explicitly.
why it matters
G_derived feeds G_derived_pos, which proves positivity for positive inputs, and G_relation_satisfied, which shows equality to the CODATA G value at the specific point (tau0, hbar_codata, c_codata). It supplies the concrete link between the recognition timescale and the measured gravitational constant inside the constants derivation chain, consistent with the K-Gate identity K = 2π / (8 ln φ).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.