[application][P2] Deco normalized-code fibers and stable product factorization

[PerAlexandersson]

Parent roadmap: #697

Independent of the exact-layer implementation except for shared deco code definitions.

Goal

Define normalized deco construction codes, eligible disjoint adjacent (0,2) pairs, subset decoration back to (1,0), the resulting inverse words, and descent-bottom monomials. Prove that each selected pair acts by the stated adjacent final-label swap, that the swaps commute because their supports are disjoint, and that the complete fiber polynomial factors into a monomial, a power of two, and factors

u_(h-j) + u_(h-j+1).

Conclude MvRealStable for every normalized fiber. If it does not materially enlarge the proof, retain independent nonnegative pair weights.

Boundaries

Do not infer stability of the sum over normalized codes. Finite enumeration may test definitions but is not proof.

Acceptance

• Exact definitions and all-rank word/swap identities.
• Checked fiber factorization and MvRealStable witness.
• No sorry, admit, new axiom, statement-only substitute, or prohibited tactic.
• Focused and full builds plus proof-status and axiom audits pass.

[PerAlexandersson]

Split into proof-natural, non-overlapping implementation issues after checking the current manuscript and executable reference model:

• [application][P1] Deco chronological normalized-code core #782 — chronological normalized-code core, including the crucial distinction between chronological eligible (0,2) pairs and transported minimum-insertion (0,1) occurrences;
• [application][P2] Deco inverse words and adjacent-label swap realization #783 — inverse-word construction and adjacent final-label swap realization (depends on [application][P1] Deco chronological normalized-code core #782);
• [foundation][P1] Boolean orbit factorization for disjoint variable swaps #784 — reusable Boolean orbit factorization for disjoint variable swaps, with a real-stability corollary (independent foundation lane);
• [application][P2] Assemble Deco normalized fiber factorization and stability #785 — descent-bottom fiber polynomial, exact factorization, and MvRealStable assembly (depends on [application][P1] Deco chronological normalized-code core #782, [application][P2] Deco inverse words and adjacent-label swap realization #783, [foundation][P1] Boolean orbit factorization for disjoint variable swaps #784).

#777 remains the umbrella and should close only after all four children are checked. #778 remains separate: it owns the global partition/sum identities and no claim that arbitrary sums of stable fibers are stable.

[PerAlexandersson]

Progress: #782 is now closed by checked commit 8e32f772. The remaining children are #783 (inverse-word swaps), #784 (generic Boolean swap-orbit factorization), and #785 (Deco polynomial/stability assembly).

[PerAlexandersson]

Foundation progress: #784 is complete at checked commit 658e3c2f. The library now has exact one-swap support classification, exact finite Boolean choice-sum/product factorization (including inactive powers of two), and checked multivariate real-stability witnesses.

The remaining dependency chain for this umbrella is now:

1. [application][P2] Deco inverse words and adjacent-label swap realization #783: construct inverse words and prove eligible chronological decorations realize independent adjacent-label choices;
2. [application][P2] Assemble Deco normalized fiber factorization and stability #785: identify each normalized Deco fiber polynomial with the [foundation][P1] Boolean orbit factorization for disjoint variable swaps #784 normal form and conclude stability;
3. [application][P3] Deco layer and fiber partition identities #778: assemble the global partition identities separately.

No Smirnov work is active; the feature-branch name is historical.

[PerAlexandersson]

The inverse-word realization child #783 is complete through e8d0bb9 (#786--#789). Every finite normalized-code decoration is now identified with its commuting adjacent-label swap orbit and preserves the inverse comparison word. The next remaining child is #785: define the descent-bottom monomial/fiber sum, identify it with the generic Boolean swap orbit, and conclude fiberwise multivariate stability.