Rank-one and doubled-point tests through two-pole responses

TwoPoleProfile.lean gives an exact scalar criterion for winnability of one factor sum. This file lifts that criterion to the two tests used by the genus-five programmes:

• rank at least one, equivalently a response match after subtracting every possible single vertex;
• winnability after subtracting a prescribed doubled vertex.

The statements are equivalences. They isolate the real work after restoring the second cross-edge without replacing it by a stronger sufficient condition. They also apply to every seam phase and to arbitrary factor divisors, not only canonical divisors or genus-two graphs.

theorem Utilities.TwoPole.sumDivisor_sub_zsmul_one_chip_inl (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (a : A.V) (n : ℤ) : sumDivisor A B p q D E - n • oneChip (Sum.inl a) = sumDivisor A B p q (D - n • oneChip a) E

Subtracting a pile at a left vertex stays entirely in the left factor.

theorem Utilities.TwoPole.sumDivisor_sub_zsmul_one_chip_inr (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (b : B.V) (n : ℤ) : sumDivisor A B p q D E - n • oneChip (Sum.inr b) = sumDivisor A B p q D (E - n • oneChip b)

Subtracting a pile at a right vertex stays entirely in the right factor.

theorem Utilities.TwoPole.sumDivisor_sub_one_chip_inl (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (a : A.V) : sumDivisor A B p q D E - oneChip (Sum.inl a) = sumDivisor A B p q (D - oneChip a) E

theorem Utilities.TwoPole.sumDivisor_sub_one_chip_inr (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (b : B.V) : sumDivisor A B p q D E - oneChip (Sum.inr b) = sumDivisor A B p q D (E - oneChip b)

def Utilities.TwoPole.HasRankOneResponseCover {A : CFGraph} {B : CFGraph} (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) : Prop

The exact factor-response data for rank one of a factor sum. The first component handles targets in the left factor and the second handles targets in the right factor.

Equations

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

theorem Utilities.TwoPole.rank_sumDivisor_ge_one_iff_responseCover (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) : rank (join A B p q) (sumDivisor A B p q D E) ≥ 1 ↔ p.HasRankOneResponseCover q D E

Exact rank-one response criterion.

theorem Utilities.TwoPole.rank_phase_sumDivisor_ge_one_iff_responseCover (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (n : ℤ) : rank (join A B p q) (phase A B p q (sumDivisor A B p q D E) n) ≥ 1 ↔ p.HasRankOneResponseCover q (D + n • oneChip p.second) (E - n • oneChip q.second)

The same exact rank-one criterion at an arbitrary seam phase.

theorem Utilities.TwoPole.winnable_sumDivisor_sub_two_inl_iff_responses (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (a : A.V) : winnable (join A B p q) (sumDivisor A B p q D E - 2 • oneChip (Sum.inl a)) ↔ ∃ (c₁ : ℤ) (c₂ : ℤ) (s : ℤ) (t : ℤ), p.IsDebitResponse (D - 2 • oneChip a) c₁ c₂ s ∧ q.IsCreditResponse E c₁ c₂ t ∧ s - t = c₁ - c₂

A doubled left target is winnable exactly when its two factor residuals have a compatible response.

theorem Utilities.TwoPole.winnable_sumDivisor_sub_two_inr_iff_responses (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (b : B.V) : winnable (join A B p q) (sumDivisor A B p q D E - 2 • oneChip (Sum.inr b)) ↔ ∃ (c₁ : ℤ) (c₂ : ℤ) (s : ℤ) (t : ℤ), p.IsDebitResponse D c₁ c₂ s ∧ q.IsCreditResponse (E - 2 • oneChip b) c₁ c₂ t ∧ s - t = c₁ - c₂

A doubled right target is winnable exactly when its two factor residuals have a compatible response.

theorem Utilities.TwoPole.winnable_phase_sumDivisor_sub_two_inl_iff_responses (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (n : ℤ) (a : A.V) : winnable (join A B p q) (phase A B p q (sumDivisor A B p q D E) n - 2 • oneChip (Sum.inl a)) ↔ ∃ (c₁ : ℤ) (c₂ : ℤ) (s : ℤ) (t : ℤ), p.IsDebitResponse (D + n • oneChip p.second - 2 • oneChip a) c₁ c₂ s ∧ q.IsCreditResponse (E - n • oneChip q.second) c₁ c₂ t ∧ s - t = c₁ - c₂

The doubled-left test at an arbitrary seam phase.

theorem Utilities.TwoPole.winnable_phase_sumDivisor_sub_two_inr_iff_responses (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (n : ℤ) (b : B.V) : winnable (join A B p q) (phase A B p q (sumDivisor A B p q D E) n - 2 • oneChip (Sum.inr b)) ↔ ∃ (c₁ : ℤ) (c₂ : ℤ) (s : ℤ) (t : ℤ), p.IsDebitResponse (D + n • oneChip p.second) c₁ c₂ s ∧ q.IsCreditResponse (E - n • oneChip q.second - 2 • oneChip b) c₁ c₂ t ∧ s - t = c₁ - c₂

The doubled-right test at an arbitrary seam phase.

theorem Utilities.TwoPole.rank_canonicalSum_ge_one_iff_responseCover (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) : rank (join A B p q) (canonicalSum A B p q) ≥ 1 ↔ p.HasRankOneResponseCover q (canonicalDivisor A) (canonicalDivisor B)

The two-edge K_A + K_B statement is exactly a canonical response cover. This theorem is useful both as a proof interface and as an honest record of the phase obligation that the one-pole Riemann--Roch argument does not see.