hbar_SI
plain-language theorem explainer
The declaration supplies the exact SI value of the reduced Planck constant as an external anchor for calibration against Recognition Science derivations. Physicists comparing RS-native units (where ħ = φ^{-5}) to laboratory measurements would cite this definition. It is a direct numerical assignment with no computational steps.
Claim. The reduced Planck constant in SI units is defined by the exact 2019 value $1.054571817 × 10^{-34}$ J s.
background
This module quarantines all empirical calibration data so that the cost-first core of Recognition Science (derived solely from the RCL) never imports external numbers. The definition provides the 2019 SI exact value for ħ. Upstream, the SingleAnchor module supplies the derived form ħ = h_SI / (2π) from the Planck constant definition, allowing consistency checks between the hardcoded anchor and algebraic reductions.
proof idea
The definition is a direct noncomputable numerical assignment. No lemmas or tactics are applied; the body is simply the literal constant.
why it matters
This anchor feeds externalCalibration_of_tau0_seconds (which builds joules_per_coh from hbar_SI / tau0_s) and the AbsolutePack structure for reference displays. It closes the loop from the RCL primitive and phi-ladder (T5–T8) to experimental comparison, enabling checks against the RS-native ħ = φ^{-5} while respecting the alpha band (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.