hbarUniverse_classifier
plain-language theorem explainer
Every reality claim inside the action-quantum universe, when taken under maximal closure from the law-of-logic primitive, receives a forced/independent classification. Citation target for anyone assembling a MaximalClosureCert on the RS-native ħ layer. The proof collapses the closure to the singleton claim h = φ⁻⁵ and tags it forced via the already-proved native-value lemma.
Claim. For every reality claim $C$ about the action-quantum universe (realizations are candidate values $h \in \mathbb{R}$), if $C$ lies in the maximal forcing closure generated from the law-of-logic primitive, then $C$ is classified: either forced in every admissible realization, or independent via an explicit pair of disagreeing admissible realizations.
background
This module is the sixth single-constant maximal-forcing instantiation, the RS-native action-quantum layer. Realizations are candidate values $h \in \mathbb{R}$. The loose class is every real; the RS gate pins $h$ to the native value $\hbar = \varphi^{-5}$ (with $\lambda_{\mathrm{rec}} = c = 1$ and tick $\tau_0$). The sole claim under closure is "$h = \varphi^{-5}$".
ClaimClassification is the two-constructor Prop that tags a claim as forced (holds in every admissible realization) or independent (an explicit disagreement witness). InClosure means the claim sits in the forcing closure of a given primitive over a claim universe. The two primitives are object-level distinction and law-of-logic; here the generator is law-of-logic.
Upstream, forced_hbar already shows the native-value claim is forced over the RS gate, wrapping Constants.hbar_eq_phi_inv_fifth. That is the algebraic content this classifier consumes.
proof idea
Term-mode proof by cases on membership. Introduce claim $C$ and the hypothesis that it lies in the closure. The closure of this universe is the singleton ${$isHbarClaim$}$, so Set.mem_singleton_iff rewrites $C$ to that claim. After substitution, apply the forced constructor of ClaimClassification to the already-proved forced_hbar. No further case analysis: one claim in scope, one forced tag.
why it matters
Feeds directly into hbarUniverseCert, the real MaximalClosureCert for the action-quantum universe (classifies := hbarUniverse_classifier). That certificate is the formal seal that the ħ layer is fully classified under maximal forcing from law-of-logic.
In the Recognition framework this is the native action-normalization boundary: $\hbar = \varphi^{-5}$ in RS units, completing the trio with the gravity surface $\kappa = 8\varphi^5$ and the electromagnetic $\alpha$ window. It is not a derivation of the SI value of Planck's constant; it fixes the dimensionless native normalization. Landmark alignment: constants in RS-native units list $\hbar = \varphi^{-5}$ alongside $c = 1$ and $G = \varphi^5/\pi$.
Closes the classifier obligation for this universe so downstream maximal-forcing assembly can treat the action quantum as a finished single-constant surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.