H_GravitationalRunning_certificate
plain-language theorem explainer
Existence of r_ref >0 satisfying |G_ratio(20 nm, r_ref) -32| <1 is certified. Researchers modeling nanoscale gravitational strengthening cite the result. The argument invokes the intermediate value theorem on the continuous G_ratio after locating scales where the ratio lies below 31 and above 33.
Claim. There exists a positive real number $r_{ref}$ such that $|G_{ratio}(20 nm, r_{ref}) - 32| < 1$, where $G_{ratio}(r, r_{ref}) = 1 + |β| (r / r_{ref})^β$ and $β$ is the running exponent.
background
Module C51 develops the hypothesis that Newton's constant runs at nanometer scales according to an exponent β drawn from the φ-ladder. G_ratio(r, r_ref) encodes the enhancement factor 1 + |β| (r/r_ref)^β. H_GravitationalRunning is the proposition asserting that some r_ref >0 makes this factor approximately 32 at r = 20 nm. Upstream constants supply G in RS-native form as λ_rec² c³ / (π ℏ) with c=1, ℏ=φ^{-5} and the status of φ-based units.
proof idea
Unfold the target proposition. Establish 20e-9 >0 by norm_num. Apply G_ratio_at_self_lt_31 to obtain a ratio below 31 at equal arguments. Invoke G_ratio_eventually_large to produce an R >20e-9 where the ratio exceeds 33. Verify continuity of the second argument of G_ratio. Restrict the interval to positive reals. Apply intermediate_value_Icc to the image interval containing 32. Extract the witness c and confirm the bounds.
why it matters
The certificate populates the hypothesis_exists slot of running_g_r4_cert. It substantiates the 20 nm prediction stated in the module doc-comment. The construction uses the φ-derived running exponent but treats r_ref as free, echoing the comment that derivation would require the Fibonacci-square conjecture or empirical input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.