diff --git a/research/leading-section-downset-audit/README.md b/research/leading-section-downset-audit/README.md
new file mode 100644
index 0000000000..2f7511c7b3
--- /dev/null
+++ b/research/leading-section-downset-audit/README.md
@@ -0,0 +1,263 @@
+# Leading-section conditioning controls all completed downsets
+
+Prepared for Brian (`JoyboyBrian`) with substantial OpenAI Codex assistance.
+Apache-2.0.
+
+This independent audit proves a stronger completed-call norm bound than the
+one retained in `rational-unitary-fft/FULL-PROOF.md` §§2–4. It applies to every
+complex matrix whose original leading sections meet the stated inverse bound,
+and to every binary tree of contiguous intervals, balanced or unbalanced.
+The key observation is that every descendant's scalar unit-LDU factors are
+principal restrictions of **one global factorization**. This avoids charging
+the Schur descendant's larger direct norm again in every scalar row bound.
+
+[Canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4202#discussioncomment-19131470).
+This answers the norm implication explicitly left inherited by
+[PR #4755](https://github.com/CrocSwap/integer-mult-bounds/pull/4755).
+It does not extend that package's physical-fragment proof or claim a new
+FFT/generator, rounded execution, physical cost, selected κ or complete
+multiplication theorem.
+
+## Theorem
+
+Let `T` be any complex `N×N` matrix, `N>=1`, with
+
+```
+Λ,Q >= 1,   ||T||₂ <= Λ,   ||T[0:k,0:k]^-1||₂ <= Q  (1<=k<=N).
+```
+
+All leading sections must be invertible. Bounds smaller than one may be
+normalized upward before applying the theorem. No Toeplitz, Hermitian,
+positivity, near-identity, dyadic-dimension or balanced-tree premise is used.
+Let an arbitrary binary contiguous interval tree recursively execute the
+upper block shear, its two children in parallel, then the lower block shear;
+a singleton executes its scalar pivot. Children may be legally interleaved.
+An atom is one complete shear or scalar, not a primitive gate inside it.
+
+Write `χ=ΛQ`, `U₀=Λ+Λ²Q`, and `W=1+sqrt(N-1)χ`. For every downset `I`
+of the resulting atomic dependency DAG, its chronological endpoint product
+`P(I)` satisfies
+
+```
+||P(I)||₂      <= Q U₀² W³,
+||P(I)^-1||₂ <= Q³ U₀² W³
+                  <= 32 N^(3/2) χ^8.
+```
+
+The common bound improves the predecessor's sufficient
+`256 N³ χ^12` at the same ideal completed-call boundary. This is a sufficient
+bound, not a sharp constant. A remaining suffix is `T P(I)^-1`, so its direct
+bound needs the additional endpoint factor `Λ`; its inverse similarly needs
+`Q`. No unit-endpoint suffix assumption is made.
+
+## 1. One global unit-LDU factorization and its row/column bounds
+
+The nonzero leading determinants give the unique factorization `T=L D U`,
+where `L,U` are respectively unit lower/upper triangular and `D` is nonsingular
+diagonal. Let `T_k=T[0:k,0:k]`. For `1<=k<N`, the last row of
+`T_k^-1 T[0:k,k:N]` equals the tail `U[k-1,k:N]`: substitute the leading
+LDU factors; the last row of unit-upper `U_k^-1` is the last coordinate row.
+Its Euclidean length is at most `QΛ=χ`.
+
+Dually, the last column of `T[k:N,0:k] T_k^-1` equals
+`L[k:N,k-1]`: the last column of unit-lower `L_k^-1` is the last coordinate
+column. Its length is at most `χ`. These are ordinary complex matrix
+products and inverses. There is no conjugation of the row/column solve.
+Both off-diagonal Frobenius norms are consequently at most
+`sqrt(N-1)χ`. The triangle inequality with the identity gives
+
+```
+||L||₂, ||U||₂ <= W.
+```
+
+This uses the **original** leading solves. Replacing `Λ` here with a generic
+Schur-descendant bound would lose the improvement.
+
+For pivot `d_k`, the scalar Schur formula gives `|d_k|<=U₀`, using the
+norms of restrictions of `T` and of `T[k-1]^-1`; for the first pivot use
+`|d_1|<=Λ<=U₀`. The last diagonal entry of `T_k^-1` is `d_k^-1`, so
+`|d_k^-1|<=Q`. Therefore
+
+```
+||D||₂ <= U₀,   ||D^-1||₂ <= Q,
+L^-1 = D U T^-1,   U^-1 = T^-1 L D,
+||L^-1||₂, ||U^-1||₂ <= V := Q U₀ W.
+```
+
+The exact order in these inverse identities is essential. Since `Q,U₀>=1`,
+`V>=W>=1`, so identity blocks fit every direct-sum estimate below.
+
+## 2. Every contiguous Schur descendant uses restrictions of the same factors
+
+For `J=[a,b)`, define `M_J=T_b/T_a`, with `T_0` the empty prefix. Block
+elimination of `T_b=L_b D_b U_b` at position `a` gives
+
+```
+M_J = L[J,J] D[J,J] U[J,J].
+```
+
+The lower-right trailing block after eliminating a leading block has exactly
+these factors. Uniqueness of scalar unit-LDU proves the claim; it is not an
+assumption that a Schur complement is itself Toeplitz. The Schur quotient
+identity then shows that any binary split at `c` produces children
+`M_[a,c)` and `M_[c,b)`. All required pivots remain nonzero.
+
+A principal restriction contracts the spectral norm. Moreover, for a
+**contiguous interval** `J`,
+
+```
+L[J,J]^-1 = L^-1[J,J],   U[J,J]^-1 = U^-1[J,J].
+```
+
+For example the entry equation for a triangular product at indices `i,j`
+uses only summation indices between `i` and `j`; these all remain in `J`.
+Thus restricting the global inverse gives the identity product on `J`.
+The same assertion need not hold for a principal set with holes, which is
+why interval ownership is a hypothesis. All descendant unit factors and
+inverses are now uniformly bounded by `W` and `V`, without a depth multiplier.
+
+At a split, write the node matrix as `[[A,B],[C,E]]`. Define
+`K=A^-1 B`, `H=C A^-1`, upper atom `R=[[I,K],[0,I]]`, and lower atom
+`B_low=[[I,0],[H,I]]`. Ordinary transpose may implement the right solve
+`H=(A.T^-1 C.T).T`; conjugate transpose without matching conjugation changes
+complex coefficients. The block endpoint identity is
+
+```
+M_J = B_low diag(M_left,M_right) R.
+```
+
+Uniqueness also gives
+
+```
+L_J = B_low diag(L_left,L_right),
+D_J = diag(D_left,D_right),
+U_J = diag(U_left,U_right) R.
+```
+
+These identities require no equal child sizes.
+
+## 3. The completed-downset factorization, with order retained
+
+For a downset `I`, let `C(I)` be the disjoint maximal fully completed subtrees.
+Define `L_C` as the direct sum of their full unit-lower factors and identity
+on other coordinates. Define `D_I` to contain a pivot exactly when that leaf
+has completed, and one otherwise. Define an upper frontier `F(I)` by stopping
+at any internal node whose upper atom is absent from `I`, descending otherwise,
+and retaining all singleton leaves. Its intervals partition the coordinates.
+Let `U_F` be the direct sum of the full unit-upper factors of those intervals.
+Then
+
+```
+P(I) = L_C D_I U_F^-1 U.
+```
+
+Proof: recursively define partial lower, diagonal and upper factors. An empty
+subtree has three identity factors. A completed leaf has `(1,d_k,1)`. An
+internal node whose upper atom is present has
+
+```
+L_partial = B_low^ε diag(L_left_partial,L_right_partial),
+D_partial = diag(D_left_partial,D_right_partial),
+U_partial = diag(U_left_partial,U_right_partial) R,
+```
+
+where `ε=1` only if the lower atom is present. In that case both children
+are completely finished. Multiplying in this order gives the executed node
+product by induction, without commuting any overlapping factors. The lower
+recursion is precisely `L_C`; the diagonal recursion is `D_I`.
+For the upper factor, induction on frontier nodes gives
+`U = U_F U_partial`, hence `U_partial=U_F^-1 U`, with the inverse on the
+left. A legal interleaving changes only products on disjoint child supports,
+which commute. Thus the factorization holds for every downset, independent
+of how a linearization reached it and independent of the tree's depth.
+
+Now `||L_C||<=W`, `||L_C^-1||<=V`, `||D_I||<=U₀`,
+`||D_I^-1||<=Q`, `||U_F||<=W`, `||U_F^-1||<=V`. The four-factor product
+and its correctly reversed inverse give
+
+```
+||P(I)|| <= W U₀ V W = Q U₀² W³,
+||P(I)^-1|| <= V W Q V = Q³ U₀² W³.
+```
+
+Finally `U₀<=2Λ²Q`, `Q³U₀²<=4Λ⁴Q⁵<=4χ⁵`, and
+`W<=2sqrt(N)χ`; this proves the common `32 N^(3/2)χ^8` bound. For `N=1`,
+`W=1` and the two downsets are identity and the one pivot. The same proof
+and estimates hold without invoking a nonexistent split.
+
+## Scope, evidence and reproduction
+
+This theorem concerns complete ideal calls. It neither improves the current
+factory's explicit allocation automatically nor bounds unfinished generator
+fragments. The existing physical-cut, perturbation, rank and rounding arguments
+would need a separate audited substitution before any implementation precision
+change. No source compiler or frozen proof is modified.
+
+The oracle implements its own matrix product, Gauss–Jordan inverse, scalar
+LDU elimination, Schur quotient, interval trees, all downsets of each selected
+tree, and frontier products. It shares only the retained exact Gaussian-rational
+scalar representation. No predecessor verifier is imported. Exact nonsymmetric,
+non-Toeplitz complex examples cover `N=1`, both `N=3` trees, all five `N=4`
+trees, and three asymmetric/balanced `N=5` choices: 11 trees and 398 downsets.
+Eight cuts have both nontrivial completed lower factors and a nontrivial upper
+frontier. Each state checks the forward and correctly reversed inverse formula,
+original leading solves, descendant restrictions and a conservative rational
+norm envelope against the squared common bound. The proof above supplies the
+universal theorem; finite checks are not substituted for it.
+
+An AST selection executes the original `full_plan` and `parallel` functions
+on one complex size-four matrix, with independent whole-shear/scalar callbacks.
+Its ten ideal atoms reproduce the matrix exactly. This binds the source's
+block schedule and ordinary right-solve direction, but does not execute actual
+FFT/generator fragments or the Full factory.
+
+Five controls discriminate a wrong frontier factor order, a singular first
+leading section despite an invertible whole matrix, a noncontiguous triangular
+inverse restriction, use of only the whole-matrix inverse bound, and replacing
+ordinary transpose by an unmatched complex adjoint in the right solve.
+The whole-inverse-only control uses `[[1/64,1],[1,0]]`: both endpoint norms
+are below two while its upper factor has an entry 64.
+
+Base `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. The
+physical-cut predecessor #4755 has head
+`653289c67733e1b0feb24ddac796003ebb827e55`. The same-ρ near-identity theorem
+#4209 has head `ccc33bfde8baadef7979fac81e28c0a6f6f278c4`; it does not
+supply the present general leading-section hypothesis. The fresh round search
+covered 299 open PRs, 3721 Discussion records and 6319 local notes with complete
+inventories. Live #4202 and the relevant predecessor heads were checked.
+Search coverage is not a novelty certificate. All source bytes are pinned in
+`SOURCES.json`; every live input is declared in `VERIFY.json`.
+
+```
+python3 scripts/research_package.py --package research/leading-section-downset-audit --check-only
+python3.12 scripts/research_package.py --package research/leading-section-downset-audit
+python3 -B scripts/check_research_commit.py --package research/leading-section-downset-audit --check-source-history
+```
+
+The registered normal and optimized commands use Python 3.12 and the standard
+library only. Run the last preflight after committing. An official export can
+be integrity-checked and `verify.py` run directly without Git. No full historical
+suite, Lean, Docker, normalized/raw Gaussian execution or multiplication replay
+is claimed. Author-process agent review is not independent human/formal
+acceptance.
+
+## Open next questions
+
+Can the sharper completed-call envelope be substituted into the actual Full
+allocation while preserving every downstream coefficient, child, physical-cut
+and data-grid inequality? First make a dependency ledger for each occurrence
+of the old envelope in `full.allocation`, including its third power in the
+operator defect and the generator/scalar fragment allowance. Merely changing
+a constant in the factory would not prove its rounded caller contract.
+
+## Attribution
+
+Jose Manuel supplied the original global scalar-LDU/frontier argument and
+polynomial completed-downset bound in `FULL-PROOF.md`, last changed at
+`7ab1bc8973cc9e606053c65f094ca3abc4a42fee`; #4205 retains it at final head
+`78c72e563173f3822fcb4efed9ceeccf05630258`. Vlado supplied the recursive
+scheduler. Classical block elimination, Schur quotient, triangular inverse
+and Frobenius inequalities underlie this proof. The new scoped contribution
+is the independent restriction-based sharpening and arbitrary interval-tree
+extension. #4209's near-identity Schur-majorant theorem has different premises;
+#4755's physical trace audit intentionally leaves the norm hypothesis open.
diff --git a/research/leading-section-downset-audit/SOURCES.json b/research/leading-section-downset-audit/SOURCES.json
new file mode 100644
index 0000000000..a3cae550e3
--- /dev/null
+++ b/research/leading-section-downset-audit/SOURCES.json
@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/capped-phase-fusion/evidence/inplace_algebra_ultra/check_circuits.py",
+      "usage": "input",
+      "git_blob": "f80c141c8116b163c2bb5a028c28212077c8d5a9",
+      "sha256": "06d1861bfe8af543908e26557ffda7e451ff176bceb9bacfaf0f04f234b336d5"
+    },
+    {
+      "path": "research/full-toeplitz-cut-audit/README.md",
+      "usage": "input",
+      "git_blob": "f088efaaa828e415db6bb152a8cbeaea1dd68dd7",
+      "sha256": "5b514f93ab3b0a37a32978a599d74c545ed19122e235f9cccfff36faefb97a9b"
+    },
+    {
+      "path": "research/rational-unitary-fft/FULL-PROOF.md",
+      "usage": "input",
+      "git_blob": "e650f46863115f810e27b403f916dd7f79b37786",
+      "sha256": "acf8c596d91b5efd35a286735d6867ff8afce64354a13f680c2fae3dab824410"
+    },
+    {
+      "path": "research/rational-unitary-fft/exact.py",
+      "usage": "input",
+      "git_blob": "aae41e6acfb2e5a4fafdd85727891eb746b57b42",
+      "sha256": "c9b89d7357210af69865690ba12e695366961f8b501a8fab9d0fefe3fb30c479"
+    },
+    {
+      "path": "research/rational-unitary-fft/full.py",
+      "usage": "input",
+      "git_blob": "7f85ad1a89e81b7dfc6b54e7bd9547120e86d5d3",
+      "sha256": "1f42d5f2858564ffb320e54ba6aa29651025491569823e25006bf5862457b803"
+    }
+  ]
+}
diff --git a/research/leading-section-downset-audit/TASK.json b/research/leading-section-downset-audit/TASK.json
new file mode 100644
index 0000000000..c3465494d7
--- /dev/null
+++ b/research/leading-section-downset-audit/TASK.json
@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Independent quantified leading-section-to-completed-downset theorem for every complex matrix and every binary contiguous interval tree, sharpening the common bound to 32 N^(3/2)(Lambda Q)^8.",
+  "scope_change_reason": "PR4755 left the completed-call norm theorem inherited. Original leading solves bound one global LDU whose interval restrictions control every descendant, yielding a stronger bound and arbitrary-tree scope; this is not another finite cut census.",
+  "bottleneck_link": "Controls the ideal completed downsets used by physical-cut and precision allocation; downstream substitution and unfinished fragments retain separate obligations.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop with a full quantified proof or exact boundary counterexample plus bounded discriminating checks; do not change the source allocation or claim the full multiplication theorem.",
+  "outcome": "completed",
+  "evidence": "README.md quantified restriction/frontier proof; verify.py 11 trees and 398 downsets, including N=1 and mixed lower/upper frontiers, source algebra binding and five controls.",
+  "author": "Brian (JoyboyBrian), with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance in source reading, independent proof, code and verification; author-process review does not imply independent human/formal acceptance.",
+  "open_questions": [
+    {
+      "question": "Can the sharper completed-downset envelope be substituted into every actual Full allocation dependency?",
+      "why_it_matters": "A better endpoint norm alone does not prove the emitted gate perturbation and data-grid budgets.",
+      "first_step": "Ledger every old-envelope occurrence in full.allocation, including the cubic operator defect and generator/scalar fragment allowances.",
+      "blocked_by": "Separate downstream precision and unfinished-fragment audit."
+    }
+  ]
+}
diff --git a/research/leading-section-downset-audit/VERIFY.json b/research/leading-section-downset-audit/VERIFY.json
new file mode 100644
index 0000000000..89c5b16ca6
--- /dev/null
+++ b/research/leading-section-downset-audit/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/capped-phase-fusion/evidence/inplace_algebra_ultra/check_circuits.py",
+    "research/full-toeplitz-cut-audit/README.md",
+    "research/rational-unitary-fft/FULL-PROOF.md",
+    "research/rational-unitary-fft/exact.py",
+    "research/rational-unitary-fft/full.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Independent LDU and frontier oracle: 11 interval trees, 398 downsets, retained algebra binding and five controls"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Independent LDU and frontier oracle: 11 interval trees, 398 downsets, retained algebra binding and five controls"
+    }
+  ]
+}
diff --git a/research/leading-section-downset-audit/verify.py b/research/leading-section-downset-audit/verify.py
new file mode 100644
index 0000000000..20e49ca5b2
--- /dev/null
+++ b/research/leading-section-downset-audit/verify.py
@@ -0,0 +1,238 @@
+"""Independent exact LDU/downset oracle; no predecessor verifier imported."""
+import ast
+import copy
+import importlib.util
+import json
+from fractions import Fraction as Q
+from pathlib import Path
+from types import SimpleNamespace
+
+ROOT = Path(__file__).resolve().parents[2]
+SOURCE = "research/capped-phase-fusion/evidence/inplace_algebra_ultra/check_circuits.py"
+spec = importlib.util.spec_from_file_location("scalar", ROOT/"research/rational-unitary-fft/exact.py")
+module = importlib.util.module_from_spec(spec)
+spec.loader.exec_module(module)
+C = module.C
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+class Matrix(list):
+    def __init__(self, rows):
+        super().__init__([[x if isinstance(x,C) else C(x) for x in row] for row in rows])
+    @property
+    def T(self):
+        return Matrix(zip(*self))
+    def __getitem__(self, key):
+        if not isinstance(key,tuple):return super().__getitem__(key)
+        i,j = key
+        if isinstance(i,int) and isinstance(j,int):return super().__getitem__(i)[j]
+        return Matrix([row[j] for row in super().__getitem__(i)])
+    def __matmul__(self, other):return mul(self,other)
+    def __sub__(self, other):return Matrix([[x-y for x,y in zip(a,b)] for a,b in zip(self,other)])
+
+
+def eye(n):return Matrix([[int(i==j) for j in range(n)] for i in range(n)])
+
+
+def mul(a,b):
+    return Matrix([[sum((a[i][k]*b[k][j] for k in range(len(b))),C())
+                    for j in range(len(b[0]))] for i in range(len(a))])
+
+
+def inv(a):
+    n=len(a); rows=[list(x)+list(y) for x,y in zip(a,eye(n))]
+    for k in range(n):
+        pivot=next((i for i in range(k,n) if rows[i][k]!=0),None)
+        need(pivot is not None,"singular leading section")
+        rows[k],rows[pivot]=rows[pivot],rows[k]
+        q=rows[k][k];rows[k]=[x/q for x in rows[k]]
+        for i in range(n):
+            if i!=k:
+                q=rows[i][k];rows[i]=[x-q*y for x,y in zip(rows[i],rows[k])]
+    return Matrix([row[n:] for row in rows])
+
+
+def ldu(t):
+    n=len(t);a=Matrix(t);lo,di,up=eye(n),eye(n),eye(n)
+    for k in range(n):
+        pivot=a[k][k];need(pivot!=0,"singular leading section");di[k][k]=pivot
+        for j in range(k+1,n):up[k][j]=a[k][j]/pivot
+        for i in range(k+1,n):
+            lo[i][k]=a[i][k]/pivot
+            for j in range(k+1,n):a[i][j]=a[i][j]-lo[i][k]*a[k][j]
+    need(mul(mul(lo,di),up)==t,"independent LDU endpoint")
+    return lo,di,up
+
+
+def block(a,lo,hi):return Matrix([row[lo:hi] for row in a[lo:hi]])
+
+
+def embed(a,lo,n):
+    out=eye(n)
+    for i,row in enumerate(a):
+        for j,x in enumerate(row):out[lo+i][lo+j]=x
+    return out
+
+
+def envelope(a):
+    def mass(row):return sum((abs(x.re)+abs(x.im) for x in row),Q(0))
+    return max(max(map(mass,a)),max(map(mass,zip(*a))))
+
+
+def schur(t,a,b):
+    if a==0:return block(t,0,b)
+    return block(t,a,b)-mul(mul(Matrix([row[:a] for row in t[a:b]]),inv(block(t,0,a))),
+                            Matrix([row[a:b] for row in t[:a]]))
+
+
+def trees(a,b):
+    if b-a==1:return [(a,b,None,None)]
+    return [(a,b,l,r) for c in range(a+1,b) for l in trees(a,c) for r in trees(c,b)]
+
+
+def build(t,tree,atoms):
+    a,b,left,right=tree;n=len(t);m=schur(t,a,b)
+    lo,di,up=ldu(m)
+    node=dict(a=a,b=b,lo=lo,di=di,up=up)
+    if left is None:
+        token=("D",a,b);atoms.append((token,embed(m,a,n)))
+        node.update(ids={token},token=token,left=None,right=None)
+    else:
+        c=left[1];split=c-a
+        aa=block(m,0,split);bb=Matrix([row[split:] for row in m[:split]])
+        cc=Matrix([row[:split] for row in m[split:]])
+        k,h=mul(inv(aa),bb),mul(cc,inv(aa))
+        upper,lower=eye(n),eye(n)
+        for i in range(split):
+            for j in range(b-c):upper[a+i][c+j]=k[i][j]
+        for i in range(b-c):
+            for j in range(split):lower[c+i][a+j]=h[i][j]
+        rt,lt=("R",a,b),("L",a,b);atoms.append((rt,upper))
+        ln,rn=build(t,left,atoms),build(t,right,atoms)
+        atoms.append((lt,lower))
+        node.update(ids=ln['ids']|rn['ids']|{rt,lt},token=rt,left=ln,right=rn)
+        # Independently check the block endpoint quotient.
+        children=mul(embed(schur(t,a,c),a,n),embed(schur(t,c,b),c,n))
+        need(mul(mul(lower,children),upper)==embed(m,a,n),"ancestor Schur split endpoint")
+    return node
+
+
+def states(node):
+    if node['left'] is None:return [set(),set(node['ids'])]
+    return [set()]+[{node['token']}|a|b for a in states(node['left']) for b in states(node['right'])]+[set(node['ids'])]
+
+
+def collected(node,state,n,kind):
+    if kind=='lower' and node['ids']<=state:return embed(node['lo'],node['a'],n)
+    if kind=='upper' and (node['left'] is None or node['token'] not in state):
+        return embed(node['up'],node['a'],n)
+    if node['left'] is None:return eye(n)
+    return mul(collected(node['left'],state,n,kind),collected(node['right'],state,n,kind))
+
+
+def audit(t,selected_trees):
+    n=len(t);lo,di,up=ldu(t);li,ui=inv(lo),inv(up)
+    lam=max(Q(1),envelope(t));q=max(Q(1),*(envelope(inv(block(t,0,k))) for k in range(1,n+1)))
+    chi=lam*q;u0=lam+lam*lam*q
+    need(mul(mul(di,up),inv(t))==li and mul(mul(inv(t),lo),di)==ui,"global inverse factor order")
+    for k in range(1,n):
+        right=mul(inv(block(t,0,k)),Matrix([row[k:] for row in t[:k]]))
+        lower=mul(Matrix([row[:k] for row in t[k:]]),inv(block(t,0,k)))
+        need(right[-1]==up[k-1][k:],"original last-row solve")
+        need([row[-1] for row in lower]==[row[k-1] for row in lo[k:]],"original last-column solve")
+        need(sum((x.norm2() for x in right[-1]),Q(0))<=chi*chi,"upper tail Euclidean budget")
+        need(sum((row[-1].norm2() for row in lower),Q(0))<=chi*chi,"lower tail Euclidean budget")
+    count=mixed=0;noncommuting=False
+    for tree in selected_trees:
+        atoms=[];node=build(t,tree,atoms)
+        def restrictions(v):
+            a,b=v['a'],v['b']
+            need((v['lo'],v['di'],v['up'])==(block(lo,a,b),block(di,a,b),block(up,a,b)),"global factor restriction")
+            need(inv(v['lo'])==block(li,a,b) and inv(v['up'])==block(ui,a,b),"contiguous inverse restriction")
+            if v['left'] is not None:restrictions(v['left']);restrictions(v['right'])
+        restrictions(node)
+        for state in states(node):
+            endpoint=eye(n)
+            for token,a in atoms:
+                if token in state:endpoint=mul(a,endpoint)
+            lc,uf=collected(node,state,n,'lower'),collected(node,state,n,'upper')
+            dpart=eye(n)
+            for k in range(n):
+                if ('D',k,k+1) in state:dpart[k][k]=di[k][k]
+            rhs=mul(mul(mul(lc,dpart),inv(uf)),up)
+            need(endpoint==rhs,"noncommuting frontier order")
+            need(inv(endpoint)==mul(mul(mul(ui,uf),inv(dpart)),inv(lc)),"downset inverse order")
+            # Spectral norm squared <= norm_1 * norm_inf <= envelope^2.
+            # The exact radical-free common theorem bound squared is 1024 N^3 chi^16.
+            need(max(envelope(endpoint)**2,envelope(inv(endpoint))**2)<=1024*n**3*chi**16,
+                 "completed downset common norm budget")
+            noncommuting |= endpoint!=mul(mul(mul(lc,dpart),up),inv(uf))
+            mixed += int(lc!=eye(n) and uf!=eye(n))
+            count+=1
+    return dict(n=n,trees=len(selected_trees),downsets=count,mixed_lower_frontier=mixed),noncommuting
+
+
+def source_binding(t):
+    n=len(t);tree=ast.parse((ROOT/SOURCE).read_bytes())
+    defs=[copy.deepcopy(x) for x in tree.body if isinstance(x,ast.FunctionDef) and x.name in {'full_plan','parallel'}]
+    need(len(defs)==2,"retained structural function selection")
+    def diagonal(ids,values):
+        a=eye(n)
+        for i,v in zip(ids,values):a[i][i]=v
+        return [[a]]
+    def shear(target,source,k):
+        a=eye(n)
+        for i,x in enumerate(target):
+            for j,y in enumerate(source):a[x][y]=k[i][j]
+        return [[a]]
+    env=dict(STATS={'full_nodes':0},diag=diagonal,lowdisp_shear=shear,
+             np=SimpleNamespace(linalg=SimpleNamespace(solve=lambda a,b:mul(inv(a),b))))
+    mod=ast.Module(body=defs,type_ignores=[]);ast.fix_missing_locations(mod)
+    exec(compile(mod,'<retained full_plan algebra only>','exec',optimize=0),env)
+    plan=env['full_plan'](list(range(n)),t);endpoint=eye(n)
+    for layer in plan:
+        for a in layer:endpoint=mul(a,endpoint)
+    need(endpoint==t,"retained compiler algebra binding")
+    return sum(map(len,plan))
+
+
+def reject(call,text):
+    try:call()
+    except ValueError as exc:need(text in str(exc),'unexpected control failure')
+    else:raise ValueError('missed control: '+text)
+
+
+def main():
+    results=[];wrong_order=False
+    for n in (1,3,4,5):
+        t=Matrix([[C(2+Q(i,5),Q(i+1,17)) if i==j else C(Q(i+2*j+1,41),Q(i-j,37))
+                   for j in range(n)] for i in range(n)])
+        choices=trees(0,n)
+        if n==5:choices=[choices[0],choices[len(choices)//2],choices[-1]]
+        result,wrong=audit(t,choices);results.append(result);wrong_order|=wrong
+        if n==4:source_atoms=source_binding(t)
+    need(wrong_order,"wrong frontier order discriminated")
+    bad=Matrix([[0,1],[1,0]]);need(mul(bad,inv(bad))==eye(2),'full endpoint invertible control')
+    reject(lambda:ldu(bad),'singular leading section')
+    u=Matrix([[1,1,0],[0,1,1],[0,0,1]])
+    sub=lambda a:Matrix([[a[i][j] for j in (0,2)] for i in (0,2)])
+    need(inv(sub(u))!=sub(inv(u)),"noncontiguous inverse restriction rejected")
+    t=Matrix([[Q(1,64),1],[1,0]])
+    need(max(envelope(t),envelope(inv(t)))<=2 and envelope(ldu(t)[2])>32,
+         "full inverse alone cannot bound shear")
+    a=Matrix([[C(1,1),1],[2,C(3,-1)]])
+    row=Matrix([[C(1,2),C(2,-1)]])
+    correct=mul(row,inv(a))
+    adjoint=Matrix([[x.conjugate() for x in r] for r in a.T])
+    wrong=mul(inv(adjoint),row.T).T  # Unmatched adjoint in the source's ordinary right solve.
+    need(correct!=wrong,"wrong complex adjoint discriminated")
+    need(any(r['mixed_lower_frontier'] for r in results),'mixed completed/frontier states covered')
+    print(json.dumps(dict(cases=results,source_algebra_atoms=source_atoms,controls=5),sort_keys=True))
+    print('PASS_LEADING_SECTION_DOWNSET_AUDIT arbitrary_interval_tree scoped_proof no_new_kappa')
+
+
+if __name__=='__main__':main()