running_g_r4_cert
plain-language theorem explainer
The theorem assembles a certificate that the reference scale r_ref for gravitational running is positive whenever r>0 and target>1, exceeds the measurement radius r when the target exceeds 1+|beta|, places the phi-rung approximation four units from the 360-unit sync period, and confirms the 20 nm enhancement hypothesis. Modelers of nanoscale gravity corrections would cite it to lock in the formal consistency of the beta exponent derived from the phi ladder. The proof is a direct term-mode construction that supplies the four required fields of a
Claim. Let $r>0$ and $t>1$. The reference scale $r_*(r,t)$ defined by $r_*(r,t)=r(t-1)/|beta|$ satisfies $r_*(r,t)>0$. When $t>1+|beta|$, one has $r<r_*(r,t)$. The rung index satisfies $r_{phi}-360=4$. The hypothesis that there exists $r_{ref}>0$ with $|G(20nm,r_{ref})/G_∞-32|<1$ holds.
background
Module C51 formalizes the claim that Newton's G is scale-dependent and strengthens at nanometer distances. The effective constant is written $G_eff(r)=G_∞(1+|beta|(r/r_ref)^beta)$ with beta=-(phi-1)/phi^5. The structure RunningGR4Cert packages four concrete statements needed to certify the 20 nm prediction: positivity of the explicit reference scale, the inequality r_ref>r under the target condition, proximity of the rung index to the eight-tick sync period 360, and existence of a suitable r_ref. Upstream, H_GravitationalRunning_certificate proves existence by combining G_ratio_at_self_lt_31 with G_ratio_eventually_large; r_ref_exact_pos and r_ref_exact_gt_r establish the two inequalities on the closed-form r_ref_exact; rung_near_sync_period records the numerical offset 4.
proof idea
The proof is a term-mode construction of the RunningGR4Cert structure. It supplies the four fields directly: r_ref_explicit is instantiated by r_ref_exact_pos, r_ref_above_r by r_ref_exact_gt_r, rung_near_360 by rung_near_sync_period, and hypothesis_exists by H_GravitationalRunning_certificate. No further rewriting or case analysis occurs.
why it matters
This declaration closes the Round-4 certificate for the running-G prediction inside the Recognition framework. It confirms that the phi-ladder-derived beta produces a consistent reference scale near the 360-unit sync period (T7) and that the 20 nm enhancement hypothesis is satisfiable. The certificate is the concrete object that would be invoked by any downstream model that needs the nanoscale G correction to be formally licensed rather than postulated. No open scaffolding remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.