Alignment of the located kernel ledger with the fiber CPS kernel

The kernel schedule keeps original positions, while the finite-Fubini/CPS schedule keeps only analytic (N,X) blocks and consumes a finite tuple. This file records the missing pointwise alignment. The central certificate LocatedRunConsecutive says exactly that a located run starts at a given position and then visits consecutive positions away from the anchor.

Rough marking is harmless here: .pair and .roughPair retain the same two positions and both kernel definitions use the same lambda * strongLambda monomial.

Assignment and consecutiveness certificates

def Anderson4D.XYCluster.locatedScheduleAssignment {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (σ : Fin m → HeppLabeledCopy mu) (bs : List (LocatedNXParityBlock Nm mu)) : Fin (nxParityScheduleArity (List.map LocatedNXParityBlock.analyticBlock bs)) → HeppLabeledCopy mu

Read a fixed position assignment in the exact tuple order consumed by a located ledger.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.locatedScheduleAssignment σ [] = Fin.elim0
• Anderson4D.XYCluster.locatedScheduleAssignment σ (Anderson4D.XYCluster.LocatedNXParityBlock.single i _a _skipped :: bs) = Fin.cons (σ i) (Anderson4D.XYCluster.locatedScheduleAssignment σ bs)

def Anderson4D.XYCluster.locatedAnchoredScheduleAssignment {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (σ : Fin m → HeppLabeledCopy mu) (left right : List (LocatedNXParityBlock Nm mu)) : Fin (nxParityScheduleArity (List.map LocatedNXParityBlock.analyticBlock left ++ List.map LocatedNXParityBlock.analyticBlock right)) → HeppLabeledCopy mu

The analogous assignment for two outward runs. It is defined in the same recursion pattern as nxAnchoredScheduleKernel, so no dependent cast is hidden at the run boundary.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.locatedAnchoredScheduleAssignment σ [] x✝ = Anderson4D.XYCluster.locatedScheduleAssignment σ x✝

theorem Anderson4D.XYCluster.ofFn_locatedScheduleAssignment {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (σ : Fin m → HeppLabeledCopy mu) (bs : List (LocatedNXParityBlock Nm mu)) : List.ofFn (locatedScheduleAssignment σ bs) = List.map σ (List.flatMap (fun (b : LocatedNXParityBlock Nm mu) => b.positionBlock.entries) bs)

theorem Anderson4D.XYCluster.ofFn_locatedAnchoredScheduleAssignment {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (σ : Fin m → HeppLabeledCopy mu) (left right : List (LocatedNXParityBlock Nm mu)) : List.ofFn (locatedAnchoredScheduleAssignment σ left right) = List.map σ (List.flatMap (fun (b : LocatedNXParityBlock Nm mu) => b.positionBlock.entries) left ++ List.flatMap (fun (b : LocatedNXParityBlock Nm mu) => b.positionBlock.entries) right)

The anchored assignment reads the two located ledgers in order. The explicit arity casts below isolate the otherwise fragile dependent normalization at the left ++ right boundary.

inductive Anderson4D.XYCluster.LocatedRunConsecutive {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (anchor : Fin m) : Fin m → List (LocatedNXParityBlock Nm mu) → Prop

A located run is consecutive away from anchor, beginning just outside previous. The endpoint of each block becomes the preceding position for the next block.

• nil {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} {anchor : Fin m} (previous : Fin m) : LocatedRunConsecutive anchor previous []
• single {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} {anchor : Fin m} (previous i : Fin m) (a : ActiveNXClass Nm mu) (skipped : Bool) (bs : List (LocatedNXParityBlock Nm mu)) (hprevious : outwardPreviousPosition anchor i = previous) (hrest : LocatedRunConsecutive anchor i bs) : LocatedRunConsecutive anchor previous (LocatedNXParityBlock.single i a skipped :: bs)
• pair {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} {anchor : Fin m} (previous i j : Fin m) (p : NXPairBlock Nm mu) (bs : List (LocatedNXParityBlock Nm mu)) (hprevious : outwardPreviousPosition anchor i = previous) (hinternal : outwardPreviousPosition anchor j = i) (hrest : LocatedRunConsecutive anchor j bs) : LocatedRunConsecutive anchor previous (LocatedNXParityBlock.pair i j p :: bs)
• roughPair {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} {anchor : Fin m} (previous i j : Fin m) (p : NXPairBlock Nm mu) (bs : List (LocatedNXParityBlock Nm mu)) (hprevious : outwardPreviousPosition anchor i = previous) (hinternal : outwardPreviousPosition anchor j = i) (hrest : LocatedRunConsecutive anchor j bs) : LocatedRunConsecutive anchor previous (LocatedNXParityBlock.roughPair i j p :: bs)

def Anderson4D.XYCluster.OutwardPositionChain {m : ℕ} (anchor : Fin m) : Fin m → List (Fin m) → Prop

Position-only version of the same consecutive-run condition.

Equations

• Anderson4D.XYCluster.OutwardPositionChain anchor x✝ [] = True
• Anderson4D.XYCluster.OutwardPositionChain anchor x✝ (i :: is) = (Anderson4D.XYCluster.outwardPreviousPosition anchor i = x✝ ∧ Anderson4D.XYCluster.OutwardPositionChain anchor i is)

theorem Anderson4D.XYCluster.locatedRunConsecutive_of_flatten_positionBlocks {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (anchor previous : Fin m) (bs : List (LocatedNXParityBlock Nm mu)) (xs : List (Fin m)) (hflat : List.flatMap PositionBlock.entries (List.map LocatedNXParityBlock.positionBlock bs) = xs) (hchain : OutwardPositionChain anchor previous xs) : LocatedRunConsecutive anchor previous bs

Any located block partition of a consecutive position list inherits the kernel alignment certificate. This is the reusable raw pairPositionRun interface; it is insensitive to rough marking.

theorem Anderson4D.XYCluster.locatedRunConsecutive_of_map_positionBlock_eq_pairPositionRun {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (anchor previous : Fin m) (bs : List (LocatedNXParityBlock Nm mu)) (phase : Bool) (xs : List (Fin m)) (hblocks : List.map LocatedNXParityBlock.positionBlock bs = pairPositionRun phase xs) (hchain : OutwardPositionChain anchor previous xs) : LocatedRunConsecutive anchor previous bs

Raw pairPositionRun wrapper. A rough-marked located list aligns whenever erasing its rough metadata recovers the raw pairing schedule.

theorem Anderson4D.XYCluster.map_positionBlock_finAnchorNXLocatedCoarseRunsWithPhases_left {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : List.map LocatedNXParityBlock.positionBlock (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left = pairPositionRun leftPhase (leftAnchorPositions anchor)

Rough marking and the canonical split retain the raw left position pairing schedule exactly.

theorem Anderson4D.XYCluster.map_positionBlock_finAnchorNXLocatedCoarseRunsWithPhases_right {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : List.map LocatedNXParityBlock.positionBlock (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right = pairPositionRun rightPhase (rightAnchorPositions anchor)

Rough marking and the canonical split retain the raw right position pairing schedule exactly.

def Anderson4D.XYCluster.FinAnchorOutwardChainCondition {m : ℕ} (anchor : Fin m) : Prop

The sole position-only condition still needed to instantiate the canonical alignment. It contains no classes, skip flags, rough marking, or kernels.

Equations

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

theorem Anderson4D.XYCluster.finAnchorOutwardChainCondition {m : ℕ} (anchor : Fin m) : FinAnchorOutwardChainCondition anchor

The canonical left/right position schedules really are consecutive outward runs.

theorem Anderson4D.XYCluster.finAnchorNXLocatedCoarseRuns_consecutive_of_chainCondition {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) (hchain : FinAnchorOutwardChainCondition anchor) : LocatedRunConsecutive anchor anchor (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left ∧ LocatedRunConsecutive anchor anchor (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right

The position-only chain condition produces both actual coarse-run certificates.

Exact kernel equalities from the certificate

theorem Anderson4D.XYCluster.locatedLedgerEliminationKernelProduct_eq_scheduleKernel {t : PlaneTree} {m : ℕ} (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 : ℝ) (anchor previous : Fin m) (σ : Fin m → HeppLabeledCopy mu) (bs : List (LocatedNXParityBlock Nm mu)) (halign : LocatedRunConsecutive anchor previous bs) : locatedLedgerEliminationKernelProduct ht hroot Nm mu z hz R anchor σ bs = nxParityScheduleKernel ht hroot Nm mu z hz R (List.map LocatedNXParityBlock.analyticBlock bs) (labeledCopyPoint z (σ previous)) (locatedScheduleAssignment σ bs)

For a consecutive located run, the product of located elimination monomials is exactly the recursive CPS assignment monomial.

theorem Anderson4D.XYCluster.locatedOutwardRunsEliminationKernelProduct_eq_anchoredScheduleKernel {t : PlaneTree} {m : ℕ} (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 : ℝ) (anchor : Fin m) (σ : Fin m → HeppLabeledCopy mu) (left right : List (LocatedNXParityBlock Nm mu)) (previous : Fin m) (hleft : LocatedRunConsecutive anchor previous left) (hright : LocatedRunConsecutive anchor anchor right) : locatedLedgerEliminationKernelProduct ht hroot Nm mu z hz R anchor σ left * locatedLedgerEliminationKernelProduct ht hroot Nm mu z hz R anchor σ right = nxAnchoredScheduleKernel ht hroot Nm mu z hz R (List.map LocatedNXParityBlock.analyticBlock left) (List.map LocatedNXParityBlock.analyticBlock right) (labeledCopyPoint z (σ anchor)) (labeledCopyPoint z (σ previous)) (locatedAnchoredScheduleAssignment σ left right)

Two consecutive outward runs give exactly nxAnchoredScheduleKernel: the right run starts from the anchor point after the left tuple has been consumed, with no cross-run factor.

theorem Anderson4D.XYCluster.edgeKernelProduct_le_finAnchorNXAnchoredScheduleKernel_of_consecutive {t : PlaneTree} {m : ℕ} (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 : ℝ) (O : Finset (AdjacentIndex m)) (leftPhase rightPhase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (σ : Fin m → HeppLabeledCopy mu) (hleft : LocatedRunConsecutive anchor anchor (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left) (hright : LocatedRunConsecutive anchor anchor (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right) : ∏ edge : AdjacentIndex m, finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz R O leftPhase rightPhase anchor cls σ edge ≤ nxAnchoredScheduleKernel ht hroot Nm mu z hz R (List.map LocatedNXParityBlock.analyticBlock (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left) (List.map LocatedNXParityBlock.analyticBlock (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right) (labeledCopyPoint z (σ anchor)) (labeledCopyPoint z (σ anchor)) (locatedAnchoredScheduleAssignment σ (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right)

Pointwise bridge ready for the finite-Fubini monotonicity theorem. The only structural inputs are the two consecutive-run certificates; all analytic kernel comparison has already been discharged by KernelSchedule.

Canonical finite-Fubini assignment

theorem Anderson4D.XYCluster.flatMap_positionEntries_finAnchorNXLocatedCoarseRuns_left {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : List.flatMap (fun (b : LocatedNXParityBlock Nm mu) => b.positionBlock.entries) (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left = leftAnchorPositions anchor

theorem Anderson4D.XYCluster.flatMap_positionEntries_finAnchorNXLocatedCoarseRuns_right {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : List.flatMap (fun (b : LocatedNXParityBlock Nm mu) => b.positionBlock.entries) (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right = rightAnchorPositions anchor

theorem Anderson4D.XYCluster.append_flatMap_positionEntries_finAnchorNXLocatedCoarseRuns {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : List.flatMap (fun (b : LocatedNXParityBlock Nm mu) => b.positionBlock.entries) (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left ++ List.flatMap (fun (b : LocatedNXParityBlock Nm mu) => b.positionBlock.entries) (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right = List.flatMap PositionBlock.entries (finAnchorPositionScheduleWithPhases leftPhase rightPhase anchor)

theorem Anderson4D.XYCluster.nxParityScheduleArity_finAnchorNXLocatedCoarseRunsWithPhases {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 (List.map LocatedNXParityBlock.analyticBlock (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left ++ List.map LocatedNXParityBlock.analyticBlock (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right) = paperTailLength mu

theorem Anderson4D.XYCluster.map_paperFinAnchorAssignmentFromTail_outwardOrder {t : PlaneTree} {mu : t.Multiplicities} (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (b : HeppLabeledCopy mu) (tail : Fin (paperTailLength mu) → HeppLabeledCopy mu) : List.map (paperFinAnchorAssignmentFromTail leftPhase rightPhase anchor b tail) (paperFinAnchorOutwardOrderWithPhases leftPhase rightPhase anchor) = List.ofFn tail

theorem Anderson4D.XYCluster.locatedAnchoredScheduleAssignment_finAnchor_fromTail {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))) (b : HeppLabeledCopy mu) (tail : Fin (paperTailLength mu) → HeppLabeledCopy mu) : locatedAnchoredScheduleAssignment (paperFinAnchorAssignmentFromTail leftPhase rightPhase anchor b tail) (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right = tail ∘ Fin.cast ⋯

The assignment reconstructed by finite Fubini is consumed by the located left/right ledgers as exactly the supplied tail tuple.

theorem Anderson4D.XYCluster.nxAnchoredScheduleKernel_congr_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 left' right' : List (NXParityBlock Nm mu)) (hleft : left = left') (hright : right = right') (anchorPoint u : Fin 4 → ℤ) (n : ℕ) (hArity : nxParityScheduleArity (left ++ right) = n) (hArity' : nxParityScheduleArity (left' ++ right') = n) (f : Fin n → HeppLabeledCopy mu) : nxAnchoredScheduleKernel ht hroot Nm mu z hz R left right anchorPoint u (f ∘ Fin.cast hArity) = nxAnchoredScheduleKernel ht hroot Nm mu z hz R left' right' anchorPoint u (f ∘ Fin.cast hArity')

theorem Anderson4D.XYCluster.edgeKernelProduct_le_finAnchorNXAnchoredScheduleKernel_fromTail {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 : ℝ) (O : Finset (AdjacentIndex (totalMultiplicity mu))) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (cls : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (b : HeppLabeledCopy mu) (tail : Fin (paperTailLength mu) → HeppLabeledCopy mu) : ∏ edge : AdjacentIndex (totalMultiplicity mu), finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz R O leftPhase rightPhase anchor cls (paperFinAnchorAssignmentFromTail leftPhase rightPhase anchor b tail) edge ≤ nxAnchoredScheduleKernel ht hroot Nm mu z hz R (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right (labeledCopyPoint z b) (labeledCopyPoint z b) (tail ∘ Fin.cast ⋯)

Canonical pointwise bound for the fixed-fiber CPS theorem. Consecutiveness, anchor reconstruction, analytic erasure, and the two arity casts are all discharged internally.