inner_pos
plain-language theorem explainer
The lemma establishes positivity of the combination ħG/(π c³) for the CODATA reference values of the reduced Planck constant, gravitational constant, and speed of light. Derivations of the Recognition Science time scale τ₀ cite this result to justify nonnegativity of intermediate expressions. The proof is a direct term-mode application of the rules preserving strict positivity under multiplication and division.
Claim. Let $c$, $ħ$, and $G$ denote the CODATA reference values for the speed of light, reduced Planck constant, and Newtonian gravitational constant. Then $0 < ħ G / (π c^3)$.
background
The module derives physical constants from Recognition Science primitives using CODATA reference values: $c = 299792458$, $ħ = 1.054571817×10^{-34}$, $G = 6.67430×10^{-11}$. The sibling lemmas c_codata_pos, hbar_codata_pos, and G_codata_pos each unfold the corresponding definition and apply norm_num to obtain strict positivity. The local setting is the extraction of derived constants such as τ₀ from these reference values.
proof idea
Term-mode proof. Apply div_pos to the product of hbar_codata_pos and G_codata_pos; the denominator positivity follows by exact application of mul_pos to Real.pi_pos and pow_pos of c_codata_pos to the third power.
why it matters
Feeds the key lemma inner_nonneg, which states $0 ≤ ħG/(π c^3)$ and supports the definition τ₀² = ħG/(π c^5) in the constants derivation. It is also referenced by the TurbineGeometry structure in the Tesla turbine model. Within the framework this positivity step precedes extraction of the fine-structure constant band and the eight-tick octave relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.