hbarForcedInvariant
plain-language theorem explainer
Register entry packaging the reduced Planck constant as a forced invariant under the law-of-logic primitive: over the RS-native gate, every admissible action quantum equals φ^{-5}. Cite it when anchoring the native action-normalization boundary or the quantum-sector forcing trio (with gravity and α). The definition only assembles already-proved forcedness and closure witnesses into the ForcedInvariant record.
Claim. The forced-invariant register for the action quantum records that the claim $h = \varphi^{-5}$ belongs to the closure of the law-of-logic primitive on the action-quantum claim universe, and is forced by the RS-native admissibility gate on candidate values $h \in \mathbb{R}$.
background
This module is the sixth single-constant maximal-forcing instantiation, now in the quantum sector. Realization carriers are candidate action quanta $h \in \mathbb{R}$. The loose class admits every real; the RS gate pins $h$ to the native constant $\hbar$. The claim under closure is exactly $h = \varphi^{-5}$, in the native gauge $\lambda_{\mathrm{rec}} = c = 1$, tick $= \tau_0$.
A forced invariant is a closure claim together with a proof of forcedness: a reality claim, a witness that it lies in the primitive's closure, and a proof that every admissible realization satisfies it. Here the primitive is the law-of-logic constructor (kept distinct from bare distinction so later modules can equate them rather than identify them silently).
Upstream, forcedness of the native value over the RS gate is already proved by rewriting through the constant identity $\hbar = \varphi^{-5}$. Over the loose class the same claim is independent: the RS value satisfies it and $0$ does not, since $\varphi^{-5} > 0$.
proof idea
Structure assembly, not a fresh argument. The three ForcedInvariant fields are filled by name: the claim is the reality claim "$h = \varphi^{-5}$"; in-closure is the sibling witness that this claim sits in the law-of-logic closure of the action-quantum universe; forcedness is the sibling theorem that every RS-gate-admissible $h$ equals $\varphi^{-5}$. That forcedness theorem itself is a short rewrite: admissibility gives $h = \hbar$, then $\hbar = \varphi^{-5}$ from the constants library.
why it matters
Closes the native action-normalization surface in the maximal-forcing stack. Together with the gravity universe ($\kappa = 8\varphi^5$) and the $\alpha$ window, it completes the trio of native or dimensionless $\varphi$-expression surfaces: action normalization, gravitational coupling, and electromagnetic coupling. In RS-native units the primer fixes $\hbar = \varphi^{-5}$ (with $c = 1$, $G = \varphi^5/\pi$); this register makes that identity a forced invariant rather than a bare constant binding. No downstream consumers are wired yet in the graph; the entry is the stable citation point for any later certificate that needs the action quantum already forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.