The interpolated gain in active-P coordinates #
The two complementary elimination phases produce an oriented dyadic ratio
on every retained original edge. This file records the ratio itself and
identifies the interpolated 1/16 product with the active-P weight used
by the outer sequence estimate.
noncomputable def
Anderson4D.XYCluster.finAnchorOrientedActivePRatio
{t : PlaneTree}
{Nm : t.HeppMarking}
{mu : t.Multiplicities}
{n : ℕ}
(anchor : Fin (n + 1))
(w : Fin (n + 1) → ActivePClass Nm mu)
(j : Fin n)
:
The positive active-P ratio on an original adjacency, oriented away
from the distinguished anchor.
Equations
Instances For
theorem
Anderson4D.XYCluster.finAnchorOrientedActivePRatio_nonneg
{t : PlaneTree}
{Nm : t.HeppMarking}
{mu : t.Multiplicities}
{n : ℕ}
(anchor : Fin (n + 1))
(w : Fin (n + 1) → ActivePClass Nm mu)
(j : Fin n)
:
theorem
Anderson4D.XYCluster.anchoredOrientedActivePEdgeGain_eq_ratioGain
(theta : ℝ)
{t : PlaneTree}
{Nm : t.HeppMarking}
{mu : t.Multiplicities}
{n : ℕ}
(anchor : Fin (n + 1))
(w : Fin (n + 1) → ActivePClass Nm mu)
(j : Fin n)
:
anchoredOrientedActivePEdgeGain theta anchor w j = ratioGain theta (finAnchorOrientedActivePRatio anchor w j)
The active-P edge gain is literally ratioGain of the outward
oriented ratio, for every exponent.
theorem
Anderson4D.XYCluster.finAnchor_phaseOrientedDyadicProduct_eq_ratioGain
{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)))
:
∏
edge ∈
finAnchorPositionPhaseCarrierWithPhases leftPhase rightPhase anchor \ finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O,
finAnchorOrientedDyadicEdgeGain Nm mu anchor cls edge = ∏
j ∈
finAnchorPositionPhaseFinCarrierWithPhases leftPhase rightPhase anchor \ finAnchorNXExceptionalFinEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O,
ratioGain (1 / 8) (finAnchorOrientedActivePRatio anchor (fun (i : Fin (n + 1)) => activeNXToP Nm mu (cls i)) j)
The retained one-phase dyadic product is the 1/8 product of the
same outward ratios later used for interpolation.
theorem
Anderson4D.XYCluster.finAnchorNX_interpolatedGain_eq_orientedActivePWeight
{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)))
:
∏ j ∈ Finset.univ \ finAnchorNXInterpolatedExceptionalFinEdges Nm mu leftPhase rightPhase anchor cls O,
ratioGain (1 / 16) (finAnchorOrientedActivePRatio anchor (fun (i : Fin (n + 1)) => activeNXToP Nm mu (cls i)) j) = anchoredOrientedActivePWeight (1 / 16)
(finAnchorPositionalInterpolatedExceptionalFinEdges leftPhase rightPhase anchor O) anchor fun (i : Fin (n + 1)) =>
activeNXToP Nm mu (cls i)
The concrete interpolated product is exactly the class-independent
positional active-P weight consumed by the outer sequence theorem.