Prove multiplicative floor-error budgets at arbitrary odd counts

.github/workflows/ci.yml

@@ -46,6 +46,8 @@ jobs:
           python3 scripts/audit_balanced_offset.py
           python3 scripts/audit_balanced_near_six.py
           python3 scripts/audit_coefficient_band.py
+          python3 scripts/audit_floor_affine_error.py
+          python3 scripts/audit_floor_product_error.py
           python3 scripts/audit_eleven_halves_clock.py
 
       - name: Check exact first-descent intervals

Collatz.lean

@@ -2118,3 +2118,6 @@ import Collatz.Exploration.BalancedOffset
 import Collatz.Exploration.BalancedCompact
 import Collatz.Exploration.BalancedNearSix
 import Collatz.Exploration.Band5995
+
+import Collatz.Exploration.AffineBandExit
+import Collatz.Exploration.FloorProductError

Collatz/Exploration/AffineBandExit.lean

@@ -0,0 +1,91 @@
+import Collatz.Exploration.FloorAffineError
+import Collatz.Exploration.TimeChange
+import Collatz.Structure.AffineBound
+
+/-! Necessary coefficient-spread conditions for two endpoints to remain in a band.
+These are conditional finite-prefix results, not universal exit certificates. -/
+namespace Collatz.Exploration.AffineBandExit
+open FloorAffineError
+
+/-- Eliminate the source between a low affine endpoint and a high endpoint. -/
+theorem spread_budget {D L E H n x y B b P Q g : Nat}
+    (hx : D*x = L*n+B) (hy : H*n ≤ E*y)
+    (hf : b ≤ x) (hu : Q*y ≤ P*b)
+    (hg : P*L*E+g ≤ Q*H*D) : g*b ≤ Q*H*B := by
+  have h1 := Nat.mul_le_mul_left (Q*H*D) hf
+  have h2 := Nat.mul_le_mul_left (Q*L) hy
+  have h3 := Nat.mul_le_mul_left (L*E) hu
+  have h4 := Nat.mul_le_mul_right b hg
+  have he := congrArg (fun z => Q*H*z) hx
+  simp only [Nat.mul_add, Nat.mul_left_comm, Nat.mul_comm] at h1 h2 h3 h4 he ⊢
+  omega
+
+/-- Survival plus a coefficient gap forces a floor-dependent budget inequality. -/
+theorem floor_spread_budget {n b a c B P Q g : Nat}
+    (hb : 0 < b)
+    (hf : ∀ i, i < a → b ≤ acceleratedOrbit i n)
+    (he : 2^a*acceleratedOrbit a n = 3^oddCount n a*n+B)
+    (hl : b ≤ acceleratedOrbit a n)
+    (hu : Q*acceleratedOrbit c n ≤ P*b)
+    (hn : Q*n ≤ P*b)
+    (hh : 3^oddCount n c*n ≤ 2^c*acceleratedOrbit c n)
+    (hg : P*3^oddCount n a*2^c+g ≤ Q*3^oddCount n c*2^a) :
+    g*(weight b-oddCount n a) ≤
+      P*3^oddCount n c*oddCount n a*3^oddCount n a := by
+  have hs := spread_budget he hh hl hu hg
+  have hp := survival_offset_paid hf he
+  have h1 := Nat.mul_le_mul_right (weight b-oddCount n a) hs
+  have h2 := Nat.mul_le_mul_left (Q*3^oddCount n c) hp
+  have h3 := Nat.mul_le_mul_left
+    (3^oddCount n c*oddCount n a*3^oddCount n a) hn
+  simp only [Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm] at h1 h2 h3
+  have hbound :
+      (g*(weight b-oddCount n a))*b ≤
+      (P*3^oddCount n c*oddCount n a*3^oddCount n a)*b := by
+    simp only [Nat.mul_left_comm, Nat.mul_comm]
+    omega
+  exact Nat.le_of_mul_le_mul_right hbound hb
+
+/-- A strict failure of the budget produces an actual accelerated band exit. -/
+theorem accelerated_exit {n b a c P Q g : Nat}
+    (hb : 0 < b) (hn : Q*n ≤ P*b)
+    (hg : P*3^oddCount n a*2^c+g ≤ Q*3^oddCount n c*2^a)
+    (hstrict : P*3^oddCount n c*oddCount n a*3^oddCount n a <
+      g*(weight b-oddCount n a)) :
+    ∃ i, i ≤ max a c ∧
+      (acceleratedOrbit i n < b ∨ P*b < Q*acceleratedOrbit i n) := by
+  by_cases hf : ∀ i, i ≤ a → b ≤ acceleratedOrbit i n
+  · by_cases hu : Q*acceleratedOrbit c n ≤ P*b
+    · obtain ⟨B,he,_⟩ := AffineBound.exists_affine_bounded n a
+      obtain ⟨B',he',_⟩ := AffineBound.exists_affine_bounded n c
+      have hh : 3^oddCount n c*n ≤ 2^c*acceleratedOrbit c n := by omega
+      have hz := floor_spread_budget hb (fun i hi => hf i (by omega)) he
+        (hf a (by omega)) hu hn hh hg
+      omega
+    · exact ⟨c, Nat.le_max_right a c, Or.inr (by omega)⟩
+  · have hex : ∃ i, i ≤ a ∧ acceleratedOrbit i n < b := by
+      apply Classical.byContradiction
+      intro hno
+      apply hf
+      intro i hi
+      by_cases hlo : b ≤ acceleratedOrbit i n
+      · exact hlo
+      · exact False.elim (hno ⟨i,hi,by omega⟩)
+    obtain ⟨i,hi,hlo⟩ := hex
+    exact ⟨i,Nat.le_trans hi (Nat.le_max_left a c),Or.inl hlo⟩
+
+/-- The exit occurs within twice the accelerated horizon in the standard orbit. -/
+theorem standard_exit {n b a c P Q g : Nat}
+    (hb : 0 < b) (hn : Q*n ≤ P*b)
+    (hg : P*3^oddCount n a*2^c+g ≤ Q*3^oddCount n c*2^a)
+    (hstrict : P*3^oddCount n c*oddCount n a*3^oddCount n a <
+      g*(weight b-oddCount n a)) :
+    ∃ t, t ≤ 2*max a c ∧ (orbit t n < b ∨ P*b < Q*orbit t n) := by
+  obtain ⟨i,hi,he⟩ := accelerated_exit hb hn hg hstrict
+  refine ⟨TimeChange.clock n i,?_,?_⟩
+  · have ht := (TimeChange.clock_bounds n i).2
+    omega
+  · rw [TimeChange.orbit_at_clock]
+    exact he
+
+end Collatz.Exploration.AffineBandExit

