hbar_SI_pos
plain-language theorem explainer
Positivity of the SI reduced Planck constant supports single-anchor calibration protocols that map RS-native units to SI reporting scales. Measurement frameworks cite it when deriving joules_per_coh from tau0_seconds to keep the energy anchor positive. The tactic proof unfolds the definition of hbar_SI and chains mul_pos with div_pos after establishing denominator positivity via norm_num.
Claim. $0 < hbar_{SI}$ where $hbar_{SI}$ denotes the exact SI 2019 value of the reduced Planck constant.
background
The Single-Anchor SI Calibration module supplies an explicit seam that converts RS-native quantities (ticks, voxels, cohs, acts) to SI units from one empirical scalar tau0 in seconds. With c set to 1 in native units, meters_per_voxel follows from the SI definition of c while joules_per_coh follows from the SI definition of hbar together with the identity that one act equals one coh times one tick. Upstream, hbar_SI is the external anchor 1.054571817e-34 and h_SI_pos supplies the corresponding positivity fact; the Calibration class from CostAxioms normalizes the second derivative of the cost functional at the origin to 1.
proof idea
Unfold hbar_SI to obtain the quotient h_SI over 2 pi. Establish 0 < 2 pi by norm_num on 2 followed by mul_pos with Real.pi_pos. Apply div_pos to h_SI_pos and the denominator positivity fact.
why it matters
The result is required by externalCalibration_of_tau0_seconds when it assembles ExternalCalibration with joules_per_coh set to hbar_SI divided by tau0_s. It closes the single-anchor protocol without introducing fit parameters or altering dimensionless RS predictions, consistent with the module's explicit seam and the framework's use of exact SI anchors to scale native constants such as hbar = phi^{-5}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.