Graph transmission conditions

This module connects the graph rank infrastructure to the ASP/slipface formalization in demazure. The representative-level predicate is the direct Lean version of the defining inequalities for the transmission locus.

The pointwise predicate and restricted-test-set predicate are deliberately separated from the global condition. Later essential-set reductions can then prove that one finite set of lattice points is complete without changing the basic definition of transmission.

def Utilities.TransmissionInequality (G : CFGraph) (u v : G.V) (τ : AspPerm) (D : CFDiv G) (a b : ℤ) : Prop

The rank inequality attached to one lattice point (a,b) for a divisor representative and an ASP permutation.

Equations

• Utilities.TransmissionInequality G u v τ D a b = (rank G (D + a • oneChip u - b • oneChip v) ≥ τ.s.func (a + 1) b - 1)

def Utilities.SatisfiesTransmissionOn (G : CFGraph) (u v : G.V) (τ : AspPerm) (D : CFDiv G) (S : Set (ℤ × ℤ)) : Prop

The transmission inequalities restricted to a set of lattice points.

Equations

• Utilities.SatisfiesTransmissionOn G u v τ D S = ∀ p ∈ S, Utilities.TransmissionInequality G u v τ D p.1 p.2

def Utilities.SatisfiesTransmission (G : CFGraph) (u v : G.V) (τ : AspPerm) (D : CFDiv G) : Prop

A divisor representative satisfies the transmission condition for τ if it has the prescribed degree g + χτ and every twice-marked twist satisfies the corresponding slipface rank inequality.

Equations

• Utilities.SatisfiesTransmission G u v τ D = (CFDiv.degree D = G.genus + τ.χ ∧ ∀ (a b : ℤ), Utilities.TransmissionInequality G u v τ D a b)

theorem Utilities.degree_of_satisfiesTransmission {G : CFGraph} {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) : CFDiv.degree D = G.genus + τ.χ

The degree part of a transmission witness.

theorem Utilities.rank_twist_of_satisfiesTransmission {G : CFGraph} {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) (a b : ℤ) : rank G (D + a • oneChip u - b • oneChip v) ≥ τ.s.func (a + 1) b - 1

Extract one marked rank inequality from a transmission witness.

theorem Utilities.satisfiesTransmissionOn_of_satisfiesTransmission {G : CFGraph} {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) (S : Set (ℤ × ℤ)) : SatisfiesTransmissionOn G u v τ D S

A global transmission witness satisfies the inequalities on any chosen test set.

theorem Utilities.satisfiesTransmissionOn_mono {G : CFGraph} {u v : G.V} {τ : AspPerm} {D : CFDiv G} {S T : Set (ℤ × ℤ)} (hST : S ⊆ T) (hT : SatisfiesTransmissionOn G u v τ D T) : SatisfiesTransmissionOn G u v τ D S

Restricted transmission is monotone under shrinking the test set.

theorem Utilities.satisfiesTransmissionOn_univ_iff {G : CFGraph} {u v : G.V} {τ : AspPerm} {D : CFDiv G} : SatisfiesTransmissionOn G u v τ D Set.univ ↔ ∀ (a b : ℤ), TransmissionInequality G u v τ D a b

Checking on the entire integer lattice is equivalent to the universal inequality part of SatisfiesTransmission.

theorem Utilities.degree_twist_of_satisfiesTransmission {G : CFGraph} {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) (a b : ℤ) : CFDiv.degree (D + a • oneChip u - b • oneChip v) = G.genus + τ.χ + a - b

Every marked twist of a transmission witness has the expected affine degree.

theorem Utilities.marked_twist_linear_equiv {G : CFGraph} {D E : CFDiv G} (hDE : linearEquiv G D E) (u v : G.V) (a b : ℤ) : linearEquiv G (D + a • oneChip u - b • oneChip v) (E + a • oneChip u - b • oneChip v)

Adding the same marked twist to linearly equivalent divisors preserves linear equivalence.

theorem Utilities.transmissionInequality_of_linear_equiv {G : CFGraph} {D E : CFDiv G} (hDE : linearEquiv G D E) (u v : G.V) (τ : AspPerm) (a b : ℤ) (hD : TransmissionInequality G u v τ D a b) : TransmissionInequality G u v τ E a b

A single transmission inequality is invariant under replacing the divisor by a linearly equivalent representative.

theorem Utilities.satisfiesTransmission_of_linear_equiv {G : CFGraph} {D E : CFDiv G} (hDE : linearEquiv G D E) (u v : G.V) (τ : AspPerm) (hD : SatisfiesTransmission G u v τ D) : SatisfiesTransmission G u v τ E

The full transmission condition depends only on the divisor class.

theorem Utilities.satisfiesTransmission_linear_equiv_iff {G : CFGraph} {D E : CFDiv G} (hDE : linearEquiv G D E) (u v : G.V) (τ : AspPerm) : SatisfiesTransmission G u v τ D ↔ SatisfiesTransmission G u v τ E

Transmission is invariant under linear equivalence.

def Utilities.TransmissionExists (G : CFGraph) (u v : G.V) (τ : AspPerm) : Prop

Existence of a divisor class satisfying the graph transmission condition.

Equations

• Utilities.TransmissionExists G u v τ = ∃ (D : CFDiv G), Utilities.SatisfiesTransmission G u v τ D