Easy-access reference: Twice-Marked Banana Graphs #
This file is a single navigable index of every definition, lemma, proposition, theorem, corollary, and mathematically-substantive remark in Twice-Marked Banana Graphs, in the paper's own order, each paired with its formalization in this library.
How to read an entry.
- Definitions, conjectures, purely qualitative remarks, and items with no
Lean counterpart are recorded as plain comment blocks (
/- ... -/): a quotation or close paraphrase of the paper's statement, its TeX\labeland paper number, and (where one exists) the name of the Lean declaration that formalizes it. No new declaration is introduced for these — the existing name is the citable one. - Every proved lemma/proposition/theorem/corollary gets a statement
theorem here (named
Bananas.TwiceMarkedBananas.s<section>_...). Its statement is written over the self-contained, Mathlib-only vocabulary of the namespaceTMBin the imported vocabulary modules — the same vocabulary block, verbatim, as the statement-only audit copyTwiceMarkedBananasStatements.lean— and its proof crosses explicitly from that vocabulary to the repository's proved API through the bridge lemmas of the section Bridges to the implementation library. The docstring on each statement records the paper's statement, TeX label, and number. Where a checked statement uses a different or more explicit formulation, that is recorded explicitly — seeBananas/FORMALIZATION_NOTES.mdfor the corresponding formulation notes. - When a result has genuinely no single assembled Lean statement (either because the mechanization deliberately avoids the paper's exact formulation, or because coverage is split across several files), the entry says so and points at the closest available pieces.
- Five further entries whose types intrinsically require implementation
objects (concrete proof-carrying chain factors, the bridgeless class map,
AspPerm) are kept at the end of the file as thin wrappers over the library vocabulary; they have no counterpart in the audit copy.
Source-text licensing is recorded in THIRD_PARTY_NOTICES.md. This file is a
reference index, not new mathematics: every statement below is a direct
restatement of an existing proof. Further paper-specific reference sources are
Bananas/Sections/SectionFiveStatements.lean and
Bananas/FORMALIZATION_NOTES.md.
Bridges to the implementation library #
The imported CoreVocabulary and StatementVocabulary modules retain the
standalone statement vocabulary corresponding to TwiceMarkedBananasStatements.lean. The
declarations below are where
this file deliberately crosses into the implementation library: each
standalone notion is carried to its library counterpart by a conversion
function (toLib, toLibBanana, toLibTM, ...), and the vocabulary
predicates are shown to agree with the library predicates along those
conversions. Almost every such agreement holds by unfolding definitions; the
one genuine difference is the standalone rank, which is defined by a
definite description and is identified with the library's rank through the
library's rank_geq_iff.
Graphs #
Cross a standalone graph into the library's graph type without changing any data.
Equations
- TMB.toLib G = { V := G.V, instDecidableEq := G.instDecidableEq, instFintype := G.instFintype, instNonempty := ⋯, edges := G.edges, loopless := ⋯ }
Instances For
Read a library graph as a standalone graph.
Equations
- TMB.ofLib G = { V := G.V, instDecidableEq := G.instDecidableEq, instFintype := G.instFintype, instNonempty := ⋯, edges := G.edges, loopless := ⋯ }
Instances For
Rank #
The library rank satisfies the standalone exact-rank predicate.
The standalone rank is the library rank.
Twice-marked graphs #
Cross a standalone twice-marked graph into the library's bundle.
Instances For
Graph isomorphisms #
Cross a standalone graph isomorphism into the library's.
Equations
- TMB.toLibIso φ = { vertexEquiv := φ.vertexEquiv, map_num_edges := ⋯ }
Instances For
Read a library graph isomorphism as a standalone one.
Equations
- TMB.ofLibIso φ = { vertexEquiv := φ.vertexEquiv, map_num_edges := ⋯ }
Instances For
Cross a mark-swapping automorphism into the library's bundle.
Equations
- TMB.toLibSwap φ = { iso := TMB.toLibIso φ.iso, preserves_marked_set := ⋯, map_u := ⋯, map_v := ⋯ }
Instances For
Marked graphs and chains #
Cross a standalone marked graph into the library's bundle.
Instances For
Chain factors #
Cross a chain factor, bridging its k-general transmission proof.
Equations
- TMB.toLibFactor F = { marked := TMB.toLibMG F.marked, period := F.period, connected := ⋯, kGeneral := ⋯ }
Instances For
Weierstrass partitions and the once-marked census #
Once-marked generality at the right mark of a chain, in library form.
Bananas #
Cross a standalone banana into the library's subdivision specification.
Equations
- TMB.toLibBanana B = { core := { tail := B.tail, head := B.head }, length := B.length, core_nonempty := TMB.toLibBanana._proof_1, core_loopless := ⋯, length_pos := ⋯ }
Instances For
Read a library banana as a standalone one.
Equations
Instances For
Section 1 — Introduction #
Example 1.11 (eg:cycle). Section 1.
"If G is a cycle graph, with two marked points u,v joined by two paths of length a and b, then the torsion order of (G,u,v) is k = (a+b)/gcd(a,b) and (G,u,v) has k-general transmission [Pfl22, §2.1]."
Exact. A cycle graph marked at its two junction vertices is the genus-one
banana B : Banana g at g = 1, marked at leftEndpoint B /
rightEndpoint B, with a = B.length 0, b = B.length 1
(Bananas/Transmission/CycleTorsionOrder.lean). The paper defers its own proof to
[Pfl22, §2.1]; the argument here instead runs through the banana Jacobian
presentation of Proposition 2.14 (Bananas/Jacobian/BananaJacobianProposition214.lean):
the diagonal and strand-length relations identify k(u - v) with a multiple
of the shared coordinate step that is annihilated exactly at
k = (a+b)/gcd(a,b), and a homomorphism to ZMod (a+b) that kills exactly
the displayed relation lattice rules out any smaller witness.
Theorem 1.12 (thm:thetaSimple), part 1). Section 1.
"Let (G,u,v) be a theta graph with two marked points. 1) If u and v are located on the interiors of distinct strands of G, then all divisors on G are submodular."
Exact. Also cross-labeled cor-allSubmodSameStrand (Corollary 3.6, case 1,
⇐ direction).
Theorem 1.12 (thm:thetaSimple), part 2). Section 1.
"2) If (G,u,v) is evenly marked, meaning that u and v divide their strands into two segments with the same ratio a/b ∈ ℚ, then (G,u,v) has k-general transmission, where k is the torsion order of (G,u,v)."
Exact and unconditional. Also Corollary 4.17 (cor:evenlyMarkedKGT). The theorem discharges the
auxiliary inversion-data hypothesis.
Theorem 1.13 (thm:bngChain), part 1). Section 1. Body of the paper:
Corollary 6.16, part 1).
"Let (G_i,u_i,v_i), i = 1,…,ℓ, be a sequence of twice-marked graphs, and (G,u,v) the iterated vertex gluing. Let g_i, k_i be the genus of G_i and torsion order of (G_i,u_i,v_i). Suppose each (G_i,u_i,v_i) has k_i-general transmission. 1) If k_i > g_1+…+g_i for all i, then (G,v) is a Brill--Noether general marked graph."
Exact, with the intended left-associated MarkedGraph.chain recursion
replacing the paper's self-referential display (Bananas/FORMALIZATION_NOTES.md, "Chain
theorem notation").
Theorem 1.13 (thm:bngChain), part 2). Section 1. Body of the paper:
Corollary 6.16, part 2).
"2) If k_i > min{g_1+…+g_i, g_i+g_{i+1}+…+g_ℓ} for all i, then G is a Brill--Noether general graph."
Exact, in the paper's full graph convention (connected genus-zero factors allowed in arbitrary positions), via a recursive prefix/minimum-budget encoding rather than the paper's indexed sums.
Theorem 1.16 (thm:bananaSimple). Section 1.
"Let (G,u,v) be a banana graph of genus g ≥ 3, marked at two vertices u,v, at least one of which lies at least distance 2 from both multivalent vertices. Then there exist non-submodular divisors on (G,u,v)."
Formalization note. The checked statement includes the additional case in which the other mark
is the midpoint of a distinct length-two strand. This is represented by
CorrectedBananaSimpleException; see Bananas/FORMALIZATION_NOTES.md.
Theorem 1.17 (thm:bananas). Section 1.
"A twice-marked banana graph of genus g ≥ 3 does not have k-general transmission for any k ≥ 3."
Corrected, now complete. The published Proposition 4.19 exception family
it rests on was enlarged to CorrectedMidpointException
(Bananas/FORMALIZATION_NOTES.md); with that correction the theorem itself is exact and
unconditional.
Remark 1.18 (unlabeled), claim 1 — the endpoint pencil. Section 1.
"Another important way in which banana graphs are special is that they are always hyperelliptic: they possess a degree 2 divisor of rank 1, consisting of the two non-bivalent vertices."
Exact. Same underlying fact as Lemma 2.20 (lem:g12).
Remark 1.18 (unlabeled), claim 2 — hence not Brill–Noether general. Section 1.
"For g ≥ 3 this shows that they are not Brill--Noether general, since ρ(g,1,2) = 2-g."
Exact. (The moduli-theoretic dimension/codimension sentence preceding this in the remark is not a graph-theoretic claim and is not formalized.)
Section 2 — Background #
Lemma 2.3 (lem-bridgelessFacts), part 1). Section 2.
"If G is a bridgeless graph then 1) If u,v ∈ V(G) then u = v if and only if u ∼ v."
Corrected: formalized with TwoEdgeCutCondition as the precise no-bridge
hypothesis.
Lemma 2.12 (lem:tauChars, cited to [Pfl22, Remark 1.5, Prop 2.3]),
existence half. Section 2.
"A divisor D on (G,u,v) has a well-defined transmission permutation if and only if it is submodular. If (G,u,v) has torsion order k, or more generally if ku ∼ kv, then τ_D ∈ \widetilde{E}a_k."
Partial: only the "all divisors submodular + torsion witness ⇒ affine transmission permutation exists" direction, and only for banana graphs; the converse and uniqueness are not separately exposed. One of two paper results (with Example 1.11) the paper itself defers to [Pfl22].
Lemma 2.12 (lem:tauChars), southeast rank formula. Section 2.
"The transmission permutation is also characterized by ... r(D+au-bv)+1 = #{ℓ ≥ b : τ_D(ℓ) ≤ a}."
Lemma 2.12 (lem:tauChars), northwest rank formula. Section 2.
"... r(K_G-D-au+bv)+1 = #{ℓ < b : τ_D(ℓ) > a}."
Lemma 2.20 (lem:g12). Section 2.
"For any banana graph G = B_{n_0,…,n_g}, the divisor v_{0,0}+v_{0,n_0} has rank 1."
Exact. Same underlying fact as Remark 1.18, claim 1.
Lemma 2.21 (lem-BananaRDS). Section 2.
"For any banana graph G = B_{n_0,…,n_g} the set {v_{0,0},v_{0,n_0}} is a rank determining set."
Exact/complete.
Lemma 2.23 (unlabeled), existence half. Section 2.
"If D ∈ Pic(B_{n_0,…,n_g}) is v_{0,0}-reduced then D = av_{0,0}+bv_{0,n_0}+E where E is an effective divisor with at most one chip on each strand and no chips at either multivalent vertex, and 0 ≤ b ≤ g - deg E."
Lemma 2.23 (unlabeled), converse half. Section 2.
"Conversely, every divisor of this form is v_{0,0}-reduced."
Lemma 2.23 (unlabeled), final clause. Section 2.
"As with all reduced divisors, r(D) ≥ 0 if and only if a ≥ 0."
The Lean version proves strictly more than the paper: Bananas/SameStrand/Semibreak.lean's
bananaNormalForm_parameters_unique also gives uniqueness of (a,b,E),
which the paper only implies.
Corollary 2.24 (cor-BanaRankComp). Section 2.
"If D = av_{0,0}+bv_{0,n_0}+E has the form described above, and a,b satisfy a,b ≥ -1 and either 0 ≤ a ≤ g-deg E or 0 ≤ b ≤ g - deg E, then r(D) = min{a,b}+max{0,max{a,b}-(g-deg E)} = max{min{a,b}, deg D - g}."
Exact, in the second displayed form.
Corollary 2.25 (cor-BananaDeltaComps), part 1). Section 2.
"Given a twice-marked banana graph (B_{n_0,…,n_g},u,v): 1) If (u,v)=(v_{0,0},v_{0,n_0}) and a ≥ 0 then Δ(a(v_{0,0}+v_{0,n_0})) = δ(a ≤ g)."
Corollary 2.25 (cor-BananaDeltaComps), part 2) headline instance.
Section 2. One representative of the "one-off" family (there are four,
Bananas/CrossOneOff/BananaOneOffDeltaFamilies.lean); see that file for the others.
"2) If (u,v)=(v_{0,0},v_{0,n_0-1}) with 0 ≤ b < a ≤ g … then Δ(av_{0,0}+bv_{0,n_0}+v) = δ(a=g)."
Corollary 2.25 (cor-BananaDeltaComps), part 3) headline instance.
Section 2. This is the ledger's chosen representative of the "cross-off"
family (Bananas/CrossOneOff/BananaCrossOneOffDeltaFamilies.lean has the rest).
"3) If (u,v)=(v_{0,1},v_{1,n_1-1}) … then Δ(a(v_{0,0}+v_{0,n_0})+v_{0,m}+v_{1,n}) = 1."
Section 3 — Submodularity on Banana Graphs #
Lemma 3.2 (lemm-rank0supp), part 1). Section 3.
"1) If (G,u,v) is a twice-marked graph of genus 2 and u ≁ v, then any divisor D with Δ(D) < 0 has degree 2 and rank 0."
Lemma 3.2 (lemm-rank0supp), part 2). Section 3.
"2) If (G,u,v) is a twice-marked graph of any genus, and D is a divisor of rank 0, then Δ(D) < 0 if and only if v ∈ Supp(D)\Supp(D-u) and u ∈ Supp(D)\Supp(D-v)."
Theorem 3.4 (thm-NonSubmodGenus2), the full same-strand
equivalence 1) ⇔ 2), endpoint-inclusive. Section 3.
"Let G = θ_{n_0,n_1,n_2}, (G,u,v) a twice-marked theta graph with u ≁ v. The following are equivalent. 1) There exist divisors D with Δ(D) < 0. 2) The marked points u,v are on the same strand … and the set N_{(G,u,v)} … is nonempty. In particular there is a bijection N_{(G,u,v)} → {[D] ∈ Pic(G) : Δ(D)<0}, v_{α,k} ↦ [v_{α,k}+v_{α,i}]."
The equivalence is proved (theta_nonSubmodular_iff_same_strand, below);
the paper's u ≁ v hypothesis is derived rather than assumed. The class
bijection of 2) is proved separately in three branches (interior,
initial-endpoint, terminal-endpoint — Bananas/Theta/ThetaNegativeDivisorClasses*.lean),
not as one re-exported statement.
Lemma 3.5 (lem-SameStrand). Section 3.
"On a banana graph B_{n_0,…,n_g} if r(v_{α,i}+v_{β,j}-v_{γ,k}) = 0, then one of: 1) v_{α,i}=v_{γ,k}; 2) v_{β,j}=v_{γ,k}; 3) the bar of v_{α,i} equals v_{β,j}; 4) v_{α,i},v_{β,j},v_{γ,k} all on the same strand."
Corrected. The paper's coordinate-pair parentheticals for 1), 2), 4)
(e.g. "i.e. (α,i)=(γ,k)") are false at the two shared endpoints, where
distinct strand labels name the same physical vertex
(Bananas/FORMALIZATION_NOTES.md). The Lean statement below uses physical vertex
equality and VerticesOnCommonBananaStrand instead.
Corollary 3.6 (cor-allSubmodSameStrand), full endpoint-safe
classification. Section 3.
"Given a theta graph (G,v_{α,i},v_{β,j}) every divisor is submodular if and only if either 1) α ≠ β, or 2) α = β and (i,j) ∈ {(0,n_α-1),(0,n_α)} or (i,j) = (1,n_α) up to reordering."
Corrected then exact: clause 1) "α ≠ β" is not itself an invariant condition
(a multivalent vertex lies on every strand), so it is replaced by the
endpoint-safe ThetaAllSubmodularCoordinates
(Bananas/Theta/ThetaBoundarySubmodularity.lean).
Proposition 3.7 (labeled rem-degenerateTheta in the source, but a
\begin{prop}), distinct-loop clause. Section 3.
"On a chain of two loops, every divisor is submodular if and only if the marked points are on distinct loops or if n_α = 2 and {u,v}={v_{α,0},v_{α,1}}."
This is the distinct-loop direction; the two same-loop iff's
(chainTwoLoops_allSubmodular_same_left_arbitrary_iff /
..._same_right_arbitrary_iff) are in Bananas/Transmission/ChainTwoLoopsSameLeft.lean /
Bananas/Transmission/ChainTwoLoopsSameRight.lean, not re-wrapped here.
Corollary 3.8 (cor:suppUV), general genus. Section 3.
"If u,v are vertices on B_{n_0,…,n_g} that do not lie on the same strand, then Supp(u+v) = {u,v}."
Theorem 3.9 (thm-NSMForBanana), corrected and complete. Section 3.
"Let (G,u,v) = (B_{n_0,…,n_g},v_{α,i},v_{β,j}) be a banana graph of genus g ≥ 3. Then either: 1a) α=β and, up to swapping u,v, (i,j) ∈ {(0,n_α),(1,n_α),(0,n_α-1)}; 1b) α≠β and, up to reversing each strand, (i,j)=(1,n_β-1); or 2) there exist divisors D with Δ(D) < 0."
Formalization note. The checked statement includes the additional length-two midpoint family as
NSMForBananaLengthTwoCrossException and uses equality of represented vertices at shared endpoints
rather than equality of strand labels; see Bananas/FORMALIZATION_NOTES.md.
Section 4 — k-General Transmission in Banana Graphs #
Remark 4.1 (rem-PermInvol) — invariance under swapping the marked
points. Section 4.
"A natural question ... is whether it depends [on] the order of the pair of marked vertices. ... Thus permuting the marked vertices merely permutes the set of transmission permutations, so k-general transmission is invariant under such a swap."
Lemma 4.2 (lem:kgtImpliesTorsionOrder). Section 4.
"If (G,u,v) is a twice-marked graph with k-general transmission, then k is the torsion order of (G,u,v)."
Exact, with three explicit hypotheses beyond the paper's statement that are
genuine gaps in a literal reading (connectivity, positive genus, and mark
distinctness — see the docstring of KGeneralTransmission.isTorsionOrder,
Bananas/Transmission/TorsionOrderExact.lean).
Lemma 4.3 (lem-TO2GenTrans). Section 4.
"If (G,u,v) has torsion order 2 and every divisor is submodular then G has 2-general transmission."
Exact; connectivity is the only requirement beyond the paper statement.
Proposition 4.5 (prop-thetaTransChar), the complete five-case
table. Section 4.
"Let (G,u,v) be a rigidly marked theta graph. Let D be any degree 2 divisor. For t ∈ ℤ, define D'_t = D+t(u-v). Then τ_D(t) is t-2, t-1, t+1, t+2, or t according to five explicit linear-equivalence cases."
Exact, stated rowwise as implications; mutual exclusivity of the five cases is not needed and so is not separately proved.
Lemma 4.7 (lem:nonrecDisjoint). Section 4.
"If G has genus 2 and [D] ∈ Pic^0(G), then [D] is non-recurrent if and only if the sets {Supp(K_G-nD) : n ∈ ℤ, nD ≁ 0} are pairwise disjoint."
Theorem 4.8 (thm:kgtThetas), theta case. Section 4.
"Suppose (G,u,v) is a rigidly marked graph of genus 2 and torsion order k. Then (G,u,v) has k-general transmission if and only if [u-v] ∈ Pic^0(G) is non-recurrent."
Exact. Also proved for every nontrivial bridgeless genus-two graph as
bridgeless_genusTwo_rigid_kGeneral_iff_nonRecurrent
(Bananas/Classification/BridgelessGenusTwoCornerAlgebra.lean). "Rigidly marked" is
unbundled, as in Definition 4.4.
Lemma 4.10 (lem:invtau), theta form, in full. Section 4.
"Suppose D is submodular on a twice-marked graph (G,u,v) of genus 2. Then inv_k(τ_D) = #{[D'] ∈ T^1_D : |D'| ≠ ∅} + δ(0 ∈ T^0_D and u+v ∼ K_G)."
Exact (including the correction term). Also proved for every nontrivial
bridgeless genus-two graph as bridgeless_genusTwo_invTau_formula
(Bananas/Classification/BridgelessGenusTwoCornerAlgebra.lean). The route differs from the
paper's infinite inclusion–exclusion: three genus-two corner-sum slices,
telescoped.
Lemma 4.12 (lem:invtauGeneral), equivalent finite-period form.
Section 4.
"Let D,E be divisors on (G,u,v) of any genus with torsion order k, D submodular. Then inv_k(τ_D) = S_D(K_G) - S_D(K_G-u) - S_D(K_G-v) + S_D(K_G-u-v)."
Corrected/equivalent: valid in every genus as claimed, but expressed as a
finite sum of complementary ranks over one fundamental period rather than
the four-term S_D alternating sum (which recovers exactly by expanding
rankDelta_eq_rankPlusOne_inclusionExclusion). The extraneous variable E
in the paper's own statement is unused there too.
Theorem 4.13 (thm:g2general), bundled single-theorem form.
Section 4.
The characterization predicate packages the theta branch (case 3, via a
certified isomorphism to a Banana 2 presentation with the marks located
at explicit strand coordinates) and the wedge branch (cases 1 and 2, via a
certified isomorphism to a vertex wedge of two PointedGenusOneRigid
factors) as a disjunction; see BridgelessGenusTwoKGeneralCharacterization
in Bananas/Classification/BridgelessGenusTwoClassification.lean.
Theorem 4.13 (thm:g2general), theta branch (case 3). Section 4.
Theorem 4.13 (thm:g2general), wedge branch (cases 1 and 2),
stated intrinsically on the vertex wedge of two PointedGenusOneRigid
factors rather than the paper's literal TwoPathCycle wording. Section 4.
Lemma 4.15 (unlabeled, TeX line 1911), annihilation half. Section 4.
"If (θ_{n_0,n_1,n_2},v_{α,i},v_{β,j}) is evenly marked, then the class [v_{α,i}-v_{β,j}] is non-recurrent, with order n_α/gcd(n_α,i) = n_β/gcd(n_β,j) in Jac(θ_{n_0,n_1,n_2})."
Lemma 4.15 (unlabeled), exact-order half. Section 4.
Lemma 4.15 (unlabeled), period-equality half n_α/gcd(n_α,i) = n_β/gcd(n_β,j). Section 4.
Lemma 4.15 (unlabeled), non-recurrence half. Section 4.
Corollary 4.17 (cor:evenlyMarkedKGT). Section 4. Same content as
Theorem 1.12, part 2).
"An evenly marked theta graph (θ_{n_0,n_1,n_2},v_{α,i},v_{β,j}) has k-general transmission, where k = n_α/gcd(n_α,i) = n_β/gcd(n_β,j)."
Exact, unconditional.
Theorem 4.18, endpoint regime. Section 4.
Theorem 4.18, same-strand one-off regime. Section 4.
Theorem 4.18, corrected cross-one-off regime. Section 4.
Strengthened. The paper's marking-independent "sufficiently long"
hypothesis on the second strand (hBetaLong in the earlier formal
statement) is no longer needed: CrossOneOffLongEnough already forces
B.length alpha ≥ g + 1 ≥ 4 > 2, and the closed-form period-separation
theorem crossOneOff_cutoff_le_torsionOrder_of_not_both_two
(Bananas/CrossOneOff/CrossOneOffShortStrandPeriod.lean) supplies the needed torsion
bound for every pair of marked strand lengths outside n_alpha = n_beta = 2, which this length threshold already excludes. Only the harmless
hBeta : 1 < B.length beta hypothesis (implied for free by the old
hBetaLong) is now stated explicitly.
Proposition 4.19 (prop-bananTorsion), full corrected dichotomy.
Section 4.
"If (G,u,v) is a twice-marked banana graph of genus ≥ 3 and torsion order k where every divisor is submodular then either: 1) up to reordering, n_0=n_1=2 and (G,u,v)=(G,v_{0,1},v_{1,1}), so k=2; or 2) the torsion order is at least the genus, k ≥ g."
Formalization note. The checked exception family includes distinct-strand midpoints when at
least one supporting strand has length two. This is expressed by CorrectedMidpointException. The
length-two branch now follows from the stronger revised Lemma 4.33 (lem-midpointTorsion); see
Bananas/FORMALIZATION_NOTES.md.
Lemma 4.20 (lem-TriangleInversionII), period consequence. Section
4.
"With (G,u,v)=(B,v_{0,0},v_{0,n_0}), D=gv_{0,n_0}, τ=τ_D, for 0 ≤ b ≤ g we have τ(b)=g-b. As a consequence this yields k ≥ g."
Exact, and strictly stronger than printed: Lean proves g < k. (The
transmission-block statement itself is
exists_endpoint_transmission_block, Bananas/SameStrand/EndpointBlock.lean.)
Proposition 4.21 (prop-TriangleInversionNumber). Section 4.
"With (G,u,v) as above, we have M ≥ C(g+1,2)."
Remark 4.22 (unlabeled) — completing the genus-2 picture. Section 4.
"As a consequence this entirely completes the picture for describing k-general transmission in genus 2 ... By the above proposition, M ≥ 3, ruling out k-general transmission in such cases as well."
Exact, and stronger: proved for every g ≥ 2 and every k,
unconditionally. This is exactly what discharges the case deferred from
Theorem 4.13's theta branch.
Lemma 4.23 (lem-BananOneOff), the uniform three-row block.
Section 4.
"Let (G,u,v)=(G,v_{0,0},v_{0,n_0-1}), D=gv_{0,n_0}, τ=τ_D. If 0 ≤ b ≤ (n_0/(n_0-1))g then τ(b) is one of three residue-determined formulas. As a consequence, k > (n_0/(n_0-1))g."
Exact, in exact integral form (crossOneOffCutoff) rather than the
paper's rational cutoff; b=0 is handled separately
(transmission_oneOff_zero). The period consequence is
oneOff_affine_period_gt_cutoff, Bananas/CrossOneOff/OneOffPeriodBound.lean.
Proposition 4.25 (prop-oneOffNotGeneral), simplified equivalent
form. Section 4.
"With h(g) = f(g)(n_0-2) + min{n_0-2, f(n_0 g) - n_0 f(g)}, M ≥ C(f(g)+1,2) + f(g)h(g) + C(h(g),2)."
Exact, in an equivalent simplified form: writing f = ⌊g/(n_α-1)⌋, the
paper's four-family count is exactly choose(g,2) + f. Its KGT corollary
(oneOff_not_kGeneral_of_four_le_genus) rules out the marking for every
g ≥ 4.
Lemma 4.27 (lem-bothOffTorOrder), near-opposite interior family.
Section 4.
"The torsion order k of (G,v_{0,1},v_{1,n_1-1}) is at least g unless n_0=n_1=2, in which case k=2."
Corrected (same correction as Proposition 4.19): the exceptional branch
is CorrectedMidpointException ∧ k = 2 rather than the paper's literal
n_0=n_1=2 — for this specific marking the two agree, since zero rise does
force both strands to length two (zero_rise_cross_oneOff_forces_both_length_two).
Lemma 4.28 (lem-topOffBottomOffSimple), long-strand
specialization. Section 4.
"For max{2,g+2-n_0} ≤ b ≤ min{g-1,n_1-2} and D=gv_{0,n_0} we have τ_D(b)=g-b+2."
Partial/restricted: proved for the long-strand specialization
2 ≤ b ≤ g-1 under CrossOneOffLongEnough rather than the paper's general
two-sided range, which is subsumed by the corrected Lemma 4.30 block
below.
Corollary 4.29 (cor-bothOffMin). Section 4.
"If min{n_0,n_1} ≥ g+1, then M ≥ C(g-2,2)."
Exact count, with two hypotheses the paper does not state explicitly:
hSeparate : g ≤ k (the period-separation supplied in applications by
crossOneOff_kGeneral_period_ge_genus) and CrossOneOffLongEnough
replacing "min(n_0,n_1) ≥ g+1".
Lemma 4.30 (lem-topOffBottomOff), the corrected uniform block.
Section 4.
"If D=gv_{0,n_0}, τ=τ_D then three residue-indexed cases give τ(b) as b/n_1+1, g+(b+1)/n_1, or g+2⌊b/n_1⌋-b+2 according to b mod n_1."
Formalization note. The checked block starts at b = 2, uses a single positive-remainder
convention, and includes the +2 term in the positive-residue row; see
Bananas/FORMALIZATION_NOTES.md.
Corollary 4.31 (cor-bothOffMax). Section 4.
"When n_0 is sufficiently large relative to the genus, then we get a lower bound on M which is quadratic in g."
Formalization note. The checked target correctedCrossOneOffForcedCount separates the n = 2
and n ≥ 3 branches, and CrossOneOffLongEnough makes the length threshold explicit.
The generic affine-transmission-existence lemma
(exists_affine_transmission_of_allSubmodular,
Bananas/Transmission/TransmissionAPI.lean) supplies only that existence, not this
quadratic count, so the theorem below (from
Bananas/CrossOneOff/CrossOneOffCorrectedInversion.lean) is the one to cite.
The required period-separation inequality is derived from the torsion order, outside the midpoint
family n_alpha = n_beta = 2 already excluded by CrossOneOffLongEnough, using
crossOneOff_corrected_inversion_lower_bound_of_not_both_two
(Bananas/CrossOneOff/CrossOneOffCorrectedInversion.lean, via
crossOneOff_cutoff_le_torsionOrder_of_not_both_two,
Bananas/CrossOneOff/CrossOneOffShortStrandPeriod.lean), so it is supplied internally
from the torsion order k instead of being assumed.
Lemma 4.33 (lem-midpointTorsion), even multiples, added in the
revised manuscript. If one mark is the midpoint of a length-two strand and
1 ≤ j < n_beta / 2 on a distinct strand, no positive even k ≤ 2g - 2
annihilates the marked difference. No all-divisor submodularity or exactness
of the proposed period is assumed.
Lemma 4.33 (lem-midpointTorsion), arbitrary small multiples.
Doubling a putative positive period k < g contradicts the even-multiple
assertion, so the torsion order is at least the genus.
Section 5 — Symmetries and Quasi-Symmetries of Transmission Permutations #
Displayed equation eq-RRTauBounds, lower bound. Section 5 preamble.
"b - deg D ≤ τ_D(b) ≤ 2g + b - deg D."
Displayed equation eq-RRTauBounds, upper bound. Section 5 preamble.
Needs connectivity (Riemann's inequality); the lower bound does not.
Lemma 5.2 (lem:mpIds), part 2). Section 5. Value half only; the
substantive transport half is IsTransmissionPermutation.swap_marks
(Bananas/Transmission/KGeneralSwap.lean).
"If φ is a marked point automorphism of (G,u,v) then: ... 2) τ_D^{v,u}(-a) = -b [is equivalent to 1) τ_D(b)=a]."
Lemma 5.2 (lem:mpIds), part 3). Section 5.
"3) τ_{ι(D)}^{v,u}(a)=b, where ι(D)=K_G-D+u+v."
Stronger than the paper's value form: identifies the whole transmission
permutation of ι(D) at the exchanged marks as rawInverse tau.
Lemma 5.2 (lem:mpIds), part 4). Section 5.
"4) τ_{φ(D)}^{φ(u),φ(v)}(b)=a."
Stronger than the paper's value form (the transported data has literally
the same raw permutation tau), and generalized to an arbitrary
CFGraphIso G H rather than an automorphism, without requiring phi to
preserve the marked set.
Lemma 5.3 (lem-tauSyms), part 1). Section 5.
"Let (G,u,v) be twice-marked, φ a marked point automorphism transposing u,v. 1) If φ(D)+D ∼ K_G+u+v then δ(τ_D(b)=a)=δ(τ_D(a)=b), i.e. (τ_D)² = id."
Faithful: the hypothesis is the equivalent solved form φ(D) ∼ K_G-D+u+v, and the conclusion is the iff form, equivalent to τ²=id given
bijectivity.
Lemma 5.3 (lem-tauSyms), part 2). Section 5. Needs no
connectivity — its proof routes only through Lemma 5.2, parts 1,2,4.
"2) If φ(D)-D ∼ n(u-v) for some n∈ℤ then δ(τ_D(b)=a)=δ(τ_D(n-a)=n-b)."
Proposition 5.5 (unlabeled), the final unlabelled proposition of Section 5. Section 5.
"If φ is a marked point automorphism of (G,u,v) and D such that φ(D)+D ∼ K_G+u+v, then inv_k(τ_D) ≥ ∑_{M∈[k]} [r(D+(M-1)u-Mv) - r(D+(M-2)u-Mv)]."
The self-inverse hypothesis is deliberately refactored to a direct
hypothesis hInvolutive rather than the paper's φ(D)+D∼K_G+u+v — Lemma
5.3(1) supplies it from a marked-point automorphism, so the paper's literal
statement is the (unbundled) composite of that lemma with this one. Two
further hypotheses are made explicit: 0 < k and IsKAffine k tau
(the paper's τ_D ∈ \widetilde{E}a_k).
Section 6 — Chains of mixed torsion orders #
OnceMarkedBrillNoetherGeneral throughout is Definition 1.9, above.
Proposition 6.1 (prop:kgt-bngenl). Section 6.
"If (G,u,v) is a twice-marked graph of genus g with k-general transmission, and k ≥ g/2+1, then G is Brill--Noether general (as an unmarked graph)."
Corrected (natural-number threshold). The paper's real threshold
k ≥ g/2+1 is formalized as g+2 ≤ 2k; the naive g/2+1 ≤ k is too weak
for odd g (Bananas/FORMALIZATION_NOTES.md). Rests on a
crossing-inversion pigeonhole argument, Bananas/CrossOneOff/CrossingInversionCount.lean.
The equal-torsion chain corollary following Proposition 6.1 (unlabeled in the source). Section 6.
"Let (G_i,u_i,v_i), i=1,…,ℓ, ..., and (G,u,v) the iterated vertex gluing. If each (G_i,u_i,v_i) has k-general transmission for the same k, and k ≥ ½(g_1+…+g_ℓ)+1, then G is Brill--Noether general."
Corrected threshold, as in Proposition 6.1. The paper cites [Pfl22, Thm A]
for preservation of k-general transmission under chaining; Lean re-proves
it via the affine reduction developed for Proposition 6.13 instead of
importing it.
Corollary 6.4 (cor:bananasWithKGT). Section 6.
"The only banana graphs of genus ≥ 3 which have k-general transmission are (B_{n_0,…,n_g},v_{α,1},v_{β,1}) with α≠β, n_α=n_β=2; these examples have 2-general transmission."
Corrected, same correction as Proposition 4.19: the exceptional family
only demands the two marks be distinct-strand midpoints with at least one
strand of length two, not literally n_α=n_β=2.
Theorem 6.6 (thm:glueBNGtoKGT). Section 6.
"Let (G_1,u_1,v_1),(G_2,u_2,v_2) be twice-marked graphs of genera g_1,g_2 on which all divisors are submodular, (G,u,v)=(G,u_1,v_2) their vertex gluing. Suppose (G_1,v_1) is Brill--Noether general as a marked graph, and (G_2,u_2,v_2) has k-general transmission with k > g_1+g_2. Then (G,v) is Brill--Noether general."
Exact modulo the added connectedness hypotheses. The paper's Remark 6.7
(that u_1 and the submodularity of (G_1,u_1,v_1) are probably removable)
is not discharged: hGsub and u are still present.
The one-vertex specialization following Theorem 6.6 (unlabeled in the source). Section 6.
"If (G,u,v) is a twice-marked graph of genus g with k-general transmission, and k > g, then (G,v) is a Brill--Noether general once-marked graph."
Exact statement; the proof route differs from a literal specialization of Theorem 6.6 (an identity Demazure factor rather than a genus-0 one-vertex graph model).
Proposition 6.10 (prop:sciLambda). Section 6.
"If D is a submodular divisor on a twice-marked graph (G,u,v), then sci(τ_D) = |λ(D,v)|."
Proposition 6.14 (prop:glueMarked). Section 6.
"If (G_1,v_1),(G_2,v_2) are Brill--Noether general marked graphs of genera g_1,g_2, and G is the genus g_1+g_2 graph gluing v_1 to v_2, then G is Brill--Noether general."
Exact; the genus additivity is genus_vertexWedge, not a hypothesis. The
paper's appeal to [Pfl22, Prop. 3.15] is replaced by the library's exact
wedge rank formula
(VertexWedgeRankFormula.vertexWedge_rank_ge_iff_profile_inequalities).
Remark 6.15 (the max-formula for r(D)) is a remark with no separate
formal counterpart.
Corollary 6.16 (\Cref{thm:bngChain} — this is Theorem 1.13's body
proof, restated), part 1). Section 6.
Same statement and same Lean wrapper as s1_thm1_13a, above. The paper's
displayed definition of the iterated gluing "(G,u,v)=(G,u_1,v_ℓ)" is
self-referential (Bananas/FORMALIZATION_NOTES.md, "Chain theorem notation"; the same
pattern recurs in Corollary 6.3 and Theorem 6.6); Lean uses the intended
left-associated MarkedGraph.chain.
Corollary 6.16 (\Cref{thm:bngChain}), part 2). Section 6. Same
statement and same Lean wrapper as s1_thm1_13b, above, in the paper's full
graph convention (connected genus-zero factors allowed anywhere).
Library-vocabulary wrappers without a standalone counterpart #
The five entries below are stated over the implementation library's own
vocabulary, because their types intrinsically involve implementation
objects: concrete proof-carrying chain factors (Example 1.15), the
bridgeless degree-one class map (Lemma 2.3, part 2), and the affine
symmetric-group permutations AspPerm (Equation 6.11, Lemma 6.12,
Proposition 6.13). They have no counterpart in the statement-only audit
copy and are not part of the Comparator target list.
Example 1.15 (eg:bng). Section 1.
"As an example, we exhibit an explicit genus-8 Brill–Noether general graph using the chain construction: glue the cycle B_{3,1}, the evenly marked theta graph θ_{4,1,4} marked at (x_1,z_1), the cycle B_{3,2}, the evenly marked theta graph θ_{5,2,10} marked at (x_2,z_4), and the evenly marked theta graph θ_{6,2,3} marked at (x_4,z_2)."
Exact, as a concrete five-factor instantiation
(Bananas/Examples/ExampleBngChain.lean). The two cycle factors use
cycle_kGeneralTransmission (Example 1.11); the three theta factors use
evenlyMarkedTheta_kGeneral; the chain conclusion is
brillNoetherGeneral_mixedTorsionChain_of_minBudget. Concrete Banana g
instances are built by bananaOfLengths, a two-vertex core with g + 1
parallel positive-length strands. The five per-factor torsion orders are
4, 4, 5, 5, 3 (Bananas/Examples/ExampleBngChain.lean's bngF1–bngF5), matching
the paper's own per-factor computations rather than its displayed
4, 5, 5, 5, 3 (Bananas/FORMALIZATION_NOTES.md); the discrepancy is immaterial, since
bngChainMinBudget checks the minimum-budget hypothesis directly against
the correct values.
Lemma 2.3 (lem-bridgelessFacts), part 2). Section 2.
"2) There is a bijection between rank 0 divisors in Pic^1(G) and vertices in V(G)."
Corrected: false as printed for the edgeless one-vertex graph (whose
unique degree-one class has rank one), so an explicit nontriviality
hypothesis ∃ p q, p ≠ q is added.
Equation 6.11 (eq:tauGlued, alongside eq:starSigma). Section 6.
"If (G,u,v) is the vertex gluing of (G_1,u_1,v_1) and (G_2,u_2,v_2), D_1 submodular on G_1, D_2 submodular on G_2, then D=D_1+D_2 is submodular on G and τ_D = τ_{D_1} ⋆ τ_{D_2}."
Proved in the inequality (SatisfiesTransmission) formulation rather than
as a literal equality of permutations; the equality form used by Theorem
6.6 is exists_isTransmissionPermutation_wedgeAddDivisor_star. Equation
eq:starSigma ([PflDemProd, Thm 8.7]) is imported from the demazure
dependency as Demazure.Transpositions.starSigma.
Lemma 6.12 (lem-SciSimpleRefl). Section 6.
"Let k ≥ 2, α ∈ Asp with sci(α) ≤ k-2. For any n, sci(α ⋆ σ^k_n) ≤ sci(α)+1."
Slightly more general than the paper: instead of the specific affine
reflection σ^k_n = σ_{n+kℤ}, it takes any non-consecutive support set S
all of whose elements are congruent mod k.
Proposition 6.13 (prop:sciInvStar). Section 6.
"Suppose α ∈ Asp and β ∈ \widetilde{E}a_k satisfy k > sci(α) + inv_k(β). Then sci(α ⋆ β) ≤ sci(α) + inv_k(β)."
Literal match, with the affine Coxeter reduction discharged unconditionally.