[JoyboyBrian]

The completed-downset norm bound is a premise of the Full physical-cut and precision arguments. This package independently proves a stronger bound from the original leading-section conditioning, for every complex matrix and every binary tree of contiguous intervals, including unbalanced trees. With Λ,Q≥1, ||T||₂≤Λ and every leading inverse bounded by Q, all completed atomic downsets and their inverses are bounded by 32 N^(3/2)(ΛQ)^8, improving the retained sufficient 256 N³(ΛQ)^12 envelope. The proof restricts one global unit-LDU factorization and keeps the noncommuting frontier order P=L_C D_I U_F^-1 U explicit.

An independent exact oracle checks 11 interval trees and 398 downsets, including N=1, asymmetric trees and eight states with both completed lower factors and a nontrivial upper frontier. An algebra-only execution of the retained scheduler binds its ten size-four atoms. Five controls reject wrong factor order, a singular leading section, noncontiguous inverse restrictions, a whole-inverse-only premise and an unmatched complex adjoint. These fixtures support the written quantified proof; they do not substitute for it.

The result concerns complete ideal calls. Unfinished FFT/generator fragments, rounded execution, physical costs and substituting the new envelope into every downstream allocation remain separate obligations. No source allocation or selected frontier is changed. This follows #4755's explicit inherited-norm boundary and differs from #4209's near-identity majorant premises.

Validation: metadata/source pins; registered Python 3.12 normal and optimized replay; committed-byte/source-history preflight (10 package/input files); official export integrity; Git-free normal/optimized replay with all 11 exported files unchanged. No Lean, Docker or full historical replay. Proof and limits: research/leading-section-downset-audit/README.md.

Canonical claim: #4202 (comment)

Submission uses canonical base 624de9dc66858af0945e5f8a0942488d62280d43, priority 7. The 19:49 UTC complete refresh covered 299 open PRs, 3721 Discussion records and 6319 base local notes; scoped search and live #4202 plus relevant predecessor heads were rechecked. Search does not cover unpublished work or all historical code diffs and is not a novelty certificate.

Credit Jose Manuel's original scalar-LDU/frontier argument and polynomial bound, Vlado's scheduler, and classical block elimination/Schur/triangular norm methods. The contribution is the independent restriction-based sharpening and arbitrary interval-tree extension. Prepared for Brian (JoyboyBrian) with substantial OpenAI Codex assistance. Agent cross-review is part of the author process, not independent human/formal acceptance. Hosted CI is not yet claimed.