hbar_SI
plain-language theorem explainer
This definition supplies the reduced Planck constant in SI units by dividing the exact Planck constant by 2π. Single-anchor calibration protocols cite it when mapping RS-native act energies to joule-seconds. It is realized as a direct algebraic division of the module-local h_SI by twice pi.
Claim. $ℏ_{SI} = h_{SI} / (2π)$, where $h_{SI}$ is the exact SI Planck constant $6.62607015 × 10^{-34}$ J s.
background
The SingleAnchor module supplies a concrete single-anchor calibration protocol for reporting RS-native tick/voxel/coh/act quantities in SI units. Only one empirical scalar, seconds_per_tick (τ₀), is supplied; meters_per_voxel follows from the SI definition of c and joules_per_coh follows from ħ together with the identity 1 act = 1 coh × 1 tick. The local h_SI is defined exactly as the rational 662607015 / 10^42 to match the 2019 SI redefinition of h. Upstream anchors from ExternalAnchors supply the corresponding numerical values for both h and ħ.
proof idea
The definition is a one-line wrapper that divides the local h_SI constant by 2 * Real.pi.
why it matters
This supplies the SI ħ value required by externalCalibration_of_tau0_seconds to populate joules_per_coh and by the theorem one_act_reports_hbar, which shows that one act reports ħ in SI units. It also appears in the AbsolutePack structure for SI reference displays. In the framework it bridges the RS-native constant ħ = phi^{-5} to the SI anchor, closing the single-anchor calibration seam without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.