toReal_gravL
plain-language theorem explainer
Transport of the LogicReal lift of the RS-native Newton constant recovers the ordinary real value G. Anyone working with the LogicReal mirror of foundation constants cites this identity to move between the two presentations. The proof is a one-line round-trip via the fromReal embedding lemma.
Claim. If $\mathrm{grav}_L$ is the LogicReal lift of the RS-native Newton constant, then its real embedding equals $G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$.
background
The module LogicRealConstants places Recognition Science constants on the recovered real line: each constant is defined in LogicReal, and a companion theorem shows that transport by the real embedding recovers the existing real-valued constant from IndisputableMonolith.Constants.
Here the object being lifted is the RS-native gravitational coupling $G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$. That definition is a projection through the recognition/Planck bridge; it is not a prediction of the SI CODATA value of Newton's constant (SI conversion lives in the separate SI-bridge closure). The LogicReal lift is simply fromReal applied to that $G$.
The real embedding toReal is the standard evaluation map out of the LogicReal construction (with a related evaluation on $\mathbb{Z}[\varphi]$ sending $\langle a,b\rangle$ to $a+b\varphi$). The companion round-trip lemma states that embedding after fromReal is the identity on ordinary reals.
proof idea
One-line wrapper: apply the round-trip identity toReal_fromReal, which states that toReal (fromReal x) = x for any real $x$. Instantiating at $x=G$ and unfolding the definition of the LogicReal lift yields the claim. Marked @[simp] so downstream rewrites can discharge the transport automatically.
why it matters
Closes the Newton-constant slot in the LogicRealConstants suite (alongside the lifts of $\varphi$, the tick, the octave, $J$-bit, $E_{\mathrm{coh}}$, $\hbar$, the Einstein coupling, and $\alpha^{-1}$). In RS-native units the primer fixes $c=1$, $\hbar=\varphi^{-5}$, and $G=\varphi^5/\pi$; this theorem guarantees that the LogicReal presentation of $G$ is faithful to that real constant, so later arguments may work entirely inside LogicReal and transport results back without drift.
No downstream users are recorded yet; the lemma is infrastructure for any proof that must compare LogicReal-native gravitational statements with the ordinary real Constants API. It does not itself derive $G$ from the forcing chain (T0–T8) or from the Recognition Composition Law; it only preserves the already-chosen real value under the LogicReal embedding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.