isHbarClaim
plain-language theorem explainer
Packages the native action-quantum claim as a RealityClaim on reals: a candidate h holds exactly when h equals φ^{-5}. Cited by the RS ħ-universe classifier, forced-invariant register, and independence proofs over the loose class. Pure structure instance: label plus the equality predicate, no proof work.
Claim. The action-quantum reality claim on $\mathbb{R}$ is the predicate that a candidate reduced Planck constant $h$ satisfies $h = \varphi^{-5}$, with audit label recording that this is the parameter-free RS-native value.
background
In the Maximal Forcing stack, a RealityClaim on a carrier type $R$ is a pair of an audit label and a predicate holds : R → Prop. Forcing means the predicate is true in every admissible realization; independence means some admissible realizations satisfy it and some do not.
This module is the sixth single-constant instantiation, the RS-native action-quantum layer. The carrier is a candidate action quantum $h : \mathbb{R}$. The loose class admits every real; the RS gate pins $h$ to the native constant $\hbar$. In the native gauge ($\lambda_{\mathrm{rec}} = c = 1$, tick $\tau_0$), that constant is fixed to the parameter-free value $\varphi^{-5}$.
The module sits with the gravity surface $\kappa = 8\varphi^5$ and the $\alpha$ window as one of three native dimensionless $\varphi$-expression layers. The claim here is only the native action-normalization boundary, not a derivation of the SI value of Planck's constant.
proof idea
Definitional construction of a RealityClaim structure. The label field is the audit string; the holds field is the function $h \mapsto (h = \varphi^{-5})$. No tactics, no lemmas, no reduction: the body is the structure instance itself.
why it matters
This is the single claim object for the action-quantum universe. Downstream, hbarUniverse takes it as its singleton claim set; forced_hbar proves it is Forced over the RS gate by rewriting through Constants.hbar_eq_phi_inv_fifth; isHbarClaim_in_closure places it in the universe closure; hbarForcedInvariant registers it as a forced invariant under the law of logic; hbarUniverse_classifier classifies every closed claim by reducing to this singleton; and hbar_independent_over_Lhbar0 shows independence over the loose class (RS $\hbar$ satisfies the equality, $0$ does not).
Framework-wise it is the quantum-sector counterpart of the native gravitational coupling and the electromagnetic coupling window: the RS-native $\hbar = \varphi^{-5}$ surface (primer constants: $\hbar = \varphi^{-5}$ in RS units). It does not touch T0–T8 forcing of $J$, $\varphi$, the eight-tick octave, or $D=3$; those sit upstream of the constant identities this claim quotes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.