[application][P1] Single Deco eligible-pair inverse-word swap

[PerAlexandersson]

Parent: #783
Depends on: #782, #786, #787
Roadmap parent: #697

Goal

Prove the single eligible-pair inverse-word theorem for a normalized chronological Deco code.

For a one-based eligible start j with 3 ≤ j < h, compare the normalized pair (0,2) with the singleton exceptional decoration (1,0). Prove that the resulting inverse word is obtained by swapping exactly the final adjacent labels h-j and h-j+1.

Add a family-neutral comparison-word definition for positive integer words and the minimal insertion lemmas needed to prove that the normal and exceptional inverse words have identical ascent/descent comparison words after every common suffix.

Placement

Extend RealRooted/Applications/OEIS/A144438/InverseWord.lean; place genuinely reusable word-comparison lemmas in RealRooted/Combinatorics/MinimumInsertionWord.lean or a focused sibling if that keeps dependencies smaller.

Boundaries

Do not prove simultaneous finite decorations, orbit sums, descent-bottom monomial identities, or stability. Those remain in #783/#785.

Acceptance

• Checked singleton-decoration code theorem.
• Checked final adjacent-label swap with the stated one-based indexing.
• Checked equality of full comparison words.
• 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 7c75835 on the existing feature lane. Checked witnesses now construct singleton eligible decorations, prove exact unchanged code prefixes/suffixes, identify the resulting all-rank inverse word with the normalized inverse word under the adjacent label swap h-(j+1) <-> h-j, and prove equality of the full ascent/descent comparison word. The reusable minimum-insertion layer now includes suffix validity plus comparison-word preservation under valid common suffix decoding. Verification: focused builds 471/471 and 618/618; RealRooted.Production 9767/9767; full workspace 9889 jobs; root-import, import-architecture/self-test, tactic-coverage, proof-status/self-test, forbidden-token, line-length, and diff guards pass at budgets 1331/1210. A 12-witness axiom audit reports only propext, Classical.choice, and Quot.sound.