Counting the endpoint inversion block

This file turns the decreasing block supplied by EndpointBlock into the corresponding lower bound on the number of affine inversion classes, and assembles the resulting quadratic-versus-linear contradiction that rules out k-general transmission for the endpoint marking.

noncomputable def Bananas.endpointPairEmbedding (g : ℕ) : Sym2 (Fin g) → ℤ × ℤ

Encode an unordered endpoint pair by its minimum and one more than its maximum.

Equations

• Bananas.endpointPairEmbedding g = Sym2.lift ⟨fun (a b : Fin g) => (↑(min ↑a ↑b), ↑(max ↑a ↑b + 1)), ⋯⟩

theorem Bananas.endpointPairEmbedding_injective (g : ℕ) : Function.Injective (endpointPairEmbedding g)

theorem Bananas.endpoint_block_inversion_lower_bound {g k : ℕ} {τ : ℤ → ℤ} (hk : 0 < k) (hAffine : IsKAffine k τ) (hBlock : ∀ b ≤ g, τ ↑b = ↑(g - b)) (hfinite : (kInversions k τ).Finite) : (g + 1).choose 2 ≤ kInversionCount k τ

theorem Bananas.endpoint_marked_inversion_lower_bound {g k : ℕ} (B : Banana g) (hsub : AllSubmodular (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B))) (hk : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B)) k) : ∃ (D : CFDiv (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B)).graph) (τ : ℤ → ℤ), IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B)) D τ ∧ IsKAffine k τ ∧ (g + 1).choose 2 ≤ kInversionCount k τ

TeX labels: lem-TriangleInversionII (Lemma 4.20), prop-TriangleInversionNumber (Proposition 4.21).

With (u,v) = (v_{0,0}, v_{0,n_0}) and D = g·v_{0,n_0}, the transmission permutation contains the decreasing block τ(b) = g - b for 0 ≤ b ≤ g, yielding M ≥ choose (g+1) 2 inversion classes. The ∃ D τ form is the formal reading of the paper's M, the maximum over all divisors.

Only hk.1 (a torsion witness) is used; IsTorsionOrder is kept because the paper's M and inv_k refer to the torsion order.

The period conclusion used in Proposition 4.19 is already forced by the endpoint transmission block, before counting its inversions.

theorem Bananas.endpoint_marking_torsionOrder_gt_genus {g k : ℕ} (B : Banana g) (hsub : AllSubmodular (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B))) (hk : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B)) k) : g < k

theorem Bananas.endpoint_marking_not_kGeneral {g k : ℕ} (hg : 2 ≤ g) (B : Banana g) : ¬KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B)) k

TeX labels: thm:bananas (Theorem 1.17) / cor:bananasWithKGT (Corollary 6.4), endpoint-marking branch, unconditional.

For every genus at least two, the endpoint-marked banana (B, v_0, v_{n}) admits k-general transmission for no k at all.

The proof is an assembly of results that were already present separately. Suppose KGeneralTransmission (mark B v_0 v_n) k. Then

• all divisors are submodular (second conjunct of Definition 1.10), and by banana_kGeneral_isTorsionOrder (lem:kgtImpliesTorsionOrder, Lemma 4.2) k is the exact torsion order;
• so endpoint_marked_inversion_lower_bound (lem-TriangleInversionII 4.20 / prop-TriangleInversionNumber 4.21) supplies a divisor D whose transmission permutation has at least choose (g+1) 2 inversion classes;
• the third conjunct of Definition 1.10 supplies, for that same D, a transmission permutation with at most genus = g inversion classes;
• transmission permutations are unique (transmissionPermutation_unique), so these are the same permutation, giving choose (g+1) 2 ≤ g, false for g ≥ 2.

The quadratic-versus-linear gap is exactly the paper's argument; the only ingredient that had to be added was uniqueness, which is immediate from def-tauD (Definition 2.11).