hbar_ne_zero
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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value from the Recognition Science functional equation or RCL.
- Does not connect ħ to J-uniqueness, the phi fixed point, or the eight-tick octave.
- Does not participate in the T0-T8 forcing chain or the D = 3 derivation.
- Does not supply a first-principles proof of positivity independent of the numeric definition.
formal statement (Lean)
40lemma hbar_ne_zero : hbar ≠ 0 := ne_of_gt hbar_pos