toReal_kappaEinsteinL
plain-language theorem explainer
Transporting the LogicReal Einstein coupling back to Mathlib reals recovers κ = 8πG/c⁴ (equal to 8φ⁵ in RS-native units). Anyone working with the recovered-real embedding of RS constants cites this identity. The proof is a one-line application of the fromReal/toReal round-trip.
Claim. If $\kappa_L$ is the LogicReal lift of the Einstein coupling, then $\mathrm{toReal}(\kappa_L) = \kappa$, where $\kappa = 8\pi G/c^4$ is the Mathlib real (equal to $8\varphi^5$ in RS-native units with $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$).
background
LogicRealConstants mirrors Recognition Science constants on the recovered real line: each constant is built in LogicReal, and a companion theorem shows that transport through toReal recovers the existing Mathlib value from IndisputableMonolith.Constants.
The Einstein coupling is $\kappa = 8\pi G/c^4$, the coefficient of $T_{\mu\nu}$ in the Einstein field equations. In RS-native units ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$) this collapses to $8\varphi^5$. The LogicReal avatar is defined by kappaEinsteinL := fromReal Constants.kappa_einstein.
toReal sends a recovered real to Mathlib's $\mathbb{R}$ via the comparison equivalence; fromReal is the inverse embedding. The upstream round-trip toReal_fromReal states $\mathrm{toReal}(\mathrm{fromReal}, x)=x$ for every Mathlib real $x$.
proof idea
One-line wrapper. Because kappaEinsteinL is definitionally fromReal Constants.kappa_einstein, the goal is exactly an instance of toReal_fromReal, applied with the underscore for the real argument. Marked @[simp] so downstream rewrites discharge automatically.
why it matters
Closes the transport identity for the Einstein coupling inside the LogicReal constants suite (siblings: $\varphi$, tick, octave, $J$-bit, $E_{\mathrm{coh}}$, $\hbar$, $G$, $\alpha^{-1}$). In the RS framework $\kappa=8\varphi^5$ is the native form of the Einstein coefficient once $G=\varphi^5/\pi$ and $c=1$ are fixed by the forcing chain and the recognition composition law. No downstream consumers are wired yet (used_by empty); the lemma is infrastructure so later gravity or continuum statements can stay on the recovered line and simp back to Mathlib $\kappa$ when needed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.