gravForcedInvariant
plain-language theorem explainer
Packages the Einstein-coupling equality as a forced invariant under the law-of-logic primitive and the gravity-layer claim universe. Anyone citing the gravity-layer maximal-forcing register uses this entry. It is a structure instance that wires the kappa claim, its closure membership, and the forcedness proof already established over the RS-native gate.
Claim. The gravity-layer forced invariant is the triple $(C,\iota,F)$ where $C$ is the reality claim "$k=8\varphi^5$" on candidate Einstein couplings $k\in\mathbb{R}$, $\iota$ places $C$ in the closure of the gravity claim universe under the law-of-logic primitive, and $F$ asserts that $C$ is forced by the RS-native admissibility gate (the class that pins $k$ to the RS Einstein coupling).
background
This module is the Phase-2 gravity layer of maximal forcing: the fifth single-constant instantiation, pinning 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 real $k$; the loose class is every real, while the gate class pins $k$ to the RS-native Einstein coupling.
A forced invariant (from the MaximalForcing layer) is a closure claim together with a proof of forcedness: a reality claim on the universe's realizations, a witness that the claim lies in the primitive's closure, and a proof that every admissible realization satisfies the claim. The gravity claim universe takes realizations as reals, admissibility as the RS gate, and its sole claim as the kappa equality.
The claim itself is the predicate $k=8\varphi^5$. Upstream, forcedness of that claim over the RS gate wraps the constant identity $\kappa_{\mathrm{Einstein}}=8\varphi^5$, whose content is the parameter-free derivation $G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$ with $\hbar=\varphi^{-5}$.
proof idea
Structure-instance definition, not a tactic proof. The three fields of ForcedInvariant are filled by name: the claim field is the kappa-equality reality claim; in-closure is the already-proved membership of that claim in the gravity universe's closure under the law-of-logic primitive; forced is the theorem that every RS-gate-admissible real satisfies $k=8\varphi^5$. No new algebra is done here; the instance only registers those three ingredients under the ForcedInvariant interface.
why it matters
This is the gravitational analogue of the alpha-layer forced-register entry: a derived physical coupling forced to a parameter-free $\varphi$-expression. It records that the Einstein coupling sits in the forced-invariant ledger under the law-of-logic primitive, so downstream maximal-forcing classifiers and certificates can treat gravity on the same footing as the electromagnetic coupling.
Framework landmarks in play are the RS-native constants ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$) and the forcing of $G$ from the recognition length rather than by fit. The module doc stresses that $8\varphi^5$ is not assumed: it is forced by the RS derivation of $G$. No downstream consumers are wired yet in the graph; the immediate siblings are the gravity-universe classifier and certificate, which read this register style of packaging.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.