hbar_codata_ne_zero
plain-language theorem explainer
The lemma shows that the CODATA numerical value assigned to ħ is nonzero. Derivations of the gravitational constant from Recognition Science primitives cite it to justify algebraic steps involving inversion. The argument is a direct one-line reduction using the positivity of the same constant.
Claim. The CODATA value of the reduced Planck constant satisfies $1.054571817e-34 > 0$, hence $1.054571817e-34 ≠ 0$.
background
The module derives physical constants from Recognition Science primitives by importing explicit CODATA reference values for c, ħ and G. The definition hbar_codata fixes the real number 1.054571817e-34. Its positivity lemma, proved by unfolding the definition and applying norm_num, supplies the strict inequality 0 < hbar_codata.
proof idea
The proof is a one-line wrapper that applies ne_of_gt directly to the upstream positivity lemma hbar_codata_pos.
why it matters
The result is invoked inside G_relation_satisfied to discharge the nonzero hypothesis required when verifying that the derived gravitational constant equals the CODATA value. It therefore closes an algebraic prerequisite in the constants derivation chain that connects Recognition Science primitives to measured constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.