pith. machine review for the scientific record. sign in
def definition def or abbrev high

H_GravitationalRunning

show as:
view Lean formalization →

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.

claimThere 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  60def H_GravitationalRunning : Prop :=

proof body

Definition body.

  61  ∃ r_ref : ℝ, r_ref > 0 ∧
  62    abs (G_ratio 20e-9 r_ref - 32) < 1.0
  63
  64/-! ## Structural Properties of G_ratio -/
  65
  66/-- beta_running is strictly negative. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.