Phase 5B consolidated report

Equations in these preserved Markdown records retain their TeX notation where present; this is not a newly typeset proof edition.

Structured Factorization Phase 5B master report

Date: 2026-09-29. Primary decision: D. MATHEMATICAL NOTE SURVIVES; ALGORITHMIC NO-GO.

The frozen Phase 4/5 record reproduced, and a real PySDD + persistent Glucose4 exact pipeline now works. The new bounded pilot ran 2,100 trials with 0 failures/timeouts and no correctness disagreement. Against validation-selected B3, the primary carrier+defect+exposure method M5 had a paired geometric total-runtime ratio 2.212 (95% descriptive interval [2.008, 2.428]). Runtime and practical residual-work criteria are respectively FAIL and FAIL. This is a maintained-tool small-instance campaign, not industrial-scale validation.

What is mathematically proved

Under their explicit nonfalse, compression, support-disjointness and essentiality hypotheses, the frozen compressed-SDD cut/exposure theorem, exposure optimum, laminar carrier obstruction, defect-support crossing lemma, equality-family localization obstruction, positive irredundant-CNF baseline and CM read-once recursion survive independent proof review. A new application note proves sound inclusion-minimal support shrinking and a group-deletion oracle-query bound. These do not imply minimum-cardinality support, FPT SAT runtime, efficient global vtree search or novel priority.

One prose claim is corrected: an externally certified prime-aligned tree needs no residual search, but an ordinary solver cannot infer primeness from a failed vtree cut. Every nonsingleton exposed block is exact-refined in this implementation, including the oracle tree. This correction is in the new ledger; historical files are unchanged.

What is computationally reproduced

All six frozen campaigns and eleven archived artifacts match, excluding only timing/newline differences. Independent checks cover 458,745 cuts, 983,025 n=4 function/vtree pairs, 121,500 n=5 score calls and all 540 seeded n=5 inputs. Key counts remain 2,601 decomposable n=4 functions, fixed-tree full exposure 225, and exhaustive exposure optimum correct on all 65,535 nonfalse functions. Real-backend tests add 903 SDD compilations, 113 minimizations, 881 direct/semantic/carrier comparisons each and 1,390 SAT cuts, all with zero discrepancies.

What is newly observed

Actual SDD element/node sizes, Glucose conflicts/decisions/propagations, wall times and process memory are now measured. The primary 70-instance/ten-method/three-repetition experiment freezes inputs and code, excludes oracle truth from all heuristic payloads, and charges recompilation/probe/refinement overhead. The held-out results and separate move/SAT-reuse diagnostics are recorded with full machine-readable data. The actual runtime conclusion is specific to this implementation and synthetic generator mix.

What is prior art

Dynamic vtree rotations/swaps, SDD size minimization, graph/treewidth/hypergraph compilation, component decomposition, SAT/QBF bi-decomposition, Cartesian relation factorization, and monotone-predicate minimization all have substantial antecedents. The current audit includes 2025–2026 circuit-aware, semantic-vtree and alternative-representation work. No firstness claim is supported by absence from a web search.

What failed and what remains open

The registered primary improvement gate was not cleared, and there is no practically meaningful residual-work rescue. Do not develop an algorithm paper around a post-hoc metric switch. Universal pairwise defect localization remains refuted. No efficient exposure-optimal search theorem, general small-support guarantee, unrestricted structured-d-DNNF extraction theorem or industrial runtime improvement is established. Native integration of alternative objectives is untested; the current custom search pays full recompilation costs. Carrier-compatible early residual refinement could avoid work done by the current semantic-first/final-LCC variant.

Review and publication posture

Six internal reviewer roles cover SDD, SAT/decomposition, graph/vtree, engineering/statistics, novelty and mathematics. They found and prompted provenance safeguards and the exposed-factor/prime-certificate correction, and imposed explicit limits on the relabeling-heavy tiny benchmark, modest graph baseline and biased candidate prefix. Full findings and dispositions are preserved. This is internal adversarial review, not external peer review.

The proofs survive as a mathematical working note and the implementation as a reproducibility artifact. Publication-ready novelty is not established. A new LaTeX paper is deliberately not produced: the requested condition that a surviving contribution warrant one is not met after the current priority review. Archived theorem drafts remain preserved verbatim. Keep theorem validity, computational evidence, prior art and conjectures separate.

The submitted 117-file archive remains unchanged. The complete deliverable includes it beside this new output, plus code, lockfile, inputs/seeds, all principal logs/results, theorem/priority updates, research/review ledgers, reproducibility commands, checksums and the next gate.