hbar_SI_pos
plain-language theorem explainer
The lemma asserts that the external SI anchor for the reduced Planck constant is strictly positive. Calibration routines converting RS tick-based quantities to SI units cite it to guarantee positive energy scales in ExternalCalibration records. The proof reduces directly to a numerical check on the hardcoded positive literal via the norm_num tactic.
Claim. $0 < hbar_{SI}$ where $hbar_{SI} = 1.054571817 × 10^{-34}$ J s is the exact CODATA 2022 value.
background
The ExternalAnchors module is the sole location for empirical CODATA data entering Recognition Science; the cost-first core never imports it. Here hbar_SI is defined as the SI 2019 reduced Planck constant 1.054571817e-34. The SingleAnchor calibration module re-expresses the same quantity as h_SI / (2 pi) and separately records its positivity.
proof idea
One-line wrapper that applies the norm_num tactic directly to the definition of hbar_SI, confirming the positive floating-point literal satisfies the strict inequality.
why it matters
The result feeds externalCalibration_of_tau0_seconds, which builds an ExternalCalibration record with positive joules_per_coh = hbar_SI / tau0_s. It enforces the mechanical separation between pure RCL derivations and empirical anchors while supplying the positivity needed for downstream SI-to-RS conversions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.