hbar_derived_pos
plain-language theorem explainer
Positivity of the derived reduced Planck constant follows from positivity of the tick duration, gravitational constant and speed of light. Workers deriving constants inside Recognition Science cite the result to guarantee the expression stays positive. The argument is a term-mode proof that unfolds the definition and chains the standard positivity lemmas for multiplication and division.
Claim. If $0 < τ$, $0 < G$ and $0 < c$, then $0 < π c^5 τ^2 / G$, where the right-hand side is the expression for the derived reduced Planck constant in the Recognition Science constants derivation.
background
The Constants.Derivation module constructs expressions for the physical constants from Recognition Science primitives. The definition hbar_derived(τ, G_val, c_val) equals π c_val^5 τ^2 / G_val. Upstream results supply the fundamental tick duration τ₀ together with the CODATA reference values c = 299792458, ħ = 1.054571817×10^{-34} and G = 6.67430×10^{-11}.
proof idea
Unfolding hbar_derived exposes the quotient. The proof applies div_pos with the positive denominator G_val, then establishes positivity of the numerator by two nested mul_pos calls: one for π and c^5 (via pow_pos), the other for that product and τ^2 (via sq_pos_of_pos).
why it matters
The lemma guarantees that the derived ħ inherits the correct sign from the input primitives. It supports the larger claim that the Recognition Science forcing chain reproduces the observed constants. No downstream uses are recorded yet, but the result closes a basic consistency check before numerical comparison with hbar_codata.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.