Run-compressed inputs for Proposition 5.9

This module turns a primitive valid word before run compression into the tree, multiplicity, word, and embedding data expected by the inductive estimate of Proposition 5.9.

Every compressed leaf multiplicity is at least two

theorem Anderson4D.two_le_mergedMultiplicity_of_valid_of_noProperLeafBlock {t : PlaneTree} {M : ℕ} (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (w : Fin M → HeppLeaf t) (hvalid : w ∈ validWords (leafMultiplicity mu)) (hprimitive : NoProperLeafBlock w) (l : HeppLeaf t) : 2 ≤ mergedMultiplicity w l

A primitive valid Hepp-leaf word cannot contain only one maximal run of any leaf. The branching-root hypothesis supplies a second leaf, and the original multiplicities ensure that this second leaf occurs.

The compressed multiplicity structure

def Anderson4D.mergedMultiplicities {t : PlaneTree} {M : ℕ} (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (w : Fin M → HeppLeaf t) (hvalid : w ∈ validWords (leafMultiplicity mu)) (hprimitive : NoProperLeafBlock w) : t.Multiplicities

Extend the compressed leaf multiplicity by junk zero values away from the leaf carrier.

Equations

• Anderson4D.mergedMultiplicities hroot mu w hvalid hprimitive = { m := fun (v : t.VPos) => if hv : v ∈ t.Leaves then Anderson4D.mergedMultiplicity w ⟨v, hv⟩ else 0, two_le := ⋯ }

@[simp]

theorem Anderson4D.leafMultiplicity_mergedMultiplicities {t : PlaneTree} {M : ℕ} (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (w : Fin M → HeppLeaf t) (hvalid : w ∈ validWords (leafMultiplicity mu)) (hprimitive : NoProperLeafBlock w) (l : HeppLeaf t) : leafMultiplicity (mergedMultiplicities hroot mu w hvalid hprimitive) l = mergedMultiplicity w l

theorem Anderson4D.totalMultiplicity_mergedMultiplicities {t : PlaneTree} {M : ℕ} (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (w : Fin M → HeppLeaf t) (hvalid : w ∈ validWords (leafMultiplicity mu)) (hprimitive : NoProperLeafBlock w) : totalMultiplicity (mergedMultiplicities hroot mu w hvalid hprimitive) = (mergedWordList w).length

The total multiplicity of the compressed structure is exactly the compressed word length.

theorem Anderson4D.mergedWord_mem_validWords_mergedMultiplicities {t : PlaneTree} {M : ℕ} (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (w : Fin M → HeppLeaf t) (hvalid : w ∈ validWords (leafMultiplicity mu)) (hprimitive : NoProperLeafBlock w) : mergedWord w ∈ validWords (leafMultiplicity (mergedMultiplicities hroot mu w hvalid hprimitive))

The compressed word is valid for the constructed Hepp multiplicities.

Geometric inputs

theorem Anderson4D.IsAdmissible.isSeparatedEmbedding {t : PlaneTree} {Nm : t.HeppMarking} {R : ℕ} {z : HeppLeaf t → Fin 4 → ℤ} (hadmissible : IsAdmissible Nm R z) : IsSeparatedEmbedding Nm z

Admissibility contains the separated-embedding hypothesis of Proposition 5.9 literally.

Packaged induction input

structure Anderson4D.MergeInductiveInput {t : PlaneTree} {M : ℕ} (Nm : t.HeppMarking) (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin M → HeppLeaf t) : Type

All data needed to invoke Proposition 5.9 on the run-compressed word.

• multiplicities : t.Multiplicities
• treeValid : t.isValid = true
• rootBranch : t.rootV ∈ t.BranchNodes
• leafMultiplicity_eq : leafMultiplicity self.multiplicities = mergedMultiplicity w
• total_eq : totalMultiplicity self.multiplicities = (mergedWordList w).length
• wordValid : mergedWord w ∈ validWords (leafMultiplicity self.multiplicities)
• wordNoAdjacent : NoAdjacentEqual (mergedWord w)
• wordPrimitive : NoProperLeafBlock (mergedWord w)
• separated : IsSeparatedEmbedding Nm z
• subtreeDiameter : SatisfiesSubtreeDiameter Nm self.multiplicities z

def Anderson4D.mergeInductiveInput {t : PlaneTree} {M R : ℕ} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hadmissible : IsAdmissible Nm R z) (w : Fin M → HeppLeaf t) (hvalid : w ∈ validWords (leafMultiplicity mu)) (hprimitive : NoProperLeafBlock w) : MergeInductiveInput Nm z w

Construct the complete Proposition 5.9 input from an admissible embedding and a primitive valid original word.

Equations

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