Original-edge kernels in the anchored outward schedule

This module records the deterministic kernel bookkeeping needed before the arrangement finite-Fubini step. Original edges are assigned to the unique non-anchor endpoint farther from the anchor. Consequently the anchor is never enumerated twice and no edge is invented between the two outer endpoints.

def Anderson4D.XYCluster.outwardEdgeTargetPosition {m : ℕ} (anchor : Fin m) (edge : AdjacentIndex m) : Fin m

The endpoint of an original edge farther from the anchor.

Equations

• Anderson4D.XYCluster.outwardEdgeTargetPosition anchor edge = if ↑↑edge < ↑anchor then ↑edge else Anderson4D.adjacentSucc edge

theorem Anderson4D.XYCluster.outwardEdgeTargetPosition_ne_anchor {m : ℕ} (anchor : Fin m) (edge : AdjacentIndex m) : outwardEdgeTargetPosition anchor edge ≠ anchor

theorem Anderson4D.XYCluster.outwardEdgeTargetPosition_injective {m : ℕ} (anchor : Fin m) : Function.Injective (outwardEdgeTargetPosition anchor)

def Anderson4D.XYCluster.outwardPositionIncomingEdge {m : ℕ} (anchor i : Fin m) : Option (AdjacentIndex m)

The original edge entering a position while traversing outward. It is none exactly at the anchor.

Equations

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

@[simp]

theorem Anderson4D.XYCluster.outwardPositionIncomingEdge_anchor {m : ℕ} (anchor : Fin m) : outwardPositionIncomingEdge anchor anchor = none

theorem Anderson4D.XYCluster.outwardPositionIncomingEdge_target {m : ℕ} (anchor : Fin m) (edge : AdjacentIndex m) : outwardPositionIncomingEdge anchor (outwardEdgeTargetPosition anchor edge) = some edge

noncomputable def Anderson4D.XYCluster.outwardPositionKernel {m : ℕ} (K : AdjacentIndex m → ℝ) (anchor i : Fin m) : ℝ

Evaluate an original-edge kernel at the edge entering a position.

Equations

• Anderson4D.XYCluster.outwardPositionKernel K anchor i = (Anderson4D.XYCluster.outwardPositionIncomingEdge anchor i).elim 1 K

@[simp]

theorem Anderson4D.XYCluster.outwardPositionKernel_target {m : ℕ} (K : AdjacentIndex m → ℝ) (anchor : Fin m) (edge : AdjacentIndex m) : outwardPositionKernel K anchor (outwardEdgeTargetPosition anchor edge) = K edge

theorem Anderson4D.XYCluster.edgeKernelProduct_eq_nonanchorPositionProduct {m : ℕ} (K : AdjacentIndex m → ℝ) (anchor : Fin m) : ∏ edge : AdjacentIndex m, K edge = ∏ i ∈ Finset.univ.erase anchor, outwardPositionKernel K anchor i

Original edges are in bijection with non-anchor outward positions.

noncomputable def Anderson4D.XYCluster.locatedBlockOriginalKernelProduct {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (K : AdjacentIndex m → ℝ) (anchor : Fin m) (b : LocatedNXParityBlock Nm mu) : ℝ

Kernel factors assigned to one concrete located block.

Equations

• Anderson4D.XYCluster.locatedBlockOriginalKernelProduct Nm mu K anchor b = (List.map (Anderson4D.XYCluster.outwardPositionKernel K anchor) b.positionBlock.entries).prod

noncomputable def Anderson4D.XYCluster.locatedLedgerOriginalKernelProduct {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (K : AdjacentIndex m → ℝ) (anchor : Fin m) (bs : List (LocatedNXParityBlock Nm mu)) : ℝ

Product of the original-edge factors carried by a located ledger.

Equations

• Anderson4D.XYCluster.locatedLedgerOriginalKernelProduct Nm mu K anchor bs = (List.map (Anderson4D.XYCluster.locatedBlockOriginalKernelProduct Nm mu K anchor) bs).prod

theorem Anderson4D.XYCluster.edgeKernelProduct_eq_finAnchorNXLocatedCoarse {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)) (K : AdjacentIndex m → ℝ) : ∏ edge : AdjacentIndex m, K edge = locatedLedgerOriginalKernelProduct Nm mu K anchor (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O)

Exact original-edge decomposition through the concrete coarse schedule. Every edge occurs once, and the anchor contributes no factor.

The canonical strong-edge schedule

noncomputable def Anderson4D.XYCluster.positionPairAffectedEdges {m : ℕ} (bs : List (PositionBlock (Fin m))) : Finset (AdjacentIndex m)

Original edges incident to a scheduled pair block.

Equations

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

noncomputable def Anderson4D.XYCluster.finAnchorNXKernelStrongEdges {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) : Finset (AdjacentIndex m)

The strong-kernel edges needed by the outward elimination. Every original left edge is strong, because its traversal direction is reversed. On both sides, every edge incident to a pair is also strong; in particular this contains every precise-pair internal edge (and safely also rough-pair internal edges).

Equations

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

theorem Anderson4D.XYCluster.mem_finAnchorNXKernelStrongEdges_of_left {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) (edge : AdjacentIndex m) (hleft : ↑↑edge < ↑anchor) : edge ∈ finAnchorNXKernelStrongEdges leftPhase rightPhase anchor

theorem Anderson4D.XYCluster.finAnchorNXKernelStrongEdges_pair_internal {m : ℕ} (leftPhase rightPhase : Bool) (anchor i j : Fin m) (hpair : PositionBlock.pair i j ∈ finAnchorPositionScheduleWithPhases leftPhase rightPhase anchor) : ∃ edge ∈ finAnchorNXKernelStrongEdges leftPhase rightPhase anchor, ↑edge = i ∧ ↑i + 1 = ↑j ∨ ↑edge = j ∧ ↑j + 1 = ↑i

Every concrete scheduled pair has a strong internal original edge.

Metadata retained by rough marking

inductive Anderson4D.XYCluster.FinAnchorLocatedBlockMetadata {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)) : LocatedNXParityBlock Nm mu → Prop

