RunningGR4Cert
plain-language theorem explainer
The round-4 gravitational running certificate collects four properties: positivity of the inverted reference radius for any positive input radius and target above one, the reference radius lying strictly above the input radius once the target exceeds one plus the absolute running exponent, the phi-rung approximation differing from 360 by exactly four, and existence of the gravitational running hypothesis. A physicist checking nanometer-scale strengthening of G would cite this certificate when confirming the 20 nm enhancement model parameters. A
Claim. A structure whose fields assert: for all $r>0$ and $t>1$, the inverted reference radius $r_*(r,t)$ solving the $G$-ratio equation is positive; for all $r>0$ and $t>1+|$running exponent$|$, one has $r<r_*(r,t)$; the approximate phi-rung of the reference radius satisfies rung$-360=4$; and the hypothesis that there exists $r_*>0$ with $|G(20$ nm$)/G_∞-32|<1$ holds.
background
The module states that $G$ is not constant but runs at nanometer scales via $G_(r)=G_∞(1+|β|(r/r_)^β)$ with running exponent $β=-(φ-1)/φ^5≈-0.056$. beta_running is the definition $β=-(φ-1)/φ^5$, proved negative via $φ∈(1.61,1.62)$. H_GravitationalRunning is the proposition asserting existence of positive $r_*$ such that the ratio at 20 nm is within 1 of 32. r_ref_exact inverts the ratio formula to produce the exact reference radius achieving a chosen target. r_ref_phi_rung_approx is the natural-number rung 364, noted as four above the RS sync period 360.
proof idea
This is a structure definition whose four fields are supplied directly by the module lemmas r_ref_exact_pos, r_ref_exact_gt_r, rung_near_sync_period and H_GravitationalRunning_certificate.
why it matters
The structure is instantiated by the theorem running_g_r4_cert to certify the round-4 predictions. It supports the C51 claim of $G$ strengthening by a factor near 32 at 20 nm, consistent with the phi-ladder and eight-tick octave. The rung offset of four links the reference scale to the RS sync period. No open questions are flagged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.