gravitational_pressure
plain-language theorem explainer
Gravitational pressure is defined as the product of an enhancement factor, G_val, rho squared, and t squared. Researchers comparing nanoscale gravitational forces to Casimir effects in Recognition Science cite this when quantifying plate interactions under running G. The definition is a direct algebraic expression requiring no lemmas or reductions.
Claim. The gravitational pressure between two plates is given by $P_g = e G r^2 t^2$, where $e$ is the enhancement factor from running of $G$, $G$ is the gravitational constant, $r$ is mass density, and $t$ is plate thickness.
background
The module formalizes C51: gravitational running at nanometer scales, where $G(r) -> G_∞$ as $r -> ∞$ but strengthens to approximately 32 $G_∞$ near 20 nm. The running exponent $β = -(φ-1)/φ^5 ≈ -0.056$ follows from the φ-ladder in the Recognition framework. This definition supplies the pressure term for comparing gravitational and Casimir contributions under that enhancement.
proof idea
This is a definition implemented as the direct algebraic expression enhancement * G_val * rho ^ 2 * t ^ 2. It is a one-line wrapper with no lemmas applied and no tactic steps beyond the expression itself.
why it matters
The definition supplies the gravitational pressure term used in grav_casimir_ratio_negligible, which shows the contribution remains below 1e-10 even with nanoscale enhancement. It supports the C51 prediction of running G derived from the φ-ladder and eight-tick octave, closing the comparison between gravitational and vacuum forces at small scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.