grav_casimir_ratio_negligible
plain-language theorem explainer
The result shows gravitational pressure remains below 10^{-10} for G = 6.674e-11, length 10^4, separation 10^{-6} and enhancement factor 32, confirming the contribution is negligible against Casimir forces. Nanoscale force metrologists would cite the bound to justify ignoring gravity in Casimir setups. The verification is a direct numerical reduction after expanding the pressure expression.
Claim. With Newton's constant $G = 6.674 times 10^{-11}$, characteristic length $10^4$, separation $10^{-6}$ and running enhancement 32, the gravitational pressure satisfies $P_g < 10^{-10}$.
background
The module treats Newton's G as scale-dependent: $G_{rm eff}(r) = G_infty (1 + |beta| (r/r_{rm ref})^beta)$ where $beta approx -0.056$ follows from the phi-ladder. The pressure function assembles the force density from this running G at nanometer separations. Upstream, the scale definition supplies phi-powers while the G_ratio definition encodes the multiplicative enhancement. The setting is the explicit prediction that G reaches roughly 32 G_infty near 20 nm while recovering the macroscopic value at large r.
proof idea
The proof is a one-line term-mode wrapper: it unfolds the gravitational_pressure definition then applies norm_num to discharge the concrete numerical inequality.
why it matters
The check anchors the H_GravitationalRunning hypothesis by showing that even the enhanced nanoscale G produces a pressure too small to affect Casimir measurements. It closes a consistency objection inside the running-G module without requiring new axioms. No downstream theorems depend on it, but it supports the broader claim that RS-derived running remains compatible with existing force data at accessible scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.