hbar_codata_pos
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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of ℏ from Recognition Science primitives.
- Does not address dimensional analysis or unit conversion.
- Does not claim the value is exact beyond the CODATA assignment.
Lean usage
lemma hbar_codata_ne_zero : hbar_codata ≠ 0 := ne_of_gt hbar_codata_posformal statement (Lean)
29lemma hbar_codata_pos : 0 < hbar_codata := by unfold hbar_codata; norm_num