Remove exceptional-source errors from certified survival counts

.github/workflows/ci.yml

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

Collatz.lean

@@ -2137,3 +2137,6 @@ import Collatz.Exploration.FiniteBeattyBarrier
 
 import Collatz.Exploration.AllSourceTenThousand
 import Collatz.Exploration.CertifiedFirstCrossing
+
+import Collatz.Exploration.ExactSurvivalCounts
+import Collatz.Exploration.CertifiedSurvivalCounts

Collatz/Exploration/CertifiedSurvivalCounts.lean

@@ -0,0 +1,23 @@
+import Collatz.Exploration.ExactSurvivalCounts
+import Collatz.Exploration.CertifiedFirstCrossing
+
+/-! Apply the exact transfer to every horizon through the certified limit. -/
+namespace Collatz.Exploration.CertifiedSurvivalCounts
+open FirstLightConsequences FirstLightCounting FirstLightEventual
+
+/-- Actual survival counts are exactly coefficient counts through horizon 14186. -/
+theorem actual_count_eq {H : Nat} (hH : H≤14186) (N : Nat) :
+    NaturalDensity.predicateCount (ActualSurvival H) N =
+      PeriodicCounting.countBelow (survives H) N :=
+  ExactSurvivalCounts.actual_count_eq
+    (exactThrough_mono CertifiedFirstCrossing.exactThrough_14186 hH) N
+
+/-- Exact decomposition, with no finite exceptional-source correction. -/
+theorem actual_count_div_mod {H : Nat} (hH : H≤14186) (N : Nat) :
+    NaturalDensity.predicateCount (ActualSurvival H) N =
+      (N/2^H)*PeriodicCounting.countBelow (survives H) (2^H) +
+        PeriodicCounting.countBelow (survives H) (N%2^H) :=
+  ExactSurvivalCounts.actual_count_div_mod
+    (exactThrough_mono CertifiedFirstCrossing.exactThrough_14186 hH) N
+
+end Collatz.Exploration.CertifiedSurvivalCounts

Collatz/Exploration/ExactSurvivalCounts.lean

@@ -0,0 +1,45 @@
+import Collatz.Strategy.FirstLightEventual
+
+/-! An exact crossing certificate removes the finite count exception completely.
+These are finite-horizon statements and do not establish universal crossing. -/
+namespace Collatz.Exploration.ExactSurvivalCounts
+open FirstLightConsequences FirstLightCounting FirstLightEventual
+
+/-- An exact horizon identifies actual survival at every shifted source. -/
+theorem actual_iff_periodic {H n : Nat} (hc : ExactThrough H) :
+    ActualSurvival H n ↔ survives H n=true := (survives_iff hc).symm
+
+/-- The actual survival predicate itself is periodic on the shifted domain. -/
+theorem actual_period {H n : Nat} (hc : ExactThrough H) :
+    ActualSurvival H (n+2^H) ↔ ActualSurvival H n := by
+  rw [actual_iff_periodic hc, actual_iff_periodic hc, survives_period]
+
+/-- The actual count has no exceptional-input error at a certified horizon. -/
+theorem actual_count_eq {H : Nat} (hc : ExactThrough H) (N : Nat) :
+    NaturalDensity.predicateCount (ActualSurvival H) N =
+      PeriodicCounting.countBelow (survives H) N := by
+  have he : NaturalDensity.predicateCount (ActualSurvival H) N =
+      NaturalDensity.predicateCount (fun n => survives H n=true) N :=
+    Nat.le_antisymm
+      (NaturalDensity.predicateCount_mono (fun _ => (actual_iff_periodic hc).mp) N)
+      (NaturalDensity.predicateCount_mono (fun _ => (actual_iff_periodic hc).mpr) N)
+  rw [he, NaturalDensity.predicateCount_bool]
+
+/-- Exact full-period and remainder decomposition for actual orbit survival. -/
+theorem actual_count_div_mod {H : Nat} (hc : ExactThrough H) (N : Nat) :
+    NaturalDensity.predicateCount (ActualSurvival H) N =
+      (N/2^H)*PeriodicCounting.countBelow (survives H) (2^H) +
+        PeriodicCounting.countBelow (survives H) (N%2^H) := by
+  rw [actual_count_eq hc]
+  exact survival_count_div_mod H N
+
+/-- Both finite count bounds hold with no additive source cutoff. -/
+theorem actual_count_bounds {H : Nat} (hc : ExactThrough H) (N : Nat) :
+    (N/2^H)*PeriodicCounting.countBelow (survives H) (2^H) ≤
+      NaturalDensity.predicateCount (ActualSurvival H) N ∧
+    NaturalDensity.predicateCount (ActualSurvival H) N ≤
+      (N/2^H+1)*PeriodicCounting.countBelow (survives H) (2^H) := by
+  rw [actual_count_eq hc]
+  exact survival_count_bounds H N
+
+end Collatz.Exploration.ExactSurvivalCounts

README.md

@@ -260,7 +260,7 @@ powers of 3 and 2 forward, verifies a power bracket and gap at each endpoint,
 and proves sequential-checker soundness. `GapTenThousand.lean` evaluates the
 full scan in the Lean kernel: any n≥3,330,950 descends at a first coefficient
 crossing if that crossing occurs by horizon 10000. No crossing existence is
-asserted; smaller sources remain a separate obligation. No frontier novelty
+asserted by this scan alone; the smaller-source obligation is closed below. No frontier novelty
 or universal convergence claim is made.
 The cutoff is minimal for this scalar scan (the audit rejects 3,330,949),
 not claimed optimal for actual descent. Independent integer computation
