Completing the common product at the anchor

The common target ledger omits the distinguished anchor. Completing its occurrence and parent-scale factors costs the reciprocal of the anchor base factor. Since the occurrence atom X * sqrt Y is at least one, this is bounded by the printed occurrence factor times the full word parent-scale product and N_anchor^2.

noncomputable def Anderson4D.XYCluster.nxWordBaseScaleFactor {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {m : ℕ} (x : Fin m → ActiveNXClass Nm mu) : ℝ

Parent-scale factor attached to every position of an active word.

Equations

• Anderson4D.XYCluster.nxWordBaseScaleFactor x = ∏ i : Fin m, (↑(↑(x i)).1)⁻¹ ^ 2

theorem Anderson4D.XYCluster.paperDyadicLocalTarget_eq_occurrence_mul_scale_mul_skip {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) (skipped : Bool) : paperDyadicLocalTarget Nm mu a skipped = paper588OccurrenceAtom Nm mu a * (↑a.1)⁻¹ ^ 2 * if skipped = true then paper588SkippedAtom Nm mu a else 1

The local common target is the occurrence atom, the parent-scale factor, and the optional skipped-edge atom.

theorem Anderson4D.XYCluster.one_le_paper588OccurrenceAtom {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : ActiveNXClass Nm mu) : 1 ≤ paper588OccurrenceAtom Nm mu ↑a

Every active occurrence atom satisfies X * sqrt Y ≥ 1.

theorem Anderson4D.XYCluster.activeNXClass_parentScale_pos {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : ActiveNXClass Nm mu) : 0 < (↑a).1

Active parent scales are strictly positive.

theorem Anderson4D.XYCluster.locatedLedgerCommonProduct_finAnchor_eq_occurrence_scale_skip {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin m) (x : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : locatedLedgerCommonProduct Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor x O) = ((∏ edge : AdjacentIndex m, paper588OccurrenceAtom Nm mu ↑(x (outwardEdgeTargetPosition anchor edge))) * ∏ edge : AdjacentIndex m, (↑(↑(x (outwardEdgeTargetPosition anchor edge))).1)⁻¹ ^ 2) * ∏ edge ∈ O, paper588SkippedAtom Nm mu ↑(x (outwardEdgeTargetPosition anchor edge))

Exact factorization of the phase-independent common product into non-anchor occurrence atoms, non-anchor parent scales, and skipped atoms.

theorem Anderson4D.XYCluster.outward588_mul_wordBaseScale_mul_anchorScale_sq {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin m) (x : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : outward588WordOccurrenceFactor Nm mu anchor O x * nxWordBaseScaleFactor x * ↑(↑(x anchor)).1 ^ 2 = locatedLedgerCommonProduct Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor x O) * paper588OccurrenceAtom Nm mu ↑(x anchor)

Completing the missing anchor gives an exact identity. The only extra factor is the anchor occurrence atom; the anchor parent-scale inverse cancels against N_anchor^2.

theorem Anderson4D.XYCluster.locatedLedgerCommonProduct_finAnchor_le_completed {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin m) (x : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : locatedLedgerCommonProduct Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor x O) ≤ outward588WordOccurrenceFactor Nm mu anchor O x * nxWordBaseScaleFactor x * ↑(↑(x anchor)).1 ^ 2

Paper-facing anchor completion: the phase-independent common factor is bounded by the outward occurrence factor, the full word parent-scale factor, and the explicit N_anchor^2 cost.

Rewriting the full word parent-scale product by original leaves

theorem Anderson4D.XYCluster.nxWordBaseScaleFactor_eq_leafProduct {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) : nxWordBaseScaleFactor x = ∏ l : HeppLeaf t, ((↑(scaleN Nm (PlaneTree.parentV ↑l)))⁻¹ ^ 2) ^ leafMultiplicity mu l

A valid active class word contains exactly the leaf-multiplicity power of every original parent scale.

theorem Anderson4D.XYCluster.nxWordBaseScaleFactor_eq_leafZpowProduct {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) : nxWordBaseScaleFactor x = ∏ l : HeppLeaf t, ↑(scaleN Nm (PlaneTree.parentV ↑l)) ^ (-2 * ↑(leafMultiplicity mu l))

A valid active word supplies exactly the global inverse-square leaf-scale product that occurs on the left of (5.89).

theorem Anderson4D.XYCluster.wordBaseFactorialOuterPayoff_mul_anchorScale_sq_eq_leafPower {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (anchor : Fin m) (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) (l₀ : HeppLeaf t) (hl₀ : l₀ ∈ leavesAtNX Nm mu ↑(x anchor)) : (nxWordBaseScaleFactor x * ∏ l : HeppLeaf t, sqrtFactorial (leafMultiplicity mu l) * originalOuterLeafPayoff Nm mu compound l) * ↑(↑(x anchor)).1 ^ 2 = ((∏ l ∈ simpleLeaves t compound, sqrtFactorial (mu.m l)) * ∏ l ∈ compoundLeaves t compound, factorialThreeQuarters (mu.m l)) * singleScaleLeafPower Nm mu compound l₀

Exact end-of-(5.88) ledger after choosing an original leaf in the distinguished anchor class. The anchor-scale square completes the distinguished-parent factor in singleScaleLeafPower.

theorem Anderson4D.XYCluster.exists_anchorLeaf_wordBaseFactorialOuterPayoff_eq_leafPower {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (anchor : Fin m) (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) : ∃ l₀ ∈ leavesAtNX Nm mu ↑(x anchor), (nxWordBaseScaleFactor x * ∏ l : HeppLeaf t, sqrtFactorial (leafMultiplicity mu l) * originalOuterLeafPayoff Nm mu compound l) * ↑(↑(x anchor)).1 ^ 2 = ((∏ l ∈ simpleLeaves t compound, sqrtFactorial (mu.m l)) * ∏ l ∈ compoundLeaves t compound, factorialThreeQuarters (mu.m l)) * singleScaleLeafPower Nm mu compound l₀

Every valid active word admits an original anchor leaf realizing the exact completed payoff ledger.