Orbit lower bound for the fixed-tree incidence denominator

This file implements Proposition 5.6, Step 1. Simultaneously transporting a Hepp marking, the leaf multiplicities, an admissible embedding, and its word witness along a tree automorphism preserves realization. Consequently every marking in the orbit of a realizing marked tree supplies distinct restricted branch data in the concrete denominator fiber. Orbit--stabilizer then gives the division-free natural-number form of paper (5.12).

Transport of word and realization witnesses

theorem Anderson4D.postcomp_equiv_mem_validWords {m : ℕ} {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α ≃ β) {mult : α → ℕ} {w : Fin m → α} (hw : w ∈ validWords mult) : (fun (j : Fin m) => e (w j)) ∈ validWords fun (b : β) => mult (e.symm b)

Postcomposing a word by an equivalence merely reindexes its prescribed fiber sizes.

theorem Anderson4D.RealizesTuple.map_aut {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (h : RealizesTuple t Nm mu M y) (g : t.Aut) : RealizesTuple t (smulHeppMarking g Nm) (smulMultiplicities g mu) M y

A concrete tuple realization is preserved by simultaneous transport of all tree-indexed data along an automorphism.

Restricted data attached to transported bundles

theorem Anderson4D.scale_bound_smulHeppMarking {t : PlaneTree} {Nm : t.HeppMarking} {M : ℕ} (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (g : t.Aut) (v : t.VPos) : v ∈ t.BranchNodes → ↑(scaleN (smulHeppMarking g Nm) v) ≤ 4 * ↑M

The analytic scale bound is invariant under transport.

theorem Anderson4D.branchDataOfScaleBound_raw {t : PlaneTree} {Nm : t.HeppMarking} {M : ℕ} (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) : (PlaneTree.branchDataOfScaleBound Nm hscale).raw = Nm.canonicalRaw

The finite branch carrier obtained from a scale-bounded marking has raw view equal to the marking's canonical branch-supported view.

def Anderson4D.validRealizationDataOfAut {t : PlaneTree} {M m : ℕ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (g : t.Aut) : ValidRealizationData t M m

The valid restricted datum obtained by simultaneously transporting a fixed marking and fixed multiplicities along g.

Equations

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

theorem Anderson4D.validRealizationDataOfAut_branch_raw {t : PlaneTree} {M m : ℕ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (g : t.Aut) : (↑(validRealizationDataOfAut ht Nm mu hscale htotal g)).1.raw = g • Nm.canonicalRaw

The branch component of the transported restricted datum records exactly the transported canonical raw marking.

theorem Anderson4D.validRealizationDataOfAut_realizes {t : PlaneTree} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (hreal : RealizesTuple t Nm mu M y) (g : t.Aut) : (validRealizationDataOfAut ht Nm mu hscale htotal g).Realizes y

The transported restricted datum remains incident to the original tuple.

Injection of the marking orbit into the incidence fiber

noncomputable def Anderson4D.orbitRepresentative {t : PlaneTree} {Nm : t.HeppMarking} (N : ↑(MulAction.orbit t.Aut Nm.canonicalRaw)) : t.Aut

Choose one tree automorphism representing an element of the marking orbit. The final injection is independent of this noncanonical choice because its branch component recovers the orbit element itself.

Equations

• Anderson4D.orbitRepresentative N = Classical.choose ⋯

theorem Anderson4D.orbitRepresentative_spec {t : PlaneTree} {Nm : t.HeppMarking} (N : ↑(MulAction.orbit t.Aut Nm.canonicalRaw)) : orbitRepresentative N • Nm.canonicalRaw = ↑N

noncomputable def Anderson4D.orbitToTreeRealizationFiber {t : PlaneTree} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (hreal : RealizesTuple t Nm mu M y) (N : ↑(MulAction.orbit t.Aut Nm.canonicalRaw)) : ↥(treeRealizationFiber t M m y)

An orbit marking, together with any representative automorphism, gives a member of the concrete fixed-tree incidence fiber.

Equations

• Anderson4D.orbitToTreeRealizationFiber ht Nm mu hscale htotal hreal N = ⟨Anderson4D.validRealizationDataOfAut ht Nm mu hscale htotal (Anderson4D.orbitRepresentative N), ⋯⟩

theorem Anderson4D.orbitToTreeRealizationFiber_injective {t : PlaneTree} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (hreal : RealizesTuple t Nm mu M y) : Function.Injective (orbitToTreeRealizationFiber ht Nm mu hscale htotal hreal)

The denominator lower bound (paper (5.12))

theorem Anderson4D.markingOrbit_card_le_treeSymDenom {t : PlaneTree} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (hreal : RealizesTuple t Nm mu M y) : (MulAction.orbit t.Aut Nm.canonicalRaw).toFinset.card ≤ treeSymDenom t M m y

Distinct canonical raw markings in the automorphism orbit yield distinct elements of the concrete incidence fiber.

theorem Anderson4D.card_aut_le_treeSymDenom_mul_card_autHeppMarked {t : PlaneTree} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hreal : RealizesTuple t Nm mu M y) : Fintype.card t.Aut ≤ treeSymDenom t M m y * Fintype.card ↥(t.AutHeppMarked Nm)

Paper (5.12), stated without natural-number division:

|Aut(t)| ≤ treeSymDenom(t,M,m,y) * |Aut(t,Nm)|.

The scale and total-multiplicity bounds needed to enter the finite denominator carrier are recovered from the realization witness itself.