Shared-state elimination for the two anchored runs

The local one-parity eliminator in SingleScaleInnerAssembly returns a number and therefore forgets the final set of labeled copies. At an interior anchor, however, the right outward run must see every copy already used by the left outward run. This file supplies the continuation-passing variant needed for that finite-Fubini step.

The terminal continuation receives both the final used set and the final lattice point. In conditionedNXAnchoredRunsSum the continuation keeps the former and deliberately discards the latter: the right run restarts at the anchor point, so no artificial edge between the two outer endpoints is introduced.

noncomputable def Anderson4D.XYCluster.conditionedNXParityChainSumThen {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 : ℝ) : List (NXParityBlock Nm mu) → Finset (HeppLabeledCopy mu) → (Fin 4 → ℤ) → (Finset (HeppLabeledCopy mu) → (Fin 4 → ℤ) → ℝ) → ℝ

Continuation-passing version of conditionedNXParityChainSum.

At the empty schedule it exposes the final used-copy set and final point to tail; all nonempty cases are exactly the existing conditioned eliminator.

Equations

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

theorem Anderson4D.XYCluster.conditionedNXParityChainSumThen_mono {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 → ℤ) (tail₁ tail₂ : Finset (HeppLabeledCopy mu) → (Fin 4 → ℤ) → ℝ) (htail : ∀ (used' : Finset (HeppLabeledCopy mu)) (u' : Fin 4 → ℤ), tail₁ used' u' ≤ tail₂ used' u') : conditionedNXParityChainSumThen ht hroot Nm mu z hz R ps used u tail₁ ≤ conditionedNXParityChainSumThen ht hroot Nm mu z hz R ps used u tail₂

The CPS eliminator is monotone in its terminal continuation.

theorem Anderson4D.XYCluster.conditionedNXParityChainSumThen_const {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 K : ℝ) (ps : List (NXParityBlock Nm mu)) (used : Finset (HeppLabeledCopy mu)) (u : Fin 4 → ℤ) : (conditionedNXParityChainSumThen ht hroot Nm mu z hz R ps used u fun (_used : Finset (HeppLabeledCopy mu)) (_u : Fin 4 → ℤ) => K) = conditionedNXParityChainSum ht hroot Nm mu z hz R ps used u * K

A constant terminal continuation factors out of the CPS eliminator. This also records that the existing eliminator is the unit-terminal special case.

theorem Anderson4D.XYCluster.conditionedNXParityChainSumThen_one {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 → ℤ) : (conditionedNXParityChainSumThen ht hroot Nm mu z hz R ps used u fun (_used : Finset (HeppLabeledCopy mu)) (_u : Fin 4 → ℤ) => 1) = conditionedNXParityChainSum ht hroot Nm mu z hz R ps used u

Unit continuation recovers conditionedNXParityChainSum exactly.

theorem Anderson4D.XYCluster.conditionedNXParityChainSumThen_nonneg {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 → ℤ) (tail : Finset (HeppLabeledCopy mu) → (Fin 4 → ℤ) → ℝ) (htail : ∀ (used' : Finset (HeppLabeledCopy mu)) (u' : Fin 4 → ℤ), 0 ≤ tail used' u') : 0 ≤ conditionedNXParityChainSumThen ht hroot Nm mu z hz R ps used u tail

A nonnegative terminal continuation gives a nonnegative CPS sum.

theorem Anderson4D.XYCluster.conditionedNXParityChainSumThen_le_scaledTargetProduct : ∃ (C : ℝ), 256 ≤ C ∧ ∀ {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 : ℕ), accumulatedScale Nm mu t.rootV ≤ R → ∀ (ps : List (NXParityBlock Nm mu)) (used : Finset (HeppLabeledCopy mu)) (u : Fin 4 → ℤ) (tail : Finset (HeppLabeledCopy mu) → (Fin 4 → ℤ) → ℝ) (K : ℝ), 0 ≤ K → (∀ (used' : Finset (HeppLabeledCopy mu)) (u' : Fin 4 → ℤ), tail used' u' ≤ K) → conditionedNXParityChainSumThen ht hroot Nm mu z hz (↑R) ps used u tail ≤ K * (List.map (fun (p : NXParityBlock Nm mu) => C * nxParityBlockTarget Nm mu (↑R) p) ps).prod

