Gravity Running G Grav Dominated By Casimir On Nano

The nanometer verdict

The Casimir effect is a real, measured force: two uncharged plates placed very close together in a vacuum attract each other because quantum fluctuations of the electromagnetic field between them exert a pressure. At separations of a few nanometers, this pressure is strong. The Recognition Science declaration grav_dominated_by_casimir_on_nano is a machine-checked theorem establishing that, at such separations, the gravitational pressure predicted by the framework's own running gravitational constant (a proposed strengthening of gravity at short range) is utterly negligible compared to the Casimir pressure.

The theorem's proof is a chain of inequalities. It first shows, as a separate lemma, that for a specific set of physical inputs (a gravitational constant of 6.674e-11, a density of 1e4, a time scale of 1e-6, and an enhancement factor of 32), the gravitational pressure is less than 1e-10. The main theorem then takes any plate separation where the ideal Casimir pressure exceeds 1e7 in absolute value, and shows that this pressure, divided by 1e17, is still larger than that tiny gravitational pressure. The conclusion is that the gravitational term is smaller than the Casimir term by a factor of at least 10^17.

This is not a measurement and it is not a claim about the real world. It is a statement about the framework's own definitions: given its model of a running G and its model of the Casimir pressure, the former is negligible on the nanometer scale. The declaration does not prove that gravity actually runs, nor that the Casimir effect is the only relevant force at that scale. It only establishes a relative magnitude within the framework's formal system.

/-- Parameterized Casimir-dominance theorem: once an ideal plate configuration
has a pressure magnitude above `1e7`, the running-G gravitational pressure
example is smaller than `|P_Casimir| / 1e17`.  The legacy numeric inequality
above supplies the gravitational side; `CasimirEffectCertV2` supplies the
canonical pressure object. -/
theorem grav_dominated_by_casimir_on_nano
    (r : PlateSeparation) (hfloor : (1e7 : ℝ) < |QFT.CasimirPlateModes.idealPressure r|) :
    gravitational_pressure 6.674e-11 1e4 1e-6 32 <
      |QFT.CasimirPlateModes.idealPressure r| / 1e17 := by
  have hgrav := grav_casimir_ratio_negligible
  have hratio : (1e-10 : ℝ) < |QFT.CasimirPlateModes.idealPressure r| / 1e17 := by
    nlinarith
  linarith

/-- The gravitational contribution is negligibly small vs Casimir. -/
theorem grav_casimir_ratio_negligible :
    gravitational_pressure 6.674e-11 1e4 1e-6 32 < 1e-10 := by
  unfold gravitational_pressure; norm_num

What this page does not claim

This theorem does not prove that the gravitational constant actually runs at nanometer scales. This theorem does not claim the Casimir pressure is the only force acting between the plates. This theorem does not compare its prediction to any experimental measurement of gravity at short range.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/RunningG.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: