LhbarRS
plain-language theorem explainer
Gate class of real action-quantum candidates equal to the RS-native reduced Planck constant (φ⁻⁵ in native units). Used by anyone citing the forced native action-normalization layer or the Lhbar0→LhbarRS tightening. Defined as a singleton admissibility set inside AdmissibilityClass ℝ.
Claim. Let $L_{\hbar}^{\mathrm{RS}}$ be the admissibility class of real candidates $h$ whose admissible set is $\{ h \in \mathbb{R} \mid h = \hbar \}$, where $\hbar$ is the RS-native action quantum ($\hbar = \varphi^{-5}$ in units $\lambda_{\mathrm{rec}} = c = 1$, $\mathrm{tick} = \tau_0$), labeled "RS-native action quantum: $h = \hbar$".
background
This module is the sixth single-constant Maximal Forcing instantiation, entering the quantum sector. Realization carriers are candidate action-quantum values $h : \mathbb{R}$. The loose class $L_{\hbar}^{0}$ admits every real; the gate class here pins the candidate to the RS-native value.
An AdmissibilityClass is a pair (admissible set, label) over an abstract realization type. Here the type is $\mathbb{R}$ and the set is the singleton of the RS-native $\hbar$. Upstream, Constants.hbar is defined as $E_{\mathrm{coh}} \cdot \tau_0 = \varphi^{-5}$ in native units; the companion lemma hbar_eq_phi_inv_fifth is definitional unfold/simp, not an SI derivation.
The module frames this as native action normalization, not a claim that the CODATA SI value of Planck's constant is forced without a dimensional anchor. Together with the gravity and alpha universes it forms a trio of native $\varphi$-expression surfaces.
proof idea
Definitional construction, not a proof. The structure fields are filled directly: admissible is the set comprehension ${ h \mid h = \hbar }$ using Constants.hbar, and label is the fixed string naming the RS-native gate. No tactics or lemmas are applied at this site.
why it matters
This is the gate that turns the action-quantum claim from independent to forced. Downstream, forced_hbar shows that over this admissible set the claim $h = \varphi^{-5}$ holds by rewriting through hbar_eq_phi_inv_fifth. The claim universe hbarUniverse installs this class as its admissibility gate with claim set ${$ isHbarClaim $}$.
The tightening tighten_Lhbar0_LhbarRS and the effectiveness theorem tightening_Lhbar0_LhbarRS_effective package the contrast: over the loose class the value claim is independent (RS $\hbar$ works, $0$ fails), while over this gate it is forced. That contrast is the native action-normalization boundary later mapped into J·s by SI calibration.
In the broader RS picture this sits with $\hbar = \varphi^{-5}$ among the native constants ($c=1$, $G=\varphi^5/\pi$), completing the quantum leg of the native/dimensionless $\varphi$-expression trio alongside $\kappa = 8\varphi^5$ and the $\alpha$ window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.