h_SI
plain-language theorem explainer
The declaration supplies the exact SI 2019 value of Planck's constant as a real number for external calibration. Metrologists and RS modelers cite it when matching cost-derived predictions to laboratory units. It is a direct noncomputable assignment with no further computation or lemmas.
Claim. The Planck constant is fixed at $h = 6.62607015 × 10^{-34}$ J s by the 2019 SI redefinition.
background
The ExternalAnchors module is the single quarantined location for all CODATA and empirical calibration data that enters Recognition Science. Its policy keeps the cost-first core (RCL and J-function derivations) free of external numbers while allowing comparison modules to import anchors explicitly. The upstream SingleAnchor definition supplies the identical constant in exact rational form as 662607015 / 10^{42}.
proof idea
The definition is a direct noncomputable assignment of the decimal literal to type ℝ. No lemmas are invoked and no tactics are used; it functions as a literal constant.
why it matters
It supplies the numerical bridge that lets RS-native constants (phi-ladder masses, ħ = phi^{-5} in native units) be compared with experiment. The value is consumed by hbar_SI and the positivity lemma h_SI_pos inside SingleAnchor, closing the calibration seam between the forcing chain (T0-T8) and measured data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.