hbar_codata_pos
plain-language theorem explainer
The lemma asserts positivity of the CODATA reference value assigned to the reduced Planck constant. Derivations of Planck length, mass, and time positivity cite it as the base inequality. The proof is a one-line wrapper that unfolds the constant definition and applies numerical normalization.
Claim. $0 < 1.054571817times10^{-34}$ where the right-hand side is the CODATA reference value for the reduced Planck constant.
background
The module derives physical constants from Recognition Science primitives by importing the CODATA reference values for $c$, $hbar$, and $G$. The sibling definition hbar_codata sets the reduced Planck constant to the literal real number 1.054571817e-34. This lemma supplies the immediate positivity fact required by all subsequent inequalities that combine the three CODATA inputs.
proof idea
One-line wrapper that unfolds hbar_codata to expose the concrete positive literal, then applies norm_num to discharge the inequality.
why it matters
It is the root positivity statement feeding hbar_codata_ne_zero, inner_pos, planck_length_pos, planck_mass_pos, planck_time_pos, planck_time_inner_nonneg, and tau0_pos. These lemmas in turn support the module's derivations of Planck-scale quantities from the CODATA inputs. The result sits inside the constants layer that precedes any Recognition Science derivation of the same quantities via the phi-ladder or J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.