Assembly glue for anchored bidirectional sequence gains

This file supplies the two interfaces needed by the final finite-Fubini assembly:

• a product-level identification between the gain on the original edge order (reverse to the left of the anchor and forward to its right) and the two padded outward products;
• the active-P sequence estimate when the exceptional set is allowed to depend on the anchor.

No comparison between forward and reverse gains is used. The left product is reindexed by reflection, the right product by translation, and every extra padded factor is proved to be exactly one.

The original-edge oriented product

noncomputable def Anderson4D.anchoredOrientedCodeEdgeGain (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (a : Fin (n + 1)) (w : Fin (n + 1) → Fin ν) (j : Fin n) : ℝ

The gain attached to an edge in the original word order. Edges strictly left of the anchor are traversed outwards and hence use the reverse ratio; edges at or to the right of the anchor use the ordinary forward ratio.

Equations

• Anderson4D.anchoredOrientedCodeEdgeGain θ e a w j = if ↑j < ↑a then min 1 ((2 ^ e (w j.castSucc) / 2 ^ e (w j.succ)) ^ θ) else Anderson4D.anchoredCodeEdgeGain θ e w j

theorem Anderson4D.anchoredOrientedCodeEdgeGain_of_lt (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (a : Fin (n + 1)) (w : Fin (n + 1) → Fin ν) (j : Fin n) (hj : ↑j < ↑a) : anchoredOrientedCodeEdgeGain θ e a w j = min 1 ((2 ^ e (w j.castSucc) / 2 ^ e (w j.succ)) ^ θ)

theorem Anderson4D.anchoredOrientedCodeEdgeGain_of_le (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (a : Fin (n + 1)) (w : Fin (n + 1) → Fin ν) (j : Fin n) (hj : ↑a ≤ ↑j) : anchoredOrientedCodeEdgeGain θ e a w j = anchoredCodeEdgeGain θ e w j

noncomputable def Anderson4D.anchoredOrientedCodeWeight (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (E : Finset (Fin n)) (a : Fin (n + 1)) (w : Fin (n + 1) → Fin ν) : ℝ

The original-edge form consumed by finite-Fubini: use one exception set on the original adjacency indices and orient every retained edge away from the anchor.

Equations

• Anderson4D.anchoredOrientedCodeWeight θ e E a w = ∏ j ∈ Finset.univ \ E, Anderson4D.anchoredOrientedCodeEdgeGain θ e a w j

theorem Anderson4D.anchoredOrientedCodeWeight_eq_bidirectional (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (E : Finset (Fin n)) (a : Fin (n + 1)) (w : Fin (n + 1) → Fin ν) : anchoredOrientedCodeWeight θ e E a w = anchoredBidirectionalCodeWeight θ e E a w

Exact assembly rewrite: the single product on retained original edges, oriented away from the anchor, is the product of the two padded outward weights. This is an equality, not an inequality or a comparison of oppositely oriented gains.

The original-edge oriented product on the active carrier

noncomputable def Anderson4D.anchoredOrientedActivePEdgeGain (θ : ℝ) {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {n : ℕ} (a : Fin (n + 1)) (w : Fin (n + 1) → ActivePClass Nm mu) (j : Fin n) : ℝ

Active-P version of the original-edge gain oriented away from the anchor.

Equations

• Anderson4D.anchoredOrientedActivePEdgeGain θ a w j = if ↑j < ↑a then min 1 ((↑↑(w j.castSucc) / ↑↑(w j.succ)) ^ θ) else Anderson4D.anchoredActivePEdgeGain θ w j

noncomputable def Anderson4D.anchoredOrientedActivePWeight (θ : ℝ) {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {n : ℕ} (E : Finset (Fin n)) (a : Fin (n + 1)) (w : Fin (n + 1) → ActivePClass Nm mu) : ℝ

Active-P product in the original edge order, with one original exception set and the two directions oriented away from the anchor.

Equations

• Anderson4D.anchoredOrientedActivePWeight θ E a w = ∏ j ∈ Finset.univ \ E, Anderson4D.anchoredOrientedActivePEdgeGain θ a w j

theorem Anderson4D.anchoredOrientedActivePEdgeGain_enumeration (θ : ℝ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {n : ℕ} (a : Fin (n + 1)) (x : Fin (n + 1) → Fin (activePCount Nm mu)) (j : Fin n) : anchoredOrientedActivePEdgeGain θ a (fun (i : Fin (n + 1)) => (activePEnumeration Nm mu) (x i)) j = anchoredOrientedCodeEdgeGain θ (activePExponent Nm mu) a x j

theorem Anderson4D.anchoredOrientedActivePWeight_enumeration (θ : ℝ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {n : ℕ} (E : Finset (Fin n)) (a : Fin (n + 1)) (x : Fin (n + 1) → Fin (activePCount Nm mu)) : (anchoredOrientedActivePWeight θ E a fun (i : Fin (n + 1)) => (activePEnumeration Nm mu) (x i)) = anchoredOrientedCodeWeight θ (activePExponent Nm mu) E a x

theorem Anderson4D.anchoredOrientedActivePWeight_eq_bidirectional (θ : ℝ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {n : ℕ} (E : Finset (Fin n)) (a : Fin (n + 1)) (w : Fin (n + 1) → ActivePClass Nm mu) : anchoredOrientedActivePWeight θ E a w = anchoredBidirectionalActivePWeight θ E a w

Active-carrier form of the exact assembly rewrite. This is the bridge from the original finite-Fubini product directly to the padded bidirectional sequence weight.

Anchor-dependent exception sets on the active carrier

theorem Anderson4D.anchoredBidirectional_activeP_sum_le_varyingExceptions (θ : ℝ) (hθ : 0 < θ) (B : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (n : ℕ), activePCount Nm mu ≤ n + 1 → ∀ (E : Fin (n + 1) → Finset (Fin n)), (∀ (a : Fin (n + 1)), (E a).card ≤ B) → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight θ (E a) a w ≤ C ^ (n + 1)

The active-P anchored estimate with an exception set chosen separately at each anchor. The same fixed budget applies uniformly to every choice.

theorem Anderson4D.anchoredBidirectional_totalMultiplicity_varyingExceptions (θ : ℝ) (hθ : 0 < θ) (B : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities), let n := totalMultiplicity mu - 1; ∀ (E : Fin (n + 1) → Finset (Fin n)), (∀ (a : Fin (n + 1)), (E a).card ≤ B) → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight θ (E a) a w ≤ C ^ totalMultiplicity mu

Paper-length form of the anchor-dependent active-P estimate. With m = totalMultiplicity mu, the word has m positions and m-1 edges.

theorem Anderson4D.anchoredOriented_activeP_sum_le_varyingExceptions (θ : ℝ) (hθ : 0 < θ) (B : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (n : ℕ), activePCount Nm mu ≤ n + 1 → ∀ (E : Fin (n + 1) → Finset (Fin n)), (∀ (a : Fin (n + 1)), (E a).card ≤ B) → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredOrientedActivePWeight θ (E a) a w ≤ C ^ (n + 1)

Final assembly-facing form: sum the original-edge active-P weights when the exception set varies with the anchor. The proof rewrites each summand by the exact orientation theorem above and then invokes the bidirectional bound; no exponent comparison is involved.

theorem Anderson4D.anchoredOriented_totalMultiplicity_varyingExceptions (θ : ℝ) (hθ : 0 < θ) (B : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities), let n := totalMultiplicity mu - 1; ∀ (E : Fin (n + 1) → Finset (Fin n)), (∀ (a : Fin (n + 1)), (E a).card ≤ B) → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredOrientedActivePWeight θ (E a) a w ≤ C ^ totalMultiplicity mu

Literal paper-length version of the original-edge, anchor-varying active-P estimate.

theorem Anderson4D.anchoredBidirectional_activeP_varyingExceptions_oneSixteenth_twenty : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (n : ℕ), activePCount Nm mu ≤ n + 1 → ∀ (E : Fin (n + 1) → Finset (Fin n)), (∀ (a : Fin (n + 1)), (E a).card ≤ 20) → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight (1 / 16) (E a) a w ≤ C ^ (n + 1)

Convenience specialization at exponent 1/16 when each anchor has at most twenty skipped edges. The final even/odd union uses the forty-exception interface below.

theorem Anderson4D.anchoredBidirectional_totalMultiplicity_varyingExceptions_oneSixteenth_twenty : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities), let n := totalMultiplicity mu - 1; ∀ (E : Fin (n + 1) → Finset (Fin n)), (∀ (a : Fin (n + 1)), (E a).card ≤ 20) → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight (1 / 16) (E a) a w ≤ C ^ totalMultiplicity mu

Literal m = totalMultiplicity mu form of the twenty-exception convenience specialization.

theorem Anderson4D.anchoredBidirectional_activeP_varyingExceptions_oneSixteenth_forty : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (n : ℕ), activePCount Nm mu ≤ n + 1 → ∀ (E : Fin (n + 1) → Finset (Fin n)), (∀ (a : Fin (n + 1)), (E a).card ≤ 40) → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight (1 / 16) (E a) a w ≤ C ^ (n + 1)

Paper-facing varying-exception interface after the Step 4 even/odd geometric-mean assembly: each parity contributes at most twenty skipped edges, so their union has budget forty at exponent 1/16.

theorem Anderson4D.anchoredBidirectional_totalMultiplicity_varyingExceptions_oneSixteenth_forty : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities), let n := totalMultiplicity mu - 1; ∀ (E : Fin (n + 1) → Finset (Fin n)), (∀ (a : Fin (n + 1)), (E a).card ≤ 40) → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight (1 / 16) (E a) a w ≤ C ^ totalMultiplicity mu

Literal m = totalMultiplicity mu specialization of the paper-facing 1/16, forty-exception interface.

theorem Anderson4D.anchoredOriented_totalMultiplicity_varyingExceptions_oneSixteenth_forty : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities), let n := totalMultiplicity mu - 1; ∀ (E : Fin (n + 1) → Finset (Fin n)), (∀ (a : Fin (n + 1)), (E a).card ≤ 40) → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredOrientedActivePWeight (1 / 16) (E a) a w ≤ C ^ totalMultiplicity mu

Final paper-facing original-edge interface: exponent 1/16, the forty-edge even/odd exception budget, and literal m = totalMultiplicity mu length.

Class-independent positional exception schedule

inductive Anderson4D.XYCluster.PositionControlBlock (m : ℕ) : Type

The control data of a located parity block, with every analytic class payload erased. This is the information that can influence rough marking and the exceptional original-edge set.

• single {m : ℕ} (position : Fin m) (skipped : Bool) : PositionControlBlock m
• pair {m : ℕ} (leftPosition rightPosition : Fin m) (skipLeft skipRight : Bool) : PositionControlBlock m
• roughPair {m : ℕ} (leftPosition rightPosition : Fin m) (skipLeft skipRight : Bool) : PositionControlBlock m

def Anderson4D.XYCluster.instDecidableEqPositionControlBlock.decEq {m✝ : ℕ} (x✝ x✝¹ : PositionControlBlock m✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Anderson4D.XYCluster.instDecidableEqPositionControlBlock {m✝ : ℕ} : DecidableEq (PositionControlBlock m✝)

Equations

• Anderson4D.XYCluster.instDecidableEqPositionControlBlock = Anderson4D.XYCluster.instDecidableEqPositionControlBlock.decEq

def Anderson4D.XYCluster.positionBlockToControl {m : ℕ} (incomingSkipped : Fin m → Bool) : PositionBlock (Fin m) → PositionControlBlock m

Attach only the incoming-edge flags to a positional block.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.positionBlockToControl incomingSkipped (Anderson4D.XYCluster.PositionBlock.single i) = Anderson4D.XYCluster.PositionControlBlock.single i (incomingSkipped i)

def Anderson4D.XYCluster.LocatedNXParityBlock.positionControl {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} : LocatedNXParityBlock Nm mu → PositionControlBlock m

Erase the analytic payload of a located block.

Equations

• (Anderson4D.XYCluster.LocatedNXParityBlock.single i a skipped).positionControl = Anderson4D.XYCluster.PositionControlBlock.single i skipped
• (Anderson4D.XYCluster.LocatedNXParityBlock.pair i j p).positionControl = Anderson4D.XYCluster.PositionControlBlock.pair i j p.skipLeft p.skipRight
• (Anderson4D.XYCluster.LocatedNXParityBlock.roughPair i j p).positionControl = Anderson4D.XYCluster.PositionControlBlock.roughPair i j p.skipLeft p.skipRight

@[simp]

theorem Anderson4D.XYCluster.positionControl_locatePositionBlock {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (cls : Fin m → ActiveNXClass Nm mu) (incomingSkipped : Fin m → Bool) (b : PositionBlock (Fin m)) : (locatePositionBlock Nm mu cls incomingSkipped b).positionControl = positionBlockToControl incomingSkipped b

def Anderson4D.XYCluster.markFirstSkippedPositionPairsRough {m : ℕ} : ℕ → List (PositionControlBlock m) → List (PositionControlBlock m)

Purely positional version of “choose the first three eligible pairs”.

Equations

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

@[simp]

theorem Anderson4D.XYCluster.map_positionControl_markFirstSkippedLocatedPairsRough {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (fuel : ℕ) (bs : List (LocatedNXParityBlock Nm mu)) : List.map LocatedNXParityBlock.positionControl (markFirstSkippedLocatedPairsRough fuel bs) = markFirstSkippedPositionPairsRough fuel (List.map LocatedNXParityBlock.positionControl bs)

Erasing analytic payload commutes with rough marking.

def Anderson4D.XYCluster.positionControlExceptionalEdges {m : ℕ} : List (PositionControlBlock m) → Finset (AdjacentIndex m)

Exceptional original edges computed only from positional control data.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.positionControlExceptionalEdges [] = ∅

theorem Anderson4D.XYCluster.positionControlExceptionalEdges_map_positionControl {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (bs : List (LocatedNXParityBlock Nm mu)) : positionControlExceptionalEdges (List.map LocatedNXParityBlock.positionControl bs) = locatedExceptionalEdges bs

Erasing analytic payload does not alter the exceptional-edge union.

def Anderson4D.XYCluster.finAnchorPositionControlLedgerWithPhases {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) (O : Finset (AdjacentIndex m)) : List (PositionControlBlock m)

The raw anchored schedule with no analytic class payload.

Equations

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

theorem Anderson4D.XYCluster.map_positionControl_finAnchorNXLocatedParityLedgerWithPhases {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.positionControl (finAnchorNXLocatedParityLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = finAnchorPositionControlLedgerWithPhases leftPhase rightPhase anchor O

def Anderson4D.XYCluster.finAnchorPositionControlCoarseLedgerWithPhases {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) (O : Finset (AdjacentIndex m)) : List (PositionControlBlock m)

Pure positional coarse ledger after selecting at most three rough pairs.

Equations

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

theorem Anderson4D.XYCluster.map_positionControl_finAnchorNXLocatedCoarseLedgerWithPhases {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.positionControl (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = finAnchorPositionControlCoarseLedgerWithPhases leftPhase rightPhase anchor O

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

The concrete original-edge exception set with all analytically irrelevant class data removed.

Equations

• Anderson4D.XYCluster.finAnchorPositionalExceptionalEdgesWithPhases leftPhase rightPhase anchor O = Anderson4D.XYCluster.finAnchorPureExceptionalEdgesWithPhases leftPhase rightPhase anchor O

theorem Anderson4D.XYCluster.finAnchorNXExceptionalEdgesWithPhases_eq_positional {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)) : finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O = finAnchorPositionalExceptionalEdgesWithPhases leftPhase rightPhase anchor O

The scheduled exception set is definitionally controlled only by positions, phases, and O; its apparent cls argument carries no information.

theorem Anderson4D.XYCluster.finAnchorNXExceptionalEdgesWithPhases_independent_cls {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin m) (cls₁ cls₂ : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor cls₁ O = finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor cls₂ O

Explicit class-independence theorem for downstream finite-Fubini reindexing.

def Anderson4D.XYCluster.finAnchorPositionalExceptionalFinEdgesWithPhases {n : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (O : Finset (AdjacentIndex (n + 1))) : Finset (Fin n)

Positional exception set in the Fin n indexing used by the sequence theorems.

Equations

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

theorem Anderson4D.XYCluster.finAnchorNXExceptionalFinEdgesWithPhases_eq_positional {t : PlaneTree} {n : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (cls : Fin (n + 1) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (n + 1))) : finAnchorNXExceptionalFinEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O = finAnchorPositionalExceptionalFinEdgesWithPhases leftPhase rightPhase anchor O

theorem Anderson4D.XYCluster.finAnchorNXExceptionalFinEdgesWithPhases_independent_cls {t : PlaneTree} {n : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (cls₁ cls₂ : Fin (n + 1) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (n + 1))) : finAnchorNXExceptionalFinEdgesWithPhases Nm mu leftPhase rightPhase anchor cls₁ O = finAnchorNXExceptionalFinEdgesWithPhases Nm mu leftPhase rightPhase anchor cls₂ O

theorem Anderson4D.XYCluster.finAnchorNXInterpolatedExceptionalFinEdges_independent_cls {t : PlaneTree} {n : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (cls₁ cls₂ : Fin (n + 1) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (n + 1))) : finAnchorNXInterpolatedExceptionalFinEdges Nm mu leftPhase rightPhase anchor cls₁ O = finAnchorNXInterpolatedExceptionalFinEdges Nm mu leftPhase rightPhase anchor cls₂ O

The even/odd union is likewise independent of the analytic class word.

def Anderson4D.XYCluster.finAnchorPositionalInterpolatedExceptionalFinEdges {n : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (O : Finset (AdjacentIndex (n + 1))) : Finset (Fin n)

Pure positional even/odd exception union in sequence indexing.

Equations

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

theorem Anderson4D.XYCluster.finAnchorNXInterpolatedExceptionalFinEdges_eq_positional {t : PlaneTree} {n : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (cls : Fin (n + 1) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (n + 1))) : finAnchorNXInterpolatedExceptionalFinEdges Nm mu leftPhase rightPhase anchor cls O = finAnchorPositionalInterpolatedExceptionalFinEdges leftPhase rightPhase anchor O

theorem Anderson4D.XYCluster.card_finAnchorPositionalInterpolatedExceptionalFinEdges_le_forty {t : PlaneTree} {n : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (_cls : Fin (n + 1) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (n + 1))) : (finAnchorPositionalInterpolatedExceptionalFinEdges leftPhase rightPhase anchor O).card ≤ 40

theorem Anderson4D.XYCluster.finAnchorPositional_orientedActiveP_totalMultiplicity_oneSixteenth_le : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities), let n := totalMultiplicity mu - 1; ∀ (leftPhase rightPhase : Fin (n + 1) → Bool) (_cls : Fin (n + 1) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (n + 1))), ∑ anchor : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredOrientedActivePWeight (1 / 16) (finAnchorPositionalInterpolatedExceptionalFinEdges (leftPhase anchor) (rightPhase anchor) anchor O) anchor w ≤ C ^ totalMultiplicity mu

Concrete final counting interface with the class-independent positional even/odd exception set, original-edge orientation, exponent 1/16, and literal paper length.