From 2e5d972ae34de6c9cfbf2214d5343e19a23a6554 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 7 Oct 2026 15:43:37 +0530 Subject: [PATCH 1/5] Prove optimal finite-floor affine error weights and coefficient spread budget --- .github/workflows/ci.yml | 1 + Collatz.lean | 2 + Collatz/Exploration/AffineBandExit.lean | 47 ++++++++ Collatz/Exploration/FloorAffineError.lean | 124 ++++++++++++++++++++++ README.md | 21 ++++ RESEARCH.md | 21 ++++ scripts/audit_floor_affine_error.py | 27 +++++ scripts/test_floor_affine_error.py | 51 +++++++++ 8 files changed, 294 insertions(+) create mode 100644 Collatz/Exploration/AffineBandExit.lean create mode 100644 Collatz/Exploration/FloorAffineError.lean create mode 100644 scripts/audit_floor_affine_error.py create mode 100644 scripts/test_floor_affine_error.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1d493905..6d6a48a7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -46,6 +46,7 @@ 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_eleven_halves_clock.py - name: Check exact first-descent intervals diff --git a/Collatz.lean b/Collatz.lean index 0a64b744..565d3d2d 100644 --- a/Collatz.lean +++ b/Collatz.lean @@ -2118,3 +2118,5 @@ import Collatz.Exploration.BalancedOffset import Collatz.Exploration.BalancedCompact import Collatz.Exploration.BalancedNearSix import Collatz.Exploration.Band5995 + +import Collatz.Exploration.AffineBandExit diff --git a/Collatz/Exploration/AffineBandExit.lean b/Collatz/Exploration/AffineBandExit.lean new file mode 100644 index 00000000..9018637d --- /dev/null +++ b/Collatz/Exploration/AffineBandExit.lean @@ -0,0 +1,47 @@ +import Collatz.Exploration.FloorAffineError + +/-! 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 + +end Collatz.Exploration.AffineBandExit diff --git a/Collatz/Exploration/FloorAffineError.lean b/Collatz/Exploration/FloorAffineError.lean new file mode 100644 index 00000000..c5d538d6 --- /dev/null +++ b/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 diff --git a/README.md b/README.md index cb91734f..a38e71ca 100644 --- a/README.md +++ b/README.md @@ -87,3 +87,24 @@ own verification instructions. Conditional theorems keep their hypotheses explicit. Finite computations and almost-everywhere results do not prove convergence for every positive input. + +### Sharp finite-floor affine error budget + +`FloorAffineError.lean` proves that if accelerated states before time j stay +above b, then their exact affine offset B satisfies +`w B ≤ a (3^a n + B)` and `(w-a) B ≤ a 3^a n`, where a is the +number of odd steps and w = 3 times the least odd integer at least b, plus 1. +Natural subtraction is used in the second inequality. The endpoint need not +stay above b. The first odd step at that least odd integer proves w is the +largest valid uniform weight; this classification is formalized in Lean. + +`AffineBandExit.lean` eliminates a common source between two affine endpoints. +A positive coefficient gap g, finite lower survival, and upper-band assumptions +imply `g (w-a) ≤ P H a L` (L and H are the two powers of 3). +A strict violation therefore rules out those joint survival assumptions. +This is conditional: no universal coverage of coefficient gaps or Collatz +convergence is established. Mathematical priority has not been assessed. + +Validation: `python3 scripts/audit_floor_affine_error.py` checks 11 theorem +axiom footprints, 576,960 floor budgets, 25,699 endpoint exits, 2,001 sharpness +controls, 84,817 source-elimination cases, and rejects three false statements. diff --git a/RESEARCH.md b/RESEARCH.md index 5d1e7313..1323a144 100644 --- a/RESEARCH.md +++ b/RESEARCH.md @@ -15906,3 +15906,24 @@ Classical.choice and Quot.sound. The full library build completed 4524 jobs and repository integrity passed. Historical source hashes match all 1000 separate certificate commits. These verify the partial results and their provenance; they do not discharge ResidualCoverage. + +### Sharp finite-floor affine error budget + +`FloorAffineError.lean` proves that if accelerated states before time j stay +above b, then their exact affine offset B satisfies +`w B ≤ a (3^a n + B)` and `(w-a) B ≤ a 3^a n`, where a is the +number of odd steps and w = 3 times the least odd integer at least b, plus 1. +Natural subtraction is used in the second inequality. The endpoint need not +stay above b. The first odd step at that least odd integer proves w is the +largest valid uniform weight; this classification is formalized in Lean. + +`AffineBandExit.lean` eliminates a common source between two affine endpoints. +A positive coefficient gap g, finite lower survival, and upper-band assumptions +imply `g (w-a) ≤ P H a L` (L and H are the two powers of 3). +A strict violation therefore rules out those joint survival assumptions. +This is conditional: no universal coverage of coefficient gaps or Collatz +convergence is established. Mathematical priority has not been assessed. + +Validation: `python3 scripts/audit_floor_affine_error.py` checks 11 theorem +axiom footprints, 576,960 floor budgets, 25,699 endpoint exits, 2,001 sharpness +controls, 84,817 source-elimination cases, and rejects three false statements. diff --git a/scripts/audit_floor_affine_error.py b/scripts/audit_floor_affine_error.py new file mode 100644 index 00000000..0f76258b --- /dev/null +++ b/scripts/audit_floor_affine_error.py @@ -0,0 +1,27 @@ +#!/usr/bin/env python3 +"""Kernel build, theorem footprints, seed reproduction, and false-transfer controls.""" +import subprocess +from audit_barrier_kernel import ROOT,check_axioms,check_false_certificates +from check_proof_escapes import violations + +NAMES=['FloorAffineError','AffineBandExit'] +PREFIX='Collatz.Exploration.' + + +def main(): + for name in NAMES: + assert not violations((ROOT/f'Collatz/Exploration/{name}.lean').read_text()) + subprocess.run(['lake','build',PREFIX+'AffineBandExit'],cwd=ROOT,check=True) + subprocess.run(['python3',str(ROOT/'scripts/test_floor_affine_error.py')],cwd=ROOT,check=True) + count=sum(check_axioms(ROOT/f'Collatz/Exploration/{name}.lean',PREFIX+name) for name in NAMES) + bad=[ + 'example : Collatz.Exploration.FloorAffineError.weight 2 = 7 := by decide\n', + 'example : 11*1 ≤ 1*(3*3+1) := by decide\n', + 'example : Collatz.Exploration.FloorAffineError.oddCeil 0 = 0 := by decide\n', + ] + rejected=check_false_certificates(PREFIX+'AffineBandExit',bad) + print(f'{count} theorem axiom footprints checked; {rejected} false claims rejected') + + +if __name__=='__main__': + main() diff --git a/scripts/test_floor_affine_error.py b/scripts/test_floor_affine_error.py new file mode 100644 index 00000000..e2043f95 --- /dev/null +++ b/scripts/test_floor_affine_error.py @@ -0,0 +1,51 @@ +#!/usr/bin/env python3 +"""Independent recurrence tests, including sharp constants and endpoint exits.""" + +def main(): + checked = exited = 0 + for n in range(1, 2001): + x, C, D, B, odds, floor = n, 1, 1, 0, 0, n + for j in range(1, 101): + floor = min(floor, x) + if x % 2: + x = (3*x+1)//2 + B = 3*B+D + C *= 3 + odds += 1 + else: + x //= 2 + D *= 2 + assert D*x == C*n+B + for b in {0, 1, floor//2, floor}: + odd_ceiling = b+1 if b % 2 == 0 else b + w = 3*odd_ceiling+1 + assert w*B <= odds*(C*n+B) + assert max(w-odds, 0)*B <= odds*C*n + checked += 1 + exited += x < floor + for b in range(2001): + n = b+1 if b % 2 == 0 else b + w = 3*n+1 + assert w == 2*((3*n+1)//2) + assert w+1 > 3*n+1 # Any larger uniform weight fails at this first step. + # Exhaust the source-elimination lemma, including zero coefficients. + spread = 0 + for n in range(6): + for D in range(1, 5): + for L in range(5): + for x in range(8): + B = D*x-L*n + if B < 0: continue + for H in range(5): + for E in range(1, 4): + y = (H*n+E-1)//E + for b in range(x+1): + for P in range(5): + Q = 2 + g = Q*H*D-P*L*E + if g >= 0 and Q*y <= P*b: + assert g*b <= Q*H*B + spread += 1 + print(f'{checked} floor budgets; {exited} endpoint exits; 2001 sharpness controls; {spread} spread cases') + +if __name__ == '__main__': main() From ceffe5a529fdc97247eea80906b44192b9c3481f Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 7 Oct 2026 15:45:28 +0530 Subject: [PATCH 2/5] Derive explicit accelerated and standard exits from the floor spread criterion --- Collatz/Exploration/AffineBandExit.lean | 44 +++++++++++++++++++++++++ README.md | 4 +++ RESEARCH.md | 4 +++ scripts/test_floor_affine_error.py | 20 +++++++++++ 4 files changed, 72 insertions(+) diff --git a/Collatz/Exploration/AffineBandExit.lean b/Collatz/Exploration/AffineBandExit.lean index 9018637d..79e59163 100644 --- a/Collatz/Exploration/AffineBandExit.lean +++ b/Collatz/Exploration/AffineBandExit.lean @@ -1,4 +1,6 @@ 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. -/ @@ -44,4 +46,46 @@ theorem floor_spread_budget {n b a c B P Q g : Nat} 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 diff --git a/README.md b/README.md index a38e71ca..5485aa86 100644 --- a/README.md +++ b/README.md @@ -108,3 +108,7 @@ convergence is established. Mathematical priority has not been assessed. Validation: `python3 scripts/audit_floor_affine_error.py` checks 11 theorem axiom footprints, 576,960 floor budgets, 25,699 endpoint exits, 2,001 sharpness controls, 84,817 source-elimination cases, and rejects three false statements. + +The coefficient-gap criterion now formally produces a band exit within twice +the accelerated horizon in the ordinary orbit (`standard_exit`). Universal +coverage remains unproved. The audit includes both exit theorems (13 total). diff --git a/RESEARCH.md b/RESEARCH.md index 1323a144..57ff96d9 100644 --- a/RESEARCH.md +++ b/RESEARCH.md @@ -15927,3 +15927,7 @@ convergence is established. Mathematical priority has not been assessed. Validation: `python3 scripts/audit_floor_affine_error.py` checks 11 theorem axiom footprints, 576,960 floor budgets, 25,699 endpoint exits, 2,001 sharpness controls, 84,817 source-elimination cases, and rejects three false statements. + +The coefficient-gap criterion now formally produces a band exit within twice +the accelerated horizon in the ordinary orbit (`standard_exit`). Universal +coverage remains unproved. The audit includes both exit theorems (13 total). diff --git a/scripts/test_floor_affine_error.py b/scripts/test_floor_affine_error.py index e2043f95..6c7e4943 100644 --- a/scripts/test_floor_affine_error.py +++ b/scripts/test_floor_affine_error.py @@ -46,6 +46,26 @@ def main(): if g >= 0 and Q*y <= P*b: assert g*b <= Q*H*B spread += 1 + exits = 0 + for n in range(1, 301): + states, coeffs, counts = [n], [1], [0] + for j in range(30): + x = states[-1] + odd = x % 2 + states.append((3*x+1)//2 if odd else x//2) + coeffs.append(coeffs[-1]*(3 if odd else 1)) + counts.append(counts[-1]+odd) + for b in {1, max(1, n//6), n}: + if n > 6*b: continue + w = 3*(b+1 if b % 2 == 0 else b)+1 + for a in range(1, 30): + for c in range(1, 30): + g = coeffs[c]*2**a-6*coeffs[a]*2**c + if g > 0 and 6*coeffs[c]*counts[a]*coeffs[a] < g*max(w-counts[a], 0): + assert any(x < b or 6*b < x for x in states[:max(a,c)+1]) + exits += 1 + assert exits > 0 + print(f'{exits} nonvacuous conditional exit instances') print(f'{checked} floor budgets; {exited} endpoint exits; 2001 sharpness controls; {spread} spread cases') if __name__ == '__main__': main() From 88b3cb73aaeb19c52e2743f4ad72992ef56135c3 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 7 Oct 2026 15:47:38 +0530 Subject: [PATCH 3/5] Prove multiplicative finite-floor error bounds beyond the linear budget --- .github/workflows/ci.yml | 1 + Collatz.lean | 1 + Collatz/Exploration/FloorProductError.lean | 58 ++++++++++++++++++++++ README.md | 13 +++++ RESEARCH.md | 13 +++++ scripts/audit_floor_product_error.py | 20 ++++++++ scripts/test_floor_product_error.py | 35 +++++++++++++ 7 files changed, 141 insertions(+) create mode 100644 Collatz/Exploration/FloorProductError.lean create mode 100644 scripts/audit_floor_product_error.py create mode 100644 scripts/test_floor_product_error.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6d6a48a7..7f191fa1 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -47,6 +47,7 @@ jobs: 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 diff --git a/Collatz.lean b/Collatz.lean index 565d3d2d..1313eef1 100644 --- a/Collatz.lean +++ b/Collatz.lean @@ -2120,3 +2120,4 @@ import Collatz.Exploration.BalancedNearSix import Collatz.Exploration.Band5995 import Collatz.Exploration.AffineBandExit +import Collatz.Exploration.FloorProductError diff --git a/Collatz/Exploration/FloorProductError.lean b/Collatz/Exploration/FloorProductError.lean new file mode 100644 index 00000000..d1cccab3 --- /dev/null +++ b/Collatz/Exploration/FloorProductError.lean @@ -0,0 +1,58 @@ +import Collatz.Exploration.FloorAffineError + +/-! 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 + +end Collatz.Exploration.FloorProductError diff --git a/README.md b/README.md index 5485aa86..92f7fe6a 100644 --- a/README.md +++ b/README.md @@ -112,3 +112,16 @@ controls, 84,817 source-elimination cases, and rejects three false statements. The coefficient-gap criterion now formally produces a band exit within twice the accelerated horizon in the ordinary orbit (`standard_exit`). Universal coverage remains unproved. The audit includes both exit theorems (13 total). + +### Multiplicative floor-error budget + +`FloorProductError.lean` proves `v^a (3^a n+B) ≤ w^a 3^a n` +and consequently `v^a B ≤ (w^a-v^a)3^a n`, with v = 3 times the +least odd integer at least the finite prefix floor b, and w = v+1. +This follows by multiplying the one-step odd factors. Unlike the linear +paid bound, it remains informative when a reaches or exceeds w. +It assumes finite lower survival and proves neither universal descent nor +convergence. This elementary product method has not been assessed for priority. +The independent audit checks 278,684 products, including 192,568 cases +beyond the linear budget, 1,001 sharp factor controls, three Lean theorem +footprints, and two false statements rejected by the kernel. diff --git a/RESEARCH.md b/RESEARCH.md index 57ff96d9..7cf5b8cf 100644 --- a/RESEARCH.md +++ b/RESEARCH.md @@ -15931,3 +15931,16 @@ controls, 84,817 source-elimination cases, and rejects three false statements. The coefficient-gap criterion now formally produces a band exit within twice the accelerated horizon in the ordinary orbit (`standard_exit`). Universal coverage remains unproved. The audit includes both exit theorems (13 total). + +### Multiplicative floor-error budget + +`FloorProductError.lean` proves `v^a (3^a n+B) ≤ w^a 3^a n` +and consequently `v^a B ≤ (w^a-v^a)3^a n`, with v = 3 times the +least odd integer at least the finite prefix floor b, and w = v+1. +This follows by multiplying the one-step odd factors. Unlike the linear +paid bound, it remains informative when a reaches or exceeds w. +It assumes finite lower survival and proves neither universal descent nor +convergence. This elementary product method has not been assessed for priority. +The independent audit checks 278,684 products, including 192,568 cases +beyond the linear budget, 1,001 sharp factor controls, three Lean theorem +footprints, and two false statements rejected by the kernel. diff --git a/scripts/audit_floor_product_error.py b/scripts/audit_floor_product_error.py new file mode 100644 index 00000000..99cbd010 --- /dev/null +++ b/scripts/audit_floor_product_error.py @@ -0,0 +1,20 @@ +#!/usr/bin/env python3 +"""Kernel and numerical audit of the multiplicative floor-error bound.""" +import subprocess +from audit_barrier_kernel import ROOT, check_axioms, check_false_certificates +from check_proof_escapes import violations + +def main(): + name = 'Collatz.Exploration.FloorProductError' + source = ROOT/'Collatz/Exploration/FloorProductError.lean' + assert not violations(source.read_text()) + subprocess.run(['lake','build',name],cwd=ROOT,check=True) + subprocess.run(['python3',str(ROOT/'scripts/test_floor_product_error.py')],cwd=ROOT,check=True) + count = check_axioms(source,name) + rejected = check_false_certificates(name,[ + 'example : 4*10 ≤ 3*4*3 := by decide\n', + 'example : Collatz.Exploration.FloorProductError.base 2 = 6 := by decide\n', + ]) + print(f'{count} theorem footprints checked; {rejected} false claims rejected') + +if __name__ == '__main__': main() diff --git a/scripts/test_floor_product_error.py b/scripts/test_floor_product_error.py new file mode 100644 index 00000000..536723bf --- /dev/null +++ b/scripts/test_floor_product_error.py @@ -0,0 +1,35 @@ +#!/usr/bin/env python3 +"""Exact-integer tests of multiplicative error bounds and their limits.""" + +def main(): + cases = exhausted = 0 + for n in range(1, 1001): + x, C, D, B, a, floor = n, 1, 1, 0, 0, n + for j in range(1, 101): + floor = min(floor, x) + if x % 2: + x = (3*x+1)//2 + C *= 3 + B = 3*B+D + a += 1 + else: x //= 2 + D *= 2 + for b in {0, 1, floor//2, floor}: + m = b+1 if b % 2 == 0 else b + v, w = 3*m, 3*m+1 + assert D*x == C*n+B + assert v**a*D*x <= w**a*C*n + assert v**a*B <= (w**a-v**a)*C*n + if a >= w and B > 0: + assert v**a*B > 0 + exhausted += 1 + cases += 1 + # One-step equality witnesses the sharp factor; increasing v fails. + for b in range(1001): + m = b+1 if b % 2 == 0 else b + v, w = 3*m, 3*m+1 + assert v*(3*m+1) == 3*w*m + assert (v+1)*(3*m+1) > 3*w*m + print(f'{cases} product checks; {exhausted} cases beyond the linear budget; 1001 factor controls') + +if __name__ == '__main__': main() From fc4c7b859c5e47487a2e099792ee8b8c1abbd790 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 7 Oct 2026 15:50:02 +0530 Subject: [PATCH 4/5] Eliminate the source in product band budgets and document established product methods --- Collatz/Exploration/FloorProductError.lean | 25 ++++++++++++++++++++++ README.md | 11 ++++++++++ RESEARCH.md | 11 ++++++++++ scripts/test_floor_product_error.py | 20 +++++++++++++++++ 4 files changed, 67 insertions(+) diff --git a/Collatz/Exploration/FloorProductError.lean b/Collatz/Exploration/FloorProductError.lean index d1cccab3..4966c01a 100644 --- a/Collatz/Exploration/FloorProductError.lean +++ b/Collatz/Exploration/FloorProductError.lean @@ -1,4 +1,5 @@ import Collatz.Exploration.FloorAffineError +import Collatz.Structure.AffineBound /-! Multiplicative floor control keeps the error budget nontrivial at all odd counts. -/ namespace Collatz.Exploration.FloorProductError @@ -55,4 +56,28 @@ theorem offset_product {n b j B : Nat} 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 + end Collatz.Exploration.FloorProductError diff --git a/README.md b/README.md index 92f7fe6a..3528d02a 100644 --- a/README.md +++ b/README.md @@ -125,3 +125,14 @@ convergence. This elementary product method has not been assessed for priority. The independent audit checks 278,684 products, including 192,568 cases beyond the linear budget, 1,001 sharp factor controls, three Lean theorem footprints, and two false statements rejected by the kernel. + +`product_band_budget` additionally removes the source from two endpoints: +finite lower survival through a and an upper band constraint at c imply +`Q H 2^a v^k ≤ P 2^c L w^k`, where k counts odd steps through a. +No initial source upper bound is required. Four theorem footprints are audited. + +Priority note: products of step-error factors bounded using a minimum are +established in Simons and de Weger's cycle analysis, §3.2, Lemma 4 and +Corollary 5 ([author-hosted version 1.44](https://deweger.net/papers/%5B35a%5DSidW-3n%2B1-v1.44%5B2010%5D.pdf)). +Our finite-prefix core-Lean formulations are not evidence that this method, +or their exact corollaries, constitute new mathematics. diff --git a/RESEARCH.md b/RESEARCH.md index 7cf5b8cf..03527105 100644 --- a/RESEARCH.md +++ b/RESEARCH.md @@ -15944,3 +15944,14 @@ convergence. This elementary product method has not been assessed for priority. The independent audit checks 278,684 products, including 192,568 cases beyond the linear budget, 1,001 sharp factor controls, three Lean theorem footprints, and two false statements rejected by the kernel. + +`product_band_budget` additionally removes the source from two endpoints: +finite lower survival through a and an upper band constraint at c imply +`Q H 2^a v^k ≤ P 2^c L w^k`, where k counts odd steps through a. +No initial source upper bound is required. Four theorem footprints are audited. + +Priority note: products of step-error factors bounded using a minimum are +established in Simons and de Weger's cycle analysis, §3.2, Lemma 4 and +Corollary 5 ([author-hosted version 1.44](https://deweger.net/papers/%5B35a%5DSidW-3n%2B1-v1.44%5B2010%5D.pdf)). +Our finite-prefix core-Lean formulations are not evidence that this method, +or their exact corollaries, constitute new mathematics. diff --git a/scripts/test_floor_product_error.py b/scripts/test_floor_product_error.py index 536723bf..c30d9343 100644 --- a/scripts/test_floor_product_error.py +++ b/scripts/test_floor_product_error.py @@ -30,6 +30,26 @@ def main(): v, w = 3*m, 3*m+1 assert v*(3*m+1) == 3*w*m assert (v+1)*(3*m+1) > 3*w*m + bands = 0 + for n in range(1, 201): + states, coeffs, counts = [n], [1], [0] + for j in range(20): + x = states[-1] + odd = x % 2 + states.append((3*x+1)//2 if odd else x//2) + coeffs.append(coeffs[-1]*(3 if odd else 1)) + counts.append(counts[-1]+odd) + for a in range(1, 21): + b = min(states[:a+1]) + v = 3*(b+1 if b % 2 == 0 else b) + w = v+1 + for c in range(21): + Q = 3 + P = (Q*states[c]+b-1)//b + assert Q*states[c] <= P*b + assert Q*coeffs[c]*2**a*v**counts[a] <= P*2**c*coeffs[a]*w**counts[a] + bands += 1 + print(f'{bands} two-endpoint product band budgets') print(f'{cases} product checks; {exhausted} cases beyond the linear budget; 1001 factor controls') if __name__ == '__main__': main() From 089459d98b07366879fa03c7a269f6c2ba448a56 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 7 Oct 2026 15:51:39 +0530 Subject: [PATCH 5/5] Certify finite product band exits and compare against linear certificates --- Collatz/Exploration/FloorProductError.lean | 38 ++++++++++++++++++++++ README.md | 10 ++++++ RESEARCH.md | 10 ++++++ scripts/test_floor_product_error.py | 24 ++++++++++++++ 4 files changed, 82 insertions(+) diff --git a/Collatz/Exploration/FloorProductError.lean b/Collatz/Exploration/FloorProductError.lean index 4966c01a..b913aa68 100644 --- a/Collatz/Exploration/FloorProductError.lean +++ b/Collatz/Exploration/FloorProductError.lean @@ -1,5 +1,6 @@ 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 @@ -80,4 +81,41 @@ theorem product_band_budget {n b a c P Q : Nat} 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 diff --git a/README.md b/README.md index 3528d02a..12c9ba2d 100644 --- a/README.md +++ b/README.md @@ -136,3 +136,13 @@ established in Simons and de Weger's cycle analysis, §3.2, Lemma 4 and Corollary 5 ([author-hosted version 1.44](https://deweger.net/papers/%5B35a%5DSidW-3n%2B1-v1.44%5B2010%5D.pdf)). Our finite-prefix core-Lean formulations are not evidence that this method, or their exact corollaries, constitute new mathematics. + +The product criterion now formally produces accelerated and standard band +exits (`product_accelerated_exit`, `product_standard_exit`) within twice the +accelerated horizon. No initial source upper-band assumption is needed. +The bounded sample n=1..300, the three specified floor choices, and horizons +below 30 produced 98,910 product exit certificates versus 55,137 linear +certificates, with 44,824 product certificates absent from the linear set. +These sets need not be nested; these are sampled certificates, not distinct +orbits or a density theorem. All certified conclusions were checked directly. +The kernel audit now covers six theorem footprints. diff --git a/RESEARCH.md b/RESEARCH.md index 03527105..cf8616fd 100644 --- a/RESEARCH.md +++ b/RESEARCH.md @@ -15955,3 +15955,13 @@ established in Simons and de Weger's cycle analysis, §3.2, Lemma 4 and Corollary 5 ([author-hosted version 1.44](https://deweger.net/papers/%5B35a%5DSidW-3n%2B1-v1.44%5B2010%5D.pdf)). Our finite-prefix core-Lean formulations are not evidence that this method, or their exact corollaries, constitute new mathematics. + +The product criterion now formally produces accelerated and standard band +exits (`product_accelerated_exit`, `product_standard_exit`) within twice the +accelerated horizon. No initial source upper-band assumption is needed. +The bounded sample n=1..300, the three specified floor choices, and horizons +below 30 produced 98,910 product exit certificates versus 55,137 linear +certificates, with 44,824 product certificates absent from the linear set. +These sets need not be nested; these are sampled certificates, not distinct +orbits or a density theorem. All certified conclusions were checked directly. +The kernel audit now covers six theorem footprints. diff --git a/scripts/test_floor_product_error.py b/scripts/test_floor_product_error.py index c30d9343..9f7e2ec9 100644 --- a/scripts/test_floor_product_error.py +++ b/scripts/test_floor_product_error.py @@ -49,6 +49,30 @@ def main(): assert Q*states[c] <= P*b assert Q*coeffs[c]*2**a*v**counts[a] <= P*2**c*coeffs[a]*w**counts[a] bands += 1 + product_exits = linear_exits = extra = 0 + for n in range(1, 301): + states, coeffs, counts = [n], [1], [0] + for j in range(30): + x = states[-1]; odd = x % 2 + states.append((3*x+1)//2 if odd else x//2) + coeffs.append(coeffs[-1]*(3 if odd else 1)) + counts.append(counts[-1]+odd) + for b in {1, max(1, n//6), n}: + v = 3*(b+1 if b % 2 == 0 else b); w = v+1 + for a in range(1, 30): + k = counts[a]; L = coeffs[a] + for c in range(1, 30): + H = coeffs[c] + prod = 6*2**c*L*w**k < H*2**a*v**k + g = H*2**a-6*L*2**c + lin = n <= 6*b and g > 0 and 6*H*k*L < g*max(w-k, 0) + if prod or lin: + assert any(x < b or 6*b < x for x in states[:max(a,c)+1]) + product_exits += prod + linear_exits += lin + extra += prod and not lin + assert extra > 0 + print(f'{product_exits} product exits; {linear_exits} linear exits; {extra} additional product certificates') print(f'{bands} two-endpoint product band budgets') print(f'{cases} product checks; {exhausted} cases beyond the linear budget; 1001 factor controls')