kappa_value_pos
plain-language theorem explainer
The forced Einstein-coupling value equals $8\varphi^5$ and is strictly positive. Gravity-layer independence arguments cite it to separate the RS-native coupling from the zero candidate over the unrestricted class of real couplings. The proof is a one-line rewrite onto the already-proved positivity of the RS-native $\kappa$.
Claim. In RS-native units one has $0 < 8\varphi^{5}$, where $\varphi$ is the golden ratio fixed by self-similarity.
background
This module is the gravitational Phase-2 extension of maximal forcing. The realization carrier is a candidate Einstein coupling $k\in\mathbb{R}$. The loose class admits every real; the gate class pins $k$ to the RS-native value $\kappa=8\pi G/c^4$. In units $\lambda_{\mathrm{rec}}=c=1$ and $\hbar=\varphi^{-5}$, that value collapses to the pure number $8\varphi^5$ with no free parameter.
Upstream, kappa_einstein_eq identifies the unfolded definition of the RS Einstein coupling with $8\varphi^5$ after cancelling $\pi$, $G=\varphi^5/\pi$, and $\hbar=\varphi^{-5}$. Separately, kappa_einstein_pos proves that same coupling is positive by a chain of product and quotient positivity lemmas. The present statement simply records positivity at the forced pure-number form.
proof idea
Rewrite the goal backwards along the equality $\kappa_{\mathrm{E}}=8\varphi^5$, turning $0<8\varphi^5$ into $0<\kappa_{\mathrm{E}}$. Discharge the rewritten goal by the existing positivity lemma for the RS-native Einstein coupling. No new arithmetic is performed.
why it matters
Feeds the independence theorem over the loose gravity class: that result exhibits the RS coupling as a witness that satisfies the value claim $k=8\varphi^5$ and zero as a witness that fails it, and the failure half needs $8\varphi^5>0$. Together they show the claim is independent until the gate class is imposed, at which point the same pure number is forced.
In the broader framework this is the gravitational analogue of the alpha-universe forcing: $G$ is derived from $\lambda_{\mathrm{rec}},c,\hbar$ rather than fitted, and the Einstein coupling lands on $8\varphi^5$. It sits in the constants layer that already fixes $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$, completing the single-constant gravitational sector of maximal forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.