Uniform target-product estimate with an arbitrary bounded terminal continuation. The constant is exactly the one from conditionedNXParityChainSum_le_targetProduct.

theorem Anderson4D.XYCluster.conditionedNXParityChainSumThen_le_pow_mul_targetProduct : ∃ (C : ℝ), 256 ≤ C ∧ ∀ {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 : ℕ), accumulatedScale Nm mu t.rootV ≤ R → ∀ (ps : List (NXParityBlock Nm mu)) (used : Finset (HeppLabeledCopy mu)) (u : Fin 4 → ℤ) (tail : Finset (HeppLabeledCopy mu) → (Fin 4 → ℤ) → ℝ) (K : ℝ), 0 ≤ K → (∀ (used' : Finset (HeppLabeledCopy mu)) (u' : Fin 4 → ℤ), tail used' u' ≤ K) → conditionedNXParityChainSumThen ht hroot Nm mu z hz (↑R) ps used u tail ≤ K * C ^ ps.length * (List.map (fun (p : NXParityBlock Nm mu) => nxParityBlockTarget Nm mu (↑R) p) ps).prod

The same continuation estimate with the constant power made explicit.

Two outward runs with one genuinely shared used-copy state

noncomputable def Anderson4D.XYCluster.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 : ℝ) (left right : List (NXParityBlock Nm mu)) (used : Finset (HeppLabeledCopy mu)) (anchorPoint : Fin 4 → ℤ) : ℝ

Run the left schedule first and pass its final used-copy set to the right schedule. The right schedule restarts at anchorPoint; the terminal point of the left schedule is intentionally ignored.

Equations

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

theorem Anderson4D.XYCluster.conditionedNXAnchoredRunsSum_nonneg {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 : Fin 4 → ℤ) : 0 ≤ conditionedNXAnchoredRunsSum ht hroot Nm mu z hz R left right used anchorPoint

Both outward runs remain nonnegative when they share the used set.

theorem Anderson4D.XYCluster.conditionedNXAnchoredRunsSum_le_scaledTargetProducts : ∃ (C : ℝ), 256 ≤ C ∧ ∀ {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 : ℕ), accumulatedScale Nm mu t.rootV ≤ R → ∀ (left right : List (NXParityBlock Nm mu)) (used : Finset (HeppLabeledCopy mu)) (anchorPoint : Fin 4 → ℤ), conditionedNXAnchoredRunsSum ht hroot Nm mu z hz (↑R) left right used anchorPoint ≤ (List.map (fun (p : NXParityBlock Nm mu) => C * nxParityBlockTarget Nm mu (↑R) p) left).prod * (List.map (fun (p : NXParityBlock Nm mu) => C * nxParityBlockTarget Nm mu (↑R) p) right).prod

The shared-state two-run sum is bounded by the product of the two local target products. The same universal constant is used on both sides.

theorem Anderson4D.XYCluster.conditionedNXAnchoredRunsSum_le_pow_mul_targetProducts : ∃ (C : ℝ), 256 ≤ C ∧ ∀ {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 : ℕ), accumulatedScale Nm mu t.rootV ≤ R → ∀ (left right : List (NXParityBlock Nm mu)) (used : Finset (HeppLabeledCopy mu)) (anchorPoint : Fin 4 → ℤ), conditionedNXAnchoredRunsSum ht hroot Nm mu z hz (↑R) left right used anchorPoint ≤ C ^ (left.length + right.length) * (List.map (fun (p : NXParityBlock Nm mu) => nxParityBlockTarget Nm mu (↑R) p) left).prod * (List.map (fun (p : NXParityBlock Nm mu) => nxParityBlockTarget Nm mu (↑R) p) right).prod

Paper-facing normalization of the two-run bound: one factor C per elimination block, followed by the unscaled left and right target products.