Exact run-compression regrouping by profile

This is the finite-sum ledger behind paper (5.34)--(5.37). The source domain is never enlarged in an equality: it consists of valid words satisfying the paper's primitive word condition. Their compressed words are automatically no-adjacent and remain primitive. Enlargement to a larger list fiber occurs only in the cardinality upper bound.

@[reducible, inline]

abbrev Anderson4D.MergeProfileOutcome {α : Type u_1} (ml : α → ℕ) : Type u_1

A compressed outcome with its multiplicity coordinate packaged in the finite profile carrier.

Equations

• Anderson4D.MergeProfileOutcome ml = (Anderson4D.MergeMultiplicityProfile ml × List α)

def Anderson4D.mergedProfileOutcome {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (w : MergeValidWord ml) : MergeProfileOutcome ml

The packaged run-compression outcome of a valid word.

Equations

• Anderson4D.mergedProfileOutcome ml w = (Anderson4D.mergedMultiplicityProfile ml w, Anderson4D.mergedWordList ↑w)

@[simp]

theorem Anderson4D.mergedProfileOutcome_fst {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (w : MergeValidWord ml) : (mergedProfileOutcome ml w).1 = mergedMultiplicityProfile ml w

@[simp]

theorem Anderson4D.mergedProfileOutcome_snd {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (w : MergeValidWord ml) : (mergedProfileOutcome ml w).2 = mergedWordList ↑w

def Anderson4D.mergeProfileOutcomeImage {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) : Finset (MergeProfileOutcome ml)

Packaged outcomes realized by an arbitrary finite family of valid words.

Equations

• Anderson4D.mergeProfileOutcomeImage ml s = Finset.image (Anderson4D.mergedProfileOutcome ml) s

theorem Anderson4D.sum_eq_sum_mergeProfileOutcome_fibers {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) (F : MergeProfileOutcome ml → ℝ) : ∑ w ∈ s, F (mergedProfileOutcome ml w) = ∑ q ∈ mergeProfileOutcomeImage ml s, ↑{w ∈ s | mergedProfileOutcome ml w = q}.card * F q

Exact regrouping by the full packaged outcome.

theorem Anderson4D.sum_mergeProfileOutcomeImage_eq_sum_profile_fibers {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) (F : MergeProfileOutcome ml → ℝ) : ∑ q ∈ mergeProfileOutcomeImage ml s, F q = ∑ p ∈ mergeMultiplicityProfileImage ml s, ∑ q ∈ mergeProfileOutcomeImage ml s with q.1 = p, F q

Exact regrouping of realized compressed outcomes by their multiplicity profile.

theorem Anderson4D.sum_eq_sum_profile_then_outcome_fibers {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) (F : MergeProfileOutcome ml → ℝ) : ∑ w ∈ s, F (mergedProfileOutcome ml w) = ∑ p ∈ mergeMultiplicityProfileImage ml s, ∑ q ∈ mergeProfileOutcomeImage ml s with q.1 = p, ↑{w ∈ s | mergedProfileOutcome ml w = q}.card * F q

The literal two-stage regrouping used in the final assembly: first by compressed multiplicity profile, then by the compressed representative list.

theorem Anderson4D.card_filter_mergedProfileOutcome_le_two_pow {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) (q : MergeProfileOutcome ml) : {w ∈ s | mergedProfileOutcome ml w = q}.card ≤ 2 ^ M

A fixed packaged-outcome fiber has at most 2^M elements. The proof injects the exact finite source fiber into the larger fiber obtained by remembering only the compressed list, and then invokes the run-composition count.

def Anderson4D.primitiveMergeWordFamily {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) : Finset (MergeValidWord ml)

The primitive source domain from Proposition 5.7, represented without dropping or adding any word.

Equations

• Anderson4D.primitiveMergeWordFamily ml = {w : Anderson4D.MergeValidWord ml | Anderson4D.NoProperLeafBlock ↑w}

theorem Anderson4D.mem_primitive_mergeProfileOutcomeImage_restrictions {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (q : MergeProfileOutcome ml) (hq : q ∈ mergeProfileOutcomeImage ml (primitiveMergeWordFamily ml)) : NoAdjacentEqual (listWord q.2) ∧ NoProperLeafBlock (listWord q.2)

Every outcome in the exact primitive image has the two restrictions required for the Proposition 5.9 input: no adjacent equal letters and the primitive word condition.

theorem Anderson4D.sum_comp_mergedProfileOutcome_le_two_pow_mul_sum {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) (F : MergeProfileOutcome ml → ℝ) (hF : ∀ q ∈ mergeProfileOutcomeImage ml s, 0 ≤ F q) : ∑ w ∈ s, F (mergedProfileOutcome ml w) ≤ 2 ^ M * ∑ q ∈ mergeProfileOutcomeImage ml s, F q

Pulling a nonnegative compressed-outcome weight back to original words costs at most the run-composition factor 2^M.

theorem Anderson4D.sum_mergeProfileOutcomeImage_le_two_pow_sum_mul {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) (F : MergeProfileOutcome ml → ℝ) (B : ℝ) (hB : 0 ≤ B) (hprofile : ∀ p ∈ mergeMultiplicityProfileImage ml s, ∑ q ∈ mergeProfileOutcomeImage ml s with q.1 = p, F q ≤ B) : ∑ q ∈ mergeProfileOutcomeImage ml s, F q ≤ (2 ^ ∑ a : α, ml a) * B

If the total compressed-outcome contribution is bounded uniformly for each realized profile, then the profile count contributes at most 2^(∑ ml).

theorem Anderson4D.sum_comp_mergedProfileOutcome_le_two_pow_mul_two_pow_sum {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) (F : MergeProfileOutcome ml → ℝ) (B : ℝ) (hB : 0 ≤ B) (hF : ∀ q ∈ mergeProfileOutcomeImage ml s, 0 ≤ F q) (hprofile : ∀ p ∈ mergeMultiplicityProfileImage ml s, ∑ q ∈ mergeProfileOutcomeImage ml s with q.1 = p, F q ≤ B) : ∑ w ∈ s, F (mergedProfileOutcome ml w) ≤ 2 ^ M * ((2 ^ ∑ a : α, ml a) * B)

General two-ledger bound: one 2^M for expansions of a fixed compressed outcome and one 2^(∑ ml) for possible multiplicity profiles.

theorem Anderson4D.primitive_merge_regroup_le_four_pow {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (hsum : ∑ a : α, ml a = M) (F : MergeProfileOutcome ml → ℝ) (B : ℝ) (hB : 0 ≤ B) (hF : ∀ q ∈ mergeProfileOutcomeImage ml (primitiveMergeWordFamily ml), 0 ≤ F q) (hprofile : ∀ p ∈ mergeMultiplicityProfileImage ml (primitiveMergeWordFamily ml), ∑ q ∈ mergeProfileOutcomeImage ml (primitiveMergeWordFamily ml) with q.1 = p, F q ≤ B) : ∑ w ∈ primitiveMergeWordFamily ml, F (mergedProfileOutcome ml w) ≤ 4 ^ M * B

Final-assembly-facing form on the exact primitive domain. When the original multiplicities sum to the word length, the two binary ledgers combine to the explicit loss 4^M.

Fixed-profile words for the Proposition 5.9 call

def Anderson4D.MergeMultiplicityProfile.total {α : Type u_1} [Fintype α] {ml : α → ℕ} (p : MergeMultiplicityProfile ml) : ℕ

Total length encoded by a packaged multiplicity profile.

Equations

• p.total = ∑ a : α, p.toNat a

theorem Anderson4D.mergeProfileOutcome_length_eq_total {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) (p : MergeMultiplicityProfile ml) (q : MergeProfileOutcome ml) (hq : q ∈ mergeProfileOutcomeImage ml s) (hqp : q.1 = p) : q.2.length = p.total

Every realized outcome whose first coordinate is p has the length encoded by p.

theorem Anderson4D.listWord_mem_validWords_profile_toNat {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) (q : MergeProfileOutcome ml) (hq : q ∈ mergeProfileOutcomeImage ml s) : listWord q.2 ∈ validWords q.1.toNat

The list representative of every realized outcome has exactly its profile multiplicity before the harmless length transport.

def Anderson4D.primitiveProfileOutcomeFiber {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (p : MergeMultiplicityProfile ml) : Finset (MergeProfileOutcome ml)

The exact compressed-outcome fiber at a fixed multiplicity profile, retaining the primitive source domain.

Equations

• Anderson4D.primitiveProfileOutcomeFiber ml p = {q ∈ Anderson4D.mergeProfileOutcomeImage ml (Anderson4D.primitiveMergeWordFamily ml) | q.1 = p}

def Anderson4D.primitiveProfileFiberWord {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (p : MergeMultiplicityProfile ml) (q : ↥(primitiveProfileOutcomeFiber ml p)) : Fin p.total → α

A fixed-profile outcome, cast to the common profile length.

Equations

• Anderson4D.primitiveProfileFiberWord ml p q = Anderson4D.castListWord✝ (↑q).2 ⋯

@[simp]

theorem Anderson4D.ofFn_primitiveProfileFiberWord {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (p : MergeMultiplicityProfile ml) (q : ↥(primitiveProfileOutcomeFiber ml p)) : List.ofFn (primitiveProfileFiberWord ml p q) = (↑q).2

theorem Anderson4D.primitiveProfileFiberWord_mem_validWords {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (p : MergeMultiplicityProfile ml) (q : ↥(primitiveProfileOutcomeFiber ml p)) : primitiveProfileFiberWord ml p q ∈ validWords p.toNat

Fixed-profile outcome words are honest words with multiplicity p.toNat.

theorem Anderson4D.primitiveProfileFiberWord_restrictions {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (p : MergeMultiplicityProfile ml) (q : ↥(primitiveProfileOutcomeFiber ml p)) : NoAdjacentEqual (primitiveProfileFiberWord ml p q) ∧ NoProperLeafBlock (primitiveProfileFiberWord ml p q)

The common-length representative retains both paper restrictions.

theorem Anderson4D.primitiveProfileFiberWord_injective {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (p : MergeMultiplicityProfile ml) : Function.Injective (primitiveProfileFiberWord ml p)

Distinct fixed-profile compressed outcomes give distinct common-length words.

theorem Anderson4D.primitiveSeparatedChainWeight_profileFiberWord {t : PlaneTree} {M : ℕ} (ml : HeppLeaf t → ℕ) (p : MergeMultiplicityProfile ml) (z : HeppLeaf t → Fin 4 → ℤ) (q : ↥(primitiveProfileOutcomeFiber ml p)) : primitiveSeparatedChainWeight z (primitiveProfileFiberWord ml p q) = heppChainWeight z (listWord (↑q).2)

On a fixed profile fiber, the transported primitive-separated weight is the chain weight of the original compressed list.

theorem Anderson4D.sum_primitiveProfileFiber_chainWeight_le_wordSum {t : PlaneTree} {M : ℕ} (ml : HeppLeaf t → ℕ) (p : MergeMultiplicityProfile ml) (z : HeppLeaf t → Fin 4 → ℤ) : ∑ q : ↥(primitiveProfileOutcomeFiber ml p), heppChainWeight z (listWord (↑q).2) ≤ wordSum p.toNat (primitiveSeparatedChainWeight z)

The compressed chain-weight sum for one realized profile embeds into the exact wordSum to which Proposition 5.9 applies. No word-domain equality is claimed: the last step enlarges by nonnegativity.