LgravRS
plain-language theorem explainer
Defines the RS-native gravity gate: the set of Einstein couplings equal to κ = 8πG/c⁴. Anyone citing the forced gravitational coupling or the Lgrav0→LgravRS tightening uses this class as the admissibility filter. It is a one-line set comprehension inside AdmissibilityClass, not a proved statement.
Claim. The RS-native gravity admissibility class is the singleton $\{k \in \mathbb{R} : k = \kappa\}$ where $\kappa = 8\pi G/c^4$ is the Einstein field-equation coupling in RS-native units (equivalently $8\varphi^5$).
background
This module is the gravity layer of Maximal Forcing (Phase 2): a single-constant instantiation that pins the Einstein coupling the way the alpha layer pins the electromagnetic coupling. The carrier is a candidate real $k$; the loose class admits every real; the gate class admits only the RS-native value.
An admissibility class is a pair (admissible set, label). The RS-native Einstein coupling is $\kappa = 8\pi G/c^4$. With the RS projection $G = \lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$ and units $\lambda_{\mathrm{rec}} = c = 1$, $\hbar = \varphi^{-5}$, one gets $\kappa = 8\varphi^5$. That identity is proved elsewhere as kappa_einstein_eq; this definition only names the gate set.
The primer landmarks in play are the RS-native constants ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$) and the forcing pattern: tighten the class until the physical claim becomes forced rather than independent.
proof idea
Definition, not a proof. The admissible field is the singleton set comprehension ${k \mid k = \kappa}$ with $\kappa$ the named Einstein coupling constant; the label is a fixed string. No tactics or lemmas are applied at this site.
why it matters
This is the gate that makes the gravity-layer claim forced. Downstream, forced_kappa shows that over this admissible set the coupling equals $8\varphi^5$, wrapping the parameter-free derivation of $G$. The claim universe gravUniverse installs this class as its admissibility filter with the single claim "$k = 8\varphi^5$".
The tightening tighten_Lgrav0_LgravRS records that every RS-gate realization is loosely admissible. Effectiveness is certified by tightening_Lgrav0_LgravRS_effective: the value claim is independent over the loose class (RS value works, $0$ fails) but forced over this gate. That is the gravitational analogue of the alpha-universe pattern: a derived coupling forced to a pure $\varphi$-expression with no fitted parameter.
Framework landmarks: RS-native $G = \varphi^5/\pi$ and $\hbar = \varphi^{-5}$ do the real work behind $\kappa = 8\varphi^5$; the definition itself only packages the gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.