sync_period_factored
plain-language theorem explainer
The arithmetic identity 360 = 8 × 45 anchors the reference length scale r_ref in the running gravitational constant model to the eight-tick period of the D=3 forcing chain. Nanoscale gravity researchers would invoke this to eliminate free parameters from the beta exponent in G_eff(r). The proof reduces to a single norm_num tactic that verifies the multiplication directly.
Claim. $360 = 8 × 45$, where the factor of 8 is the tick count from the D=3 forcing chain and 45 is the gap parameter on the phi-ladder for the reference scale ell0 · phi^360.
background
The module formalizes running of Newton's G at nanometer scales via G_eff(r) = G_∞ (1 + |β| (r / r_ref)^β) with β = -(phi - 1)/phi^5. The reference scale is tied to ell0 (the fundamental voxel length, defined as c · tau0 with tau0^2 = hbar G / (pi c^5)) multiplied by phi raised to the sync exponent. Upstream results supply the period definition as phi^k, rung assignments that label discrete phi-tiers, and the ell0 derivation from Constants.Derivation.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to confirm the integer equality 360 = 8 * 45.
why it matters
This supplies the numerical factorization that links the sync period to the 360 exponent in r_ref, closing an arithmetic step required by the gravitational running prediction. It directly instantiates the eight-tick octave (T7) from the unified forcing chain and the D=3 spatial dimension. No downstream theorems are recorded, but the identity supports the beta_running family and the zero-parameter claim for r_ref modulo the 4-rung offset.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.