@@ -284,3 +284,21 @@ interval checker whose leaves reuse the existing orbit scan.
 Audit: four Beatty theorem footprints, 344,004 exact non-descent prefixes for
 reach 64 and cutoff 868, and two false cap/time controls rejected. The balanced
 checker has one audited theorem footprint and two false controls rejected.
+
+### Certified first-crossing descent through horizon 14186
+
+`AllSourceTenThousand.lean` closes the exceptional-source obligation in the
+endpoint scan by reusing `AssetA.drops_within_224`. Its inherited range covers
+every source below 3,998,720. `CertifiedFirstCrossing.lean` then combines that
+range with the localized Beatty barrier and the banked 8951-odd-step certificate.
+For every n>1, a first coefficient crossing by 14186 is the first actual descent.
+Any discrepancy must occur later. The theorem does not prove crossing existence
+for every source; it adapts existing accumulator arguments without a priority
+claim. The inherited stopping record at 1,126,015 is also proved to be a first
+coefficient crossing at step 224.
+
+Both CI runs passed complete Lean compilation and the audit: 12 theorem
+footprints, 3,998,718 independently checked sources, and three false controls
+rejected. An additional independent census found that step 224 is attained by
+both 1,126,015 and 2,252,031 in this range; the second observation is computational,
+not separately a Lean theorem in this addition.

RESEARCH.md

@@ -16102,7 +16102,7 @@ powers of 3 and 2 forward, verifies a power bracket and gap at each endpoint,
 and proves sequential-checker soundness. `GapTenThousand.lean` evaluates the
 full scan in the Lean kernel: any n≥3,330,950 descends at a first coefficient
 crossing if that crossing occurs by horizon 10000. No crossing existence is
-asserted; smaller sources remain a separate obligation. No frontier novelty
+asserted by this scan alone; the smaller-source obligation is closed below. No frontier novelty
 or universal convergence claim is made.
 The cutoff is minimal for this scalar scan (the audit rejects 3,330,949),
 not claimed optimal for actual descent. Independent integer computation
@@ -16126,3 +16126,21 @@ interval checker whose leaves reuse the existing orbit scan.
 Audit: four Beatty theorem footprints, 344,004 exact non-descent prefixes for
 reach 64 and cutoff 868, and two false cap/time controls rejected. The balanced
 checker has one audited theorem footprint and two false controls rejected.
+
+### Certified first-crossing descent through horizon 14186
+
+`AllSourceTenThousand.lean` closes the exceptional-source obligation in the
+endpoint scan by reusing `AssetA.drops_within_224`. Its inherited range covers
+every source below 3,998,720. `CertifiedFirstCrossing.lean` then combines that
+range with the localized Beatty barrier and the banked 8951-odd-step certificate.
+For every n>1, a first coefficient crossing by 14186 is the first actual descent.
+Any discrepancy must occur later. The theorem does not prove crossing existence
+for every source; it adapts existing accumulator arguments without a priority
+claim. The inherited stopping record at 1,126,015 is also proved to be a first
+coefficient crossing at step 224.
+
+Both CI runs passed complete Lean compilation and the audit: 12 theorem
+footprints, 3,998,718 independently checked sources, and three false controls
+rejected. An additional independent census found that step 224 is attained by
+both 1,126,015 and 2,252,031 in this range; the second observation is computational,
+not separately a Lean theorem in this addition.

scripts/audit_exact_survival_counts.py

@@ -0,0 +1,54 @@
+#!/usr/bin/env python3
+"""Independently compare exact survival and periodic count decompositions."""
+import subprocess
+from audit_barrier_kernel import ROOT, check_axioms, check_false_certificates
+from check_proof_escapes import violations
+
+
+def census():
+    prefixes=counts=0
+    for H in range(11):
+        values=[]
+        for n in range(2000):
+            start=n+2; x=start; a=0; actual=heavy=True
+            for j in range(1,H+1):
+                if x%2:
+                    x=(3*x+1)//2; a+=1
+                else:
+                    x//=2
+                actual=actual and start<=x
+                heavy=heavy and 2**j<=3**a
+            assert actual==heavy, (H,n,x,a)
+            values.append(int(actual)); prefixes+=1
+        sums=[0]
+        for value in values:
+            sums.append(sums[-1]+value)
+        p=2**H; c=sums[p]
+        for N in range(2001):
+            assert sums[N]==(N//p)*c+sums[N%p], (H,N)
+            assert (N//p)*c<=sums[N]<=(N//p+1)*c
+            counts+=1
+    assert (prefixes,counts)==(22000,22011)
+    return prefixes,counts
+
+
+def main():
+    prefixes,counts=census()
+    parts=['ExactSurvivalCounts','CertifiedSurvivalCounts']
+    for part in parts:
+        assert not violations((ROOT/f'Collatz/Exploration/{part}.lean').read_text())
+    name='Collatz.Exploration.CertifiedSurvivalCounts'
+    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.PeriodicCounting.countBelow (Collatz.FirstLightCounting.survives 2) 2 = 0 := by decide\n',
+        'example : Collatz.PeriodicCounting.countBelow (Collatz.FirstLightCounting.survives 2) 4 = 2 := by decide\n',
+    ])
+    print(f'{prefixes} independent survival classifications; {counts} exact count checks; '
+          f'{footprints} theorem footprints; {false} false controls')
+    print('Zero exceptional-source count error through horizon 14186; no universal crossing proved.')
+
+
+if __name__=='__main__':
+    main()