Words, the definitional factorial ledger, and word-level collapse

PAPER_MAP node D-ledger for Deng–Shen (arXiv:2607.10105), implementing the pure word model of DESIGN §5.5: all §5.4 permutation sums with multiplicities ((5.15), (5.33)) are stated as sums over word maps w : Fin M → α with prescribed fiber sizes (validWords), never over labeled copies.

• Anderson4D.validWords, Anderson4D.inducedWord — admissible words and the word induced by a labeled arrangement σ : Fin M ≃ Σ a, Fin (mult a).
• Anderson4D.card_arrangements_fiber, Anderson4D.ledger_sum — a valid word is induced by exactly ∏ a, (mult a)! labeled arrangements, so any statistic summed over labeled arrangements equals ∏ a, (mult a)! times its sum over valid words.
• Anderson4D.wordSum, Anderson4D.paperSum — the definitional ledger paperSum mult F := (∏ a, ((mult a)! : ℝ)) * wordSum mult F; statements of P-5.7/P-5.9/P-5.10 put paperSum on the left-hand side, and paperSum_eq_sum_arrangements converts at statement boundaries.
• Anderson4D.NoAdjacentEqual — the "no adjacent equal letters" side condition of (5.15)/(5.33), with a decidability instance.
• Anderson4D.wordCollapseEquiv — the §5.4.1 collapse as an honest word-level Equiv: a word over A ⊕ B is the same data as its nonempty blocks (maximal runs of inside letters) plus its collapsed word over Unit ⊕ B with markers pairwise non-adjacent and marker count = block count. Letter counts transport (count_inl_collapse, count_inr_collapse).
• Anderson4D.wordSumFiltered, Anderson4D.paperSumFiltered — restricted sums over words satisfying a side condition, with monotonicity for nonnegative F.

This is the stable word carrier used by the permutation-sum formalization.

The word-level collapse equivalence

def Anderson4D.NoTwoAdjacentMarkers {B : Type u_2} (s : List (Unit ⊕ B)) : Prop

No two adjacent letters of s are both markers (Sum.inl _). This expresses that the marked positions come from maximal runs of inside letters.

Equations

• Anderson4D.NoTwoAdjacentMarkers s = List.IsChain (fun (x y : Unit ⊕ B) => x.isLeft = false ∨ y.isLeft = false) s

def Anderson4D.markerCount {B : Type u_2} (s : List (Unit ⊕ B)) : ℕ

The number of markers in a collapsed word. Stated via countP Sum.isLeft so that no decidable equality on B is needed; see markerCount_eq_count for the version with List.count (Sum.inl ()).

Equations

• Anderson4D.markerCount s = List.countP (fun (x : Unit ⊕ B) => x.isLeft) s

def Anderson4D.collapse {A : Type u_1} {B : Type u_2} : List (A ⊕ B) → List (List A) × List (Unit ⊕ B)

Collapse a word into its list of blocks (maximal runs of inside letters) and its collapsed word (each maximal run replaced by one marker Sum.inl ()).

Equations

