Extend certified first-crossing descent to 2592 and classify feasible times

.github/workflows/ci.yml

@@ -25,6 +25,8 @@ jobs:
           # The project has no Lake test target, so keep testing disabled.
           auto-config: false
           build: true
+          # Build the library before lean-action saves the Lake cache.
+          build-args: Collatz
           test: false
           # lean-action caches the .lake directory by default; make it explicit.
           use-github-cache: true
@@ -43,3 +45,6 @@ jobs:
 
       - name: Check stopping atlas and horizon extension
         run: python3 scripts/audit_stopping_atlas.py
+
+      - name: Check depth-fifteen passage atlas and horizon 2592
+        run: python3 scripts/audit_passage_atlas.py

Collatz.lean

@@ -2103,3 +2103,5 @@ import Collatz.Search.InverseIntervalEarlyStop
 import Collatz.Strategy.StoppingCorrectionBounds
 import Collatz.Strategy.ProductDescentCheck
 import Collatz.Research.StoppingAtlas.All
+
+import Collatz.Research.PassageAtlas.All

Collatz/Research/PassageAtlas/All.lean

@@ -0,0 +1,4 @@
+import Collatz.Research.PassageAtlas.FeasibleTimes
+import Collatz.Research.PassageAtlas.Counting
+import Collatz.Research.PassageAtlas.Certificates
+import Collatz.Research.PassageAtlas.SolutionBridge