isKappaClaim
plain-language theorem explainer
Packages the gravity-layer assertion that a candidate Einstein coupling equals $8\varphi^5$ as a single reality claim on $\mathbb{R}$. Cited by anyone closing or classifying the RS gravity universe, and by the independence check over the loose class. Pure structure instance: audit label plus the equality predicate; no proof content.
Claim. The reality claim on a real candidate Einstein coupling $k$ asserting $k = 8\varphi^{5}$, with audit label that this is the parameter-free Einstein coupling.
background
In the maximal-forcing stack, a reality claim is a pair of an audit-facing label and a predicate holds on realizations. Here the realization carrier is a candidate Einstein-coupling value $k:\mathbb{R}$.
The module is the Phase-2 gravity layer: the analogue of the alpha universe for the gravitational sector. In RS-native units ($\lambda_{\mathrm{rec}}=c=1$, $\hbar=\varphi^{-5}$) the Einstein coupling $\kappa=8\pi G/c^4$ reduces to the pure number $8\varphi^5$ once $G=\varphi^5/\pi$ is substituted. The loose class admits every real; the RS gate pins $k$ to that native value.
Upstream, RealityClaim supplies only the structure (label plus predicate). The numerical identity itself lives in Constants.kappa_einstein_eq and is invoked by the forcing theorems that consume this claim.
proof idea
Definitional construction, not a proof. Instantiates RealityClaim ℝ by setting the label string and taking holds to be the predicate $k\mapsto k=8\varphi^5$. No tactics, no lemmas.
why it matters
Single claim under closure for the gravity-layer claim universe. It is the sole element of gravUniverse.claims, so membership in the closure is immediate singleton membership (isKappaClaim_in_closure). Over the RS gate it is forced (forced_kappa), wrapping the parameter-free derivation $G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$ with $\hbar=\varphi^{-5}$; that forced entry is registered as gravForcedInvariant and exhausts the classifier gravUniverse_classifier.
Over the loose class the same claim is independent: the RS value satisfies it and $0$ does not (kappa_independent_over_Lgrav0), so the tightening from loose to RS gate is effective. Framework landmark: with $c=1$ and $G=\varphi^5/\pi$ one has $\kappa=8\pi G=8\varphi^5$, the gravitational twin of the alpha-layer forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.