Exact side, class, and skip metadata of a block in the anchored located schedule. Separate rough constructors make the effect of marking explicit without weakening any payload equality.

• leftSingle {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)} (i : Fin m) (hmem : PositionBlock.single i ∈ pairPositionRun leftPhase (leftAnchorPositions anchor)) : FinAnchorLocatedBlockMetadata Nm mu leftPhase rightPhase anchor cls O (LocatedNXParityBlock.single i (cls i) (positionIncomingSkipped O PositionDirection.reverse i))
• rightSingle {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)} (i : Fin m) (hmem : PositionBlock.single i ∈ pairPositionRun rightPhase (rightAnchorPositions anchor)) : FinAnchorLocatedBlockMetadata Nm mu leftPhase rightPhase anchor cls O (LocatedNXParityBlock.single i (cls i) (positionIncomingSkipped O PositionDirection.forward i))
• leftPair {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)} (i j : Fin m) (hmem : PositionBlock.pair i j ∈ pairPositionRun leftPhase (leftAnchorPositions anchor)) : FinAnchorLocatedBlockMetadata Nm mu leftPhase rightPhase anchor cls O (LocatedNXParityBlock.pair i j (Anderson4D.XYCluster.scheduledPairPayload✝ Nm mu cls (positionIncomingSkipped O PositionDirection.reverse) i j))
• rightPair {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)} (i j : Fin m) (hmem : PositionBlock.pair i j ∈ pairPositionRun rightPhase (rightAnchorPositions anchor)) : FinAnchorLocatedBlockMetadata Nm mu leftPhase rightPhase anchor cls O (LocatedNXParityBlock.pair i j (Anderson4D.XYCluster.scheduledPairPayload✝ Nm mu cls (positionIncomingSkipped O PositionDirection.forward) i j))
• leftRoughPair {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)} (i j : Fin m) (hmem : PositionBlock.pair i j ∈ pairPositionRun leftPhase (leftAnchorPositions anchor)) : FinAnchorLocatedBlockMetadata Nm mu leftPhase rightPhase anchor cls O (LocatedNXParityBlock.roughPair i j (Anderson4D.XYCluster.scheduledPairPayload✝ Nm mu cls (positionIncomingSkipped O PositionDirection.reverse) i j))
• rightRoughPair {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)} (i j : Fin m) (hmem : PositionBlock.pair i j ∈ pairPositionRun rightPhase (rightAnchorPositions anchor)) : FinAnchorLocatedBlockMetadata Nm mu leftPhase rightPhase anchor cls O (LocatedNXParityBlock.roughPair i j (Anderson4D.XYCluster.scheduledPairPayload✝ Nm mu cls (positionIncomingSkipped O PositionDirection.forward) i j))

theorem Anderson4D.XYCluster.finAnchorNXLocatedCoarse_block_metadata {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)) (b : LocatedNXParityBlock Nm mu) (hb : b ∈ finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) : FinAnchorLocatedBlockMetadata Nm mu leftPhase rightPhase anchor cls O b

Every coarse located block retains its exact raw side and payload.

Pointwise local factors in CPS order

def Anderson4D.XYCluster.outwardPreviousPosition {m : ℕ} (anchor i : Fin m) : Fin m

The position immediately closer to the anchor in the outward run.

Equations

• Anderson4D.XYCluster.outwardPreviousPosition anchor i = if hleft : ↑i < ↑anchor then ⟨↑i + 1, ⋯⟩ else if hright : ↑anchor < ↑i then ⟨↑i - 1, ⋯⟩ else anchor

noncomputable def Anderson4D.XYCluster.locatedBlockEliminationKernel {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) : LocatedNXParityBlock Nm mu → ℝ

