rung_offset

formal source

 301theorem N_tau_conjecture_eq_142 : N_tau_conjecture = 142 := by native_decide
 302
 303/-- The 16-rung offset is 2^4 = 4² (second non-trivial perfect square). -/
 304def rung_offset : ℕ := 16
 305
 306theorem rung_offset_is_power_of_2 : rung_offset = 2 ^ 4 := by native_decide
 307
 308theorem rung_offset_is_perfect_square : rung_offset = 4 ^ 2 := by native_decide
 309
 310theorem rung_offset_is_two_8tick_cycles : rung_offset = 2 * 8 := by native_decide
 311
 312/-- The conjectured galactic radius rung.
 313    N_r = N_τ - 16 = 142 - 16 = 126 -/
 314def N_r_conjecture : ℕ := N_tau_conjecture - rung_offset
 315
 316theorem N_r_conjecture_eq_126 : N_r_conjecture = 126 := by native_decide
 317
 318/-- If the conjecture is correct, N_r = N_τ - 16 exactly. -/
 319theorem rung_relationship : N_r_conjecture = N_tau_conjecture - rung_offset := rfl
 320
 321/-! ## Summary
 322
 323| Parameter | RS Formula | Status |
 324|-----------|------------|--------|
 325| α = 1 - 1/φ ≈ 0.382 | **DERIVED** (algebraic) |
 326| Υ★ = φ ≈ 1.618 | **DERIVED** (MassToLight.lean) |
 327| C_ξ = 2φ⁻⁴ ≈ 0.292 | **HAS RS BASIS** (numerical match 2%) |
 328| p = 1 - αLock/4 ≈ 0.952 | **HAS RS BASIS** (numerical match 0.2%) |
 329| A = 1 + αLock/2 ≈ 1.096 | **HAS RS BASIS** (numerical match 3%) |
 330| a₀, r₀ | **LINKED** via τ★ constraint |
 331| N_τ = F_12 - 2 | **CONJECTURED** (Fibonacci-square) |
 332
 333If the Fibonacci-square conjecture is correct, this model has ZERO phenomenological
 334parameters — all seven are derived from φ plus the Fibonacci-square selection. -/