Improve the finite first-light cutoff and prove scalar gap descent

.github/workflows/ci.yml

@@ -54,6 +54,7 @@ jobs:
           python3 scripts/audit_floor_product_descent.py
           python3 scripts/audit_product_delay_certificates.py
           python3 scripts/audit_product_thresholds.py
+          python3 scripts/audit_coefficient_gap_threshold.py
           python3 scripts/audit_eleven_halves_clock.py
 
       - name: Check exact first-descent intervals

Collatz.lean

@@ -2127,3 +2127,4 @@ import Collatz.Exploration.ExactTraceProduct
 import Collatz.Exploration.FloorProductDescent
 import Collatz.Exploration.ProductDelayCertificates
 import Collatz.Exploration.ProductThresholds
+import Collatz.Exploration.CoefficientGapThreshold

Collatz/Exploration/CoefficientGapThreshold.lean

@@ -0,0 +1,58 @@
+import Collatz.Exploration.ProductThresholds
+import Collatz.Exploration.FloorBudgetComparison
+import Collatz.Strategy.FirstLightDescent
+
+/-! A linear sufficient source-floor threshold for each light coefficient pair.
+These are conditional descent tools based on classical Bernoulli bounds. -/
+namespace Collatz.Exploration.CoefficientGapThreshold
+open FloorAffineError FloorProductError ProductThresholds FloorBudgetComparison
+
+/-- A scalar margin implies the full powered product test. -/
+theorem passes_of_scalar {C D k b : Nat}
+    (hc : C*weight b < D*(weight b-k)) : Passes C D k b := by
+  have hw : 0 < weight b^k := Nat.pow_pos (by unfold weight; omega)
+  have h1 := Nat.mul_lt_mul_of_pos_right hc hw
+  have h2 := Nat.mul_le_mul_left D (ratio_comparison b k)
+  simp only [Nat.mul_assoc,Nat.mul_left_comm,Nat.mul_comm] at h1 h2
+  have hh : (C*weight b^k)*weight b < (D*base b^k)*weight b := by
+    simp only [Nat.mul_left_comm,Nat.mul_comm]
+    omega
+  exact Nat.lt_of_mul_lt_mul_right hh
+
+/-- The required floor weight scales with odd count and reciprocal coefficient gap. -/
+theorem passes_of_gap {C D k b : Nat} (hl : C ≤ D)
+    (hg : k*D < (D-C)*weight b) : Passes C D k b := by
+  apply passes_of_scalar
+  have he : (D-C)*weight b = D*weight b-C*weight b := Nat.sub_mul _ _ _
+  have hm : D*(weight b-k) = D*weight b-D*k := Nat.mul_sub _ _ _
+  have hc := Nat.mul_le_mul_right (weight b) hl
+  rw [he] at hg
+  rw [hm]
+  have hk : k*D=D*k := Nat.mul_comm _ _
+  omega
+
+/-- Gap-specific scalar source thresholds certify descent, with no individual trace products. -/
+theorem descent_of_gap {n j : Nat} (hn : 0 < n)
+    (hl : 3^oddCount n j ≤ 2^j)
+    (hg : oddCount n j*2^j < (2^j-3^oddCount n j)*weight n) :
+    ∃ i, i ≤ j ∧ acceleratedOrbit i n < n := by
+  apply FloorProductDescent.descent_before hn
+  exact passes_of_gap hl hg
+
+/-- Improve the existing H*3^H cutoff using the first-light accumulator bound. -/
+theorem first_light_below_horizon {H n j : Nat} (hj : j ≤ H)
+    (hn : H*2^H < 3*n)
+    (hf : FirstLightDescent.FirstLight n j) : acceleratedOrbit j n < n := by
+  by_cases hd : acceleratedOrbit j n < n
+  · exact hd
+  · have hb := FirstLightDescent.failure_bound hf (by omega)
+    have ha := Nat.le_trans (AffineExact.oddCount_le_self n j) hj
+    have hp : 3^oddCount n j ≤ 2^H := Nat.le_trans (Nat.le_of_lt hf.1)
+      (Nat.pow_le_pow_right (by decide) hj)
+    have hm := Nat.mul_le_mul ha hp
+    have hg : 1 ≤ 2^j-3^oddCount n j := by have := hf.1; omega
+    have hl := Nat.mul_le_mul_left (3*n) hg
+    simp only [Nat.mul_assoc,Nat.mul_left_comm,Nat.mul_comm] at hl hb
+    omega
+
+end Collatz.Exploration.CoefficientGapThreshold

README.md

