Phase-independent common product

The common local target in the anchored elimination depends on the word, the anchor, and the omitted-edge set, but not on the pairing phase. This file expands the located ledger to the product over all non-anchor positions and records that independence as an exact equality.

def Anderson4D.XYCluster.outwardPositionSkipped {m : ℕ} (O : Finset (AdjacentIndex m)) (anchor i : Fin m) : Bool

Whether the original edge entering a non-anchor position in the outward traversal belongs to O. The anchor value is harmless because the anchor is erased from every product below.

Equations

• Anderson4D.XYCluster.outwardPositionSkipped O anchor i = Option.any (fun (edge : Anderson4D.AdjacentIndex m) => decide (edge ∈ O)) (Anderson4D.XYCluster.outwardPositionIncomingEdge anchor i)

@[simp]

theorem Anderson4D.XYCluster.outwardPositionSkipped_of_lt {m : ℕ} (O : Finset (AdjacentIndex m)) (anchor i : Fin m) (hi : ↑i < ↑anchor) : outwardPositionSkipped O anchor i = positionIncomingSkipped O PositionDirection.reverse i

@[simp]

theorem Anderson4D.XYCluster.outwardPositionSkipped_of_gt {m : ℕ} (O : Finset (AdjacentIndex m)) (anchor i : Fin m) (hi : ↑anchor < ↑i) : outwardPositionSkipped O anchor i = positionIncomingSkipped O PositionDirection.forward i

@[simp]

theorem Anderson4D.XYCluster.outwardPositionSkipped_target {m : ℕ} (O : Finset (AdjacentIndex m)) (anchor : Fin m) (edge : AdjacentIndex m) : outwardPositionSkipped O anchor (outwardEdgeTargetPosition anchor edge) = decide (edge ∈ O)

@[simp]

theorem Anderson4D.XYCluster.locatedBlockCommonTarget_locatePositionBlock {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (cls : Fin m → ActiveNXClass Nm mu) (incomingSkipped : Fin m → Bool) (b : PositionBlock (Fin m)) : locatedBlockCommonTarget Nm mu (locatePositionBlock Nm mu cls incomingSkipped b) = (List.map (fun (i : Fin m) => paperDyadicLocalTarget Nm mu (↑(cls i)) (incomingSkipped i)) b.entries).prod

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

Turning selected precise pairs into rough pairs does not change their common local factors.

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

Reindex a non-anchor position product by the unique original edge whose outward target is that position.

theorem Anderson4D.XYCluster.locatedLedgerCommonProduct_finAnchor_eq_outward {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)) : locatedLedgerCommonProduct Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = ∏ i ∈ Finset.univ.erase anchor, paperDyadicLocalTarget Nm mu (↑(cls i)) (outwardPositionSkipped O anchor i)

Exact phase-free normal form of the common located ledger: one local target for every non-anchor word position, with the actual outward incoming edge.

theorem Anderson4D.XYCluster.locatedLedgerCommonProduct_finAnchor_phase_independent {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase leftPhase' rightPhase' : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : locatedLedgerCommonProduct Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = locatedLedgerCommonProduct Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase' rightPhase' anchor cls O)

The common factor is exactly invariant under independent phase flips.

theorem Anderson4D.XYCluster.locatedLedgerCommonProduct_finAnchor_eq_edgeProduct {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)) : locatedLedgerCommonProduct Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = ∏ edge : AdjacentIndex m, paperDyadicLocalTarget Nm mu (↑(cls (outwardEdgeTargetPosition anchor edge))) (decide (edge ∈ O))

Equivalent edge-indexed normal form. This makes the skipped factors line up definitionally with the outward occurrence ledger.