• Anderson4D.collapse [] = ([], [])
• Anderson4D.collapse (Sum.inr b :: w) = ((Anderson4D.collapse w).1, Sum.inr b :: (Anderson4D.collapse w).2)
• Anderson4D.collapse [Sum.inl a] = ([[a]], [Sum.inl ()])
• Anderson4D.collapse (Sum.inl a :: Sum.inl a' :: w) = (List.modifyHead (fun (x : List A) => a :: x) (Anderson4D.collapse (Sum.inl a' :: w)).1, (Anderson4D.collapse (Sum.inl a' :: w)).2)
• Anderson4D.collapse (Sum.inl a :: Sum.inr b :: w) = ([a] :: (Anderson4D.collapse (Sum.inr b :: w)).1, Sum.inl () :: (Anderson4D.collapse (Sum.inr b :: w)).2)

def Anderson4D.expand {A : Type u_1} {B : Type u_2} : List (List A) → List (Unit ⊕ B) → List (A ⊕ B)

Substitute the i-th block for the i-th marker (in order): the inverse of collapse. On inputs violating the block/marker bookkeeping it silently drops the offending data; such inputs are excluded by the subtype in wordCollapseEquiv.

Equations

• Anderson4D.expand x✝ [] = []
• Anderson4D.expand x✝ (Sum.inr b :: s) = Sum.inr b :: Anderson4D.expand x✝ s
• Anderson4D.expand [] (Sum.inl val :: s) = Anderson4D.expand [] s
• Anderson4D.expand (blk :: bs) (Sum.inl val :: s) = List.map Sum.inl blk ++ Anderson4D.expand bs s

Small facts about NoTwoAdjacentMarkers

theorem Anderson4D.nta_nil {B : Type u_2} : NoTwoAdjacentMarkers []

theorem Anderson4D.nta_cons_inr {B : Type u_2} {s : List (Unit ⊕ B)} (b : B) (h : NoTwoAdjacentMarkers s) : NoTwoAdjacentMarkers (Sum.inr b :: s)

theorem Anderson4D.nta_inl_cons_inr {B : Type u_2} {s : List (Unit ⊕ B)} (u : Unit) (b : B) (h : NoTwoAdjacentMarkers (Sum.inr b :: s)) : NoTwoAdjacentMarkers (Sum.inl u :: Sum.inr b :: s)

theorem Anderson4D.nta_of_cons {B : Type u_2} {x : Unit ⊕ B} {s : List (Unit ⊕ B)} (h : NoTwoAdjacentMarkers (x :: s)) : NoTwoAdjacentMarkers s

theorem Anderson4D.nta_marker_head {B : Type u_2} {u : Unit} {y : Unit ⊕ B} {s : List (Unit ⊕ B)} (h : NoTwoAdjacentMarkers (Sum.inl u :: y :: s)) : ∃ (b : B), y = Sum.inr b

After a marker, the next letter (if any) is an outside letter.

Structure of collapse

theorem Anderson4D.collapse_inl_cons {A : Type u_1} {B : Type u_2} (w : List (A ⊕ B)) (a : A) : ∃ (tl : List A) (bs : List (List A)) (s : List (Unit ⊕ B)), collapse (Sum.inl a :: w) = ((a :: tl) :: bs, Sum.inl () :: s)

A word starting with an inside letter collapses to a first block starting with that letter and a collapsed word starting with a marker.

theorem Anderson4D.collapse_inlRun_append {A : Type u_1} {B : Type u_2} (as : List A) (a : A) (w : List (A ⊕ B)) (hw : w = [] ∨ ∃ (b : B) (w' : List (A ⊕ B)), w = Sum.inr b :: w') : collapse (List.map Sum.inl (a :: as) ++ w) = ((a :: as) :: (collapse w).1, Sum.inl () :: (collapse w).2)

Collapsing a nonempty inside run prepended to a word that does not start with an inside letter: the run becomes the first block and contributes one marker.

theorem Anderson4D.expand_shape {A : Type u_1} {B : Type u_2} (bs : List (List A)) (s : List (Unit ⊕ B)) (hs : s = [] ∨ ∃ (b : B) (s' : List (Unit ⊕ B)), s = Sum.inr b :: s') : expand bs s = [] ∨ ∃ (b : B) (w' : List (A ⊕ B)), expand bs s = Sum.inr b :: w'

expand never produces a word starting with an inside letter, provided the collapsed word does not start with a marker.

theorem Anderson4D.collapse_spec {A : Type u_1} {B : Type u_2} (w : List (A ⊕ B)) : (∀ blk ∈ (collapse w).1, blk ≠ []) ∧ markerCount (collapse w).2 = (collapse w).1.length ∧ NoTwoAdjacentMarkers (collapse w).2

The three structural invariants of a collapsed word: all blocks are nonempty, the marker count equals the block count, and no two markers are adjacent.

theorem Anderson4D.collapse_expand {A : Type u_1} {B : Type u_2} (s : List (Unit ⊕ B)) (bs : List (List A)) (hbs : ∀ blk ∈ bs, blk ≠ []) (hlen : markerCount s = bs.length) (hnta : NoTwoAdjacentMarkers s) : collapse (expand bs s) = (bs, s)

Right inverse: collapsing an expansion recovers the block/marker data.

theorem Anderson4D.expand_collapse {A : Type u_1} {B : Type u_2} (w : List (A ⊕ B)) : expand (collapse w).1 (collapse w).2 = w

Left inverse: expanding the collapse of a word recovers the word.

def Anderson4D.wordCollapseEquiv (A : Type u_3) (B : Type u_4) : List (A ⊕ B) ≃ { p : List (List A) × List (Unit ⊕ B) // (∀ blk ∈ p.1, blk ≠ []) ∧ markerCount p.2 = p.1.length ∧ NoTwoAdjacentMarkers p.2 }

Word-level collapse equivalence (§5.4.1 collapse, DESIGN §5.5). A word over A ⊕ B is the same data as a list of nonempty blocks over A together with a collapsed word over Unit ⊕ B whose marker count equals the number of blocks and in which no two markers are adjacent. The forward map is collapse; the inverse substitutes the i-th block for the i-th marker.

Equations

• One or more equations did not get rendered due to their size.

Letter-count transport

Mathlib's Sum.instBEq currently has no LawfulBEq instance, so we first record how == computes on constructors; this lets simp normalize List.count on sum types.

@[simp]

theorem Anderson4D.inl_beq_inl {A : Type u_1} {B : Type u_2} [BEq A] [BEq B] (a a' : A) : (Sum.inl a == Sum.inl a') = (a == a')

@[simp]

theorem Anderson4D.inr_beq_inr {A : Type u_1} {B : Type u_2} [BEq A] [BEq B] (b b' : B) : (Sum.inr b == Sum.inr b') = (b == b')

@[simp]

theorem Anderson4D.inl_beq_inr {A : Type u_1} {B : Type u_2} [BEq A] [BEq B] (a : A) (b : B) : (Sum.inl a == Sum.inr b) = false

@[simp]

theorem Anderson4D.inr_beq_inl {A : Type u_1} {B : Type u_2} [BEq A] [BEq B] (a : A) (b : B) : (Sum.inr b == Sum.inl a) = false

theorem Anderson4D.markerCount_eq_count {B : Type u_2} [DecidableEq B] (s : List (Unit ⊕ B)) : markerCount s = List.count (Sum.inl ()) s

With decidable equality available, markerCount is the count of the marker letter.

theorem Anderson4D.count_inl_collapse {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] (a : A) (w : List (A ⊕ B)) : List.count (Sum.inl a) w = (List.map (fun (blk : List A) => List.count a blk) (collapse w).1).sum

Inside-letter counts sum over the blocks of the collapse.

theorem Anderson4D.count_inr_collapse {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] (b : B) (w : List (A ⊕ B)) : List.count (Sum.inr b) w = List.count (Sum.inr b) (collapse w).2

Outside-letter counts are preserved by the collapse.

Concrete sanity checks (A := Bool, B := Fin 2)

The factorial ledger

def Anderson4D.sigmaFstFiber {ι : Type u_3} {β : ι → Type u_4} (a : ι) : { x : (i : ι) × β i // x.fst = a } ≃ β a

The fiber of a sigma type over a point a of the base.

Equations

• Anderson4D.sigmaFstFiber a = { toFun := fun (x : { x : (i : ι) × β i // x.fst = a }) => ⋯ ▸ (↑x).snd, invFun := fun (y : β a) => ⟨⟨a, y⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def Anderson4D.inducedWord {α : Type u_3} {M : ℕ} (mult : α → ℕ) (σ : Fin M ≃ (a : α) × Fin (mult a)) : Fin M → α

The word induced by a labeled arrangement: forget the labels.

Equations

• Anderson4D.inducedWord mult σ j = (σ j).fst

def Anderson4D.toFiberEquiv {α : Type u_3} {M : ℕ} (mult : α → ℕ) (w : Fin M → α) (σ : Fin M ≃ (a : α) × Fin (mult a)) (hσ : ∀ (j : Fin M), (σ j).fst = w j) (a : α) : { j : Fin M // w j = a } ≃ Fin (mult a)

The family of fiber bijections extracted from a labeled arrangement inducing w.

Equations

• Anderson4D.toFiberEquiv mult w σ hσ a = (σ.subtypeEquiv ⋯).trans (Anderson4D.sigmaFstFiber a)

def Anderson4D.arrangementEquivFiberEquivs {α : Type u_3} {M : ℕ} (mult : α → ℕ) (w : Fin M → α) : { σ : Fin M ≃ (a : α) × Fin (mult a) // ∀ (j : Fin M), (σ j).fst = w j } ≃ ((a : α) → { j : Fin M // w j = a } ≃ Fin (mult a))

A labeled arrangement inducing the word w is the same data as a family of bijections from the fibers of w to the multiplicity index sets.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.card_arrangements_fiber {α : Type u_3} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) (w : Fin M → α) (hw : ∀ (a : α), {j : Fin M | w j = a}.card = mult a) : Fintype.card { σ : Fin M ≃ (a : α) × Fin (mult a) // ∀ (j : Fin M), (σ j).fst = w j } = ∏ a : α, (mult a).factorial

Fiber-count lemma. A word w with the fiber condition #{j | w j = a} = mult a is induced by exactly ∏ a, (mult a)! labeled arrangements: the (mult a)! relabelings within each letter fiber act freely and transitively.

theorem Anderson4D.inducedWord_fiber_card {α : Type u_3} [DecidableEq α] {M : ℕ} (mult : α → ℕ) (σ : Fin M ≃ (a : α) × Fin (mult a)) (a : α) : {j : Fin M | inducedWord mult σ j = a}.card = mult a

Every induced word satisfies the fiber condition.

def Anderson4D.validWords {α : Type u_3} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) : Finset (Fin M → α)

The words Fin M → α satisfying the fiber condition for mult: DESIGN §5.5's admissible words with prescribed letter multiplicities (paper (5.15), (5.33)).

Equations

• Anderson4D.validWords mult = {w : Fin M → α | ∀ (a : α), {j : Fin M | w j = a}.card = mult a}

theorem Anderson4D.inducedWord_mem_validWords {α : Type u_3} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) (σ : Fin M ≃ (a : α) × Fin (mult a)) : inducedWord mult σ ∈ validWords mult

theorem Anderson4D.card_arrangements_inducing {α : Type u_3} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) {w : Fin M → α} (hw : w ∈ validWords mult) : {σ : Fin M ≃ (a : α) × Fin (mult a) | inducedWord mult σ = w}.card = ∏ a : α, (mult a).factorial

Finset.filter form of the fiber-count lemma: the labeled arrangements inducing a fixed valid word w number exactly ∏ a, (mult a)!.

theorem Anderson4D.ledger_sum {α : Type u_3} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) (F : (Fin M → α) → ℕ) : ∑ σ : Fin M ≃ (a : α) × Fin (mult a), F (inducedWord mult σ) = (∏ a : α, (mult a).factorial) * ∑ w ∈ validWords mult, F w

Factorial ledger (ℕ-valued statistics). Summing any word statistic over all labeled arrangements counts each admissible word exactly ∏ a, (mult a)! times. (This is where the (s+1)!⁻¹ of (5.45)(i) comes from: it cancels the ledger factor, and is not produced by the collapse itself.)

theorem Anderson4D.ledger_sum_real {α : Type u_3} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) (F : (Fin M → α) → ℝ) : ∑ σ : Fin M ≃ (a : α) × Fin (mult a), F (inducedWord mult σ) = (∏ a : α, ↑(mult a).factorial) * ∑ w ∈ validWords mult, F w

Factorial ledger, real-valued form: the version consumed by the analytic estimates (the statistics of §5.4 are real).

The definitional ledger

paperSum is defined as ∏ a, (mult a)! times the raw word sum. Statements of P-5.7, P-5.9, P-5.10 and R-decomp's (5.10) put paperSum on the left-hand side with the paper's right-hand sides verbatim; internal proofs manipulate wordSum and convert only at statement boundaries via paperSum_eq_sum_arrangements.

def Anderson4D.wordSum {α : Type u_3} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) (F : (Fin M → α) → ℝ) : ℝ

Sum of a real word statistic over the admissible words for mult.

Equations

• Anderson4D.wordSum mult F = ∑ w ∈ Anderson4D.validWords mult, F w

def Anderson4D.paperSum {α : Type u_3} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) (F : (Fin M → α) → ℝ) : ℝ

The paper's labeled-arrangement sum, defined through the factorial ledger: paperSum mult F = (∏ a, (mult a)!) * wordSum mult F.

Equations

• Anderson4D.paperSum mult F = (∏ a : α, ↑(mult a).factorial) * Anderson4D.wordSum mult F

theorem Anderson4D.paperSum_eq_sum_arrangements {α : Type u_3} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) (F : (Fin M → α) → ℝ) : paperSum mult F = ∑ σ : Fin M ≃ (a : α) × Fin (mult a), F (inducedWord mult σ)

Statement-boundary conversion. The definitional paperSum equals the honest sum over labeled arrangements; this is the only bridge the analytic layer needs.

Restricted word sums

Sums over the admissible words satisfying a side condition P (e.g. the adjacency and primitivity restrictions of (5.15)/(5.33)), with the monotonicity in P used by the estimates.

def Anderson4D.wordSumFiltered {α : Type u_3} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) (P : (Fin M → α) → Prop) [DecidablePred P] (F : (Fin M → α) → ℝ) : ℝ

Sum of a real word statistic over the admissible words satisfying P.

Equations

• Anderson4D.wordSumFiltered mult P F = ∑ w ∈ Anderson4D.validWords mult with P w, F w

def Anderson4D.paperSumFiltered {α : Type u_3} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) (P : (Fin M → α) → Prop) [DecidablePred P] (F : (Fin M → α) → ℝ) : ℝ

The paperSum analogue of wordSumFiltered: ledger factor times restricted sum.

Equations

• Anderson4D.paperSumFiltered mult P F = (∏ a : α, ↑(mult a).factorial) * Anderson4D.wordSumFiltered mult P F

theorem Anderson4D.wordSumFiltered_le_wordSum {α : Type u_3} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) (P : (Fin M → α) → Prop) [DecidablePred P] (F : (Fin M → α) → ℝ) (hF : ∀ w ∈ validWords mult, 0 ≤ F w) : wordSumFiltered mult P F ≤ wordSum mult F

Dropping a side condition can only increase a sum of nonnegative statistics.

theorem Anderson4D.paperSumFiltered_le_paperSum {α : Type u_3} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) (P : (Fin M → α) → Prop) [DecidablePred P] (F : (Fin M → α) → ℝ) (hF : ∀ w ∈ validWords mult, 0 ≤ F w) : paperSumFiltered mult P F ≤ paperSum mult F

Dropping a side condition can only increase a paperSum of nonnegative statistics.

Word predicates (paper (5.15)/(5.33) side conditions)

Primitivity of words is not defined here: in the paper it is relative to the tree structure and enters only with the collapse induction.

def Anderson4D.NoAdjacentEqual {α : Type u_3} {M : ℕ} (w : Fin M → α) : Prop

Paper (5.15)/(5.33) side condition: no two adjacent positions of the word carry equal letters.

Equations

• Anderson4D.NoAdjacentEqual w = ∀ (j : Fin M) (h : ↑j + 1 < M), w j ≠ w ⟨↑j + 1, h⟩

@[implicit_reducible]

instance Anderson4D.instDecidableNoAdjacentEqualOfDecidableEq {α : Type u_3} {M : ℕ} [DecidableEq α] (w : Fin M → α) : Decidable (NoAdjacentEqual w)

Equations

• Anderson4D.instDecidableNoAdjacentEqualOfDecidableEq w = Anderson4D.instDecidableNoAdjacentEqualOfDecidableEq._aux_1 w