@@ -216,3 +216,17 @@ the thresholds are exact for this test, not optimal for actual descent.
 Audit: eight theorem footprints, 12,006 threshold checks, 1,893 matching
 odd-count descent cases, two false controls rejected. The method remains a
 specialization of known product bounds, with no established frontier novelty.
+
+### Scalar gap criterion and improved finite first-light cutoff
+
+`CoefficientGapThreshold.lean` proves that `a D < (D-C) w(n)` suffices
+for descent by j when C=3^a≤D=2^j. The scalar margin implies the full
+product test by the classical Bernoulli comparison.
+A separate corollary uses the existing first-light accumulator bound to
+improve the coarse repository cutoff n>H*3^H to 3*n>H*2^H:
+if a first coefficient crossing occurs by H, descent occurs at that crossing.
+It proves no existence of a crossing and no universal convergence.
+No frontier novelty has been established for this elementary improvement.
+Audit: four theorem footprints, 53,361 scalar cases, 16,043 valid scalar
+certificates, 179,303 descent cases, 2,924 first-light cutoff cases,
+and two false controls rejected.

RESEARCH.md

@@ -16058,3 +16058,17 @@ the thresholds are exact for this test, not optimal for actual descent.
 Audit: eight theorem footprints, 12,006 threshold checks, 1,893 matching
 odd-count descent cases, two false controls rejected. The method remains a
 specialization of known product bounds, with no established frontier novelty.
+
+### Scalar gap criterion and improved finite first-light cutoff
+
+`CoefficientGapThreshold.lean` proves that `a D < (D-C) w(n)` suffices
+for descent by j when C=3^a≤D=2^j. The scalar margin implies the full
+product test by the classical Bernoulli comparison.
+A separate corollary uses the existing first-light accumulator bound to
+improve the coarse repository cutoff n>H*3^H to 3*n>H*2^H:
+if a first coefficient crossing occurs by H, descent occurs at that crossing.
+It proves no existence of a crossing and no universal convergence.
+No frontier novelty has been established for this elementary improvement.
+Audit: four theorem footprints, 53,361 scalar cases, 16,043 valid scalar
+certificates, 179,303 descent cases, 2,924 first-light cutoff cases,
+and two false controls rejected.

scripts/audit_coefficient_gap_threshold.py

@@ -0,0 +1,56 @@
+#!/usr/bin/env python3
+"""Exact scalar-to-product and conditional descent audit."""
+import subprocess
+from audit_barrier_kernel import ROOT,check_axioms,check_false_certificates
+from check_proof_escapes import violations
+
+def main():
+    name='Collatz.Exploration.CoefficientGapThreshold'
+    source=ROOT/'Collatz/Exploration/CoefficientGapThreshold.lean'
+    assert not violations(source.read_text())
+    subprocess.run(['lake','build',name],cwd=ROOT,check=True)
+    tested=certified=0
+    for C in range(11):
+        for D in range(11):
+            for k in range(21):
+                for b in range(21):
+                    v=3*(b+1 if b%2==0 else b);w=v+1
+                    if C*w<D*max(w-k,0):assert C*w**k<D*v**k
+                    if C<=D and k*D<(D-C)*w:
+                        assert C*w<D*max(w-k,0)
+                        assert C*w**k<D*v**k
+                        certified+=1
+                    tested+=1
+    orbit_cases=0
+    for n in range(1,2001):
+        x=n;C=D=1;a=0;desc=False
+        w=3*(n+1 if n%2==0 else n)+1
+        for j in range(101):
+            if C<=D and a*D<(D-C)*w:
+                assert desc;orbit_cases+=1
+            odd=x%2;a+=odd
+            x=(3*x+1)//2 if odd else x//2
+            C*=3 if odd else 1;D*=2
+            desc |= x<n
+    cutoff_cases=0
+    for H in range(1,33):
+        cutoff=H*2**H//3+1
+        for n in range(cutoff,cutoff+100):
+            x=n;C=D=1
+            for j in range(1,H+1):
+                odd=x%2
+                x=(3*x+1)//2 if odd else x//2
+                C*=3 if odd else 1;D*=2
+                if C<D:
+                    assert H*2**H<3*n and x<n
+                    cutoff_cases+=1
+                    break
+    print(f'{cutoff_cases} first-light cutoff cases')
+    axioms=check_axioms(source,name)
+    bad=check_false_certificates(name,[
+        'example : 3*4 < 2*(4-1) := by decide\n',
+        'example : 41*2^65 < (2^65-3^41)*4 := by decide\n',
+    ])
+    print(f'{tested} scalar cases; {certified} valid scalar certificates; {orbit_cases} descent cases; {axioms} theorem footprints; {bad} false controls')
+
+if __name__=='__main__':main()