The occurrence ledger in the single-scale estimate

This file isolates the phase-independent bookkeeping used immediately after (5.88). The statistic paperNXSkippedOccurrenceCount O x a is the literal paper statistic: it counts skipped adjacency indices whose right endpoint has (N,X) class a. It therefore depends only on the class word and the omitted-edge set, not on a summation phase, parity choice, or anchor.

The main results are:

• the pointwise ledger s_{N,X} ≤ m_{N,X};
• the exact global ledger ∑ s_{N,X} = |O|;
• an exact regrouping of the two occurrence factors in (5.88) by (N,X);
• the resulting factorial bound (5.89);
• an exact count of the labeled-copy choices in an anchor fiber.

The right-endpoint convention here is intentionally distinct from the orientation-dependent incoming-edge convention used by an outward summation schedule. No class-by-class identification of those two conventions is asserted.

The literal right-endpoint occurrence statistic

def Anderson4D.nxWordOccurrenceCount {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {m : ℕ} (x : Fin m → ActiveNXClass Nm mu) (a : NXClass) : ℕ

Number of positions of an active (N,X) word which have underlying class a.

Equations

• Anderson4D.nxWordOccurrenceCount x a = {i : Fin m | ↑(x i) = a}.card

def Anderson4D.paperNXSkippedOccurrenceCount {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {m : ℕ} (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (a : NXClass) : ℕ

Paper's s_{N,X} below (5.88): skipped adjacencies classified by the class of their right endpoint j+1.

Equations

• Anderson4D.paperNXSkippedOccurrenceCount O x a = {j ∈ O | ↑(x (Anderson4D.adjacentSucc j)) = a}.card

theorem Anderson4D.adjacentSucc_injective {m : ℕ} : Function.Injective adjacentSucc

The successor map on adjacency indices is injective.

def Anderson4D.assignedNXSkippedOccurrenceCount {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {m : ℕ} (q : AdjacentIndex m → Fin m) (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (a : NXClass) : ℕ

Occurrence count for an arbitrary assignment of each skipped adjacency to one word position. The outward elimination will instantiate q by the endpoint farther from the anchor.

Equations

• Anderson4D.assignedNXSkippedOccurrenceCount q O x a = {j ∈ O | ↑(x (q j)) = a}.card

theorem Anderson4D.assignedNXSkippedOccurrenceCount_le_wordOccurrenceCount {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {m : ℕ} (q : AdjacentIndex m → Fin m) (hq : Function.Injective q) (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (a : NXClass) : assignedNXSkippedOccurrenceCount q O x a ≤ nxWordOccurrenceCount x a

An injective edge-to-position assignment cannot charge a class more often than that class occurs in the full word.

theorem Anderson4D.nxWordOccurrenceCount_eq_multiplicityNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) (a : NXClass) (ha : a ∈ nxCarrier Nm mu) : nxWordOccurrenceCount x a = multiplicityNX Nm mu a

A valid active class word contains m_{N,X} occurrences of every active class.

theorem Anderson4D.paperNXSkippedOccurrenceCount_le_wordOccurrenceCount {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {m : ℕ} (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (a : NXClass) : paperNXSkippedOccurrenceCount O x a ≤ nxWordOccurrenceCount x a

Every skipped right-endpoint occurrence is an occurrence of the same class in the whole word.

theorem Anderson4D.paperNXSkippedOccurrenceCount_le_multiplicityNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) (a : NXClass) (ha : a ∈ nxCarrier Nm mu) : paperNXSkippedOccurrenceCount O x a ≤ multiplicityNX Nm mu a

The pointwise occurrence ledger used by factorial absorption: s_{N,X} ≤ m_{N,X}.

theorem Anderson4D.assignedNXSkippedOccurrenceCount_le_multiplicityNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (q : AdjacentIndex m → Fin m) (hq : Function.Injective q) (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) (a : NXClass) (ha : a ∈ nxCarrier Nm mu) : assignedNXSkippedOccurrenceCount q O x a ≤ multiplicityNX Nm mu a

The generic assigned occurrence ledger satisfies s_{N,X} ≤ m_{N,X} whenever the edge-to-position assignment is injective.

theorem Anderson4D.sum_paperNXSkippedOccurrenceCount {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) : ∑ a ∈ nxCarrier Nm mu, paperNXSkippedOccurrenceCount O x a = O.card

Exact global occurrence ledger: every omitted adjacency contributes once, to the class of its right endpoint.

theorem Anderson4D.sum_assignedNXSkippedOccurrenceCount {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (q : AdjacentIndex m → Fin m) (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) : ∑ a ∈ nxCarrier Nm mu, assignedNXSkippedOccurrenceCount q O x a = O.card

Every skipped edge contributes once for any assigned-position convention; injectivity is not needed for this total ledger.

Exact regrouping of the occurrence factors in (5.88)

noncomputable def Anderson4D.paper588OccurrenceAtom {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) : ℝ

The phase-independent factor X Y^(1/2) contributed by one occurrence of an (N,X) class in (5.88).

Equations

• Anderson4D.paper588OccurrenceAtom Nm mu a = ↑a.2 * √↑(Anderson4D.singleScaleSigma2 Nm mu a).2

noncomputable def Anderson4D.paper588SkippedAtom {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) : ℝ

The factor (XY)^(-1/2) contributed when an adjacency is omitted.

Equations

• Anderson4D.paper588SkippedAtom Nm mu a = (√↑(a.2 * (Anderson4D.singleScaleSigma2 Nm mu a).2))⁻¹

noncomputable def Anderson4D.paper588WordOccurrenceFactor {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) : ℝ

The two common occurrence products on the left of the per-fiber factorial comparison following (5.88).

Equations

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

theorem Anderson4D.prod_word_eq_prod_pow_occurrenceCount {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (x : Fin m → ActiveNXClass Nm mu) (f : NXClass → ℝ) : ∏ i : Fin m, f ↑(x i) = ∏ a ∈ nxCarrier Nm mu, f a ^ nxWordOccurrenceCount x a

Regroup an arbitrary position product by the underlying active (N,X) class.

theorem Anderson4D.prod_skippedEdges_eq_prod_pow_skippedOccurrenceCount {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (f : NXClass → ℝ) : ∏ j ∈ O, f ↑(x (adjacentSucc j)) = ∏ a ∈ nxCarrier Nm mu, f a ^ paperNXSkippedOccurrenceCount O x a

Regroup an arbitrary skipped-edge product by the right-endpoint class.

theorem Anderson4D.prod_assignedSkippedEdges_eq_prod_pow_occurrenceCount {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (q : AdjacentIndex m → Fin m) (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (f : NXClass → ℝ) : ∏ j ∈ O, f ↑(x (q j)) = ∏ a ∈ nxCarrier Nm mu, f a ^ assignedNXSkippedOccurrenceCount q O x a

Regroup a skipped-edge product for an arbitrary assigned-position convention.

noncomputable def Anderson4D.assigned588WordOccurrenceFactor {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (q : AdjacentIndex m → Fin m) (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) : ℝ

Occurrence factor with a caller-specified assignment of skipped edges to word positions.

Equations

• Anderson4D.assigned588WordOccurrenceFactor Nm mu q O x = (∏ i : Fin m, Anderson4D.paper588OccurrenceAtom Nm mu ↑(x i)) * ∏ j ∈ O, Anderson4D.paper588SkippedAtom Nm mu ↑(x (q j))

theorem Anderson4D.assigned588WordOccurrenceFactor_eq_classProduct {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (q : AdjacentIndex m → Fin m) (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) : assigned588WordOccurrenceFactor Nm mu q O x = ∏ a ∈ nxCarrier Nm mu, singleScalePrintedFiberFactor a.2 (singleScaleSigma2 Nm mu a).2 (multiplicityNX Nm mu a) (assignedNXSkippedOccurrenceCount q O x a)

Exact (N,X) regrouping for an assigned skipped-edge convention.

theorem Anderson4D.assigned588WordOccurrenceFactor_le_factorial {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (q : AdjacentIndex m → Fin m) (hq : Function.Injective q) (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) (s : ℕ) (hm : totalMultiplicity mu = m) (hs : O.card = s) : assigned588WordOccurrenceFactor Nm mu q O x ≤ (2 * Real.exp 1) ^ m * √↑(m - s).factorial * ∏ l : HeppLeaf t, √↑(leafMultiplicity mu l).factorial

Generic factorial absorption for any injective skipped-edge assignment.

theorem Anderson4D.paper588WordOccurrenceFactor_eq_classProduct {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) : paper588WordOccurrenceFactor Nm mu O x = ∏ a ∈ nxCarrier Nm mu, singleScalePrintedFiberFactor a.2 (singleScaleSigma2 Nm mu a).2 (multiplicityNX Nm mu a) (paperNXSkippedOccurrenceCount O x a)

Exact (N,X)-fiber regrouping of the occurrence part of (5.88).

theorem Anderson4D.paper588WordOccurrenceFactor_le_factorial {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) (s : ℕ) (hm : totalMultiplicity mu = m) (hs : O.card = s) : paper588WordOccurrenceFactor Nm mu O x ≤ (2 * Real.exp 1) ^ m * √↑(m - s).factorial * ∏ l : HeppLeaf t, √↑(leafMultiplicity mu l).factorial

The phase-independent occurrence/factorial ledger: the literal common factor in (5.88) is bounded by the factorial expression in (5.89).

The independent anchor-copy counting cost

The phase-independent outward occurrence ledger

def Anderson4D.XYCluster.outwardNXSkippedOccurrenceCount {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {m : ℕ} (anchor : Fin m) (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (a : NXClass) : ℕ

Skipped occurrences charged to the unique endpoint farther from the anchor, exactly as in the outward kernel schedule.

Equations

• Anderson4D.XYCluster.outwardNXSkippedOccurrenceCount anchor O x a = Anderson4D.assignedNXSkippedOccurrenceCount (Anderson4D.XYCluster.outwardEdgeTargetPosition anchor) O x a

noncomputable def Anderson4D.XYCluster.outward588WordOccurrenceFactor {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (anchor : Fin m) (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) : ℝ

Equations

• Anderson4D.XYCluster.outward588WordOccurrenceFactor Nm mu anchor O x = Anderson4D.assigned588WordOccurrenceFactor Nm mu (Anderson4D.XYCluster.outwardEdgeTargetPosition anchor) O x

theorem Anderson4D.XYCluster.outwardNXSkippedOccurrenceCount_le_multiplicityNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (anchor : Fin m) (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) (a : NXClass) (ha : a ∈ nxCarrier Nm mu) : outwardNXSkippedOccurrenceCount anchor O x a ≤ multiplicityNX Nm mu a

theorem Anderson4D.XYCluster.sum_outwardNXSkippedOccurrenceCount {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (anchor : Fin m) (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) : ∑ a ∈ nxCarrier Nm mu, outwardNXSkippedOccurrenceCount anchor O x a = O.card

theorem Anderson4D.XYCluster.outward588WordOccurrenceFactor_le_factorial {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (anchor : Fin m) (O : Finset (AdjacentIndex m)) (x : Fin m → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) (s : ℕ) (hm : totalMultiplicity mu = m) (hs : O.card = s) : outward588WordOccurrenceFactor Nm mu anchor O x ≤ (2 * Real.exp 1) ^ m * √↑(m - s).factorial * ∏ l : HeppLeaf t, √↑(leafMultiplicity mu l).factorial

The occurrence factor actually produced by the anchored outward schedule obeys the same factorial estimate as the paper's right-endpoint factor.

theorem Anderson4D.XYCluster.card_labeledCopiesAtNX_eq_multiplicityNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) : (labeledCopiesAtNX Nm mu a).card = multiplicityNX Nm mu a

A full (N,X) fiber contains exactly m_{N,X} labeled copies.

theorem Anderson4D.XYCluster.card_conditionedCopiesAtNX_le_multiplicityNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (used : Finset (HeppLabeledCopy mu)) (a : NXClass) : (conditionedCopiesAtNX Nm mu used a).card ≤ multiplicityNX Nm mu a

Deleting already exposed copies can only reduce the cardinality of a fiber, so every conditioned choice set has size at most m_{N,X}.

@[simp]

theorem Anderson4D.XYCluster.conditionedCopiesAtNX_empty {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) : conditionedCopiesAtNX Nm mu ∅ a = labeledCopiesAtNX Nm mu a

With no previously used copies, conditioning leaves the full fiber.

theorem Anderson4D.XYCluster.card_anchorCopyChoices_eq_multiplicityNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (x : Fin m → ActiveNXClass Nm mu) (anchor : Fin m) : (conditionedCopiesAtNX Nm mu ∅ ↑(x anchor)).card = multiplicityNX Nm mu ↑(x anchor)

Exact count for the independent choice of the copy at an anchor position.

theorem Anderson4D.XYCluster.sum_anchorCopyChoices_le_multiplicity_mul {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (x : Fin m → ActiveNXClass Nm mu) (anchor : Fin m) (F : HeppLabeledCopy mu → ℝ) (K : ℝ) (hF : ∀ c ∈ conditionedCopiesAtNX Nm mu ∅ ↑(x anchor), F c ≤ K) : ∑ c ∈ conditionedCopiesAtNX Nm mu ∅ ↑(x anchor), F c ≤ ↑(multiplicityNX Nm mu ↑(x anchor)) * K

A uniformly bounded summand over the independent anchor-copy choices costs at most the exact anchor multiplicity.

theorem Anderson4D.XYCluster.card_anchorCopyChoices_le_totalMultiplicity {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {m : ℕ} (x : Fin m → ActiveNXClass Nm mu) (anchor : Fin m) : (conditionedCopiesAtNX Nm mu ∅ ↑(x anchor)).card ≤ totalMultiplicity mu

The number of possible anchor copies never exceeds the total number of labeled copies.