rung_near_sync_period
plain-language theorem explainer
The theorem establishes that the approximate phi-rung for the reference scale in the gravitational running model sits exactly four units above the 360-unit RS synchronization period. Researchers modeling nanoscale G enhancement would cite the alignment to anchor the 20 nm / 32x prediction. The proof is a direct native computation of the pre-defined constant difference.
Claim. Let $r_{ref, phi, approx}$ be the approximate rung on the phi-ladder for the reference scale. Then $r_{ref, phi, approx} - 360 = 4$.
background
The RunningG module formalizes the claim that Newton's constant runs at nanometer scales, with $G_{eff}(r) = G_∞ (1 + |β| (r/r_{ref})^β)$ where $β ≈ -0.056$ follows from the phi-ladder. The reference rung is supplied by the constant 364, which is compared to the synchronization period 360 = lcm(8,45). The eight-tick octave comes from the fundamental time quantum tick = 1, while the gap factor 45 is the product of closure and Fibonacci factors in the Gap45 derivation.
proof idea
The proof is a one-line term that applies native_decide to evaluate the arithmetic difference between the pre-defined constant r_ref_phi_rung_approx = 364 and the synchronization period 360.
why it matters
This supplies the rung_near_360 field inside the RunningGR4Cert certificate that certifies the running-G prediction. It numerically closes the link between the phi-rung approximation and the eight-tick by gap-45 sync period that appears in the T7 octave and T8 dimension steps of the forcing chain. The result is used directly by running_g_r4_cert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.