forced_hbar
plain-language theorem explainer
Over the RS-native action-quantum gate, every admissible candidate equals φ^{-5}. Cite this when registering the native reduced Planck constant as a forced invariant, or when comparing the loose versus gate-tightened classes. The proof is a short rewrite: admissibility yields equality to the native hbar, then the constant identity supplies φ^{-5}.
Claim. Let the RS-native action-quantum class be the set of reals $h$ with $h$ equal to the RS-native reduced Planck constant. Then for every such $h$, the claim $h = \varphi^{-5}$ holds; equivalently, that claim is forced on the class.
background
This module is the sixth single-constant maximal-forcing layer: the quantum-sector action normalization in RS-native units ($\lambda_{\mathrm{rec}} = c = 1$, tick $\tau_0$). Realization carriers are candidate action quanta $h \in \mathbb{R}$. The loose class admits every real; the gate class admits only the RS-native value.
The native constant is defined by $\hbar = E_{\mathrm{coh}} \cdot \tau_0$ with $E_{\mathrm{coh}} = \varphi^{-5}$ and $\tau_0 = 1$, so the identity $\hbar = \varphi^{-5}$ is the native unit choice (THEOREM C-004.1). The claim under closure is exactly that identity on the candidate. Forced means: every admissible realization satisfies the claim.
Upstream, Forced is universal quantification over the admissible set; the gate class is the singleton ${h \mid h = \hbar}$; the claim predicate is $h = \varphi^{-5}$. The SI/CODATA numerical $\hbar$ is a separate object and is not used here.
proof idea
Term-style tactic proof. Introduce an admissible candidate $h$ and the membership hypothesis. Membership is definitionally $h = \hbar$. Rewrite the goal $h = \varphi^{-5}$ by that equality, then apply the constant lemma $\hbar = \varphi^{-5}$ (unfold of the native product $E_{\mathrm{coh}}\cdot\tau_0$ with $\tau_0 = 1$). No case split or arithmetic beyond the rewrite.
why it matters
Closes the forced half of the action-quantum layer: the value claim is forced on the RS gate and independent on the loose class. Downstream it fills the forced field of the forced-invariant register, discharges the classifier for the action-quantum universe (every closed claim is the $\varphi^{-5}$ claim and is forced), and pairs with the independence lemma in the explicit tightening theorem.
Together with the native gravity coupling $\kappa = 8\varphi^5$ and the $\alpha$ window, this completes the trio of native/dimensionless $\varphi$-expression surfaces. The exponent $5 = D+2$ is the structural content beyond unit choice (linked to the forcing chain's $D = 3$). It does not touch SI calibration; that map is left to later dimensional anchoring.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.