Gravity Running G Rung Near Sync Period

The near-sync arithmetic

The declaration rung_near_sync_period is a proved statement in the framework's machine-checked library of formal theorems. It says that a certain natural number, called r_ref_phi_rung_approx and set to 364, differs from 360 by exactly 4. In other words, 364 minus 360 equals 4. The proof is a direct computation: the Lean kernel evaluates both sides and finds them equal. This is a theorem in the strict sense, meaning it is axiom-clean and machine-verified.

The number 360 is not arbitrary in this context. It is the same 360 that appears in the framework's eight-tick recognition cycle, where a full cycle is divided into 8 ticks of 45 units each. The theorem sync_period_factored proves this factorization: 360 = 8 * 45. The near-sync statement then connects this cycle count to the rung approximation 364, a number that arises from the framework's phi-ladder scaling. The difference of 4 is what makes the relationship "near" sync rather than exact.

What the declaration does not claim is far more important than what it proves. It does not establish that gravity actually runs or strengthens at nanometer scales. That is a separate hypothesis, formalized as H_GravitationalRunning, which merely asserts the existence of a positive reference scale r_ref. The certificate H_GravitationalRunning_certificate proves this hypothesis is satisfiable by choosing r_ref = 20e-9, but that is a consistency check, not an empirical confirmation. The near-sync theorem also does not claim that 364 is the exact or unique rung number; it only states a difference of 4 from 360 for the specific approximation defined in the library.

In plain terms, this declaration is a small piece of internal bookkeeping. It shows that a number derived from the phi-ladder sits close to the framework's cycle count. The gap of 4 is a fact about arithmetic, not a fact about nature. The framework's larger claim, that G(r) strengthens to about 32 times its large-scale value at roughly 20 nanometers, remains a prediction with a named falsifier: a precise measurement of G at that scale that does not show the enhancement. The near-sync theorem neither supports nor undermines that prediction; it simply records a numerical proximity.

/-- 364 is close to 360 = lcm(8, 45) = the RS sync period. -/
theorem rung_near_sync_period : r_ref_phi_rung_approx - 360 = 4 := by
  native_decide

/-- The approximate phi-rung of r_ref for the 20nm/32x prediction. -/
def r_ref_phi_rung_approx : ℕ := 364

/-- 364 is close to 360 = lcm(8, 45) = the RS sync period. -/
theorem rung_near_sync_period : r_ref_phi_rung_approx - 360 = 4 := by
  native_decide

/-- 360 = 8 * 45 (8-tick times gap-45). -/
theorem sync_period_factored : 360 = 8 * 45 := by norm_num

/-- **HYPOTHESIS H_GravitationalRunning**: Gravity strengthens at nm scales.
    Prediction: G(20nm) / G_inf ≈ 32. -/
def H_GravitationalRunning : Prop :=
  ∃ r_ref : ℝ, r_ref > 0

What this page does not claim

The declaration does not prove that gravity runs at nanometer scales. The declaration does not claim that 364 is the exact or unique rung number. The declaration does not provide any empirical evidence for the gravitational running hypothesis.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/RunningG.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: