gravL
plain-language theorem explainer
The Newton constant of Recognition Science, lifted from the ordinary reals onto the logic-recovered real line. Anyone citing RS-native gravity couplings or Einstein-bridge constants on LogicReal will use this symbol. It is a one-line transport of the existing real-valued G through fromReal.
Claim. Let $G$ be the RS-native gravitational coupling $G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$. Define $\mathrm{grav}_L$ as the image of $G$ under the canonical transport from Mathlib $\mathbb{R}$ into the logic-recovered real line.
background
The module mirrors Recognition Science constants on the recovered real line LogicReal. Each constant is written as a LogicReal value; companion theorems then show that transport back through toReal recovers the ordinary real constant from Constants.
LogicReal is the Cauchy completion of the recovered rationals, realized via Mathlib's completion of $\mathbb{Q}$ and the equivalence of logic-rationals with $\mathbb{Q}$. The map fromReal sends a Mathlib real $x$ to the corresponding point on that recovered line.
Upstream, Constants.G is the RS-native gravitational coupling projection through the recognition/Planck bridge: $G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$. In RS-native units this is the familiar $G=\varphi^5/\pi$. The definition does not claim an SI prediction; SI conversion lives in the dimensional bridge.
proof idea
Pure definitional wrapper. Apply fromReal to the already-defined real constant Constants.G, yielding a term of type LogicReal. No algebraic work and no lemmas beyond the transport constructor.
why it matters
Places Newton's constant on the same recovered line as $\varphi$, the tick, the octave, $\hbar$, and $\alpha^{-1}$, so gravity sits inside the logic-real constant suite rather than only on Mathlib $\mathbb{R}$. The immediate parent is toReal_gravL, the simp theorem that toReal gravL = Constants.G, discharging the module's transport-recovery obligation for $G$. Downstream Einstein-coupling work (e.g. kappaEinsteinL) can therefore stay inside LogicReal while remaining definitionally tied to the RS-native $G=\varphi^5/\pi$ landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.