inner_nonneg
plain-language theorem explainer
The lemma establishes non-negativity of ħG/(π c³) when the constants take their CODATA numerical values. Workers deriving the tau0 parameter in the Recognition Science constants module cite it to license subsequent algebraic steps such as square-root extractions. The term-mode proof is a one-line wrapper that invokes le_of_lt on the strict-positivity sibling inner_pos.
Claim. $0 ≤ (ħ_{CODATA} · G_{CODATA}) / (π · c_{CODATA}^3)$
background
The Derivation module supplies CODATA reference values for the fundamental constants to support Recognition Science derivations. c_codata, hbar_codata and G_codata are the standard numerical constants c = 299792458, ħ = 1.054571817×10^{-34} and G = 6.67430×10^{-11}. The upstream lemma inner_pos proves the corresponding strict inequality 0 < hbar_codata * G_codata / (π * c_codata^3) by successive applications of mul_pos and div_pos to the manifestly positive constants.
proof idea
The proof is a one-line wrapper that applies the lemma inner_pos via the constructor le_of_lt.
why it matters
The result supplies the non-negativity fact required by the downstream theorem tau0_sq_eq that states τ₀² = ħG/(π c^5). It therefore anchors the constants-derivation step inside the Recognition Science framework, consistent with the T5 J-uniqueness and the phi-ladder mass formulas. No open scaffolding questions are closed by this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.