[application][P2] Deco inverse words and adjacent-label swap realization

[PerAlexandersson]

Parent: #777
Depends on: normalized-code core child of #777
Roadmap parent: #697

Goal

Define the all-rank inverse word attached to a chronological deco code, using either a checked right-inversion-vector decoder or the equivalent recursive insertion API. Prove:

• the normal (0,2) and exceptional (1,0) two-step extensions have the displayed inverse-word forms;
• replacing one eligible normalized pair by an exceptional pair swaps exactly the adjacent final labels h-j and h-j+1;
• later construction steps transport that swap to the claimed final labels;
• simultaneous selected replacements equal the product of the corresponding swaps;
• eligible-pair non-overlap gives disjoint supports and hence commutation;
• the comparison word/descent positions are unchanged.

The theorem must use chronological one-based start j, with 3 ≤ j < h.

Suggested ownership

Create RealRooted/Applications/OEIS/A144438/InverseWord.lean. Depend on the normalized-code module; do not edit it or the polynomial-factorization modules.

Boundaries

Do not prove the descent-bottom monomial orbit sum or stability here. Finite evaluation examples may be tests but are not the all-rank proof.

Acceptance

• Checked decoder or recursive inverse-word construction.
• Single-pair and finite selected-pair swap witnesses.
• Checked commutation/disjoint-support and 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]

Dependency checkpoint #786 is complete at 9321f396. The generic insertion decoder now proves the exact (0,2)/(1,0) local forms and transports their 1↔2 swap through any later suffix to the final adjacent labels.

The remaining #783 work is now application-local: identify DecoCode.inverseWord with this decoder, split the chronological code around an eligible one-based start, lift the single-pair theorem to finite nonoverlapping decorations, prove support disjointness/commutation, and establish comparison-word invariance.

[PerAlexandersson]

Dependency checkpoint #787 is complete at c7f9ccf2. Every bounded chronological DecoCode now has a checked all-rank inverse-word decoder, and the decoder has an exact prefix / two selected entries / suffix theorem around any chronological start.

The next small boundary is now purely local: specialize the generic #786 (0,2) ↔ (1,0) swap theorem at one eligible start, simplify the suffix length to final one-based labels h-j and h-j+1, and prove the corresponding comparison word is unchanged. Finite nonoverlapping decorations and commutation follow in the subsequent checkpoint.

[PerAlexandersson]

Child #788 is complete at 7c75835: one eligible Deco pair has an exact final adjacent-label swap theorem and a checked inverse-word comparison/descent-word invariance theorem. The remaining bounded child is #789, lifting this to finite nonoverlapping decorations with swap commutation.

[PerAlexandersson]

Completed through #786, #787, #788, and #789, culminating in e8d0bb9. The all-rank decoder, displayed pair forms, later-step swap transport, exact singleton and finite selected-pair swap identities, disjoint-support commutation, and full comparison/descent-word invariance are all checked. This leaves sibling #785 as the next normalized-fiber polynomial/stability assembly boundary.