G_derived_pos
plain-language theorem explainer
The lemma shows that the expression G_derived(τ, ħ, c) = π c⁵ τ² / ħ is strictly positive whenever τ, ħ, and c are positive reals. Workers deriving physical constants from Recognition Science primitives cite it to guarantee that the gravitational constant formula remains positive and dimensionally consistent. The proof is a short term-mode reduction that unfolds the definition and chains the standard real-number positivity lemmas div_pos, mul_pos, pow_pos, and sq_pos_of_pos.
Claim. Let τ, ħ, c ∈ ℝ with τ > 0, ħ > 0, c > 0. Then π c⁵ τ² / ħ > 0.
background
In the Constants.Derivation module the function G_derived is introduced as the explicit algebraic expression π c⁵ τ² / ħ, obtained by rearranging the standard Planck-scale relation for G in terms of the fundamental tick duration τ, reduced Planck constant ħ, and speed of light c. The module sits inside the broader Recognition Science program that derives all constants from a single functional equation and the eight-tick octave structure; the CODATA reference values c_codata, hbar_codata, and G_codata are imported as concrete numerical anchors. Upstream results supply the placeholder τ₀ (fundamental tick duration) and the codata constants, but the present lemma is stated for arbitrary positive reals so that it can be instantiated later at the specific RS-native values.
proof idea
The term proof first unfolds G_derived to expose the quotient π c⁵ τ² / ħ. It then invokes div_pos with the second hypothesis ħ > 0, reducing the goal to positivity of the numerator. The numerator is shown positive by a single exact application of mul_pos to three factors: Real.pi_pos, (pow_pos hc 5) for c⁵ > 0, and (sq_pos_of_pos hτ) for τ² > 0.
why it matters
This positivity result closes a small but necessary gap in the constant-derivation pipeline that ultimately aims to recover G = φ⁵ / π in RS-native units. It sits alongside the sibling lemmas c_codata_pos, hbar_codata_pos, and G_codata_pos, preparing the ground for the forthcoming equality G_derived τ₀ ħ_codata c_codata = G_codata. Because the framework fixes G via the phi-ladder and the Recognition Composition Law, a sign error here would propagate into every mass and length scale derived from the same primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.