Collatz/Exploration/FloorAffineError.lean

@@ -0,0 +1,124 @@
+import Collatz.Exploration.CoefficientBand
+
+/-! Affine-error control from lower survival, without a heavy-coefficient
+hypothesis. All floor assumptions refer to an explicitly finite prefix. -/
+namespace Collatz.Exploration.FloorAffineError
+open CoefficientBand
+
+/-- The least odd natural number at least b. Only odd states inject affine error. -/
+def oddCeil (b : Nat) : Nat := if b%2=0 then b+1 else b
+
+def weight (b : Nat) : Nat := 3*oddCeil b+1
+
+theorem oddCeil_ge (b : Nat) : b ≤ oddCeil b := by unfold oddCeil; split <;> omega
+
+theorem oddCeil_odd (b : Nat) : oddCeil b%2=1 := by unfold oddCeil; split <;> omega
+
+theorem oddCeil_le_of_odd {b x : Nat} (hx : x%2=1) (hb : b ≤ x) : oddCeil b ≤ x := by
+  unfold oddCeil
+  split <;> omega
+
+/-- The odd affine update preserves an error budget paid by the orbit floor. -/
+theorem odd_error_update {b j B D T : Nat} (hB : (3*b+1)*B ≤ j*T) (hD : b*D ≤ T) :
+    (3*b+1)*(3*B+D) ≤ (j+1)*(3*T+D) := by
+  have h3 := Nat.mul_le_mul_left 3 hB
+  have hd3 := Nat.mul_le_mul_left 3 hD
+  simp only [Nat.mul_add, Nat.add_mul, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm] at h3 hd3 ⊢
+  omega
+
+/-- Lower survival controls the affine constant relative to the actual endpoint.
+No coefficient is assumed heavy, and the endpoint itself need not survive. -/
+theorem survival_affine_bound (n b j : Nat)
+    (hfloor : ∀ i, i < j → b ≤ acceleratedOrbit i n) :
+    ∃ B : Nat, 2^j*acceleratedOrbit j n = 3^oddCount n j*n+B ∧
+      weight b*B ≤ oddCount n j*(3^oddCount n j*n+B) := by
+  induction j with
+  | zero => refine ⟨0,by simp,by simp⟩
+  | succ j ih =>
+    obtain ⟨B,heq,hB⟩ := ih (fun i hi => hfloor i (by omega))
+    rcases Arith.mod_two_eq_zero_or_one (acceleratedOrbit j n) with he | ho
+    · refine ⟨B,?_,?_⟩
+      · rw [acceleratedOrbit_succ_step, Density.oddCount_succ_last, he, Nat.add_zero, Nat.pow_succ]
+        have hx : 2*acceleratedStep (acceleratedOrbit j n) = acceleratedOrbit j n := by
+          simp only [acceleratedStep, he, ↓reduceIte]
+          omega
+        rw [Nat.mul_assoc, hx]
+        exact heq
+      · rw [Density.oddCount_succ_last, he, Nat.add_zero]
+        exact hB
+    · refine ⟨3*B+2^j,?_,?_⟩
+      · rw [acceleratedOrbit_succ_step, Density.oddCount_succ_last, ho, Nat.pow_succ, Nat.pow_succ]
+        have hx : 2*acceleratedStep (acceleratedOrbit j n) = 3*acceleratedOrbit j n+1 := by
+          simp only [acceleratedStep, show acceleratedOrbit j n%2 ≠ 0 by omega, ↓reduceIte]
+          omega
+        rw [Nat.mul_assoc, hx, Nat.mul_add, Nat.mul_one]
+        have hh : 2^j*(3*acceleratedOrbit j n) = 3*(2^j*acceleratedOrbit j n) := by ac_rfl
+        rw [hh, heq, Nat.mul_add]
+        ac_rfl
+      · have hlo := Nat.mul_le_mul_left (2^j)
+          (oddCeil_le_of_odd ho (hfloor j (by omega)))
+        rw [heq] at hlo
+        have hD : oddCeil b*2^j ≤ 3^oddCount n j*n+B := by simpa only [Nat.mul_comm] using hlo
+        have hu := odd_error_update (b := oddCeil b) hB hD
+        rw [Density.oddCount_succ_last, ho, Nat.pow_succ]
+        have ht : (3^oddCount n j*3)*n+(3*B+2^j) = 3*(3^oddCount n j*n+B)+2^j := by
+          rw [Nat.mul_add]
+          ac_rfl
+        rw [ht]
+        exact hu
+
+/-- The same floor budget holds for any exact affine constant at that time. -/
+theorem survival_offset_budget {n b j B : Nat}
+    (hfloor : ∀ i, i < j → b ≤ acceleratedOrbit i n)
+    (heq : 2^j*acceleratedOrbit j n = 3^oddCount n j*n+B) :
+    weight b*B ≤ oddCount n j*(3^oddCount n j*n+B) := by
+  obtain ⟨B',heq',hb⟩ := survival_affine_bound n b j hfloor
+  have : B = B' := by omega
+  subst B'
+  exact hb
+
+/-- The paid offset bound is useful when the odd-step count is below the floor weight. -/
+theorem survival_offset_paid {n b j B : Nat}
+    (hfloor : ∀ i, i < j → b ≤ acceleratedOrbit i n)
+    (heq : 2^j*acceleratedOrbit j n = 3^oddCount n j*n+B) :
+    (weight b-oddCount n j)*B ≤ oddCount n j*3^oddCount n j*n := by
+  have hb := survival_offset_budget hfloor heq
+  rw [Nat.sub_mul]
+  simp only [Nat.mul_add, Nat.mul_assoc] at hb ⊢
+  omega
+
+/-- No larger uniform floor weight is possible: the first odd step at oddCeil b is sharp. -/
+theorem weight_optimal (b F : Nat)
+    (h : ∀ n j B : Nat, (∀ i, i < j → b ≤ acceleratedOrbit i n) →
+      2^j*acceleratedOrbit j n = 3^oddCount n j*n+B →
+      F*B ≤ oddCount n j*(3^oddCount n j*n+B)) : F ≤ weight b := by
+  let n := oddCeil b
+  have ho : n%2=1 := oddCeil_odd b
+  have hc : oddCount n 1 = 1 := by
+    simpa using Congruence.oddCount_succ_of_odd ho 0
+  have hf : ∀ i, i < 1 → b ≤ acceleratedOrbit i n := by
+    intro i hi
+    have : i=0 := by omega
+    subst i
+    exact oddCeil_ge b
+  have he : 2^1*acceleratedOrbit 1 n = 3^oddCount n 1*n+1 := by
+    rw [hc]
+    change 2*acceleratedStep n = 3*n+1
+    simp only [acceleratedStep, show n%2 ≠ 0 by omega, ↓reduceIte]
+    omega
+  have hh := h n 1 1 hf he
+  rw [hc] at hh
+  simpa only [Nat.pow_one, Nat.one_mul, Nat.mul_one, weight, n] using hh
+
+/-- Exact classification of all valid uniform weights for this finite floor budget. -/
+theorem uniform_weight_iff (b F : Nat) :
+    (∀ n j B : Nat, (∀ i, i < j → b ≤ acceleratedOrbit i n) →
+      2^j*acceleratedOrbit j n = 3^oddCount n j*n+B →
+      F*B ≤ oddCount n j*(3^oddCount n j*n+B)) ↔ F ≤ weight b := by
+  constructor
+  · exact weight_optimal b F
+  · intro hF n j B hf he
+    have hm := Nat.mul_le_mul_right B hF
+    exact Nat.le_trans hm (survival_offset_budget hf he)
+
+end Collatz.Exploration.FloorAffineError

