Deterministic minimal-scale anchors

Step 4 of the proof of Proposition 5.10 cuts a class word at a position whose parent scale is minimal. This file makes that choice deterministic and proves that it depends only on the fixed (N,X) word, not on a labeled arrangement in its fiber.

noncomputable def Anderson4D.minimalNXScaleAnchor {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {m : ℕ} (hm : 0 < m) (x : Fin m → ActiveNXClass Nm mu) : Fin m

A deterministic position at which the first coordinate of an active (N,X) word is minimal.

Equations

• Anderson4D.minimalNXScaleAnchor hm x = Function.argmin fun (i : Fin m) => (↑(x i)).1

theorem Anderson4D.minimalNXScaleAnchor_le {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {m : ℕ} (hm : 0 < m) (x : Fin m → ActiveNXClass Nm mu) (i : Fin m) : (↑(x (minimalNXScaleAnchor hm x))).1 ≤ (↑(x i)).1

noncomputable def Anderson4D.totalMultiplicityNXScaleAnchor {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) : Fin (totalMultiplicity mu)

Paper-length anchor; totalMultiplicity ≥ 2 makes the carrier nonempty without an additional hypothesis.

Equations

• Anderson4D.totalMultiplicityNXScaleAnchor Nm mu x = Anderson4D.minimalNXScaleAnchor ⋯ x

theorem Anderson4D.totalMultiplicityNXScaleAnchor_le {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (i : Fin (totalMultiplicity mu)) : (↑(x (totalMultiplicityNXScaleAnchor Nm mu x))).1 ≤ (↑(x i)).1

theorem Anderson4D.mem_arrangementsAtNXWord_iff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (σ : HeppArrangement mu) : σ ∈ arrangementsAtNXWord Nm mu x ↔ arrangementNXWord Nm mu σ = x

theorem Anderson4D.arrangement_parentScale_eq_NXWord {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (σ : HeppArrangement mu) (hσ : σ ∈ arrangementsAtNXWord Nm mu x) (i : Fin (totalMultiplicity mu)) : scaleN Nm (PlaneTree.parentV ↑(σ i).fst) = (↑(x i)).1

Every arrangement in a fixed (N,X)-word fiber has exactly the class word's parent scale at each position.

theorem Anderson4D.arrangement_anchor_parentScale_minimal {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (σ : HeppArrangement mu) (hσ : σ ∈ arrangementsAtNXWord Nm mu x) (i : Fin (totalMultiplicity mu)) : scaleN Nm (PlaneTree.parentV ↑(σ (totalMultiplicityNXScaleAnchor Nm mu x)).fst) ≤ scaleN Nm (PlaneTree.parentV ↑(σ i).fst)

The distinguished labeled copy selected at the deterministic word anchor has minimal parent scale among all positions of every arrangement in the fiber.