H_GravitationalRunning
plain-language theorem explainer
Gravity strengthens at nanometer scales under this hypothesis, which states that there exists a positive reference scale making the gravitational ratio at 20 nm approximately 32. Physicists examining scale-dependent gravity effects would cite it to test the Recognition Science running-G prediction. The definition directly encodes the claim via an existential quantifier on the G_ratio function.
Claim. There exists a positive real number $r_{ref}$ such that $|G_{ratio}(20×10^{-9}, r_{ref}) - 32| < 1$, where $G_{ratio}(r, r_{ref})$ denotes the effective gravitational enhancement factor at scale $r$.
background
The RunningG module formalizes the running of Newton's constant G at small scales, with $G_{eff}(r)$ approaching $G_∞$ at large $r$ and increasing as $r$ decreases according to a power law with negative exponent beta_running ≈ -0.056. This exponent originates from the phi-ladder in PhiForcingDerived, where J-cost structures determine self-similar scaling. The module imports constants and relies on ledger factorization for the underlying multiplicative structure. Upstream, NucleosynthesisTiers provides density tiers consistent with phi-powers, while SpectralEmergence ensures the three-dimensional spatial content D=3 that underpins the gravitational sector.
proof idea
The declaration is a direct definition of the hypothesis proposition. It applies the G_ratio function from the sibling definition beta_running and checks the absolute deviation from 32 at the 20 nm scale.
why it matters
This hypothesis is the core prediction of the C51 gravitational running module and is used by the certificate theorem H_GravitationalRunning_certificate to establish satisfiability. It also appears in the RunningGR4Cert structure. The statement connects the phi-derived running exponent beta to the eight-tick octave scaling in the Recognition framework, predicting observable strengthening of gravity at nanometer distances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.