hbar_ne_zero
plain-language theorem explainer
The lemma asserts that the CODATA numerical value of the reduced Planck constant is nonzero. Researchers performing numeric comparisons between RS-native units and empirical data would cite it to guarantee that divisions by ħ remain defined. The proof is a one-line wrapper that invokes ne_of_gt on the separate positivity lemma.
Claim. $ ħ ≠ 0 $ where $ ħ $ denotes the CODATA 2018 numerical value of the reduced Planck constant.
background
The Codata module quarantines empirical SI/CODATA constants from the certified Recognition Science surface so that the main certificate chain never depends on measured numbers. It defines hbar as the literal floating-point constant 1.054571817e-34 and proves positivity in a separate lemma. Upstream results include the RS-native hbar definition ħ = φ^{-5} in Constants and the positivity statement obtained by unfolding and applying norm_num.
proof idea
The proof is a one-line wrapper that applies the library lemma ne_of_gt directly to the already-proved positivity result hbar_pos.
why it matters
It supplies a hygiene fact required whenever downstream code imports the CODATA value for numeric checks against the phi-ladder mass formula or the alpha band. The parent results are the positivity lemmas in Constants and the various hbar definitions scattered across Information and Quantum modules. It touches the open separation between the certified T0-T8 chain and empirical reference values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.