Collatz/Exploration/FloorProductError.lean

@@ -0,0 +1,121 @@
+import Collatz.Exploration.FloorAffineError
+import Collatz.Structure.AffineBound
+import Collatz.Exploration.TimeChange
+
+/-! Multiplicative floor control keeps the error budget nontrivial at all odd counts. -/
+namespace Collatz.Exploration.FloorProductError
+open FloorAffineError
+
+def base (b : Nat) : Nat := 3*oddCeil b
+
+/-- Each odd state contributes a factor bounded by the least admissible odd state. -/
+theorem odd_factor {b x : Nat} (ho : x%2=1) (hf : b ≤ x) :
+    base b*(3*x+1) ≤ 3*weight b*x := by
+  have h := oddCeil_le_of_odd ho hf
+  unfold base weight
+  simp only [Nat.mul_add, Nat.add_mul, Nat.mul_one]
+  have he : 3*oddCeil b*(3*x) = 3*(3*oddCeil b)*x := by ac_rfl
+  rw [he]
+  omega
+
+/-- Product error control from a finite lower floor, with no restriction on odd count. -/
+theorem survival_product (n b j : Nat)
+    (hf : ∀ i, i < j → b ≤ acceleratedOrbit i n) :
+    base b^oddCount n j*(2^j*acceleratedOrbit j n) ≤
+      weight b^oddCount n j*(3^oddCount n j*n) := by
+  induction j with
+  | zero => simp
+  | succ j ih =>
+    have hp := ih (fun i hi => hf i (by omega))
+    rcases Arith.mod_two_eq_zero_or_one (acceleratedOrbit j n) with he | ho
+    · rw [acceleratedOrbit_succ_step, Density.oddCount_succ_last, he, Nat.add_zero, Nat.pow_succ]
+      have hx : 2*acceleratedStep (acceleratedOrbit j n) = acceleratedOrbit j n := by
+        simp only [acceleratedStep,he,↓reduceIte]
+        omega
+      rw [Nat.mul_assoc (2^j),hx]
+      exact hp
+    · have hl := odd_factor ho (hf j (by omega))
+      have hm := Nat.mul_le_mul_left (base b^oddCount n j*2^j) hl
+      have hh := Nat.mul_le_mul_left (3*weight b) hp
+      rw [acceleratedOrbit_succ_step, Density.oddCount_succ_last,ho,
+        Nat.pow_succ,Nat.pow_succ,Nat.pow_succ,Nat.pow_succ]
+      have hx : 2*acceleratedStep (acceleratedOrbit j n) = 3*acceleratedOrbit j n+1 := by
+        simp only [acceleratedStep,show acceleratedOrbit j n%2 ≠ 0 by omega,↓reduceIte]
+        omega
+      rw [Nat.mul_assoc (2^j),hx]
+      simp only [Nat.mul_assoc,Nat.mul_left_comm,Nat.mul_comm] at hm hh ⊢
+      exact Nat.le_trans hm hh
+
+/-- An exponential paid budget remains informative when the linear weight is exhausted. -/
+theorem offset_product {n b j B : Nat}
+    (hf : ∀ i, i < j → b ≤ acceleratedOrbit i n)
+    (he : 2^j*acceleratedOrbit j n = 3^oddCount n j*n+B) :
+    base b^oddCount n j*B ≤
+      (weight b^oddCount n j-base b^oddCount n j)*(3^oddCount n j*n) := by
+  have hp := survival_product n b j hf
+  rw [he,Nat.mul_add] at hp
+  rw [Nat.sub_mul]
+  omega
+
+/-- Source elimination with multiplicative error control; no initial upper bound is needed. -/
+theorem product_band_budget {n b a c P Q : Nat}
+    (hb : 0 < b)
+    (hf : ∀ i, i < a → b ≤ acceleratedOrbit i n)
+    (hl : b ≤ acceleratedOrbit a n)
+    (hu : Q*acceleratedOrbit c n ≤ P*b) :
+    Q*3^oddCount n c*2^a*base b^oddCount n a ≤
+      P*2^c*3^oddCount n a*weight b^oddCount n a := by
+  have hp := survival_product n b a hf
+  obtain ⟨B,he,_⟩ := AffineBound.exists_affine_bounded n c
+  have hh : 3^oddCount n c*n ≤ 2^c*acceleratedOrbit c n := by omega
+  have h1 := Nat.mul_le_mul_left (base b^oddCount n a*2^a) hl
+  have h2 := Nat.mul_le_mul_left (Q*3^oddCount n c) hp
+  have h3 := Nat.mul_le_mul_left (Q*weight b^oddCount n a*3^oddCount n a) hh
+  have h4 := Nat.mul_le_mul_left (weight b^oddCount n a*3^oddCount n a*2^c) hu
+  have h5 := Nat.mul_le_mul_left (Q*3^oddCount n c) h1
+  simp only [Nat.mul_assoc,Nat.mul_left_comm,Nat.mul_comm] at h2 h3 h4 h5
+  have hz :
+      (Q*3^oddCount n c*2^a*base b^oddCount n a)*b ≤
+      (P*2^c*3^oddCount n a*weight b^oddCount n a)*b := by
+    simp only [Nat.mul_assoc,Nat.mul_left_comm,Nat.mul_comm]
+    omega
+  exact Nat.le_of_mul_le_mul_right hz hb
+
+/-- Strict product spread forces a finite exit, at any odd-step count. -/
+theorem product_accelerated_exit {n b a c P Q : Nat}
+    (hb : 0 < b)
+    (hs : P*2^c*3^oddCount n a*weight b^oddCount n a <
+      Q*3^oddCount n c*2^a*base b^oddCount n a) :
+    ∃ i, i ≤ max a c ∧
+      (acceleratedOrbit i n < b ∨ P*b < Q*acceleratedOrbit i n) := by
+  by_cases hf : ∀ i, i ≤ a → b ≤ acceleratedOrbit i n
+  · by_cases hu : Q*acceleratedOrbit c n ≤ P*b
+    · have hh := product_band_budget hb (fun i hi => hf i (by omega))
+        (hf a (by omega)) hu
+      omega
+    · exact ⟨c,Nat.le_max_right a c,Or.inr (by omega)⟩
+  · have hex : ∃ i, i ≤ a ∧ acceleratedOrbit i n < b := by
+      apply Classical.byContradiction
+      intro hno
+      apply hf
+      intro i hi
+      by_cases hlo : b ≤ acceleratedOrbit i n
+      · exact hlo
+      · exact False.elim (hno ⟨i,hi,by omega⟩)
+    obtain ⟨i,hi,hlo⟩ := hex
+    exact ⟨i,Nat.le_trans hi (Nat.le_max_left a c),Or.inl hlo⟩
+
+/-- The product-certified exit has an explicit ordinary-step horizon. -/
+theorem product_standard_exit {n b a c P Q : Nat}
+    (hb : 0 < b)
+    (hs : P*2^c*3^oddCount n a*weight b^oddCount n a <
+      Q*3^oddCount n c*2^a*base b^oddCount n a) :
+    ∃ t, t ≤ 2*max a c ∧ (orbit t n < b ∨ P*b < Q*orbit t n) := by
+  obtain ⟨i,hi,he⟩ := product_accelerated_exit hb hs
+  refine ⟨TimeChange.clock n i,?_,?_⟩
+  · have ht := (TimeChange.clock_bounds n i).2
+    omega
+  · rw [TimeChange.orbit_at_clock]
+    exact he
+
+end Collatz.Exploration.FloorProductError