kappaEinsteinL
plain-language theorem explainer
Embeds the Einstein coupling κ = 8πG/c⁴ as a point on the recovered real line LogicReal. Anyone working with RS field equations or curvature sources in the logic-native setting cites this. The body is a one-line transport of the Mathlib real Constants.kappa_einstein via fromReal.
Claim. Define the recovered Einstein coupling $\kappa_L \in \mathrm{LogicReal}$ by transporting the RS-native real $\kappa = 8\pi G/c^4$ across the canonical equivalence into the Cauchy completion of the recovered rationals.
background
LogicRealConstants mirrors Recognition Science constants on the recovered real line. Each constant is a LogicReal value; companion theorems show that toReal recovers the Mathlib real from IndisputableMonolith.Constants.
LogicReal is the Cauchy completion of the recovered rationals, wrapped to avoid polluting Mathlib instances while reusing the completed real line. fromReal sends a Mathlib real $x$ to that wrapper via the inverse of the comparison equivalence.
Upstream, Constants.kappa_einstein is the Einstein coupling $\kappa = 8\pi G/c^4$. In RS-native units ($c = 1$, $\hbar = \varphi^{-5}$, $G = \varphi^5/\pi$) this simplifies to $\kappa = 8\varphi^5$, the coefficient of $T_{\mu\nu}$ in the Einstein field equations.
proof idea
One-line definitional wrapper: apply fromReal to Constants.kappa_einstein. No tactics or intermediate lemmas; the mathematical content lives in the upstream real constant and in the fromReal transport.
why it matters
Places the Einstein coupling on the same recovered line as $\varphi$, the tick, the octave, $\hbar$, and $\alpha^{-1}$, so curvature-source identities can be stated without leaving the logic-native real type.
The sole immediate consumer is toReal_kappaEinsteinL, the simp lemma proving toReal kappaEinsteinL = Constants.kappa_einstein. That closes the round-trip for this constant in the module's transport program.
In the RS framework, $\kappa = 8\varphi^5$ is the native Einstein coefficient once $G = \varphi^5/\pi$ and $c = 1$ are fixed; this definition is the LogicReal handle for that landmark value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.