[application][P2] Assemble Deco normalized fiber factorization and stability

[PerAlexandersson]

Parent: #777
Depends on: the normalized-code core, inverse-word swap realization, and Boolean swap-orbit factorization children of #777
Roadmap parent: #697

Goal

Define the descent-bottom monomial of a Deco inverse word and the complete polynomial of one normalized-code fiber. Combine the checked word/swap theorem with the generic Boolean orbit factorization to prove the exact factorization into a monomial, a power of two, and factors

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

Conclude a checked MvRealStable witness for every normalized fiber. Include the height-six normalized code (0,0,0,2,0,2) as a verified example only if it stays small.

Suggested ownership

Create RealRooted/Applications/OEIS/A144438/NormalizedFiber.lean. Do not edit prerequisite modules except for narrowly reviewed API fixes.

Boundaries

Do not infer stability of the sum over normalized codes. Do not prove the global partition or equality with the recurrence-defined total; those belong to #778.

Acceptance

• Exact descent-bottom monomial and fiber-sum definitions.
• Checked factorization equality.
• Checked all-rank MvRealStable theorem for each normalized fiber.
• Optional independent nonnegative pair weights only if already supported by the foundation theorem.
• No sorry, admit, new axiom, statement-only substitute, or prohibited tactic.
• Focused and full builds plus proof-status and axiom audits pass.

[PerAlexandersson]

Decomposed into bounded children after #783 closed: #790 owns the reusable comparison-bottom support/monomial and relabeling equivariance foundation; #791 owns the Deco-specific eligible left-label/right-label classification and fixed support; #792 owns only the finite fiber sum, Boolean factorization, and stability assembly. Work proceeds in that dependency order.

[PerAlexandersson]

Child #790 is complete at 34b8f63. The reusable descent-bottom support and squarefree monomial now have checked minimum-insertion nodup semantics and comparison-preserving relabeling equivariance. Next is #791, classifying the two final labels attached to every eligible normalized Deco pair.

[PerAlexandersson]

Child #791 is complete at f8eb647. The corrected active/inactive endpoint classification is now checked; #792 is the sole remaining child and owns the exact decoration sum, Boolean factorization (including inactive multiplicity), and fiberwise stability.