[application][P1] Finite Deco decoration swap orbit and commutation

[PerAlexandersson]

Parent: #783
Depends on: #788
Roadmap parent: #697

Goal

Lift the single eligible-pair theorem to every finite DecoNormalizedCode.Decoration.

Prove that selected starts have pairwise disjoint final adjacent-label supports, hence their transpositions commute. Package a deterministic finite swap action and prove that the inverse word of D.exceptionalize is exactly the corresponding product of swaps applied to the normalized inverse word. Derive comparison-word invariance for every decoration.

Boundaries

Do not form the descent-bottom monomial orbit sum or prove stability; #785 owns that assembly.

Acceptance

• Checked disjoint-support and commutation witnesses.
• Checked finite simultaneous-decoration inverse-word equality.
• Checked comparison-word invariance.
• No sorry, admit, new axiom, statement-only substitute, or prohibited tactic.
• Focused and full builds plus proof-status and axiom audits pass.

[PerAlexandersson]

Completed in e8d0bb9 on the existing feature lane. The new DecorationOrbit module proves disjoint final-label support for distinct eligible starts, pointwise and word-level swap commutation, a deterministic finite swap action, the exact simultaneous-decoration inverse-word identity, and comparison-word invariance for every decoration. InverseWord now exposes generic checked two-code (0,2) to (1,0) replacement bridges reused by both singleton and finite proofs. Verification: focused 619/619; RealRooted.Production 9768/9768; full workspace 9890 jobs; all repository guards pass at budgets 1332/1211. Fifteen representative witnesses use only propext, Classical.choice, and Quot.sound.