Anchored reindexing for the arrangement Fubini step

The two outward elimination runs must enumerate every non-anchor position exactly once while retaining the same labeled copy at the anchor. This file packages that positional fact as an actual equivalence of Fin (n + 1).

The equivalence sends position zero to the anchor and then follows the flattened left/right schedule. Precomposition therefore reindexes labeled arrangements bijectively; in particular this operation cannot introduce an extra factorial or duplicate the anchor.

def Anderson4D.XYCluster.scheduleTail {α : Type u_1} {n : ℕ} (order : List α) (hlen : order.length = n) : Fin n → α

Read a length-n list as a function on Fin n.

Equations

• Anderson4D.XYCluster.scheduleTail order hlen i = order.get (Fin.cast ⋯ i)

theorem Anderson4D.XYCluster.scheduleTail_injective {α : Type u_1} {n : ℕ} (order : List α) (hlen : order.length = n) (hnodup : order.Nodup) : Function.Injective (scheduleTail order hlen)

theorem Anderson4D.XYCluster.scheduleTail_mem {α : Type u_1} {n : ℕ} (order : List α) (hlen : order.length = n) (i : Fin n) : scheduleTail order hlen i ∈ order

def Anderson4D.XYCluster.anchoredScheduleFunction {n : ℕ} (anchor : Fin (n + 1)) (order : List (Fin (n + 1))) (hlen : order.length = n) : Fin (n + 1) → Fin (n + 1)

The function which places anchor first and then reads the supplied schedule. The hypotheses say precisely that the schedule lists every non-anchor position once.

Equations

• Anderson4D.XYCluster.anchoredScheduleFunction anchor order hlen = Fin.cons anchor (Anderson4D.XYCluster.scheduleTail order hlen)

theorem Anderson4D.XYCluster.anchoredScheduleFunction_injective {n : ℕ} (anchor : Fin (n + 1)) (order : List (Fin (n + 1))) (hlen : order.length = n) (hnodup : order.Nodup) (hcover : ∀ (i : Fin (n + 1)), i ∈ order ↔ i ≠ anchor) : Function.Injective (anchoredScheduleFunction anchor order hlen)

noncomputable def Anderson4D.XYCluster.anchoredScheduleEquiv {n : ℕ} (anchor : Fin (n + 1)) (order : List (Fin (n + 1))) (hlen : order.length = n) (hnodup : order.Nodup) (hcover : ∀ (i : Fin (n + 1)), i ∈ order ↔ i ≠ anchor) : Fin (n + 1) ≃ Fin (n + 1)

The anchored schedule is a genuine permutation of the position type. Using an Equiv here, rather than a quotient or a cardinality identity, lets later sums be reindexed without any multiplicity factor.

Equations

• Anderson4D.XYCluster.anchoredScheduleEquiv anchor order hlen hnodup hcover = Equiv.ofBijective (Anderson4D.XYCluster.anchoredScheduleFunction anchor order hlen) ⋯

noncomputable def Anderson4D.XYCluster.anchoredScheduleEquivTo {β : Type u_1} [Fintype β] [DecidableEq β] {n : ℕ} (anchor : β) (order : List β) (hlen : order.length = n) (hnodup : order.Nodup) (hcover : ∀ (b : β), b ∈ order ↔ b ≠ anchor) (hcard : Fintype.card β = n + 1) : Fin (n + 1) ≃ β

Version of anchoredScheduleEquiv whose target is an arbitrary finite type of cardinality n+1. This avoids relying on a syntactic presentation of the paper length as a successor.

Equations

• Anderson4D.XYCluster.anchoredScheduleEquivTo anchor order hlen hnodup hcover hcard = Equiv.ofBijective (Fin.cons anchor (Anderson4D.XYCluster.scheduleTail order hlen)) ⋯

@[simp]

theorem Anderson4D.XYCluster.anchoredScheduleEquivTo_zero {β : Type u_1} [Fintype β] [DecidableEq β] {n : ℕ} (anchor : β) (order : List β) (hlen : order.length = n) (hnodup : order.Nodup) (hcover : ∀ (b : β), b ∈ order ↔ b ≠ anchor) (hcard : Fintype.card β = n + 1) : (anchoredScheduleEquivTo anchor order hlen hnodup hcover hcard) 0 = anchor

@[simp]

