Word-independent minimal anchor scale

Every valid active (N,X) word contains every active class with its prescribed positive multiplicity. Consequently the value of the minimal parent scale is independent of the ordering of the word. Together with the base-scale regrouping, this makes the scale coefficient used after the fixed-fiber estimate common to the entire outer word sum.

theorem Anderson4D.XYCluster.activeNXMultiplicity_pos {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : ActiveNXClass Nm mu) : 0 < activeNXMultiplicity Nm mu a

Every active (N,X) class has positive prescribed mass.

theorem Anderson4D.XYCluster.exists_position_eq_activeNXClass_of_valid {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) (a : ActiveNXClass Nm mu) : ∃ (i : Fin m), x i = a

Every active letter occurs somewhere in every valid active word.

theorem Anderson4D.XYCluster.totalMultiplicityNXScaleAnchor_scale_eq_of_valid {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (x y : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) (hy : y ∈ validWords (activeNXMultiplicity Nm mu)) : (↑(x (totalMultiplicityNXScaleAnchor Nm mu x))).1 = (↑(y (totalMultiplicityNXScaleAnchor Nm mu y))).1

The minimal parent-scale value does not depend on the ordering of a valid active word.

theorem Anderson4D.XYCluster.nxWordBaseScaleFactor_eq_of_valid {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (x y : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) (hy : y ∈ validWords (activeNXMultiplicity Nm mu)) : nxWordBaseScaleFactor x = nxWordBaseScaleFactor y

The full word base-scale product is likewise independent of the ordering of a valid active word.

theorem Anderson4D.XYCluster.completedNXWordBaseScaleFactor_eq_of_valid {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (x y : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) (hy : y ∈ validWords (activeNXMultiplicity Nm mu)) : nxWordBaseScaleFactor x * ↑(↑(x (totalMultiplicityNXScaleAnchor Nm mu x))).1 ^ 2 = nxWordBaseScaleFactor y * ↑(↑(y (totalMultiplicityNXScaleAnchor Nm mu y))).1 ^ 2

The completed base-scale coefficient appearing after anchor completion is common to all valid active words.