dimensionless_G_derived
plain-language theorem explainer
RS assigns the dimensionless Newton coupling $G m_e^2/(\hbar c)$ the numerical value $1.75\times10^{-45}$. Anyone building the RS observables bundle cites this slot. The body is a bare constant assignment: a scaffold pending the full Planck-scale coherence derivation from the cost structure.
Claim. The RS-predicted dimensionless gravitational coupling is fixed at the placeholder value $G\, m_e^2/(\hbar c) = 1.75\times 10^{-45}$.
background
The Observables module separates a cost-first core (predictions from $\varphi$ and the $J$-cost structure) from an external-anchor section that imports CODATA bounds. Tracked quantities are all dimensionless: $\alpha^{-1}$, $m_e/m_\mu$, $m_p/m_e$, and $G m_e^2/(\hbar c)$. This avoids SI unit anchors.
Upstream cost machinery (ObserverForcing, MultiplicativeRecognizer, RungCoarsen) defines recognition cost via the $J$-cost $J(x)=(x+x^{-1})/2-1$ on positive ratios. In RS-native units the primer fixes $G=\varphi^5/\pi$, $c=1$, $\hbar=\varphi^{-5}$; the dimensionless combination here folds in electron mass so the number can be compared to CODATA without unit conversion.
The doc-comment marks this entry as a scaffold: "Planck-scale coupling from coherence structure," full derivation still in progress.
proof idea
No proof. The declaration is a noncomputable def equal to the literal real $1.75\times10^{-45}$. There is no lemma application, algebraic reduction, or tactic script; it is a placeholder constant awaiting replacement by a derived expression from the cost/coherence chain.
why it matters
Fills the dimensionless_G field of rsObservables, the RS-predicted DimensionlessObservables record compared against empirical bounds. Without a concrete number in this slot, the exclusivity/observables interface cannot claim a gravitational prediction.
In the broader framework, $G$ is forced in RS-native units as $\varphi^5/\pi$ (primer constants). The dimensionless form $G m_e^2/(\hbar c)$ is the calibration-safe observable the verification layer actually checks. Closing the scaffold means deriving $1.75\times10^{-45}$ (or its refined successor) from the $\varphi$-ladder mass formula and the eight-tick/coherence structure rather than inserting it by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.