theorem Anderson4D.XYCluster.anchoredScheduleEquivTo_succ {β : Type u_1} [Fintype β] [DecidableEq β] {n : ℕ} (anchor : β) (order : List β) (hlen : order.length = n) (hnodup : order.Nodup) (hcover : ∀ (b : β), b ∈ order ↔ b ≠ anchor) (hcard : Fintype.card β = n + 1) (i : Fin n) : (anchoredScheduleEquivTo anchor order hlen hnodup hcover hcard) i.succ = scheduleTail order hlen i

@[simp]

theorem Anderson4D.XYCluster.anchoredScheduleEquiv_zero {n : ℕ} (anchor : Fin (n + 1)) (order : List (Fin (n + 1))) (hlen : order.length = n) (hnodup : order.Nodup) (hcover : ∀ (i : Fin (n + 1)), i ∈ order ↔ i ≠ anchor) : (anchoredScheduleEquiv anchor order hlen hnodup hcover) 0 = anchor

@[simp]

theorem Anderson4D.XYCluster.anchoredScheduleEquiv_succ {n : ℕ} (anchor : Fin (n + 1)) (order : List (Fin (n + 1))) (hlen : order.length = n) (hnodup : order.Nodup) (hcover : ∀ (i : Fin (n + 1)), i ∈ order ↔ i ≠ anchor) (i : Fin n) : (anchoredScheduleEquiv anchor order hlen hnodup hcover) i.succ = scheduleTail order hlen i

def Anderson4D.XYCluster.finAnchorOutwardOrderWithPhases {n : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) : List (Fin (n + 1))

The concrete outward order used by the one-parity schedule.

Equations

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

@[simp]

theorem Anderson4D.XYCluster.length_finAnchorOutwardOrderWithPhases {n : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) : (finAnchorOutwardOrderWithPhases leftPhase rightPhase anchor).length = n

theorem Anderson4D.XYCluster.nodup_finAnchorOutwardOrderWithPhases {n : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) : (finAnchorOutwardOrderWithPhases leftPhase rightPhase anchor).Nodup

@[simp]

theorem Anderson4D.XYCluster.mem_finAnchorOutwardOrderWithPhases_iff {n : ℕ} (leftPhase rightPhase : Bool) (anchor i : Fin (n + 1)) : i ∈ finAnchorOutwardOrderWithPhases leftPhase rightPhase anchor ↔ i ≠ anchor

noncomputable def Anderson4D.XYCluster.finAnchorOutwardEquivWithPhases {n : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) : Fin (n + 1) ≃ Fin (n + 1)

Concrete permutation which reads the anchor first and then all positions in the exact left-outward/right-outward block order.

Equations

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

@[simp]

theorem Anderson4D.XYCluster.finAnchorOutwardEquivWithPhases_zero {n : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) : (finAnchorOutwardEquivWithPhases leftPhase rightPhase anchor) 0 = anchor

def Anderson4D.XYCluster.reindexArrangement {ι : Type u_1} {β : Type u_2} (e : ι ≃ ι) (σ : ι ≃ β) : ι ≃ β

Precompose an arrangement by a permutation of its positions.

Equations

• Anderson4D.XYCluster.reindexArrangement e σ = e.trans σ

def Anderson4D.XYCluster.arrangementReindexEquiv {ι : Type u_1} {β : Type u_2} (e : ι ≃ ι) : ι ≃ β ≃ (ι ≃ β)

Position reindexing is itself a bijection on the arrangement carrier.

Equations

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

def Anderson4D.XYCluster.arrangementDomainEquiv {ι : Type u_1} {κ : Type u_2} {β : Type u_3} (e : ι ≃ κ) : κ ≃ β ≃ (ι ≃ β)

Change the position type of an arrangement by precomposition. Unlike arrangementReindexEquiv, the two position types may merely be equivalent; this is used below to replace the paper length m by (m - 1) + 1.

Equations

