Lgrav0

This module is the gravity layer of Maximal Forcing (Phase 2): a single-constant instantiation that pins the Einstein field-equation coupling $\kappa = 8\pi G/c^4$. In RS-native units ($\lambda_{\mathrm{rec}} = c = 1$, $\hbar = \varphi^{-5}$) that coupling is forced to the pure number $8\varphi^5$ with no fitted parameter. The realization carrier is a candidate coupling $k:\mathbb{R}$.

An admissibility class is a pair of a set of admissible realizations and a label string. Different phases instantiate the carrier type differently; here the carrier is simply $\mathbb{R}$. The RS-native gravitational constant is $G = \lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$, and the tightened gate class later pins $k$ to the derived Einstein coupling built from that $G$.

The module pattern mirrors the electromagnetic alpha layer: start from a totally loose class, tighten by an RS gate, then prove the value claim is independent over the loose class and forced over the gate.

Pure structure instance, not a proof. The admissible field is set to Set.univ (every real), and the label records the informal reading "every candidate Einstein-coupling value". No lemmas are applied.

This is the loose baseline against which the gravity gate is measured. Downstream, LgravRS restricts to ${k \mid k = \kappa_{\mathrm{einstein}}}$, and tighten_Lgrav0_LgravRS records that restriction as a legitimate tightening. Independence of the claim "$k = 8\varphi^5$" over this loose class is proved by exhibiting the RS value (which satisfies it) and $0$ (which does not, since $8\varphi^5 > 0$). The effectiveness theorem then packages independence over the loose class with forcedness over the gate, showing the RS derivation of $G$ does real work rather than assuming $8\varphi^5$. Framework landmark: RS-native $G = \varphi^5/\pi$ (with $c=1$, $\hbar=\varphi^{-5}$) yields $\kappa = 8\varphi^5$.