forced_kappa
plain-language theorem explainer
Over the RS-native gravity gate, every admissible Einstein coupling equals $8\varphi^5$. Gravity-layer classifiers and the Lgrav0/LgravRS tightening theorem cite this. The proof is a short rewrite: admissibility pins $k$ to $\kappa_{\mathrm{E}}$, then Constants.kappa_einstein_eq supplies the pure $\varphi$ value.
Claim. Let the RS-native gravity gate be the set of real candidates $k$ with $k = \kappa_{\mathrm{E}}$ (Einstein coupling $8\pi G/c^4$ in RS units). The claim "$k = 8\varphi^5$" is forced on that gate: every admissible $k$ satisfies $k = 8\varphi^5$.
background
This module is the gravity layer of Maximal Forcing (Phase 2): the gravitational analogue of the alpha universe. Realization carriers are candidate Einstein couplings $k:\mathbb{R}$. The loose class admits every real; the gate class LgravRS restricts to $k = \kappa_{\mathrm{E}}$, the RS-native value of $8\pi G/c^4$.
In RS-native units ($\lambda_{\mathrm{rec}}=c=1$, $\hbar=\varphi^{-5}$), the constant $\kappa_{\mathrm{E}}$ is defined as $8\pi G/c^4$. The upstream identity kappa_einstein_eq rewrites it to $8\varphi^5$ via $G=\varphi^5/\pi$ from $G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$. The claim isKappaClaim is exactly "$k=8\varphi^5$".
Forced means: a claim holds in every realization inside the admissible set. Here the admissible set is a singleton, so forcing reduces to evaluating that singleton against the $\varphi$-expression.
proof idea
Tactic proof, four steps. Introduce an admissible $k$ with witness $k=\kappa_{\mathrm{E}}$. Goal becomes $k=8\varphi^5$. Rewrite the witness, then apply kappa_einstein_eq, which unfolds $G$, $\hbar$, $c$ locks and simplifies to $8\varphi^5$. No case split; the gate is already a singleton.
why it matters
Pins the Einstein field-equation coupling as a parameter-free $\varphi$-number, the gravitational twin of the alpha-layer forcing. Feeds three parents: gravForcedInvariant (registers the claim as a forced invariant of the gravity universe), gravUniverse_classifier (every closed claim is classified, and the only closed claim is this one), and tightening_Lgrav0_LgravRS_effective (independence over the loose class plus forcing over the gate, proving the RS gate is a genuine tightening).
Framework landmarks: $G=\varphi^5/\pi$ and $\hbar=\varphi^{-5}$ in RS units, so $\kappa=8\varphi^5$ is derived, not fitted. Completes the fifth single-constant instantiation in Maximal Forcing. No open scaffold remains on this edge; the real work sits in the Constants derivation of $G$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.