Transmission inequalities outside the special slipface locus are automatic

For a divisor of transmission degree g + χ, the twist at (a,b) has degree g + χ + a - b. Graph Riemann--Roch gives the universal lower bound

rank(T) ≥ deg(T) - g = χ + a - b.

On the other hand a slipface is bounded below by max 0 (a+1-b+χ). Therefore, whenever the slipface equals this generic baseline, the corresponding transmission inequality is automatic:

• baseline 0 asks only for rank ≥ -1;
• baseline a+1-b+χ > 0 asks for rank ≥ χ+a-b, exactly the RR lower bound.

Thus only rows with strict slipface excess over the generic baseline need to be checked. This is the Schubert-special locus on which an essential-set theorem should operate.

theorem Utilities.rank_ge_degree_sub_genus {G : CFGraph} (hconn : graphConnected G) (D : CFDiv G) : rank G D ≥ CFDiv.degree D - G.genus

Universal Riemann--Roch lower bound r(D) ≥ deg(D)-g.

def Utilities.SpecialTransmissionPair (τ : AspPerm) (a b : ℤ) : Prop

A row is special when its ASP slipface lies strictly above the generic slipface of the same shift.

Equations

• Utilities.SpecialTransmissionPair τ a b = (τ.s.func (a + 1) b > max 0 (a + 1 - b + τ.χ))

def Utilities.SpecialTransmissionSet (τ : AspPerm) : Set (ℤ × ℤ)

The special row set.

Equations

• Utilities.SpecialTransmissionSet τ = {p : ℤ × ℤ | Utilities.SpecialTransmissionPair τ p.1 p.2}

theorem Utilities.slipface_eq_baseline_of_not_special (τ : AspPerm) (a b : ℤ) (h : ¬SpecialTransmissionPair τ a b) : τ.s.func (a + 1) b = max 0 (a + 1 - b + τ.χ)

A nonspecial row is exactly on the generic slipface baseline.

theorem Utilities.transmissionInequality_of_not_special {G : CFGraph} (hconn : graphConnected G) (u v : G.V) (τ : AspPerm) (D : CFDiv G) (hDegree : CFDiv.degree D = G.genus + τ.χ) (a b : ℤ) (h : ¬SpecialTransmissionPair τ a b) : TransmissionInequality G u v τ D a b

Every nonspecial row is automatic for a connected graph once the divisor has transmission degree.

theorem Utilities.satisfiesTransmission_iff_special {G : CFGraph} (hconn : graphConnected G) (u v : G.V) (τ : AspPerm) (D : CFDiv G) : SatisfiesTransmission G u v τ D ↔ CFDiv.degree D = G.genus + τ.χ ∧ ∀ (a b : ℤ), SpecialTransmissionPair τ a b → TransmissionInequality G u v τ D a b

Full transmission is equivalent, on a connected graph, to checking only the special slipface rows together with the degree equation.

theorem Utilities.satisfiesTransmission_iff_specialSet {G : CFGraph} (hconn : graphConnected G) (u v : G.V) (τ : AspPerm) (D : CFDiv G) : SatisfiesTransmission G u v τ D ↔ CFDiv.degree D = G.genus + τ.χ ∧ SatisfiesTransmissionOn G u v τ D (SpecialTransmissionSet τ)

Set-level special-row formulation.