Compute exact Collatz first-descent intervals and certify the finite census

[Chessing234]

Exact first-descent indices were known to form an interval, but their boundaries were not computed by that result. This adds an exact affine solver and proves that the computed interval classifies every index in a dyadic residue class, including all failures. It also proves refinement composition and finite membership conservation, classifies periodic candidates, and isolates universal interval coverage as an equivalent form of Collatz.

The certificate atlas covers all 1,022 canonical classes at depths 1–9. Its 100 separately checked commits contain generated certificates, not 100 independent discoveries. Additional examples cover exact first-descent times 59 and 65. The literature review includes primary sources and Hercher's June 2026 corrigendum.

Validation:

• New aggregate build passed (130 jobs); all 4,153 public theorems passed transitive axiom auditing with only standard Lean logical axioms.
• 16 Python tests passed, with 119,634 counted independent checks; three intentionally false Lean certificates were rejected.
• Deterministic generation, source hashes, and whitespace checks passed.
• 12,101 new nonblank, noncomment Lean code lines, excluding audit commands; 103 commits relative to ca585a9.

The local audit builds the new aggregate and its dependencies, not all historical repository targets. No proof of Collatz, global coverage, or literature-level novelty is claimed. The finite depth-16 census found no finite nonempty exact-time intervals; that observation remains explicitly experimental.

See Research/DescentIntervals/README.md and verification.json for mathematical statements, reproduction commands, and evidence. This PR is based on the existing research branch so its diff contains only this investigation.