hbar_constraint
plain-language theorem explainer
The ℏ-constraint is the matching condition that equates the exact SI-2019 reduced Planck constant to the RS-native value φ^{-5} scaled by the bridge factors a_M a_L²/a_T. Anyone proving uniqueness of the SI calibration map cites this predicate as one of the three closing equations. It is a pure definitional equality on an SIBridge record, not a derived identity.
Claim. For a bridge $b$ with positive conversion factors $a_T$ (seconds per tick), $a_L$ (metres per voxel), and $a_M$ (kilograms per coherence-mass), the $\hbar$-constraint is the proposition $\hbar_{\mathrm{SI}} = \hbar_{\mathrm{RS}} \cdot (a_M \cdot a_L^2 / a_T)$, where $\hbar_{\mathrm{RS}} = \varphi^{-5}$ and $\hbar_{\mathrm{SI}}$ is the exact SI-2019 value.
background
Recognition Science predicts the dimensionless triple $c_{\mathrm{RS}}=1$, $\hbar_{\mathrm{RS}}=\varphi^{-5}$, $G_{\mathrm{RS}}=\varphi^5/\pi$ in native units, together with the recognition/Planck identity $G\cdot\pi\cdot\hbar=\lambda_{\mathrm{rec}}^2 c^3$ at $\lambda_{\mathrm{rec}}=1$. Converting to SI requires three positive scale factors collected in an SIBridge: $a_T$ (s/tick), $a_L$ (m/voxel), $a_M$ (kg/coherence-mass).
Under SI-2019, $c_{\mathrm{SI}}$ and $\hbar_{\mathrm{SI}}$ are exact definitional anchors; $G_{\mathrm{SI}}$ is the CODATA measurement that fixes this particular bridge. Matching dimensions against the three RS predictions yields the c-, ℏ-, and G-constraints. The module proves that those three equations uniquely determine the calibration (in particular $\tau_0=\sqrt{\pi},\tau_{\mathrm{Planck}}$).
Upstream, $\hbar_{\mathrm{SI}}$ is the external SI-2019 anchor $1.054571817\times 10^{-34},\mathrm{J\cdot s}$, while $\hbar_{\mathrm{RS}}$ is the RS-native constant $\varphi^{-5}$.
proof idea
Definitional one-liner. The body is the equality $\mathtt{hbar_SI} = \mathtt{hbar_RS} \cdot (b.a_M \cdot b.a_L^2 / b.a_T)$ with no tactics, lemmas, or proof obligations. Positivity of the bridge factors is carried by the SIBridge structure fields and is not re-proved here.
why it matters
This predicate is one of the three conjuncts of IsClosedBridge, the closed-calibration predicate for the dimensional bridge. Downstream, aM_aT_eq_of_c_hbar uses the c- and ℏ-constraints together to obtain $a_M\cdot a_T = \hbar_{\mathrm{SI}}/(\hbar_{\mathrm{RS}}, c_{\mathrm{SI}}^2)$, which feeds the uniqueness argument culminating in $a_T^2 = \pi,\hbar_{\mathrm{SI}} G_{\mathrm{SI}}/c_{\mathrm{SI}}^5$ (i.e. $\tau_0=\sqrt{\pi},\tau_{\mathrm{Planck}}$).
In the broader framework it realises the SI half of the native prediction $\hbar=\varphi^{-5}$ (primer constants in RS-native units). The module closes the conversion map once the dimensional anchor is supplied; it does not predict the SI value of $G$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.