Certify all-source first-crossing descent through horizon 14186

.github/workflows/ci.yml

@@ -59,6 +59,7 @@ jobs:
           python3 scripts/audit_sharp_survival_counts.py
           python3 scripts/audit_gap_endpoint_certificates.py
           python3 scripts/audit_finite_beatty_barrier.py
+          python3 scripts/audit_certified_first_crossing.py
           python3 scripts/audit_eleven_halves_clock.py
 
       - name: Check exact first-descent intervals

Collatz.lean

@@ -2134,3 +2134,6 @@ import Collatz.Exploration.GapTenThousand
 
 import Collatz.Exploration.BalancedFirstLightScan
 import Collatz.Exploration.FiniteBeattyBarrier
+
+import Collatz.Exploration.AllSourceTenThousand
+import Collatz.Exploration.CertifiedFirstCrossing

Collatz/Exploration/AllSourceTenThousand.lean

@@ -0,0 +1,44 @@
+import Collatz.Strategy.AssetA
+import Collatz.Strategy.FirstLightConsequences
+import Collatz.Exploration.GapTenThousand
+
+/-! Combining inherited bounded stopping certificates with the endpoint scan.
+The first-crossing hypothesis is retained: this does not establish convergence. -/
+namespace Collatz.Exploration.AllSourceTenThousand
+open FirstLightDescent FirstLightConsequences
+
+/-- The existing verified orbit range supplies all exceptional first crossings. -/
+theorem small_first_light {n : Nat} (hn : 1 < n) (hN : n < 3998720) :
+    ∃ k : Nat, k ≤ 224 ∧ FirstLight n k ∧ acceleratedOrbit k n < n := by
+  obtain ⟨t, ht, hd⟩ := AssetA.drops_within_224 (by omega) (by omega : n < 3998720)
+  obtain ⟨k, hk, hf⟩ := exists_first_light n t (AffineObstruction.light_of_drop hd)
+  exact ⟨k, by omega, hf,
+    FirstLightCertificates.descent_at_first_light_le_256 hn (by omega) hf⟩
+
+/-- Every source above one descends at its first coefficient crossing by 10000. -/
+theorem descent_at_first_light {n j : Nat} (hn : 1 < n) (hj : j ≤ 10000)
+    (hf : FirstLight n j) : acceleratedOrbit j n < n := by
+  by_cases hlarge : 3330950 ≤ n
+  · exact GapTenThousand.descent_at_first_light hlarge hj hf
+  · obtain ⟨k, _, hk, hd⟩ := small_first_light hn (by omega)
+    have he : j = k := first_light_unique hf hk
+    simpa only [he] using hd
+
+/-- Interface to the existing finite-horizon stopping-time theory. -/
+theorem exactThrough_ten_thousand : ExactThrough 10000 :=
+  fun _ _ hn hj hf => descent_at_first_light hn hj hf
+
+/-- Coefficient crossing and first actual descent agree throughout this horizon. -/
+theorem first_descent_iff_first_light {n j : Nat} (hn : 1 < n) (hj : j ≤ 10000) :
+    FirstDescent n j ↔ FirstLight n j :=
+  FirstLightConsequences.first_descent_iff_first_light exactThrough_ten_thousand hn hj
+
+/-- A failed first-crossing descent must lie strictly beyond the certified horizon. -/
+theorem discrepancy_after_ten_thousand {n j : Nat} (hn : 1 < n)
+    (hf : FirstLight n j) (hfail : n ≤ acceleratedOrbit j n) : 10000 < j := by
+  by_cases hj : j ≤ 10000
+  · have := descent_at_first_light hn hj hf
+    omega
+  · omega
+
+end Collatz.Exploration.AllSourceTenThousand

Collatz/Exploration/CertifiedFirstCrossing.lean

@@ -0,0 +1,57 @@
+import Collatz.Exploration.AllSourceTenThousand
+import Collatz.Exploration.FiniteBeattyBarrier
+import Collatz.Strategy.PreCertified
+
+/-! Reuse the banked sharper accumulator certificate through horizon 14186.
+Theorem statements retain crossing existence as a hypothesis. -/
+namespace Collatz.Exploration.CertifiedFirstCrossing
+open FirstLightDescent FirstLightConsequences
+
+/-- The finite Beatty barrier extends exact crossing descent to every source. -/
+theorem descent_at_first_light {n j : Nat} (hn : 1 < n) (hj : j ≤ 14186)
+    (hf : FirstLight n j) : acceleratedOrbit j n < n := by
+  by_cases hc : 3997765 ≤ n
+  · exact FiniteBeattyBarrier.first_light_descent_through hc
+      PreCertified.bank_8951 PreCertified.pow_gap_8951 hj hf
+  · obtain ⟨k, _, hk, hd⟩ := AllSourceTenThousand.small_first_light hn (by omega)
+    have he : j=k := first_light_unique hf hk
+    simpa only [he] using hd
+
+/-- The improved horizon can be passed to the existing stopping-time theory. -/
+theorem exactThrough_14186 : ExactThrough 14186 :=
+  fun _ _ hn hj hf => descent_at_first_light hn hj hf
+
+/-- The two first-event predicates agree for every source greater than one. -/
+theorem first_descent_iff_first_light {n j : Nat} (hn : 1 < n) (hj : j ≤ 14186) :
+    FirstDescent n j ↔ FirstLight n j :=
+  FirstLightConsequences.first_descent_iff_first_light exactThrough_14186 hn hj
+
+/-- Any first-crossing discrepancy must occur strictly after this horizon. -/
+theorem discrepancy_after_14186 {n j : Nat} (hn : 1 < n) (hf : FirstLight n j)
+    (hfail : n ≤ acceleratedOrbit j n) : 14186 < j := by
+  by_cases hj : j ≤ 14186
+  · have := descent_at_first_light hn hj hf
+    omega
+  · omega
+
+/-- Heavy prefixes characterize finite actual survival at the improved horizon. -/
+theorem no_descent_iff_heavy (n : Nat) (hn : 1 < n) :
+    (∀ j, j ≤ 14186 → n ≤ acceleratedOrbit j n) ↔
+      (∀ j, j ≤ 14186 → 2 ^ j ≤ 3 ^ oddCount n j) :=
+  FirstLightConsequences.no_descent_iff_heavy_prefix exactThrough_14186 hn
+
+/-- The inherited extremal stopping witness is also an exact coefficient crossing. -/
+theorem record_first_light : FirstLight 1126015 224 := by
+  apply (first_descent_iff_first_light (by decide) (by decide)).mp
+  obtain ⟨k, hk, hd⟩ := AssetA.drops_within_224 (n := 1126015) (by decide) (by decide)
+  have he : k=224 := by
+    by_cases hl : k ≤ 223
+    · have := AssetA.sigma_1126015_ge k hl
+      omega
+    · omega
+  refine ⟨?_, ?_⟩
+  · simpa only [he] using hd
+  · intro j hj
+    exact AssetA.sigma_1126015_ge j (by omega)
+
+end Collatz.Exploration.CertifiedFirstCrossing

