Propagate the sharper finite cutoff to survival and stopping-time periodicity

.github/workflows/ci.yml

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

Collatz.lean

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

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

Collatz/Exploration/SharpFirstLightEventual.lean

@@ -0,0 +1,58 @@
+import Collatz.Exploration.CoefficientGapThreshold
+import Collatz.Strategy.FirstLightCounting
+
+/-! Propagate the sharper finite cutoff to survival and first-stopping periodicity.
+The proofs reuse existing residue results; no universal crossing is assumed. -/
+namespace Collatz.Exploration.SharpFirstLightEventual
+open CoefficientGapThreshold FirstLightDescent FirstLightConsequences FirstLightCounting
+
+/-- Any light prefix in the window guarantees a descent for starts above the threshold. -/
+theorem descent_by_light_above_threshold {H n k : Nat} (hk : k≤H)
+    (hn : H*2^H<3*n) (hl : 3^oddCount n k<2^k) :
+    ∃ j, j≤k ∧ acceleratedOrbit j n<n := by
+  obtain ⟨j, hj, hf⟩ := exists_first_light n k hl
+  exact ⟨j, hj, first_light_below_horizon (by omega) hn hf⟩
+
+/-- Every finite horizon has an exact coefficient classification beyond an explicit cutoff. -/
+theorem no_descent_iff_heavy_above_threshold {H n : Nat} (hn : H*2^H<3*n) :
+    (∀ j, j≤H → n≤acceleratedOrbit j n) ↔ heavyCheck H n=true := by
+  rw [heavyCheck_iff]
+  constructor
+  · intro h j hj
+    by_cases hl : 3^oddCount n j<2^j
+    · obtain ⟨i, hi, hd⟩ := descent_by_light_above_threshold hj hn hl
+      have := h i (by omega)
+      omega
+    · omega
+  · intro h j hj
+    by_cases hd : acceleratedOrbit j n<n
+    · have hl := AffineObstruction.light_of_drop hd
+      have := h j hj
+      omega
+    · omega
+
+/-- Above the cutoff, the first actual descent and first coefficient crossing agree. -/
+theorem first_descent_iff_first_light_above_threshold {H n k : Nat}
+    (hn : H*2^H<3*n) (hk : k≤H) : FirstDescent n k ↔ FirstLight n k := by
+  constructor
+  · intro hd
+    refine ⟨AffineObstruction.light_of_drop hd.1, ?_⟩
+    intro j hj
+    by_cases hl : 3^oddCount n j<2^j
+    · obtain ⟨i, hi, hdrop⟩ := descent_by_light_above_threshold (by omega : j≤H) hn hl
+      have := hd.2 i (by omega)
+      omega
+    · omega
+  · intro hf
+    exact ⟨first_light_below_horizon hk hn hf, no_descent_before_first_light hf⟩
+
+/-- At every finite horizon, first stopping times are eventually periodic. -/
+theorem first_descent_congr_above_threshold {H n m k : Nat}
+    (hn : H*2^H<3*n) (hm : H*2^H<3*m) (hk : k≤H)
+    (hmod : n%2^H=m%2^H) : FirstDescent n k ↔ FirstDescent m k := by
+  rw [first_descent_iff_first_light_above_threshold hn hk,
+    first_descent_iff_first_light_above_threshold hm hk]
+  exact FirstLightPeriodicity.firstLight_congr hk hmod
+
+
+end Collatz.Exploration.SharpFirstLightEventual

README.md

@@ -216,3 +216,27 @@ 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.
+
+### Survival classification at the sharper cutoff
+
+`SharpFirstLightEventual.lean` propagates 3*n>H*2^H to exact finite-horizon
+no-descent/heavy-prefix equivalence, first-descent/first-light equivalence,
+and first-stopping-time agreement for equal residues modulo 2^H above the
+cutoff. It reuses existing residue and accumulator theory and improves the
+sufficient source interval; it proves no eventual crossing for every source.
+Audit: four theorem footprints, 2,050 paired residue checks through horizon
+40, and two false controls rejected. Frontier novelty is not established.

RESEARCH.md

@@ -16058,3 +16058,27 @@ 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.
+
+### Survival classification at the sharper cutoff
+
+`SharpFirstLightEventual.lean` propagates 3*n>H*2^H to exact finite-horizon
+no-descent/heavy-prefix equivalence, first-descent/first-light equivalence,
+and first-stopping-time agreement for equal residues modulo 2^H above the
+cutoff. It reuses existing residue and accumulator theory and improves the
+sufficient source interval; it proves no eventual crossing for every source.
+Audit: four theorem footprints, 2,050 paired residue checks through horizon
+40, and two false controls rejected. Frontier novelty is not established.

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

scripts/audit_sharp_finite_survival.py

@@ -0,0 +1,38 @@
+#!/usr/bin/env python3
+"""Independent paired orbit tests above the improved finite cutoff."""
+import subprocess
+from audit_barrier_kernel import ROOT,check_axioms,check_false_certificates
+from check_proof_escapes import violations
+
+def events(n,H):
+    x=n;C=D=1;cross=drop=None
+    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 and cross is None:cross=j
+        if x<n and drop is None:drop=j
+    return cross,drop
+
+def main():
+    name='Collatz.Exploration.SharpFirstLightEventual'
+    source=ROOT/'Collatz/Exploration/SharpFirstLightEventual.lean'
+    assert not violations(source.read_text())
+    subprocess.run(['lake','build',name],cwd=ROOT,check=True)
+    pairs=0
+    for H in range(41):
+        cutoff=H*2**H//3+1
+        for offset in range(50):
+            n=cutoff+offset;m=n+2**H
+            assert H*2**H<3*n and H*2**H<3*m
+            left,right=events(n,H),events(m,H)
+            assert left[0]==left[1] and right[0]==right[1]
+            assert left==right
+            pairs+=1
+    axioms=check_axioms(source,name)
+    bad=check_false_certificates(name,[
+        'example : Collatz.FirstLightCounting.heavyCheck 2 1 = true := by decide\n',
+        'example : Collatz.acceleratedOrbit 8 7 < 7 := by decide\n',
+    ])
+    print(f'{pairs} paired residue checks; {axioms} theorem footprints; {bad} false controls')
+
+if __name__=='__main__':main()