Documentation

Anderson4D.PermSum.SingleScaleFiberCPS

Fixed-fiber Fubini to the shared-state CPS eliminator #

The arrangement fiber exposes the anchor and then a Fin-indexed outward tail. This file gives the analytic block schedule its own exact arity, class word, and assignment monomial. Repeated use of the exact classifiedTupleSum_succ identity identifies the resulting finite sum with the conditioned eliminator, including the shared used-copy state between the left and right runs.

Sequential class words and assignment monomials #

def Anderson4D.XYCluster.nxParityBlockArity {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} :

NXParityBlock Nm mu → ℕ

Number of labeled copies consumed by one analytic block.

Equations

Instances For

def Anderson4D.XYCluster.nxParityScheduleArity {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} :

List (NXParityBlock Nm mu) → ℕ

Total number of copies consumed by an analytic schedule.

Equations

Instances For

@[simp]

theorem Anderson4D.XYCluster.nxParityScheduleArity_append {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (ps qs : List (NXParityBlock Nm mu)) :

nxParityScheduleArity (ps ++ qs) = nxParityScheduleArity ps + nxParityScheduleArity qs

def Anderson4D.XYCluster.nxParityScheduleClasses {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (ps : List (NXParityBlock Nm mu)) :

Fin (nxParityScheduleArity ps) → NXClass

Underlying (N,X) class word consumed by a schedule.

Equations

Instances For

def Anderson4D.XYCluster.nxParityBlockClassList {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} :

NXParityBlock Nm mu → List NXClass

The same class word as an ordinary list, useful for comparing the analytic schedule with the flattened paper-position schedule.

Equations

Instances For

def Anderson4D.XYCluster.nxParityScheduleClassList {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (ps : List (NXParityBlock Nm mu)) :

Equations

Anderson4D.XYCluster.nxParityScheduleClassList ps = List.flatMap Anderson4D.XYCluster.nxParityBlockClassList ps

Instances For

@[simp]

theorem Anderson4D.XYCluster.length_nxParityScheduleClassList {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (ps : List (NXParityBlock Nm mu)) :

(nxParityScheduleClassList ps).length = nxParityScheduleArity ps

@[simp]

theorem Anderson4D.XYCluster.ofFn_nxParityScheduleClasses {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (ps : List (NXParityBlock Nm mu)) :

List.ofFn (nxParityScheduleClasses ps) = nxParityScheduleClassList ps

@[simp]

theorem Anderson4D.XYCluster.nxParityBlockClassList_positionBlockToNXParityBlock {α : Type u_1} {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (cls : α → ActiveNXClass Nm mu) (incomingSkipped : α → Bool) (b : PositionBlock α) :

nxParityBlockClassList (positionBlockToNXParityBlock Nm mu cls incomingSkipped b) = List.map (fun (i : α) => ↑(cls i)) b.entries

Attaching payloads to a position block records exactly the classes of its entries, in traversal order.

theorem Anderson4D.XYCluster.nxParityScheduleClassList_map_positionBlocks {α : Type u_1} {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (cls : α → ActiveNXClass Nm mu) (incomingSkipped : α → Bool) (bs : List (PositionBlock α)) :

nxParityScheduleClassList (List.map (positionBlockToNXParityBlock Nm mu cls incomingSkipped) bs) = List.map (fun (i : α) => ↑(cls i)) (List.flatMap PositionBlock.entries bs)

theorem Anderson4D.XYCluster.nxParityScheduleClassList_markFirstSkippedPairsRough {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (fuel : ℕ) (ps : List (NXParityBlock Nm mu)) :

nxParityScheduleClassList (markFirstSkippedPairsRough fuel ps) = nxParityScheduleClassList ps

Rough-pair marking changes only the estimate selected for a pair, not the ordered class word which is summed over.

theorem Anderson4D.XYCluster.nxParityScheduleClassList_finAnchorNXCoarseLedgerWithPhases {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (cls : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (totalMultiplicity mu))) :

nxParityScheduleClassList (finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = List.map (fun (i : Fin (totalMultiplicity mu)) => ↑(cls i)) (paperFinAnchorOutwardOrderWithPhases leftPhase rightPhase anchor)

The analytic coarse ledger spells the paper's concrete outward class word exactly; rough marking neither permutes nor duplicates a position.

@[simp]

theorem Anderson4D.XYCluster.nxParityScheduleArity_finAnchorNXCoarseRunsWithPhases {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (cls : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (totalMultiplicity mu))) :

nxParityScheduleArity (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).ledger = paperTailLength mu

@[simp]

theorem Anderson4D.XYCluster.scheduleTail_nxParityScheduleClassList {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (ps : List (NXParityBlock Nm mu)) (i : Fin (nxParityScheduleArity ps)) :

scheduleTail (nxParityScheduleClassList ps) ⋯ i = nxParityScheduleClasses ps i

theorem Anderson4D.XYCluster.scheduleTail_map {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (xs : List α) (hlen : xs.length = n) (i : Fin n) :

scheduleTail (List.map f xs) ⋯ i = f (scheduleTail xs hlen i)

scheduleTail commutes with mapping an ordinary finite list.

@[simp]

theorem Anderson4D.XYCluster.nxParityScheduleArity_finAnchorNXCoarseLedgerWithPhases {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (cls : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (totalMultiplicity mu))) :

nxParityScheduleArity (finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = paperTailLength mu

theorem Anderson4D.XYCluster.nxParityScheduleClasses_finAnchorNXCoarseLedgerWithPhases {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (cls : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (totalMultiplicity mu))) (i : Fin (nxParityScheduleArity (finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O))) :

nxParityScheduleClasses (finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) i = ↑(cls ((paperFinAnchorOutwardEquivWithPhases leftPhase rightPhase anchor) (Fin.cast ⋯ i).succ))

The recursive CPS class function is exactly the class word exposed by the paper's concrete outward equivalence.

theorem Anderson4D.XYCluster.nxParityScheduleClasses_finAnchorNXCoarseLedgerWithPhases_fun {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (cls : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (totalMultiplicity mu))) :

nxParityScheduleClasses (finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = (fun (i : Fin (paperTailLength mu)) => ↑(cls ((paperFinAnchorOutwardEquivWithPhases leftPhase rightPhase anchor) i.succ))) ∘ Fin.cast ⋯

@[simp]

theorem Anderson4D.XYCluster.ofFn_scheduleTail {α : Type u_1} {n : ℕ} (order : List α) (hlen : order.length = n) :

List.ofFn (scheduleTail order hlen) = order

theorem Anderson4D.XYCluster.ofFn_comp_finCast {α : Type u_1} {m n : ℕ} (h : m = n) (f : Fin n → α) :

List.ofFn (f ∘ Fin.cast h) = List.ofFn f

theorem Anderson4D.XYCluster.ofFn_finAnchorOutward_tailClasses {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (cls : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) :

(List.ofFn fun (i : Fin (paperTailLength mu)) => ↑(cls ((paperFinAnchorOutwardEquivWithPhases leftPhase rightPhase anchor) i.succ))) = List.map (fun (i : Fin (totalMultiplicity mu)) => ↑(cls i)) (paperFinAnchorOutwardOrderWithPhases leftPhase rightPhase anchor)

theorem Anderson4D.XYCluster.nxParityScheduleClasses_finAnchorNXCoarseRunsWithPhases_fun {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (cls : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (totalMultiplicity mu))) :

let runs := finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O; nxParityScheduleClasses runs.ledger = (fun (i : Fin (paperTailLength mu)) => ↑(cls ((paperFinAnchorOutwardEquivWithPhases leftPhase rightPhase anchor) i.succ))) ∘ Fin.cast ⋯

Reconstructing the full position assignment #

noncomputable def Anderson4D.XYCluster.paperFinAnchorAssignmentFromTail {t : PlaneTree} {mu : t.Multiplicities} (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (b : HeppLabeledCopy mu) (tail : Fin (paperTailLength mu) → HeppLabeledCopy mu) :

Fin (totalMultiplicity mu) → HeppLabeledCopy mu

Insert the exposed anchor copy in front of an outward tail and transport the result back to the original paper positions.

Equations

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

Instances For

@[simp]

theorem Anderson4D.XYCluster.paperFinAnchorAssignmentFromTail_anchor {t : PlaneTree} {mu : t.Multiplicities} (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (b : HeppLabeledCopy mu) (tail : Fin (paperTailLength mu) → HeppLabeledCopy mu) :

paperFinAnchorAssignmentFromTail leftPhase rightPhase anchor b tail anchor = b

@[simp]

theorem Anderson4D.XYCluster.paperFinAnchorAssignmentFromTail_outward {t : PlaneTree} {mu : t.Multiplicities} (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (b : HeppLabeledCopy mu) (tail : Fin (paperTailLength mu) → HeppLabeledCopy mu) (i : Fin (paperTailLength mu)) :

paperFinAnchorAssignmentFromTail leftPhase rightPhase anchor b tail ((paperFinAnchorOutwardEquivWithPhases leftPhase rightPhase anchor) i.succ) = tail i

def Anderson4D.XYCluster.finTupleHead {β : Type u_1} {n : ℕ} (f : Fin (n + 1) → β) :

β

Head of a nonempty finite tuple, with a stable simplification rule.

Equations

Anderson4D.XYCluster.finTupleHead f = f 0

Instances For

@[simp]

theorem Anderson4D.XYCluster.finTupleHead_cons {β : Type u_1} {n : ℕ} (b : β) (f : Fin n → β) :

finTupleHead (Fin.cons b f) = b

noncomputable def Anderson4D.XYCluster.nxParityScheduleKernel {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (ps : List (NXParityBlock Nm mu)) :

(Fin 4 → ℤ) → (Fin (nxParityScheduleArity ps) → HeppLabeledCopy mu) → ℝ

Lambda/strongLambda monomial attached to a complete sequential assignment. The endpoint of each block is the preceding point for the next block.

Equations

One or more equations did not get rendered due to their size.
Anderson4D.XYCluster.nxParityScheduleKernel ht hroot Nm mu z hz R [] x✝ _f = 1

Instances For

noncomputable def Anderson4D.XYCluster.nxAnchoredScheduleKernel {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (left right : List (NXParityBlock Nm mu)) :

(Fin 4 → ℤ) → (Fin 4 → ℤ) → (Fin (nxParityScheduleArity (left ++ right)) → HeppLabeledCopy mu) → ℝ

Assignment monomial for two outward runs. The right run starts only after all left copies have been consumed, but its geometric starting point is reset to the anchor.

Equations

One or more equations did not get rendered due to their size.
Anderson4D.XYCluster.nxAnchoredScheduleKernel ht hroot Nm mu z hz R [] x✝³ x✝² x✝¹ x✝ = Anderson4D.XYCluster.nxParityScheduleKernel ht hroot Nm mu z hz R x✝³ x✝² x✝

Instances For

Exact tuple-sum recursion #

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

(classifiedTupleSum classify used classes fun (f : Fin n → β) => c * F f) = c * classifiedTupleSum classify used classes F

theorem Anderson4D.XYCluster.classifiedTupleSum_mono {β : Type u_1} {α : Type u_2} [Fintype β] [DecidableEq β] [DecidableEq α] {n : ℕ} (classify : β → α) (used : Finset β) (classes : Fin n → α) (F G : (Fin n → β) → ℝ) (hFG : ∀ (f : Fin n → β), ClassTupleAdmissible classify used classes f → F f ≤ G f) :

classifiedTupleSum classify used classes F ≤ classifiedTupleSum classify used classes G

theorem Anderson4D.XYCluster.classifiedTupleSum_nxParityScheduleKernel {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (ps : List (NXParityBlock Nm mu)) (used : Finset (HeppLabeledCopy mu)) (u : Fin 4 → ℤ) :

classifiedTupleSum (labeledCopyNXClass Nm mu) used (nxParityScheduleClasses ps) (nxParityScheduleKernel ht hroot Nm mu z hz R ps u) = conditionedNXParityChainSum ht hroot Nm mu z hz R ps used u

Exact finite-Fubini identity for one analytic schedule.

theorem Anderson4D.XYCluster.classifiedTupleSum_nxAnchoredScheduleKernel {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (left right : List (NXParityBlock Nm mu)) (used : Finset (HeppLabeledCopy mu)) (anchorPoint u : Fin 4 → ℤ) :

classifiedTupleSum (labeledCopyNXClass Nm mu) used (nxParityScheduleClasses (left ++ right)) (nxAnchoredScheduleKernel ht hroot Nm mu z hz R left right anchorPoint u) = conditionedNXParityChainSumThen ht hroot Nm mu z hz R left used u fun (usedAfterLeft : Finset (HeppLabeledCopy mu)) (_leftEndpoint : Fin 4 → ℤ) => conditionedNXParityChainSum ht hroot Nm mu z hz R right usedAfterLeft anchorPoint

Exact two-run identity with one shared used-copy state and a geometric reset at the anchor. No concatenated analytic chain is introduced.

theorem Anderson4D.XYCluster.classifiedTupleSum_nxAnchoredScheduleKernel_cast {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (left right : List (NXParityBlock Nm mu)) (used : Finset (HeppLabeledCopy mu)) (anchorPoint u : Fin 4 → ℤ) (n : ℕ) (hArity : nxParityScheduleArity (left ++ right) = n) (classes : Fin n → NXClass) (hClasses : nxParityScheduleClasses (left ++ right) = classes ∘ Fin.cast hArity) :

(classifiedTupleSum (labeledCopyNXClass Nm mu) used classes fun (f : Fin n → HeppLabeledCopy mu) => nxAnchoredScheduleKernel ht hroot Nm mu z hz R left right anchorPoint u (f ∘ Fin.cast hArity)) = conditionedNXParityChainSumThen ht hroot Nm mu z hz R left used u fun (usedAfterLeft : Finset (HeppLabeledCopy mu)) (_leftEndpoint : Fin 4 → ℤ) => conditionedNXParityChainSum ht hroot Nm mu z hz R right usedAfterLeft anchorPoint

The exact two-run identity is invariant under casting the finite tuple length. This is the dependent transport used by the paper-length Fubini formula.

theorem Anderson4D.XYCluster.sum_arrangementsAtNXWord_le_conditionedNXAnchoredRunsSum {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (left right : List (NXParityBlock Nm mu)) (hArity : nxParityScheduleArity (left ++ right) = paperTailLength mu) (hClasses : nxParityScheduleClasses (left ++ right) = (fun (i : Fin (paperTailLength mu)) => ↑(x ((paperFinAnchorOutwardEquivWithPhases leftPhase rightPhase anchor) i.succ))) ∘ Fin.cast hArity) (F : (Fin (totalMultiplicity mu) → HeppLabeledCopy mu) → ℝ) (hF : ∀ b ∈ conditionedCopiesAtNX Nm mu ∅ ↑(x anchor), ∀ (tail : Fin (paperTailLength mu) → HeppLabeledCopy mu), ClassTupleAdmissible (labeledCopyNXClass Nm mu) {b} (fun (i : Fin (paperTailLength mu)) => ↑(x ((paperFinAnchorOutwardEquivWithPhases leftPhase rightPhase anchor) i.succ))) tail → (F fun (j : Fin (totalMultiplicity mu)) => Fin.cons b tail ((paperFinAnchorOutwardEquivWithPhases leftPhase rightPhase anchor).symm j)) ≤ nxAnchoredScheduleKernel ht hroot Nm mu z hz R left right (labeledCopyPoint z b) (labeledCopyPoint z b) (tail ∘ Fin.cast hArity)) :

∑ σ ∈ arrangementsAtNXWord Nm mu x, F ⇑σ ≤ ∑ b ∈ conditionedCopiesAtNX Nm mu ∅ ↑(x anchor), conditionedNXAnchoredRunsSum ht hroot Nm mu z hz R left right {b} (labeledCopyPoint z b)

Abstract fixed-fiber bridge. Once a pointwise scheduled-kernel bound is supplied, the exact paper Fubini identity and the shared-state CPS recursion sum it without an overcount or an extra factorial.

theorem Anderson4D.XYCluster.sum_arrangementsAtNXWord_le_finAnchorNXCoarseRunsSum_of_pointwise {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (totalMultiplicity mu))) (F : (Fin (totalMultiplicity mu) → HeppLabeledCopy mu) → ℝ) (hF : ∀ b ∈ conditionedCopiesAtNX Nm mu ∅ ↑(x anchor), ∀ (tail : Fin (paperTailLength mu) → HeppLabeledCopy mu), ClassTupleAdmissible (labeledCopyNXClass Nm mu) {b} (fun (i : Fin (paperTailLength mu)) => ↑(x ((paperFinAnchorOutwardEquivWithPhases leftPhase rightPhase anchor) i.succ))) tail → F (paperFinAnchorAssignmentFromTail leftPhase rightPhase anchor b tail) ≤ let runs := finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor x O; nxAnchoredScheduleKernel ht hroot Nm mu z hz R runs.left runs.right (labeledCopyPoint z b) (labeledCopyPoint z b) (tail ∘ Fin.cast ⋯)) :

have runs := finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor x O; ∑ σ ∈ arrangementsAtNXWord Nm mu x, F ⇑σ ≤ ∑ b ∈ conditionedCopiesAtNX Nm mu ∅ ↑(x anchor), conditionedNXAnchoredRunsSum ht hroot Nm mu z hz R runs.left runs.right {b} (labeledCopyPoint z b)

Canonical coarse-schedule specialization of the abstract fixed-fiber bridge. The caller now supplies only the pointwise kernel comparison; all length and class-word transports are discharged here.