Compare floor-error budgets using classical Bernoulli inequalities

.github/workflows/ci.yml

@@ -48,6 +48,8 @@ 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_floor_budget_comparison.py
           python3 scripts/audit_eleven_halves_clock.py
 
       - name: Check exact first-descent intervals

Collatz.lean

@@ -2121,3 +2121,5 @@ import Collatz.Exploration.Band5995
 
 import Collatz.Exploration.AffineBandExit
 import Collatz.Exploration.FloorProductError
+import Collatz.Exploration.ProductSpreadObstruction
+import Collatz.Exploration.FloorBudgetComparison

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<w. -/
+theorem ratio_comparison (b k : Nat) :
+    (weight b-k)*weight b^k ≤ weight b*base b^k := by
+  have hh := bernoulli_neighbors (base b) k
+  have hw : base b+1=weight b := by unfold base weight; rfl
+  rw [hw,Nat.pow_succ] at hh
+  rw [Nat.sub_mul]
+  simp only [Nat.mul_comm] at hh ⊢
+  omega
+
+/-- Compare the paid-offset coefficients when the linear denominator is positive. -/
+theorem paid_ratio_comparison {b k : Nat} (hk : k ≤ weight b) :
+    (weight b-k)*(weight b^k-base b^k) ≤ k*base b^k := by
+  have hr := ratio_comparison b k
+  have he := congrArg (fun z => z*base b^k) (Nat.sub_add_cancel hk)
+  rw [Nat.add_mul] at he
+  rw [Nat.mul_sub]
+  omega
+
+end Collatz.Exploration.FloorBudgetComparison

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

README.md

@@ -146,3 +146,24 @@ 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.
+
+### 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.

RESEARCH.md

@@ -15965,3 +15965,24 @@ 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.
+
+### 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.

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()

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()