Certify stopping atlas and extend first-crossing descent through 1538

[Chessing234]

This extends the conditional first-coefficient-crossing descent theorem from 1024 to 1538 steps for every input greater than one, reusing the checked exceptional range below 99730. The next arithmetic gap fails at step 1539 and would require threshold 330588; the failure is explicitly distinguished from an orbit counterexample.

The change also proves horizon-parametric interval shape, finite first-event/survivor conservation, a composition-sensitive periodic discrepancy bound A(M-A), and a power-band obstruction excluding exact stopping time 11. A complete census at depths 10–13 adds 15,360 distinct residue classes with universally quantified affine endpoints and exact stopping intervals.

The 1000 batch commits are individually checked, disjoint certificate units, not 1000 independent discoveries. Merge with a merge commit to preserve every commit. The work does not prove universal crossing existence or the Collatz conjecture. Research/StoppingAtlas/README.md contains literature attribution, technique boundaries, reproduction commands, and precise remaining obligations.

Validation: the new audit builds all added Lean modules, checks all 61,724 named theorem axiom footprints, rejects four deliberately false certificates, and runs 981,534 independent integer checks. The new target and audit pass locally, as do the full core library build and scripts/check_integrity.sh (including the repository-wide proof-escape screen and existing frontier axiom checks). CI additionally builds the full core library, runs the existing integrity checks, and repeats the new audit. The addition has 176,883 Lean code lines, excluding comments, blank lines, and the generated axiom-print driver. The separate Mathlib extension is not changed or included in this verification claim.