hbar_codata_pos
plain-language theorem explainer
The lemma asserts that the CODATA numerical value assigned to ℏ is strictly positive. Derivations of Planck length, mass, time, and the inner expression for τ₀ cite it to obtain the required inequalities. The proof is a one-line wrapper that unfolds the definition and invokes norm_num on the explicit decimal.
Claim. $0 < 1.054571817 × 10^{-34}$ where the right-hand side is the CODATA reference value for ℏ.
background
The Constants.Derivation module embeds standard CODATA reference values for c, ℏ, and G to anchor subsequent derivations of Planck units and related quantities. The definition hbar_codata simply records the numerical value 1.054571817e-34. This lemma depends directly on that definition and is invoked by eight downstream positivity statements.
proof idea
One-line wrapper that unfolds hbar_codata to expose the literal decimal and applies norm_num to discharge the inequality.
why it matters
It supplies the base positivity fact used by hbar_codata_ne_zero, inner_pos, planck_length_pos, planck_mass_pos, planck_time_pos, planck_time_inner_nonneg, tau0_pos, and tau0_planck_relation. In the Recognition Science setting these inequalities guarantee that the derived Planck scales remain positive before they enter mass-ladder formulas or the eight-tick octave relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.