Precise gain glue #
The target ledger records precise-pair gains in traversal order. On the left of the anchor this is the reverse of the original word order; on the right it is the original forward order. This module identifies every retained original edge with a concrete precise ledger block and compares the two products without ever comparing a forward ratio pointwise with its reverse.
@[implicit_reducible]
noncomputable def
Anderson4D.XYCluster.locatedNXParityBlockDecidableEq
{t : PlaneTree}
{m : ℕ}
{Nm : t.HeppMarking}
{mu : t.Multiplicities}
:
DecidableEq (LocatedNXParityBlock Nm mu)
Equations
Instances For
The upper endpoint of an original adjacency edge.
Equations
- Anderson4D.XYCluster.adjacentRightPosition edge = ⟨↑↑edge + 1, ⋯⟩
Instances For
noncomputable def
Anderson4D.XYCluster.finAnchorOrientedDyadicEdgeGain
{t : PlaneTree}
{m : ℕ}
(Nm : t.HeppMarking)
(mu : t.Multiplicities)
(anchor : Fin m)
(cls : Fin m → ActiveNXClass Nm mu)
(edge : AdjacentIndex m)
:
The dyadic ratio on an original edge, oriented outward from the anchor. Strictly left edges use the reversed original ratio; right edges use the ordinary forward ratio.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.XYCluster.finAnchorOrientedDyadicEdgeGain_left_eq_reverseOriginal
{t : PlaneTree}
{m : ℕ}
(Nm : t.HeppMarking)
(mu : t.Multiplicities)
(anchor : Fin m)
(cls : Fin m → ActiveNXClass Nm mu)
(edge : AdjacentIndex m)
(hleft : ↑↑edge < ↑anchor)
:
finAnchorOrientedDyadicEdgeGain Nm mu anchor cls edge = dyadicForwardGain (singleScaleSigma2 Nm mu ↑(cls (adjacentRightPosition edge))) (singleScaleSigma2 Nm mu ↑(cls ↑edge))
On the left, the outward gain is the original-edge ratio with its endpoint order reversed.
theorem
Anderson4D.XYCluster.finAnchorOrientedDyadicEdgeGain_right_eq_forwardOriginal
{t : PlaneTree}
{m : ℕ}
(Nm : t.HeppMarking)
(mu : t.Multiplicities)
(anchor : Fin m)
(cls : Fin m → ActiveNXClass Nm mu)
(edge : AdjacentIndex m)
(hright : ↑anchor ≤ ↑↑edge)
:
finAnchorOrientedDyadicEdgeGain Nm mu anchor cls edge = dyadicForwardGain (singleScaleSigma2 Nm mu ↑(cls ↑edge)) (singleScaleSigma2 Nm mu ↑(cls (adjacentRightPosition edge)))
On the right, the outward gain is the ordinary original-edge forward ratio.
def
Anderson4D.XYCluster.finAnchorRetainedPhaseEdges
{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))
:
Finset (AdjacentIndex m)
The selected phase edges which were not charged to a coarse block.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Anderson4D.XYCluster.mem_finAnchorRetainedPhaseEdges
{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))
(edge : AdjacentIndex m)
:
edge ∈ finAnchorRetainedPhaseEdges Nm mu leftPhase rightPhase anchor cls O ↔ edge ∈ finAnchorPositionPhaseCarrierWithPhases leftPhase rightPhase anchor ∧ edge ∉ finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O
theorem
Anderson4D.XYCluster.finAnchorNXLocatedCoarseLedgerWithPhases_nodup
{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))
:
(finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O).Nodup
The concrete coarse ledger has no repeated located block.
noncomputable def
Anderson4D.XYCluster.retainedEdgePreciseBlock
{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))
(edge : AdjacentIndex m)
:
LocatedNXParityBlock Nm mu
Choose the concrete precise coarse-ledger block which accounts for a retained edge. The fallback branch is unreachable on the retained finset.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.XYCluster.retainedEdgePreciseBlock_spec
{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))
(edge : AdjacentIndex m)
(hedge : edge ∈ finAnchorRetainedPhaseEdges Nm mu leftPhase rightPhase anchor cls O)
:
retainedEdgePreciseBlock Nm mu leftPhase rightPhase anchor cls O edge ∈ finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O ∧ ∃ (i : Fin m) (j : Fin m) (p : NXPairBlock Nm mu),
retainedEdgePreciseBlock Nm mu leftPhase rightPhase anchor cls O edge = LocatedNXParityBlock.pair i j p ∧ p.left = cls i ∧ p.right = cls j ∧ (i ∈ leftAnchorPositions anchor ∧ j ∈ leftAnchorPositions anchor ∧ ↑edge = j ∧ ↑j + 1 = ↑i ∧ p.skipRight = decide (edge ∈ O) ∨ i ∈ rightAnchorPositions anchor ∧ j ∈ rightAnchorPositions anchor ∧ ↑edge = i ∧ ↑i + 1 = ↑j ∧ p.skipRight = decide (edge ∈ O))
theorem
Anderson4D.XYCluster.retainedEdgePreciseBlock_gain_eq
{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))
(edge : AdjacentIndex m)
(hedge : edge ∈ finAnchorRetainedPhaseEdges Nm mu leftPhase rightPhase anchor cls O)
:
locatedBlockPreciseGain Nm mu (retainedEdgePreciseBlock Nm mu leftPhase rightPhase anchor cls O edge) = finAnchorOrientedDyadicEdgeGain Nm mu anchor cls edge
noncomputable def
Anderson4D.XYCluster.retainedPreciseBlocks
{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))
:
Finset (LocatedNXParityBlock Nm mu)
Concrete precise blocks selected by the retained original edges.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.XYCluster.retainedPreciseBlocks_gainProduct_eq
{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 ∈ retainedPreciseBlocks Nm mu leftPhase rightPhase anchor cls O, locatedBlockPreciseGain Nm mu b = ∏ edge ∈ finAnchorRetainedPhaseEdges Nm mu leftPhase rightPhase anchor cls O,
finAnchorOrientedDyadicEdgeGain Nm mu anchor cls edge
theorem
Anderson4D.XYCluster.finAnchorNXCoarse_preciseGainProduct_le_retainedPhaseProduct
{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))
:
locatedLedgerPreciseGainProduct Nm mu
(finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) ≤ ∏ edge ∈ finAnchorRetainedPhaseEdges Nm mu leftPhase rightPhase anchor cls O,
finAnchorOrientedDyadicEdgeGain Nm mu anchor cls edge
The concrete precise-gain ledger is bounded by the product on exactly the
retained original phase edges. This is the direction required for the
upper estimate: any additional precise ledger factors are in [0,1].
The left factors are definitionally reverse original-edge ratios, while the right factors are forward ratios; no forward/reverse comparison is used.
theorem
Anderson4D.XYCluster.finAnchorNXCoarse_preciseGainProduct_le_phaseCarrier_sdiff_exception
{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))
:
locatedLedgerPreciseGainProduct Nm mu
(finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) ≤ ∏
edge ∈
finAnchorPositionPhaseCarrierWithPhases leftPhase rightPhase anchor \ finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O,
finAnchorOrientedDyadicEdgeGain Nm mu anchor cls edge
Literal carrier-minus-exception form of the precise-gain bound.