scripts/audit_all_source_ten_thousand.py

@@ -0,0 +1,48 @@
+#!/usr/bin/env python3
+"""Check the all-source conditional theorem and reproduce the finite census."""
+import subprocess
+from audit_barrier_kernel import ROOT, check_axioms, check_false_certificates
+from check_proof_escapes import violations
+
+
+def first_crossing(n, horizon):
+    x=n; C=D=1
+    for j in range(horizon+1):
+        if C<D:
+            return j, x
+        if x%2:
+            x=(3*x+1)//2
+            C*=3
+        else:
+            x//=2
+        D*=2
+    return None
+
+
+def main():
+    parts=['BalancedFirstLightScan', 'AllSourceTenThousand']
+    for part in parts:
+        assert not violations((ROOT/f'Collatz/Exploration/{part}.lean').read_text())
+    latest=(0,0)
+    for n in range(2,3330950):
+        result=first_crossing(n,256)
+        assert result is not None and result[1]<n, (n,result)
+        if result[0]>latest[1]:
+            latest=(n,result[0])
+    assert latest==(1126015,224), latest
+    name='Collatz.Exploration.AllSourceTenThousand'
+    subprocess.run(['lake','build','Collatz.Exploration.BalancedFirstLightScan'],cwd=ROOT,check=True)
+    subprocess.run(['lake','build',name],cwd=ROOT,check=True)
+    footprints=sum(check_axioms(ROOT/f'Collatz/Exploration/{part}.lean',
+        f'Collatz.Exploration.{part}') for part in parts)
+    false=check_false_certificates('Collatz.Exploration.BalancedFirstLightScan',[
+        'example : Collatz.Exploration.BalancedFirstLightScan.checkTree 1 2 3 1 = true := by decide\n',
+        'set_option maxRecDepth 100000 in\nset_option maxHeartbeats 0 in\nexample : Collatz.FirstLightScan.check 223 1126015 = true := by decide\n',
+    ])
+    print(f'3330948 independently checked sources; latest crossing {latest}; '
+          f'{footprints} theorem footprints; {false} false controls')
+    print('First crossing by 10000 implies descent for every n>1; crossing existence remains open.')
+
+
+if __name__=='__main__':
+    main()

scripts/audit_certified_first_crossing.py

@@ -0,0 +1,35 @@
+#!/usr/bin/env python3
+"""Audit the all-source finite crossing horizons without assuming existence."""
+import subprocess
+from audit_all_source_ten_thousand import first_crossing
+from audit_barrier_kernel import ROOT, check_axioms, check_false_certificates
+from check_proof_escapes import violations
+
+
+def main():
+    parts=['BalancedFirstLightScan','AllSourceTenThousand','CertifiedFirstCrossing']
+    for part in parts:
+        assert not violations((ROOT/f'Collatz/Exploration/{part}.lean').read_text())
+    latest=(0,0)
+    for n in range(2,3998720):
+        result=first_crossing(n,256)
+        assert result is not None and result[1]<n, (n,result)
+        if result[0]>latest[1]:
+            latest=(n,result[0])
+    assert latest==(1126015,224), latest
+    name='Collatz.Exploration.CertifiedFirstCrossing'
+    subprocess.run(['lake','build',name],cwd=ROOT,check=True)
+    footprints=sum(check_axioms(ROOT/f'Collatz/Exploration/{part}.lean',
+        f'Collatz.Exploration.{part}') for part in parts)
+    false=check_false_certificates(name,[
+        'example : Collatz.acceleratedOrbit 2 1 < 1 := by decide\n',
+        'set_option maxRecDepth 200000 in\nset_option maxHeartbeats 0 in\nset_option exponentiation.threshold 20000 in\nexample : (2:Nat)^14187 < 3^8951 := by decide\n',
+        'set_option maxRecDepth 100000 in\nset_option maxHeartbeats 0 in\nexample : Collatz.FirstLightDescent.FirstLight 1126015 223 := by decide\n',
+    ])
+    print(f'3998718 independently checked sources; latest crossing {latest}; '
+          f'{footprints} theorem footprints; {false} false controls')
+    print('Exact first-crossing descent through 14186 is conditional on crossing existence.')
+
+
+if __name__=='__main__':
+    main()