• Anderson4D.XYCluster.arrangementDomainEquiv e = { toFun := fun (σ : κ ≃ β) => e.trans σ, invFun := fun (σ : ι ≃ β) => e.symm.trans σ, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Anderson4D.XYCluster.arrangementDomainEquiv_apply {ι : Type u_1} {κ : Type u_2} {β : Type u_3} (e : ι ≃ κ) (σ : κ ≃ β) (i : ι) : ((arrangementDomainEquiv e) σ) i = σ (e i)

@[simp]

theorem Anderson4D.XYCluster.arrangementReindexEquiv_apply {ι : Type u_1} {β : Type u_2} (e : ι ≃ ι) (σ : ι ≃ β) (i : ι) : ((arrangementReindexEquiv e) σ) i = σ (e i)

@[simp]

theorem Anderson4D.XYCluster.arrangementReindexEquiv_symm_apply {ι : Type u_1} {β : Type u_2} (e : ι ≃ ι) (σ : ι ≃ β) (i : ι) : ((arrangementReindexEquiv e).symm σ) i = σ (e.symm i)

def Anderson4D.XYCluster.reindexNXWord {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (e : Fin m ≃ Fin m) (x : Fin m → ActiveNXClass Nm mu) : Fin m → ActiveNXClass Nm mu

Reindex a fixed active (N,X) word by the same position permutation.

Equations

• Anderson4D.XYCluster.reindexNXWord Nm mu e x i = x (e i)

@[simp]

theorem Anderson4D.XYCluster.reindexNXWord_symm_apply {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (e : Fin m ≃ Fin m) (x : Fin m → ActiveNXClass Nm mu) : reindexNXWord Nm mu e.symm (reindexNXWord Nm mu e x) = x

@[simp]

theorem Anderson4D.XYCluster.arrangementNXWord_reindex {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (e : Fin (totalMultiplicity mu) ≃ Fin (totalMultiplicity mu)) (σ : HeppArrangement mu) : arrangementNXWord Nm mu (reindexArrangement e σ) = reindexNXWord Nm mu e (arrangementNXWord Nm mu σ)

theorem Anderson4D.XYCluster.reindexArrangement_mem_arrangementsAtNXWord_iff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (e : Fin (totalMultiplicity mu) ≃ Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (σ : HeppArrangement mu) : reindexArrangement e σ ∈ arrangementsAtNXWord Nm mu (reindexNXWord Nm mu e x) ↔ σ ∈ arrangementsAtNXWord Nm mu x

noncomputable def Anderson4D.XYCluster.arrangementsAtNXWordReindexEquiv {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (e : Fin (totalMultiplicity mu) ≃ Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) : ↥(arrangementsAtNXWord Nm mu x) ≃ ↥(arrangementsAtNXWord Nm mu (reindexNXWord Nm mu e x))

The fixed-class-word arrangement fiber is carried bijectively to the reindexed class-word fiber. This is the fiberwise form needed after the outer finite-Fubini decomposition.

Equations

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

@[simp]

theorem Anderson4D.XYCluster.arrangementsAtNXWordReindexEquiv_pullback {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (e : Fin (totalMultiplicity mu) ≃ Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (σ : ↥(arrangementsAtNXWord Nm mu x)) : reindexArrangement e.symm ↑((arrangementsAtNXWordReindexEquiv Nm mu e x) σ) = ↑σ

theorem Anderson4D.XYCluster.sum_arrangementsAtNXWord_reindex {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (e : Fin (totalMultiplicity mu) ≃ Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (F : HeppArrangement mu → ℝ) : ∑ σ ∈ arrangementsAtNXWord Nm mu x, F σ = ∑ τ ∈ arrangementsAtNXWord Nm mu (reindexNXWord Nm mu e x), F (reindexArrangement e.symm τ)

Exact fiberwise sum reindexing. The right-hand fiber has the class word in anchored order, and its summand is pulled back to the original position order. No multiplicity coefficient appears.

theorem Anderson4D.XYCluster.sum_arrangements_reindex {ι : Type u_1} {β : Type u_2} [Fintype ι] [Fintype β] [DecidableEq ι] [DecidableEq β] (e : ι ≃ ι) (F : ι ≃ β → ℝ) : ∑ σ : ι ≃ β, F σ = ∑ σ : ι ≃ β, F ((arrangementReindexEquiv e).symm σ)

Exact finite-Fubini reindexing of the full arrangement sum. There is no cardinality coefficient: the right side is merely the same carrier read in anchored schedule order.

theorem Anderson4D.XYCluster.sum_arrangements_finAnchorOutward_reindex {t : PlaneTree} {mu : t.Multiplicities} {n : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (F : Fin (n + 1) ≃ HeppLabeledCopy mu → ℝ) : ∑ σ : Fin (n + 1) ≃ HeppLabeledCopy mu, F σ = ∑ σ : Fin (n + 1) ≃ HeppLabeledCopy mu, F ((arrangementReindexEquiv (finAnchorOutwardEquivWithPhases leftPhase rightPhase anchor)).symm σ)

Concrete anchored specialization. The summation variable on the right has its zeroth labeled copy equal to the original arrangement's anchor copy.

The non-vacuous paper-length carrier

@[simp]

theorem Anderson4D.XYCluster.card_heppLabeledCopy {t : PlaneTree} (mu : t.Multiplicities) : Fintype.card (HeppLabeledCopy mu) = totalMultiplicity mu

The labeled-copy carrier has exactly the paper word length.

def Anderson4D.XYCluster.paperTailLength {t : PlaneTree} (mu : t.Multiplicities) : ℕ

Number of positions remaining after the distinguished anchor is fixed.

Equations

• Anderson4D.XYCluster.paperTailLength mu = Anderson4D.totalMultiplicity mu - 1

@[simp]

theorem Anderson4D.XYCluster.one_le_paperTailLength {t : PlaneTree} (mu : t.Multiplicities) : 1 ≤ paperTailLength mu

@[simp]

theorem Anderson4D.XYCluster.paperTailLength_add_one {t : PlaneTree} (mu : t.Multiplicities) : paperTailLength mu + 1 = totalMultiplicity mu

def Anderson4D.XYCluster.paperPositionEquiv {t : PlaneTree} (mu : t.Multiplicities) : Fin (paperTailLength mu + 1) ≃ Fin (totalMultiplicity mu)

Canonical cast from the head-plus-tail positions to the paper positions.

Equations

• Anderson4D.XYCluster.paperPositionEquiv mu = (Fin.castOrderIso ⋯).toEquiv

def Anderson4D.XYCluster.paperArrangementEquivHeadTailPositions {t : PlaneTree} (mu : t.Multiplicities) : HeppArrangement mu ≃ (Fin (paperTailLength mu + 1) ≃ HeppLabeledCopy mu)

Every paper arrangement may therefore be read, non-vacuously, as one head followed by exactly paperTailLength tail positions.

Equations

• Anderson4D.XYCluster.paperArrangementEquivHeadTailPositions mu = Anderson4D.XYCluster.arrangementDomainEquiv (Anderson4D.XYCluster.paperPositionEquiv mu)

@[simp]

theorem Anderson4D.XYCluster.card_heppLabeledCopy_eq_paperTailLength_add_one {t : PlaneTree} (mu : t.Multiplicities) : Fintype.card (HeppLabeledCopy mu) = paperTailLength mu + 1

def Anderson4D.XYCluster.paperFinAnchorOutwardOrderWithPhases {t : PlaneTree} {mu : t.Multiplicities} (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) : List (Fin (totalMultiplicity mu))

The actual left-outward/right-outward list on paper positions.

Equations

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

@[simp]

theorem Anderson4D.XYCluster.length_paperFinAnchorOutwardOrderWithPhases {t : PlaneTree} {mu : t.Multiplicities} (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) : (paperFinAnchorOutwardOrderWithPhases leftPhase rightPhase anchor).length = paperTailLength mu

theorem Anderson4D.XYCluster.nodup_paperFinAnchorOutwardOrderWithPhases {t : PlaneTree} {mu : t.Multiplicities} (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) : (paperFinAnchorOutwardOrderWithPhases leftPhase rightPhase anchor).Nodup

@[simp]

theorem Anderson4D.XYCluster.mem_paperFinAnchorOutwardOrderWithPhases_iff {t : PlaneTree} {mu : t.Multiplicities} (leftPhase rightPhase : Bool) (anchor i : Fin (totalMultiplicity mu)) : i ∈ paperFinAnchorOutwardOrderWithPhases leftPhase rightPhase anchor ↔ i ≠ anchor

noncomputable def Anderson4D.XYCluster.paperFinAnchorOutwardEquivWithPhases {t : PlaneTree} {mu : t.Multiplicities} (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) : Fin (paperTailLength mu + 1) ≃ Fin (totalMultiplicity mu)

Concrete paper-position equivalence: zero is the anchor and the tail is exactly the schedule used by finAnchorNXCoarseRunsWithPhases.

Equations

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

@[simp]

theorem Anderson4D.XYCluster.paperFinAnchorOutwardEquivWithPhases_zero {t : PlaneTree} {mu : t.Multiplicities} (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) : (paperFinAnchorOutwardEquivWithPhases leftPhase rightPhase anchor) 0 = anchor

@[simp]

theorem Anderson4D.XYCluster.paperFinAnchorOutwardEquivWithPhases_succ {t : PlaneTree} {mu : t.Multiplicities} (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (i : Fin (paperTailLength mu)) : (paperFinAnchorOutwardEquivWithPhases leftPhase rightPhase anchor) i.succ = scheduleTail (paperFinAnchorOutwardOrderWithPhases leftPhase rightPhase anchor) ⋯ i

Exposing the anchored head and the outward tail

structure Anderson4D.XYCluster.AnchoredTailAssignment (β : Type u_1) (n : ℕ) : Type u_1

An anchor copy followed by an injective list of all remaining copies. The first field is required not to occur in the tail; together with tail injectivity this is exactly injectivity of Fin.cons.

• anchorCopy : β
• outwardCopies : Fin n → β
• anchor_not_range : self.anchorCopy ∉ Set.range self.outwardCopies
• outward_injective : Function.Injective self.outwardCopies

noncomputable def Anderson4D.XYCluster.arrangementEquivAnchoredTail {β : Type u_1} [Fintype β] {n : ℕ} (hcard : Fintype.card β = n + 1) : Fin (n + 1) ≃ β ≃ AnchoredTailAssignment β n

When the codomain has n+1 elements, arrangements are exactly an anchor copy followed by an injective tail avoiding that anchor. This is the carrier-level finite-Fubini decomposition before class conditions or weights are imposed.

Equations

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

def Anderson4D.XYCluster.ClassifiedAnchoredTailAssignment {β : Type u_1} {α : Type u_2} {n : ℕ} (classify : β → α) (x : Fin (n + 1) → α) : Type u_1

Class constraints on an anchored-tail assignment.

Equations

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

noncomputable def Anderson4D.XYCluster.classifiedArrangementEquivAnchoredTail {β : Type u_1} {α : Type u_2} [Fintype β] {n : ℕ} (hcard : Fintype.card β = n + 1) (classify : β → α) (x : Fin (n + 1) → α) : { σ : Fin (n + 1) ≃ β // ∀ (i : Fin (n + 1)), classify (σ i) = x i } ≃ ClassifiedAnchoredTailAssignment classify x

Fiberwise version of arrangementEquivAnchoredTail: a classified arrangement is exactly a classified anchor copy and classified outward tail. The class condition is pointwise and no counting factor is used.

Equations

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

Exact conditioned tuple sums

def Anderson4D.XYCluster.classifiedAvailableValues {β : Type u_1} {α : Type u_2} [Fintype β] [DecidableEq β] [DecidableEq α] (classify : β → α) (used : Finset β) (a : α) : Finset β

Values of a prescribed class which are not in the used set.

Equations

• Anderson4D.XYCluster.classifiedAvailableValues classify used a = {b : β | classify b = a} \ used

@[simp]

theorem Anderson4D.XYCluster.mem_classifiedAvailableValues_iff {β : Type u_1} {α : Type u_2} [Fintype β] [DecidableEq β] [DecidableEq α] (classify : β → α) (used : Finset β) (a : α) (b : β) : b ∈ classifiedAvailableValues classify used a ↔ classify b = a ∧ b ∉ used

def Anderson4D.XYCluster.ClassTupleAdmissible {β : Type u_1} {α : Type u_2} {n : ℕ} (classify : β → α) (used : Finset β) (classes : Fin n → α) (f : Fin n → β) : Prop

A tuple has the prescribed class word, is injective, and avoids all previously used values.

Equations

• Anderson4D.XYCluster.ClassTupleAdmissible classify used classes f = ((∀ (i : Fin n), classify (f i) = classes i) ∧ Function.Injective f ∧ ∀ (i : Fin n), f i ∉ used)

noncomputable def Anderson4D.XYCluster.classTupleEquivClassifiedArrangement {β : Type u_1} {α : Type u_2} [Fintype β] [DecidableEq β] {n : ℕ} (hcard : Fintype.card β = n + 1) (classify : β → α) (classes : Fin (n + 1) → α) : { f : Fin (n + 1) → β // ClassTupleAdmissible classify ∅ classes f } ≃ { σ : Fin (n + 1) ≃ β // ∀ (i : Fin (n + 1)), classify (σ i) = classes i }

At equal finite cardinalities, an admissible full tuple with no previously used values is exactly a classified arrangement. This equivalence rules out the vacuous unequal-cardinality case before the weighted Fubini identity is specialized to the paper carrier.

Equations

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

theorem Anderson4D.XYCluster.classTupleAdmissible_cons_iff {β : Type u_1} {α : Type u_2} [DecidableEq β] {n : ℕ} (classify : β → α) (used : Finset β) (classes : Fin (n + 1) → α) (b : β) (tail : Fin n → β) : ClassTupleAdmissible classify used classes (Fin.cons b tail) ↔ classify b = classes 0 ∧ b ∉ used ∧ ClassTupleAdmissible classify (insert b used) (Fin.tail classes) tail

noncomputable def Anderson4D.XYCluster.classifiedTupleSum {β : Type u_1} {α : Type u_2} [Fintype β] [DecidableEq β] [DecidableEq α] {n : ℕ} (classify : β → α) (used : Finset β) (classes : Fin n → α) (F : (Fin n → β) → ℝ) : ℝ

The exact finite sum over injective classified tuples avoiding used. Writing it as a full Fintype sum with an indicator makes reindexing by Fin.consEquiv transparent.

Equations

• Anderson4D.XYCluster.classifiedTupleSum classify used classes F = ∑ f : Fin n → β, if Anderson4D.XYCluster.ClassTupleAdmissible classify used classes f then F f else 0

@[simp]

theorem Anderson4D.XYCluster.classifiedTupleSum_zero {β : Type u_1} {α : Type u_2} [Fintype β] [DecidableEq β] [DecidableEq α] (classify : β → α) (used : Finset β) (classes : Fin 0 → α) (F : (Fin 0 → β) → ℝ) : classifiedTupleSum classify used classes F = F Fin.elim0

theorem Anderson4D.XYCluster.classifiedTupleSum_empty_eq_sum_classifiedArrangements {β : Type u_1} {α : Type u_2} [Fintype β] [DecidableEq β] [DecidableEq α] {n : ℕ} (hcard : Fintype.card β = n + 1) (classify : β → α) (classes : Fin (n + 1) → α) (F : (Fin (n + 1) → β) → ℝ) : classifiedTupleSum classify ∅ classes F = ∑ σ : { σ : Fin (n + 1) ≃ β // ∀ (i : Fin (n + 1)), classify (σ i) = classes i }, F ⇑↑σ

With no used values and matching cardinalities, the full-tuple indicator sum is the sum over classified arrangements. This is the exact bridge between the arrangement fiber and the recursive conditioned tuple sum.

theorem Anderson4D.XYCluster.classifiedTupleSum_succ {β : Type u_1} {α : Type u_2} [Fintype β] [DecidableEq β] [DecidableEq α] {n : ℕ} (classify : β → α) (used : Finset β) (classes : Fin (n + 1) → α) (F : (Fin (n + 1) → β) → ℝ) : classifiedTupleSum classify used classes F = ∑ b ∈ classifiedAvailableValues classify used (classes 0), classifiedTupleSum classify (insert b used) (Fin.tail classes) fun (tail : Fin n → β) => F (Fin.cons b tail)

One exact finite-Fubini step: expose the head copy in its conditioned class fiber, insert it into used, and continue with the tail. This is an identity, not an overcount.

theorem Anderson4D.XYCluster.classifiedTupleSum_succ_succ {β : Type u_1} {α : Type u_2} [Fintype β] [DecidableEq β] [DecidableEq α] {n : ℕ} (classify : β → α) (used : Finset β) (classes : Fin (n + 2) → α) (F : (Fin (n + 2) → β) → ℝ) : classifiedTupleSum classify used classes F = ∑ b ∈ classifiedAvailableValues classify used (classes 0), ∑ c ∈ classifiedAvailableValues classify (insert b used) (classes 1), classifiedTupleSum classify (insert c (insert b used)) (Fin.tail (Fin.tail classes)) fun (tail : Fin n → β) => F (Fin.cons b (Fin.cons c tail))

theorem Anderson4D.XYCluster.sum_classifiedArrangements_eq_anchor_classifiedTuple {β : Type u_1} {α : Type u_2} [Fintype β] [DecidableEq β] [DecidableEq α] {n : ℕ} (hcard : Fintype.card β = n + 1) (classify : β → α) (classes : Fin (n + 1) → α) (F : (Fin (n + 1) → β) → ℝ) : ∑ σ : { σ : Fin (n + 1) ≃ β // ∀ (i : Fin (n + 1)), classify (σ i) = classes i }, F ⇑↑σ = ∑ b ∈ classifiedAvailableValues classify ∅ (classes 0), classifiedTupleSum classify {b} (Fin.tail classes) fun (tail : Fin n → β) => F (Fin.cons b tail)

Exact head/tail decomposition of a classified arrangement fiber. The head is chosen once, the recursive tail avoids it, and no factorial coefficient or duplicate anchor is introduced.

def Anderson4D.XYCluster.labeledCopyActiveNXClass {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : HeppLabeledCopy mu → ActiveNXClass Nm mu

Active (N,X) classifier on the actual labeled-copy carrier.

Equations

• Anderson4D.XYCluster.labeledCopyActiveNXClass Nm mu c = Anderson4D.leafActiveNX Nm mu c.fst

def Anderson4D.XYCluster.labeledCopyNXClass {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : HeppLabeledCopy mu → NXClass

The underlying paper (N,X) classifier used by the local eliminator.

Equations

• Anderson4D.XYCluster.labeledCopyNXClass Nm mu c = Anderson4D.singleScaleSigma1 Nm mu c.fst

noncomputable def Anderson4D.XYCluster.arrangementsAtNXWordDomainEquiv {t : PlaneTree} {n : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (e : Fin n ≃ Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) : ↥(arrangementsAtNXWord Nm mu x) ≃ { τ : Fin n ≃ HeppLabeledCopy mu // ∀ (i : Fin n), labeledCopyNXClass Nm mu (τ i) = ↑(x (e i)) }

After any position reindexing, a fixed (N,X) arrangement fiber is exactly the corresponding subtype of pointwise-classified arrangements.

Equations

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

theorem Anderson4D.XYCluster.sum_arrangementsAtNXWord_eq_anchor_classifiedTuple {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (e : Fin (paperTailLength mu + 1) ≃ Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (F : (Fin (totalMultiplicity mu) → HeppLabeledCopy mu) → ℝ) : ∑ σ ∈ arrangementsAtNXWord Nm mu x, F ⇑σ = ∑ b ∈ classifiedAvailableValues (labeledCopyNXClass Nm mu) ∅ ↑(x (e 0)), classifiedTupleSum (labeledCopyNXClass Nm mu) {b} (fun (i : Fin (paperTailLength mu)) => ↑(x (e i.succ))) fun (tail : Fin (paperTailLength mu) → HeppLabeledCopy mu) => F fun (j : Fin (totalMultiplicity mu)) => Fin.cons b tail (e.symm j)

Exact weighted head/tail Fubini formula for an actual fixed (N,X) word fiber. The arbitrary equivalence e will be instantiated by the concrete outward schedule; its zeroth position is the distinguished anchor.

theorem Anderson4D.XYCluster.classifiedAvailableValues_labeledCopyNXClass {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (used : Finset (HeppLabeledCopy mu)) (a : NXClass) : classifiedAvailableValues (labeledCopyNXClass Nm mu) used a = conditionedCopiesAtNX Nm mu used a

The generic conditioned carrier is definitionally the project carrier conditionedCopiesAtNX on labeled copies.

theorem Anderson4D.XYCluster.sum_arrangementsAtNXWord_eq_finAnchorOutward_classifiedTuple {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (F : (Fin (totalMultiplicity mu) → HeppLabeledCopy mu) → ℝ) : ∑ σ ∈ arrangementsAtNXWord Nm mu x, F ⇑σ = ∑ b ∈ conditionedCopiesAtNX Nm mu ∅ ↑(x anchor), classifiedTupleSum (labeledCopyNXClass Nm mu) {b} (fun (i : Fin (paperTailLength mu)) => ↑(x ((paperFinAnchorOutwardEquivWithPhases leftPhase rightPhase anchor) i.succ))) fun (tail : Fin (paperTailLength mu) → HeppLabeledCopy mu) => F fun (j : Fin (totalMultiplicity mu)) => Fin.cons b tail ((paperFinAnchorOutwardEquivWithPhases leftPhase rightPhase anchor).symm j)

Concrete fixed-fiber Fubini formula in the exact outward order used by the two shared-state elimination runs. Its outer carrier is already the project's conditioned (N,X) copy carrier.