From fca11553e376e6bc65b4c577ee686f7c03f3b390 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 7 Oct 2026 15:54:50 +0530 Subject: [PATCH 1/2] Formalize the coefficient corridor obstruction to product spread certificates --- .github/workflows/ci.yml | 1 + Collatz.lean | 1 + .../Exploration/ProductSpreadObstruction.lean | 34 +++++++++++++++ README.md | 10 +++++ RESEARCH.md | 10 +++++ scripts/audit_product_spread_obstruction.py | 41 +++++++++++++++++++ 6 files changed, 97 insertions(+) create mode 100644 Collatz/Exploration/ProductSpreadObstruction.lean create mode 100644 scripts/audit_product_spread_obstruction.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7f191fa1..e3c24e42 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -48,6 +48,7 @@ jobs: python3 scripts/audit_coefficient_band.py python3 scripts/audit_floor_affine_error.py python3 scripts/audit_floor_product_error.py + python3 scripts/audit_product_spread_obstruction.py python3 scripts/audit_eleven_halves_clock.py - name: Check exact first-descent intervals diff --git a/Collatz.lean b/Collatz.lean index 1313eef1..bc0a459f 100644 --- a/Collatz.lean +++ b/Collatz.lean @@ -2121,3 +2121,4 @@ import Collatz.Exploration.Band5995 import Collatz.Exploration.AffineBandExit import Collatz.Exploration.FloorProductError +import Collatz.Exploration.ProductSpreadObstruction diff --git a/Collatz/Exploration/ProductSpreadObstruction.lean b/Collatz/Exploration/ProductSpreadObstruction.lean new file mode 100644 index 00000000..839522b1 --- /dev/null +++ b/Collatz/Exploration/ProductSpreadObstruction.lean @@ -0,0 +1,34 @@ +import Collatz.Exploration.FloorProductError + +/-! A limitation of product spread certificates, not a claim of band survival. -/ +namespace Collatz.Exploration.ProductSpreadObstruction +open FloorAffineError FloorProductError + +/-- A coefficient pair already inside the target width cannot trigger strict product spread. -/ +theorem no_strict_spread {L H D E P Q b k : Nat} + (hc : Q*H*D ≤ P*E*L) : + Q*H*D*base b^k ≤ P*E*L*weight b^k := by + have hw : base b ≤ weight b := by unfold base weight; omega + exact Nat.mul_le_mul hc (Nat.pow_le_pow_left hw k) + +/-- A coefficient corridor [1,R] prevents strict width-R spread for every floor. -/ +theorem corridor_obstruction {L H D E R b k : Nat} + (hl : D ≤ L) (hh : H ≤ R*E) : + H*D*base b^k ≤ R*E*L*weight b^k := by + have hc : H*D ≤ R*E*L := by + have h1 := Nat.mul_le_mul_right D hh + have h2 := Nat.mul_le_mul_left (R*E) hl + exact Nat.le_trans h1 h2 + have hz := no_strict_spread (Q := 1) (P := R) (b := b) (k := k) (by simpa using hc) + simpa using hz + +/-- Apply the limitation to the actual odd-count coefficients of an orbit. -/ +theorem orbit_corridor_obstruction {n a c R b : Nat} + (hl : 2^a ≤ 3^oddCount n a) + (hh : 3^oddCount n c ≤ R*2^c) : + ¬ (R*2^c*3^oddCount n a*weight b^oddCount n a < + 3^oddCount n c*2^a*base b^oddCount n a) := by + have h := corridor_obstruction (b := b) (k := oddCount n a) hl hh + omega + +end Collatz.Exploration.ProductSpreadObstruction diff --git a/README.md b/README.md index 12c9ba2d..90ea9d36 100644 --- a/README.md +++ b/README.md @@ -146,3 +146,13 @@ 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. + +### Product-spread obstruction + +`ProductSpreadObstruction.lean` proves that if `Q H D ≤ P E L`, the +product correction cannot yield strict spread: `Q H D v^k ≤ P E L w^k`. +Consequently a coefficient corridor [1,R] prevents width-R product-spread +certificates for all floor choices and odd counts. This is a limitation of +the sufficient exit test, not a proof of actual survival or a counterexample +to Collatz. Balanced parity prefixes at lengths 16,64,256,1024 are independently +checked using exact integer comparisons. Three general Lean lemmas are audited. diff --git a/RESEARCH.md b/RESEARCH.md index cf8616fd..def90565 100644 --- a/RESEARCH.md +++ b/RESEARCH.md @@ -15965,3 +15965,13 @@ 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. + +### Product-spread obstruction + +`ProductSpreadObstruction.lean` proves that if `Q H D ≤ P E L`, the +product correction cannot yield strict spread: `Q H D v^k ≤ P E L w^k`. +Consequently a coefficient corridor [1,R] prevents width-R product-spread +certificates for all floor choices and odd counts. This is a limitation of +the sufficient exit test, not a proof of actual survival or a counterexample +to Collatz. Balanced parity prefixes at lengths 16,64,256,1024 are independently +checked using exact integer comparisons. Three general Lean lemmas are audited. diff --git a/scripts/audit_product_spread_obstruction.py b/scripts/audit_product_spread_obstruction.py new file mode 100644 index 00000000..f4f998bf --- /dev/null +++ b/scripts/audit_product_spread_obstruction.py @@ -0,0 +1,41 @@ +#!/usr/bin/env python3 +"""Kernel audit and exact coefficient-corridor obstruction checks.""" +import subprocess +from audit_barrier_kernel import ROOT, check_axioms, check_false_certificates +from check_proof_escapes import violations +from test_six_band_prefixes import balanced_residue + +def main(): + name='Collatz.Exploration.ProductSpreadObstruction' + source=ROOT/'Collatz/Exploration/ProductSpreadObstruction.lean' + assert not violations(source.read_text()) + subprocess.run(['lake','build',name],cwd=ROOT,check=True) + pairs=0 + for K in [16,64,256,1024]: + _,bits=balanced_residue(K) + C,D=1,1 + coeffs=[(C,D)] + for bit in bits: + C*=3 if bit else 1; D*=2 + assert D<=C<3*D + coeffs.append((C,D)) + for L,D in coeffs: + for H,E in coeffs: + assert H*D<=3*E*L + pairs+=1 + checked=0 + for b in range(31): + v=3*(b+1 if b%2==0 else b);w=v+1 + for k in range(31): + for A in range(31): + for Z in range(A,31): + assert A*v**k<=Z*w**k + checked+=1 + count=check_axioms(source,name) + bad=check_false_certificates(name,[ + 'example : 4*1 ≤ 3*1*1 := by decide\n', + 'example : 4*4^1 ≤ 3*3^1 := by decide\n', + ]) + print(f'{pairs} corridor pairs; {checked} product controls; {count} theorem footprints; {bad} false claims rejected') + +if __name__=='__main__': main() From fba2f891570c7180f68874dc5ed38caa170170f9 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 7 Oct 2026 15:58:30 +0530 Subject: [PATCH 2/2] Compare linear and multiplicative floor budgets using integer Bernoulli bounds --- .github/workflows/ci.yml | 1 + Collatz.lean | 1 + .../Exploration/FloorBudgetComparison.lean | 38 +++++++++++++++++++ README.md | 11 ++++++ RESEARCH.md | 11 ++++++ scripts/audit_floor_budget_comparison.py | 28 ++++++++++++++ 6 files changed, 90 insertions(+) create mode 100644 Collatz/Exploration/FloorBudgetComparison.lean create mode 100644 scripts/audit_floor_budget_comparison.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e3c24e42..ecb59a64 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -49,6 +49,7 @@ jobs: python3 scripts/audit_floor_affine_error.py python3 scripts/audit_floor_product_error.py python3 scripts/audit_product_spread_obstruction.py + python3 scripts/audit_floor_budget_comparison.py python3 scripts/audit_eleven_halves_clock.py - name: Check exact first-descent intervals diff --git a/Collatz.lean b/Collatz.lean index bc0a459f..f7be25ce 100644 --- a/Collatz.lean +++ b/Collatz.lean @@ -2122,3 +2122,4 @@ import Collatz.Exploration.Band5995 import Collatz.Exploration.AffineBandExit import Collatz.Exploration.FloorProductError import Collatz.Exploration.ProductSpreadObstruction +import Collatz.Exploration.FloorBudgetComparison diff --git a/Collatz/Exploration/FloorBudgetComparison.lean b/Collatz/Exploration/FloorBudgetComparison.lean new file mode 100644 index 00000000..afb6f909 --- /dev/null +++ b/Collatz/Exploration/FloorBudgetComparison.lean @@ -0,0 +1,38 @@ +import Collatz.Exploration.FloorProductError + +/-! Integer Bernoulli comparison of the two floor-error budgets. +The underlying inequality is classical; no priority claim is made. -/ +namespace Collatz.Exploration.FloorBudgetComparison +open FloorAffineError FloorProductError + +/-- Cleared-denominator Bernoulli inequality for neighboring positive bases. -/ +theorem bernoulli_neighbors (v k : Nat) : + (v+1)^(k+1) ≤ (v+1)*v^k+k*(v+1)^k := by + induction k with + | zero => simp + | succ k ih => + have h1 := Nat.mul_le_mul_left v ih + have h2 := Nat.mul_le_mul_left (k*(v+1)^k) (show v ≤ v+1 by omega) + simp only [Nat.pow_succ,Nat.mul_add,Nat.add_mul,Nat.mul_one,Nat.one_mul,Nat.mul_left_comm,Nat.mul_comm] at h1 h2 ⊢ + omega + +/-- The multiplicative offset ratio is no worse than the linear ratio when k z*base b^k) (Nat.sub_add_cancel hk) + rw [Nat.add_mul] at he + rw [Nat.mul_sub] + omega + +end Collatz.Exploration.FloorBudgetComparison diff --git a/README.md b/README.md index 90ea9d36..efc63841 100644 --- a/README.md +++ b/README.md @@ -156,3 +156,14 @@ certificates for all floor choices and odd counts. This is a limitation of the sufficient exit test, not a proof of actual survival or a counterexample to Collatz. Balanced parity prefixes at lengths 16,64,256,1024 are independently checked using exact integer comparisons. Three general Lean lemmas are audited. + +### Comparison of floor-error budgets + +`FloorBudgetComparison.lean` proves a classical cleared-denominator Bernoulli +inequality and deduces `(w-k)w^k ≤ w v^k` and +`(w-k)(w^k-v^k) ≤ k v^k` for k≤w, where w=v+1 is the floor weight. +Thus the multiplicative paid-offset ratio is no worse than the linear ratio +where the linear denominator is positive. This compares bounds, not exit +certificate sets (the sets use different additional assumptions). +Audit: 20,301 exact integer comparisons including v=0, three theorem footprints, +and two false controls rejected. This is classical mathematics, not frontier novelty. diff --git a/RESEARCH.md b/RESEARCH.md index def90565..67aa633c 100644 --- a/RESEARCH.md +++ b/RESEARCH.md @@ -15975,3 +15975,14 @@ certificates for all floor choices and odd counts. This is a limitation of the sufficient exit test, not a proof of actual survival or a counterexample to Collatz. Balanced parity prefixes at lengths 16,64,256,1024 are independently checked using exact integer comparisons. Three general Lean lemmas are audited. + +### Comparison of floor-error budgets + +`FloorBudgetComparison.lean` proves a classical cleared-denominator Bernoulli +inequality and deduces `(w-k)w^k ≤ w v^k` and +`(w-k)(w^k-v^k) ≤ k v^k` for k≤w, where w=v+1 is the floor weight. +Thus the multiplicative paid-offset ratio is no worse than the linear ratio +where the linear denominator is positive. This compares bounds, not exit +certificate sets (the sets use different additional assumptions). +Audit: 20,301 exact integer comparisons including v=0, three theorem footprints, +and two false controls rejected. This is classical mathematics, not frontier novelty. diff --git a/scripts/audit_floor_budget_comparison.py b/scripts/audit_floor_budget_comparison.py new file mode 100644 index 00000000..84412a9d --- /dev/null +++ b/scripts/audit_floor_budget_comparison.py @@ -0,0 +1,28 @@ +#!/usr/bin/env python3 +"""Audit classical Bernoulli comparison for finite-floor error budgets.""" +import subprocess +from audit_barrier_kernel import ROOT, check_axioms, check_false_certificates +from check_proof_escapes import violations + +def main(): + name='Collatz.Exploration.FloorBudgetComparison' + source=ROOT/'Collatz/Exploration/FloorBudgetComparison.lean' + assert not violations(source.read_text()) + subprocess.run(['lake','build',name],cwd=ROOT,check=True) + count=0 + for v in range(101): + w=v+1 + for k in range(201): + assert w**(k+1)<=w*v**k+k*w**k + assert max(w-k,0)*w**k<=w*v**k + if k<=w: + assert (w-k)*(w**k-v**k)<=k*v**k + count+=1 + axioms=check_axioms(source,name) + bad=check_false_certificates(name,[ + 'example : 4^3 ≤ 4*3^2+1*4^2 := by decide\n', + 'example : (4-2)*(4^2-3^2) ≤ 1*3^2 := by decide\n', + ]) + print(f'{count} exact comparisons; {axioms} theorem footprints; {bad} false controls rejected') + +if __name__=='__main__': main()