The local lambda/strongLambda monomial consumed by one CPS block at a fixed arrangement.

Equations

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

noncomputable def Anderson4D.XYCluster.locatedLedgerEliminationKernelProduct {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) (bs : List (LocatedNXParityBlock Nm mu)) : ℝ

Equations

• Anderson4D.XYCluster.locatedLedgerEliminationKernelProduct ht hroot Nm mu z hz R anchor σ bs = (List.map (Anderson4D.XYCluster.locatedBlockEliminationKernel ht hroot Nm mu z hz R anchor σ) bs).prod

noncomputable def Anderson4D.XYCluster.finAnchorNXArrangementEdgeKernel {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) (edge : AdjacentIndex m) : ℝ

The fixed-arrangement original-edge kernel with the canonical schedule of strong cutoffs.

Equations

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

theorem Anderson4D.XYCluster.locatedBlockOriginalKernelProduct_le_eliminationKernel {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) (b : LocatedNXParityBlock Nm mu) (hb : b ∈ finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) : locatedBlockOriginalKernelProduct Nm mu (finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz R O leftPhase rightPhase anchor cls σ) anchor b ≤ locatedBlockEliminationKernel ht hroot Nm mu z hz R anchor σ b

For each concrete block in the marked anchored ledger, the original-edge factors assigned to its positions are bounded by the lambda/strongLambda monomial in the outward CPS order.

theorem Anderson4D.XYCluster.edgeKernelProduct_le_finAnchorNXLocatedEliminationProduct {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) : ∏ edge : AdjacentIndex m, finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz R O leftPhase rightPhase anchor cls σ edge ≤ locatedLedgerEliminationKernelProduct ht hroot Nm mu z hz R anchor σ (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O)

The complete original-edge product of a fixed arrangement is bounded by the product of the outward local elimination monomials. The proof uses the exact edge-to-position bijection, so there is no anchor factor and no edge joining the two outward runs.

Split back into the two outward CPS runs

structure Anderson4D.XYCluster.AnchoredLocatedNXParityRuns {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Type

The position-retaining counterpart of AnchoredNXParityRuns. Its ledger is bookkeeping only; the two lists remain distinct analytic runs.

• left : List (LocatedNXParityBlock Nm mu)
• right : List (LocatedNXParityBlock Nm mu)

def Anderson4D.XYCluster.AnchoredLocatedNXParityRuns.ledger {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (runs : AnchoredLocatedNXParityRuns Nm mu) : List (LocatedNXParityBlock Nm mu)

Equations

• runs.ledger = runs.left ++ runs.right

def Anderson4D.XYCluster.finAnchorNXLocatedCoarseRunsWithPhases {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)) : AnchoredLocatedNXParityRuns Nm mu

Split the concrete marked ledger at exactly the same raw-left length as finAnchorNXCoarseRunsWithPhases.

Equations

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

theorem Anderson4D.XYCluster.finAnchorNXLocatedCoarseRunsWithPhases_ledger {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)) : (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).ledger = finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O

theorem Anderson4D.XYCluster.map_analyticBlock_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.analyticBlock (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left = (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left

After erasing positions, the concrete left split is definitionally the left run consumed by conditionedNXAnchoredRunsSum.

theorem Anderson4D.XYCluster.map_analyticBlock_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.analyticBlock (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right = (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right

After erasing positions, the concrete right split is definitionally the right run consumed by conditionedNXAnchoredRunsSum.

theorem Anderson4D.XYCluster.edgeKernelProduct_le_finAnchorNXLocatedOutwardRunsProduct {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) : ∏ edge : AdjacentIndex m, finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz R O leftPhase rightPhase anchor cls σ edge ≤ locatedLedgerEliminationKernelProduct ht hroot Nm mu z hz R anchor σ (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left * locatedLedgerEliminationKernelProduct ht hroot Nm mu z hz R anchor σ (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right

Fixed-arrangement kernel schedule in the exact two-run order: the left monomial is completed first, then the right monomial restarts at the anchor. The right-hand side contains no cross-run factor.

theorem Anderson4D.XYCluster.finAnchorNXKernelSchedule_CPS_interface {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) : ∏ edge : AdjacentIndex m, finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz R O leftPhase rightPhase anchor cls σ edge ≤ locatedLedgerEliminationKernelProduct ht hroot Nm mu z hz R anchor σ (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left * locatedLedgerEliminationKernelProduct ht hroot Nm mu z hz R anchor σ (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right ∧ List.map LocatedNXParityBlock.analyticBlock (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left = (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left ∧ List.map LocatedNXParityBlock.analyticBlock (finAnchorNXLocatedCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right = (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right

Assembly-facing certificate: the fixed-arrangement kernel bound and the two exact erasures to the analytic runs expected by conditionedNXAnchoredRunsSum.