hbar_pos
plain-language theorem explainer
The lemma asserts that the reduced Planck constant drawn from the CODATA 2018 numeric value is strictly positive. Bridge constructions and physical-assumption structures cite it to guarantee ħ > 0 when deriving quantities such as the recognition length. The proof is a one-line wrapper that unfolds the constant definition and applies norm_num to the positive literal.
Claim. $0 < 1.054571817e-34$ where the right-hand side is the CODATA 2018 value of the reduced Planck constant in SI units.
background
The Codata module isolates empirical SI/CODATA constants from the certified Recognition Science surface so that the main certificate chain never depends on measured numeric values. Here ħ is defined directly as the 2018 CODATA literal 1.054571817e-34. Upstream results supply the RS-native counterpart ħ = φ^{-5} via the identity ħ = E_coh · τ₀, while this Codata version supplies the measured anchor used for numeric comparisons in computation-limits and entanglement-entropy modules.
proof idea
The proof is a one-line wrapper: unfold hbar reduces the goal to 0 < 1.054571817e-34, after which norm_num discharges the numeric inequality.
why it matters
This positivity result supports downstream lemmas such as lambda_rec_pos and the Physical structure in Bridge.DataCore, which require 0 < B.hbar for derivations of λ_rec = √(ħ G / c³). It supplies the empirical half of the positivity pair that parallels the RS-native hbar_pos (THEOREM C-004.1) without touching the forcing chain or the phi-ladder. The module doc explicitly quarantines these constants so the certified surface remains independent of CODATA numbers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.