feat(Schonhage): add Section 4 cube and box decomposition #2160

Finite prerequisite for #1394's remaining tuned1.9992 route. Native conservative subquadratic execution is in #2159; Corollary26 needs a different box-based data structure, not just tighter logarithmic absorption. Fresh open issue/PR searches found no competing cube/box/Corollary26 implementation claim.

Owner: root coordinator/implementation author, session codex-root-3sum-20261101, ordinary branch work/three-sum-section-four-boxes-20261101 from exact #2159 2f6fb39d0. Existing native solver/host PR refs stay unchanged.

Acceptance:

• Reuse existing Schönhage Term/Leaf/OutStr, encodings, contribution/order/tiling mathematics. Add finite cubes, stars, leaves, signed values and canonical boxes with exact counts and boundary cases.
• Prove the Section4 leaf-to-box partition with disjointness/uniqueness and valuation identity, plus the finite box dynamic-program recurrence and cardinal bound needed by Lemma29. Keep low-order contributions explicit; no omitted terms.
• Search Mathlib/CSLib before adding ordered-subset helpers; put genuinely reusable helpers in a small suitable topic module and migrate concrete clients.
• Checked nontrivial signed/cancellation, valid/invalid box and empty/zero-threshold clients; source statements/premises and locator mapping at the exact pin; scoped checks, hosted full validation and independent whole-layer review before integration.

Primary source: anthropics/formal-math@16a5ce4, 3sum-apsp/PaperStatements.lean Section4 definitions, and ThreeSumApsp/Sec4/{Boxes,BoxesFromLeaves,Lemma27_28,Lemma29}.lean. Preserve Anthropic authorship and distinguish finite algebra/counting from execution. This issue supplies no native data structure or charged-time claim. Native computed box enumeration/trie preprocessing/query code, Corollary26 integration, improved ET parameters and final tuned1.9992 composition remain under #1394 after this prerequisite.

The milestone closes only after these finite criteria integrate; full #1394 remains open.