Marked rank profiles and attained wedge convolution

A pointed rank profile records the ranks of every integral twist at one marked vertex. The exact vertex-wedge threshold formula implies more than a family of lower bounds: the tropical convolution of two realized profiles is attained at an integer phase and equals the wedge rank. This formulation is suited to recursive attachments and avoids any min or sInf interface.

def Utilities.PointedRankProfile (G : CFGraph) (D : CFDiv G) (q : G.V) (F : ℤ → ℤ) : Prop

A function which records every integral one-point twist rank of D.

Equations

• Utilities.PointedRankProfile G D q F = ∀ (t : ℤ), rank G (D + t • oneChip q) = F t

theorem Utilities.rank_sub_zsmul_one_chip_eq_of_pointedRankProfile (G : CFGraph) (D : CFDiv G) (q : G.V) (F : ℤ → ℤ) (hF : PointedRankProfile G D q F) (t : ℤ) : rank G (D - t • oneChip q) = F (-t)

Subtractive form of a realized pointed rank profile.

theorem Utilities.vertexWedge_rank_eq_iff_profile_inequalities_and_attained (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (r : ℤ) : rank (vertexWedge G H x y) (wedgeAddDivisor G H x y D E) = r ↔ (∀ (ell : ℤ), rank G (D - (ell + 1) • oneChip x) + rank H (E + ell • oneChip y) + 1 ≥ r) ∧ ∃ (ell : ℤ), rank G (D - (ell + 1) • oneChip x) + rank H (E + ell • oneChip y) + 1 = r

The raw factor-rank convolution is attained, and its attained value is exactly the rank of the wedge divisor.

theorem Utilities.vertexWedge_rank_eq_iff_pointedRankProfile_convolution_attained (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (F Q : ℤ → ℤ) (hF : PointedRankProfile G D x F) (hQ : PointedRankProfile H E y Q) (r : ℤ) : rank (vertexWedge G H x y) (wedgeAddDivisor G H x y D E) = r ↔ (∀ (ell : ℤ), F (-(ell + 1)) + Q ell + 1 ≥ r) ∧ ∃ (ell : ℤ), F (-(ell + 1)) + Q ell + 1 = r

Exact attained tropical convolution for two realized pointed profiles.

Pendant-profile rewrites for same-side transmission

def Utilities.WedgeSameLeftTransmissionProfileWithRightProfile (G : CFGraph) (H : CFGraph) (x : G.V) (_y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : G.V) (tau : AspPerm) (Q : ℤ → ℤ) : Prop

Same-left transmission data after replacing the unmarked right pendant factor by its realized pointed rank profile.

Equations

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

theorem Utilities.wedgeSameLeftTransmissionProfile_iff_withRightProfile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : G.V) (tau : AspPerm) (Q : ℤ → ℤ) (hQ : PointedRankProfile H E y Q) : WedgeSameLeftTransmissionProfile G H x y D E p q tau ↔ WedgeSameLeftTransmissionProfileWithRightProfile G H x y D E p q tau Q

A realized right-factor profile rewrites the exact same-left transmission profile without loss.

def Utilities.WedgeSameRightTransmissionProfileWithLeftProfile (G : CFGraph) (H : CFGraph) (_x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : H.V) (tau : AspPerm) (F : ℤ → ℤ) : Prop

Same-right transmission data after replacing the unmarked left pendant factor by its realized pointed rank profile.

Equations

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

theorem Utilities.wedgeSameRightTransmissionProfile_iff_withLeftProfile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : H.V) (tau : AspPerm) (F : ℤ → ℤ) (hF : PointedRankProfile G D x F) : WedgeSameRightTransmissionProfile G H x y D E p q tau ↔ WedgeSameRightTransmissionProfileWithLeftProfile G H x y D E p q tau F

A realized left-factor profile rewrites the exact same-right transmission profile without loss.