Genus-two corner algebra without a theta presentation

These are the graph-generic degree slices in the finite proof of Lemma 4.10. The hypotheses isolate exactly what bridgelessness supplies: every one-chip divisor has rank zero.

theorem Bananas.rank_canonical_sub_one_chip_zero_of_genus_two (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (q : G.V) (hOne : rank G (oneChip q) = 0) : rank G (canonicalDivisor G - oneChip q) = 0

In connected genus two, the canonical divisor minus a chip has rank zero whenever that chip has rank zero.

theorem Bananas.degreeZero_slice_eq_two_mul_rankPlusOne_of_genus_two (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (X : CFDiv G) (hDeg : CFDiv.degree X = 0) : rankPlusOne G X * rankPlusOne G (canonicalDivisor G - X) = 2 * rankPlusOne G X

The degree-zero slice has the same value as in the theta proof on every connected genus-two graph.

theorem Bananas.degreeZero_mul_canonical_sub_add_one_chip_of_genus_two (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (X : CFDiv G) (q : G.V) (hOne : rank G (oneChip q) = 0) (hDeg : CFDiv.degree X = 0) : rankPlusOne G X * rankPlusOne G (canonicalDivisor G - (X + oneChip q)) = rankPlusOne G X

A degree-zero slice remains its principality indicator after the dual divisor is shifted by one chip.

theorem Bananas.degreeOne_slice_eq_rankPlusOne_of_genus_two (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (hRankZero : ∀ (X : CFDiv G), CFDiv.degree X = 1 → 0 ≤ rank G X → rank G X = 0) (X : CFDiv G) (hDeg : CFDiv.degree X = 1) : rankPlusOne G X * rankPlusOne G (canonicalDivisor G - X) = rankPlusOne G X

In genus two, the degree-one slice is idempotent once degree-one effective divisors have rank zero.

theorem Bananas.degreeTwo_first_three_cancel_of_genus_two (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (u v : G.V) (hOneU : rank G (oneChip u) = 0) (hOneV : rank G (oneChip v) = 0) (X : CFDiv G) (hDeg : CFDiv.degree X = 2) : (rankPlusOne G X - rankPlusOne G (X - oneChip u) - rankPlusOne G (X - oneChip v)) * rankPlusOne G (canonicalDivisor G - X) = 0

In degree two, the first three marked inclusion--exclusion terms cancel after multiplication by the canonical complement. This is the only degree-two calculation needed before the residual correction term in Lemma 4.10.

theorem Bananas.degreeZero_twistContribution_eq_of_genus_two (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (u v : G.V) (D : CFDiv G) (b : ℤ) : markedRankDelta G u v (fixedDegreeTwist G u v D 0 b) * rankPlusOne G (canonicalDivisor G - fixedDegreeTwist G u v D 0 b) = 2 * rankPlusOne G (fixedDegreeTwist G u v D 0 b)

The degree-zero fixed-twist contribution in the finite inversion sum.

theorem Bananas.degreeOne_twistContribution_eq_of_genus_two (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (u v : G.V) (hOneU : rank G (oneChip u) = 0) (hOneV : rank G (oneChip v) = 0) (hRankZero : ∀ (X : CFDiv G), CFDiv.degree X = 1 → 0 ≤ rank G X → rank G X = 0) (D : CFDiv G) (b : ℤ) : markedRankDelta G u v (fixedDegreeTwist G u v D 1 b) * rankPlusOne G (canonicalDivisor G - fixedDegreeTwist G u v D 1 b) = rankPlusOne G (fixedDegreeTwist G u v D 1 b) - rankPlusOne G (fixedDegreeTwist G u v D 0 b) - rankPlusOne G (fixedDegreeTwist G u v D 0 (b + 1))

The degree-one fixed-twist contribution, with its two degree-zero boundary terms made explicit.

theorem Bananas.degreeTwo_twistContribution_eq_of_genus_two (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (u v : G.V) (hOneU : rank G (oneChip u) = 0) (hOneV : rank G (oneChip v) = 0) (D : CFDiv G) (b : ℤ) : markedRankDelta G u v (fixedDegreeTwist G u v D 2 b) * rankPlusOne G (canonicalDivisor G - fixedDegreeTwist G u v D 2 b) = rankPlusOne G (fixedDegreeTwist G u v D 0 (b + 1)) * rankPlusOne G (canonicalDivisor G - fixedDegreeTwist G u v D 2 b)

After the degree-two cancellation, only the degree-zero correction product survives.

theorem Bananas.threeDegreeTwistContribution_eq_telescoping_of_genus_two (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (u v : G.V) (hOneU : rank G (oneChip u) = 0) (hOneV : rank G (oneChip v) = 0) (hRankZero : ∀ (X : CFDiv G), CFDiv.degree X = 1 → 0 ≤ rank G X → rank G X = 0) (D : CFDiv G) (b : ℤ) : threeDegreeTwistContribution G u v D b = rankPlusOne G (fixedDegreeTwist G u v D 1 b) + rankPlusOne G (fixedDegreeTwist G u v D 0 b) - rankPlusOne G (fixedDegreeTwist G u v D 0 (b + 1)) + rankPlusOne G (fixedDegreeTwist G u v D 0 (b + 1)) * rankPlusOne G (canonicalDivisor G - fixedDegreeTwist G u v D 2 b)

Pointwise telescoping of the three fixed-degree slices, now independent of a theta presentation.

noncomputable def Bananas.bridgelessGenusTwoCornerWeight (G : CFGraph) (X : CFDiv G) : ℤ

The three possible complementary-rank values at a selected corner of an arbitrary connected genus-two graph.

Equations

• Bananas.bridgelessGenusTwoCornerWeight G X = if CFDiv.degree X = 0 then 2 else if CFDiv.degree X = 1 then 1 else if CFDiv.degree X = 2 ∧ linearEquiv G X (canonicalDivisor G) then 1 else 0

theorem Bananas.complement_rank_add_one_eq_bridgelessGenusTwoCornerWeight (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (u v : G.V) (hRankZero : ∀ (X : CFDiv G), CFDiv.degree X = 1 → 0 ≤ rank G X → rank G X = 0) (X : CFDiv G) (hDelta : rankDelta (mark G u v) X = 1) : rank G (canonicalDivisor G - X) + 1 = bridgelessGenusTwoCornerWeight G X

Exact pointwise genus-two reduction of a selected transmission corner's complementary rank, without a theta presentation.

theorem Bananas.intCast_kInversionCount_eq_sum_bridgelessGenusTwoCornerWeight (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (u v : G.V) (hRankZero : ∀ (X : CFDiv G), CFDiv.degree X = 1 → 0 ≤ rank G X → rank G X = 0) (D : CFDiv G) (k : ℕ) (tau : ℤ → ℤ) (hk : 0 < k) (hTau : IsTransmissionPermutation (mark G u v) D tau) (hAffine : IsKAffine k tau) : ↑(kInversionCount k tau) = ∑ b : Fin k, bridgelessGenusTwoCornerWeight G (D + tau ↑↑b • oneChip u - ↑↑b • oneChip v)

The finite inversion count is the sum of the three-valued corner weights on every connected genus-two graph satisfying the bridgeless degree-one rank condition. This removes the theta presentation from the first half of Lemma 4.10.

theorem Bananas.bridgelessGenusTwoCornerWeight_eq_threeDegreeTwistContribution (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (u v : G.V) (hRankZero : ∀ (X : CFDiv G), CFDiv.degree X = 1 → 0 ≤ rank G X → rank G X = 0) (D : CFDiv G) (tau : ℤ → ℤ) (hTau : IsTransmissionPermutation (mark G u v) D tau) (b : ℤ) : bridgelessGenusTwoCornerWeight G (transmissionCorner (mark G u v) D tau b) = threeDegreeTwistContribution G u v D b

A selected transmission corner contributes exactly its matching one of the three fixed-degree slices.

theorem Bananas.intCast_kInversionCount_eq_sum_threeDegreeTwistContribution_of_genus_two (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (u v : G.V) (hRankZero : ∀ (X : CFDiv G), CFDiv.degree X = 1 → 0 ≤ rank G X → rank G X = 0) (D : CFDiv G) (k : ℕ) (tau : ℤ → ℤ) (hk : 0 < k) (hTau : IsTransmissionPermutation (mark G u v) D tau) (hAffine : IsKAffine k tau) : ↑(kInversionCount k tau) = ∑ b : Fin k, threeDegreeTwistContribution G u v D ↑↑b

Finite three-degree form of the inversion sum on an arbitrary bridgeless genus-two graph.

theorem Bananas.intCast_kInversionCount_eq_effectiveResidues_ncard_of_bridgeless_rigid (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (u v : G.V) (hOneU : rank G (oneChip u) = 0) (hOneV : rank G (oneChip v) = 0) (hRankZero : ∀ (X : CFDiv G), CFDiv.degree X = 1 → 0 ≤ rank G X → rank G X = 0) (D : CFDiv G) (k : ℕ) (tau : ℤ → ℤ) (hk : TorsionWitness (mark G u v) k) (hTau : IsTransmissionPermutation (mark G u v) D tau) (hAffine : IsKAffine k tau) (hRigid : ¬linearEquiv G (oneChip u + oneChip v) (canonicalDivisor G)) : ↑(kInversionCount k tau) = ↑(effectiveDegreeOneTwistResidues (mark G u v) D k).ncard

Correction-free, arbitrary bridgeless genus-two form of Lemma 4.10.

theorem Bananas.kInversionCount_eq_effectiveResidues_ncard_of_bridgeless_rigid (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (u v : G.V) (hOneU : rank G (oneChip u) = 0) (hOneV : rank G (oneChip v) = 0) (hRankZero : ∀ (X : CFDiv G), CFDiv.degree X = 1 → 0 ≤ rank G X → rank G X = 0) (D : CFDiv G) (k : ℕ) (tau : ℤ → ℤ) (hk : TorsionWitness (mark G u v) k) (hTau : IsTransmissionPermutation (mark G u v) D tau) (hAffine : IsKAffine k tau) (hRigid : ¬linearEquiv G (oneChip u + oneChip v) (canonicalDivisor G)) : kInversionCount k tau = (effectiveDegreeOneTwistResidues (mark G u v) D k).ncard

Natural-number form of the correction-free bridgeless genus-two inversion identity.

theorem Bananas.bridgelessGenusTwoRigid_kGeneral_iff_nonRecurrent (G : CFGraph) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hGenus : G.genus = 2) (u v : G.V) (k : ℕ) (hSub : AllSubmodular (mark G u v)) (hTO : IsTorsionOrder (mark G u v) k) (hRigid : ¬linearEquiv G (oneChip u + oneChip v) (canonicalDivisor G)) : KGeneralTransmission (mark G u v) k ↔ NonRecurrent (mark G u v) k

The full arbitrary-bridgeless version of Theorem 4.8. TwoEdgeCutCondition is the library's literal no-bridge condition; the nontriviality hypothesis excludes the vacuous one-vertex graph, where a one-chip divisor has rank one.

theorem Bananas.intCast_kInversionCount_eq_effectiveResidues_add_correction_of_bridgeless (G : CFGraph) (hConnected : _root_.graphConnected G) (hGenus : G.genus = 2) (u v : G.V) (hOneU : rank G (oneChip u) = 0) (hOneV : rank G (oneChip v) = 0) (hRankZero : ∀ (X : CFDiv G), CFDiv.degree X = 1 → 0 ≤ rank G X → rank G X = 0) (D : CFDiv G) (k : ℕ) (tau : ℤ → ℤ) (hk : IsTorsionOrder (mark G u v) k) (hTau : IsTransmissionPermutation (mark G u v) D tau) (hAffine : IsKAffine k tau) : ↑(kInversionCount k tau) = ↑(effectiveDegreeOneTwistResidues (mark G u v) D k).ncard + invTauCorrection (mark G u v) D

Full arbitrary-bridgeless genus-two form of Lemma 4.10, including the canonical correction term.

theorem Bananas.bridgeless_genusTwo_invTau_formula (G : CFGraph) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hGenus : G.genus = 2) (u v : G.V) (D : CFDiv G) (k : ℕ) (τ : ℤ → ℤ) (hTO : IsTorsionOrder (mark G u v) k) (hτ : IsTransmissionPermutation (mark G u v) D τ) (hAffine : IsKAffine k τ) : ↑(kInversionCount k τ) = ↑(effectiveDegreeOneTwistResidues (mark G u v) D k).ncard + invTauCorrection (mark G u v) D

TeX label: lem:invtau (Lemma 4.10), at the paper's full bridgeless genus-two scope.

TwoEdgeCutCondition is the formal no-bridge condition. The explicit nontriviality hypothesis excludes the one-vertex edgeless graph, whose degree-one class has rank one and is not covered by the paper's intended bridgeless convention.

theorem Bananas.bridgeless_genusTwo_rigid_kGeneral_iff_nonRecurrent (G : CFGraph) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hGenus : G.genus = 2) (u v : G.V) (k : ℕ) (hSub : AllSubmodular (mark G u v)) (hTO : IsTorsionOrder (mark G u v) k) (hRigid : ¬linearEquiv G (oneChip u + oneChip v) (canonicalDivisor G)) : KGeneralTransmission (mark G u v) k ↔ NonRecurrent (mark G u v) k

TeX label: lem:invtau (Lemma 4.10), at the paper's full bridgeless genus-two scope.