gravUniverse_classifier
plain-language theorem explainer
Every reality claim in the gravity-layer universe that lies in the law-of-logic forcing closure is classified: the sole in-scope claim (Einstein coupling equals the RS-native value) is forced. Gravity-sector maximal-closure certificates cite this. The proof collapses the closure to a singleton and applies the forced-kappa witness.
Claim. For every reality claim $C$ on the gravity-layer realization carrier, if $C$ lies in the forcing closure of the law-of-logic primitive for the gravity universe, then $C$ is classified: either forced in every admissible realization or independent via an explicit witness. In this universe the only such $C$ is the kappa claim, and it is forced.
background
This module is Phase 2 of maximal forcing in the gravitational sector. The realization carrier is a candidate Einstein coupling $k:\mathbb{R}$. The loose class is every real; the RS gate pins $k$ to the native value $\kappa=8\varphi^5$ (from $\kappa=8\pi G/c^4$ with $\lambda_{\mathrm{rec}}=c=1$, $\hbar=\varphi^{-5}$, and $G=\varphi^5/\pi$).
A ClaimUniverse packages admissibility and the claim set under study. InClosure means the claim sits in the forcing closure generated from a Primitive (here lawOfLogic). ClaimClassification is an inductive Prop with two constructors: forced (holds in every admissible realization) and independent (two admissible realizations disagree).
The gravity universe's closed claim set is the singleton containing the kappa equality claim. Upstream, forced_kappa already shows that claim is forced over the RS gate class.
proof idea
Term-mode proof after a short tactic spine. Introduce claim $C$ and membership $hC$ in the law-of-logic closure. From the universe construction the closure is a singleton, so Set.mem_singleton_iff yields $C=$ the kappa claim; substitute. Discharge with ClaimClassification.forced forced_kappa, the existing forced-witness for that claim. No case split on independence is needed.
why it matters
This is the classifier half of a real MaximalClosureCert for the gravity layer. Downstream, gravUniverseCert sets classifies := gravUniverse_classifier, packaging the certificate that every in-scope claim is decided.
Framework role: gravitational analogue of the alpha-universe story. Where electromagnetism pins $\alpha$, this layer pins the Einstein coupling to the parameter-free value $8\varphi^5$ forced from RS-native $G$, $c$, and $\hbar$. It sits in the maximal-forcing stack that closes physical couplings from the law-of-logic primitive, consistent with the forcing chain's $\varphi$-fixed geometry (T5–T6) and the RS constants $G=\varphi^5/\pi$, $\hbar=\varphi^{-5}$.
Together with the companion independence result over the loose class, it shows the RS gate does real work: the value is forced only after the gate, not assumed a priori.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.