Standalone marked-banana statement vocabulary

Marked divisors, transmission permutations, exceptional configurations, and finite counting expressions used by the paper-facing theorem statements.

def TMB.Banana.graph {g : ℕ} (B : Banana g) : CFGraph

Replace every labelled strand by a path of its specified length.

Equations

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

def TMB.Banana.pathVertex {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : B.PathPosition α) : B.Vertex

The vertex at a path position along a strand, measured from the strand's tail.

Equations

• B.pathVertex α i = if hzero : ↑i = 0 then B.coreVertex (B.tail α) else if hlast : ↑i = B.length α then B.coreVertex (B.head α) else B.interiorVertex α ⟨↑i - 1, ⋯⟩

def TMB.Banana.IsInteriorPosition {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : B.PathPosition α) : Prop

Interior positions exclude the two shared endpoints.

Equations

• B.IsInteriorPosition α i = (0 < ↑i ∧ ↑i < B.length α)

def TMB.bananaOfLengths (g : ℕ) (length : Fin (g + 1) → ℕ) (hpos : ∀ (α : Fin (g + 1)), 0 < length α) : Banana g

Construct a banana from positive strand lengths, every strand oriented from 0 to 1.

Equations

• TMB.bananaOfLengths g length hpos = { tail := fun (x : Fin (g + 1)) => 0, head := fun (x : Fin (g + 1)) => 1, length := length, core_loopless := ⋯, length_pos := hpos }

def TMB.strandVertex {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : B.PathPosition α) : B.graph.V

The vertex v_{α,i} at normalized position i along strand α, measured from multivalent vertex 0; the stored orientation of the strand is reversed when necessary.

Equations

• TMB.strandVertex B α i = B.pathVertex α (if B.tail α = 0 then i else ⟨B.length α - ↑i, ⋯⟩)

def TMB.strandMirror {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : B.PathPosition α) : B.PathPosition α

Reflection of a strand coordinate.

Equations

• TMB.strandMirror B α i = ⟨B.length α - ↑i, ⋯⟩

def TMB.leftEndpoint {g : ℕ} (B : Banana g) : B.graph.V

The two multivalent vertices.

Equations

• TMB.leftEndpoint B = B.coreVertex 0

def TMB.rightEndpoint {g : ℕ} (B : Banana g) : B.graph.V

The multivalent banana endpoint corresponding to core pole 1.

Equations

• TMB.rightEndpoint B = B.coreVertex 1

def TMB.TwoPathCycle.spec (length : Fin 2 → ℕ) (hLength : ∀ (edge : Fin 2), 0 < length edge) : Banana 1

A two-path cycle is the genus-one banana with the prescribed lengths.

Equations

• TMB.TwoPathCycle.spec length hLength = { tail := fun (x : Fin (1 + 1)) => 0, head := fun (x : Fin (1 + 1)) => 1, length := length, core_loopless := ⋯, length_pos := hLength }

Twice-marked graphs and transmission

structure TMB.TwiceMarked : Type 1

A graph with two ordered marked vertices.

• graph : CFGraph

  The underlying graph carrying the two ordered marks used for rank differences and transmission.

• u : self.graph.V

  The first marked vertex, used for the first one-chip subtraction in the rank difference.

• v : self.graph.V

  The second marked vertex, used for the second one-chip subtraction in the rank difference.

@[reducible, inline]

abbrev TMB.mark (G : CFGraph) (u v : G.V) : TwiceMarked

Mark two vertices.

Equations

• TMB.mark G u v = { graph := G, u := u, v := v }

noncomputable def TMB.rankDelta (M : TwiceMarked) (D : CFDiv M.graph) : ℤ

The marked second difference of divisor rank.

Equations

• TMB.rankDelta M D = TMB.rank M.graph D - TMB.rank M.graph (D - TMB.oneChip M.u) - TMB.rank M.graph (D - TMB.oneChip M.v) + TMB.rank M.graph (D - TMB.oneChip M.u - TMB.oneChip M.v)

def TMB.twist (M : TwiceMarked) (D : CFDiv M.graph) (a b : ℤ) : CFDiv M.graph

A two-point twist of a divisor.

Equations

• TMB.twist M D a b = D + a • TMB.oneChip M.u + b • TMB.oneChip M.v

def TMB.Submodular (M : TwiceMarked) (D : CFDiv M.graph) : Prop

Submodularity of every marked twist.

Equations

• TMB.Submodular M D = ∀ (a b : ℤ), 0 ≤ TMB.rankDelta M (TMB.twist M D a b)

def TMB.AllSubmodular (M : TwiceMarked) : Prop

Every divisor is submodular.

Equations

• TMB.AllSubmodular M = ∀ (D : TMB.CFDiv M.graph), TMB.Submodular M D

def TMB.TorsionWitness (M : TwiceMarked) (k : ℕ) : Prop

A positive multiple killing the marked difference.

Equations

• TMB.TorsionWitness M k = (0 < k ∧ TMB.linearEquiv M.graph (↑k • (TMB.oneChip M.u - TMB.oneChip M.v)) 0)

def TMB.IsTorsionOrder (M : TwiceMarked) (k : ℕ) : Prop

The least positive torsion witness.

Equations

• TMB.IsTorsionOrder M k = (TMB.TorsionWitness M k ∧ ∀ (m : ℕ), TMB.TorsionWitness M m → k ≤ m)

def TMB.IsTransmissionPermutation (M : TwiceMarked) (D : CFDiv M.graph) (τ : ℤ → ℤ) : Prop

Rank-difference characterization of a transmission permutation.

Equations

• TMB.IsTransmissionPermutation M D τ = (Function.Bijective τ ∧ ∀ (a b : ℤ), (if τ b = a then 1 else 0) = TMB.rankDelta M (D + a • TMB.oneChip M.u - b • TMB.oneChip M.v))

def TMB.IsKAffine (k : ℕ) (τ : ℤ → ℤ) : Prop

Period-k affine permutations.

Equations

• TMB.IsKAffine k τ = ∀ (n : ℤ), τ (n + ↑k) = τ n + ↑k

def TMB.kInversions (k : ℕ) (τ : ℤ → ℤ) : Set (ℤ × ℤ)

Fundamental-domain representatives of affine inversions.

Equations

• TMB.kInversions k τ = {p : ℤ × ℤ | p.1 < p.2 ∧ τ p.1 > τ p.2 ∧ 0 ≤ p.1 ∧ p.1 < ↑k}

noncomputable def TMB.kInversionCount (k : ℕ) (τ : ℤ → ℤ) : ℕ

Number of affine inversions.

Equations

• TMB.kInversionCount k τ = (TMB.kInversions k τ).ncard

def TMB.KGeneralTransmission (M : TwiceMarked) (k : ℕ) : Prop

k-general transmission.

Equations

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

def TMB.BrillNoetherGeneral (G : CFGraph) : Prop

Brill--Noether generality in the nonexistence direction.

Equations

• TMB.BrillNoetherGeneral G = ∀ (r d : ℤ), 0 ≤ r → TMB.BNExists G r d → 0 ≤ TMB.bnNumber G r d

def TMB.thetaExceptionalPositions {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i j : B.PathPosition α) : Set (B.PathPosition α)

The exceptional same-strand position set from Theorem 3.4.

Equations

• TMB.thetaExceptionalPositions B α i j = {q : B.PathPosition α | ↑↑q ≠ ↑(B.length α) - ↑↑i ∧ ↑↑q ≠ ↑↑j ∧ ↑↑j - ↑↑i ≤ ↑↑q ∧ ↑↑q ≤ ↑↑j - ↑↑i + ↑(B.length α)}

def TMB.EvenlyMarkedTheta (B : Banana 2) (α β : Fin 3) (i : B.PathPosition α) (j : B.PathPosition β) : Prop

Even marking on two distinct theta strands, by cross multiplication.

Equations

• TMB.EvenlyMarkedTheta B α β i j = (α ≠ β ∧ 0 < ↑i ∧ ↑i < B.length α ∧ 0 < ↑j ∧ ↑j < B.length β ∧ ↑i * B.length β = ↑j * B.length α)

Chains of factors

structure TMB.KGeneralChainFactor : Type 1

One factor in a mixed-torsion chain.

• marked : MarkedGraph

  The connected marked graph forming this factor of the mixed-torsion chain.

• period : ℕ

  The period parameter for the factor's certified general transmission property.

• connected : graphConnected self.marked.graph
• kGeneral : KGeneralTransmission (mark self.marked.graph self.marked.left self.marked.right) self.period

def TMB.ChainPrefixBudget : ℤ → List KGeneralChainFactor → Prop

Prefix-genus period inequalities.

Equations

• TMB.ChainPrefixBudget x✝ [] = True
• TMB.ChainPrefixBudget x✝ (F :: rest) = (x✝ + TMB.genus F.marked.graph < ↑F.period ∧ TMB.ChainPrefixBudget (x✝ + TMB.genus F.marked.graph) rest)

def TMB.chainFactorGenus (L : List KGeneralChainFactor) : ℤ

Total genus of a list of chain factors.

Equations

• TMB.chainFactorGenus L = (List.map (fun (F : TMB.KGeneralChainFactor) => TMB.genus F.marked.graph) L).sum

def TMB.ChainMinBudget (L : List KGeneralChainFactor) : Prop

Sharp two-sided torsion budget for a chain.

Equations

• TMB.ChainMinBudget L = ∀ (i : ℕ) (hi : i < L.length), min (TMB.chainFactorGenus (List.take (i + 1) L)) (TMB.chainFactorGenus (List.drop i L)) < ↑(L.get ⟨i, hi⟩).period

Weierstrass partitions and the once-marked census

def TMB.poleOrderSet (G : CFGraph) (v : G.V) (D : CFDiv G) (i : ℕ) : Set ℤ

Twists at the marked point having rank at least i.

Equations

• TMB.poleOrderSet G v D i = {ell : ℤ | ↑i ≤ TMB.rank G (D + ell • TMB.oneChip v)}

noncomputable def TMB.poleOrder (G : CFGraph) (v : G.V) (D : CFDiv G) (i : ℕ) : ℤ

Pole order s_i(D, v): the least twist of rank at least i.

Equations

• TMB.poleOrder G v D i = sInf (TMB.poleOrderSet G v D i)

noncomputable def TMB.weierstrassPartInt (G : CFGraph) (v : G.V) (D : CFDiv G) (i : ℕ) : ℤ

The ith Weierstrass part i + g - deg D - s_i(D, v), over ℤ.

Equations

• TMB.weierstrassPartInt G v D i = ↑i + TMB.genus G - TMB.deg D - TMB.poleOrder G v D i

noncomputable def TMB.weierstrassPart (G : CFGraph) (v : G.V) (D : CFDiv G) (i : ℕ) : ℕ

The ith Weierstrass part as a natural number.

Equations

• TMB.weierstrassPart G v D i = (TMB.weierstrassPartInt G v D i).toNat

noncomputable def TMB.weierstrassSize {G : CFGraph} (_hconn : graphConnected G) (v : G.V) (D : CFDiv G) : ℕ

Size |λ(D, v)| of the Weierstrass partition: the sum of its parts. On a connected graph only the first g parts can be nonzero, so the sum is taken over those.

Equations

• TMB.weierstrassSize _hconn v D = ∑ i ∈ Finset.range (TMB.genus G).toNat, TMB.weierstrassPart G v D i

def TMB.onceMarkedPart (lambda : YoungDiagram) (i : ℕ) : ℕ

The ith part of a Young diagram, extended by zero.

Equations

• TMB.onceMarkedPart lambda i = lambda.rowLens.getD i 0

def TMB.OnceMarkedCensusContains (G : CFGraph) (v : G.V) (lambda : YoungDiagram) : Prop

Membership of a partition in the divisor census of a once-marked graph: some divisor has λ_i(D, v) ≥ λ_i for every i, written as the rank test r(D + (i + g - deg D - λ_i) v) ≥ i.

Equations

• TMB.OnceMarkedCensusContains G v lambda = ∃ (D : TMB.CFDiv G), ∀ (i : ℕ), TMB.rank G (D + (↑i + TMB.genus G - TMB.deg D - ↑(TMB.onceMarkedPart lambda i)) • TMB.oneChip v) ≥ ↑i

def TMB.OnceMarkedBrillNoetherGeneral (G : CFGraph) (v : G.V) : Prop

Once-marked Brill--Noether generality: every partition in the divisor census has size at most the genus.

Equations

• TMB.OnceMarkedBrillNoetherGeneral G v = ∀ (lambda : YoungDiagram), TMB.OnceMarkedCensusContains G v lambda → ↑lambda.card ≤ TMB.genus G

Support complexes and rank determining sets

def TMB.rankSupport (G : CFGraph) (D : CFDiv G) : Set G.V

Support on which deleting one chip leaves nonnegative rank.

Equations

• TMB.rankSupport G D = {x : G.V | 0 ≤ TMB.rank G (D - TMB.oneChip x)}

def TMB.DivisorSupportedOn {G : CFGraph} (A : Set G.V) (E : CFDiv G) : Prop

A divisor is supported on A.

Equations

• TMB.DivisorSupportedOn A E = ∀ (x : G.V), E x ≠ 0 → x ∈ A

def TMB.restrictedRankGeq (G : CFGraph) (A : Set G.V) (D : CFDiv G) (r : ℤ) : Prop

Restricted rank lower bound.

Equations

• TMB.restrictedRankGeq G A D r = ∀ (E : TMB.CFDiv G), TMB.effective E → TMB.deg E = r → TMB.DivisorSupportedOn A E → TMB.winnable G (D - E)

def TMB.RankDetermining (G : CFGraph) (A : Set G.V) : Prop

A set tests every divisor-rank lower bound.

Equations

• TMB.RankDetermining G A = ∀ (D : TMB.CFDiv G) (r : ℤ), TMB.restrictedRankGeq G A D r ↔ TMB.rankGeq G D r

Banana normal forms and exceptional families

def TMB.semibreakDivisor {g : ℕ} (B : Banana g) (chips : (α : Fin (g + 1)) → Option (Fin (B.length α - 1))) : CFDiv B.graph

A semibreak divisor has at most one chosen interior chip per strand.

Equations

• TMB.semibreakDivisor B chips (Sum.inl val) = 0
• TMB.semibreakDivisor B chips (Sum.inr ⟨α, offset⟩) = if chips α = some offset then 1 else 0

def TMB.IsSemibreak {g : ℕ} (B : Banana g) (E : CFDiv B.graph) : Prop

Membership in the semibreak family.

Equations

• TMB.IsSemibreak B E = ∃ (chips : (α : Fin (g + 1)) → Option (Fin (B.length α - 1))), E = TMB.semibreakDivisor B chips

def TMB.bananaNormalForm {g : ℕ} (B : Banana g) (a b : ℤ) (E : CFDiv B.graph) : CFDiv B.graph

Endpoint/semibreak normal form.

Equations

• TMB.bananaNormalForm B a b E = a • TMB.oneChip (TMB.leftEndpoint B) + b • TMB.oneChip (TMB.rightEndpoint B) + E

def TMB.endpointPencilDivisor {g : ℕ} (B : Banana g) : CFDiv B.graph

The endpoint hyperelliptic pencil.

Equations

• TMB.endpointPencilDivisor B = TMB.oneChip (TMB.leftEndpoint B) + TMB.oneChip (TMB.rightEndpoint B)

def TMB.FarFromBananaEndpoints {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : B.PathPosition α) : Prop

A position at distance at least two from both endpoints.

Equations

• TMB.FarFromBananaEndpoints B α i = (2 ≤ ↑i ∧ ↑i + 2 ≤ B.length α)

def TMB.CorrectedBananaSimpleException {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (i : B.PathPosition α) (j : B.PathPosition β) : Prop

Corrected exceptional family for Theorem 1.16.

Equations

• TMB.CorrectedBananaSimpleException B α β i j = (α ≠ β ∧ B.length β = 2 ∧ ↑j = 1 ∨ α ≠ β ∧ B.length α = 2 ∧ ↑i = 1)

def TMB.CorrectedMidpointException {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (i : B.PathPosition α) (j : B.PathPosition β) : Prop

Corrected midpoint exception in high genus.

Equations

• TMB.CorrectedMidpointException B α β i j = (α ≠ β ∧ 2 * ↑i = B.length α ∧ 2 * ↑j = B.length β ∧ (B.length α = 2 ∨ B.length β = 2))

def TMB.VertexOnBananaStrand {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (x : B.graph.V) : Prop

A vertex lies on a normalized banana strand.

Equations

• TMB.VertexOnBananaStrand B α x = ∃ (i : B.PathPosition α), x = TMB.strandVertex B α i

def TMB.VerticesOnCommonBananaStrand {g : ℕ} (B : Banana g) (x y z : B.graph.V) : Prop

Three vertices lie on one common strand.

Equations

• TMB.VerticesOnCommonBananaStrand B x y z = ∃ (α : Fin (g + 1)), TMB.VertexOnBananaStrand B α x ∧ TMB.VertexOnBananaStrand B α y ∧ TMB.VertexOnBananaStrand B α z

def TMB.NSMForBananaInteriorException {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (i : B.PathPosition α) (j : B.PathPosition β) : Prop

The corrected cross-strand exceptional coordinates of Theorem 3.9 for two strictly interior marks.

Equations

• TMB.NSMForBananaInteriorException B α β i j = (α ≠ β ∧ (↑i = 1 ∧ ↑j + 1 = B.length β ∨ ↑i + 1 = B.length α ∧ ↑j = 1 ∨ B.length α = 2 ∧ ↑i = 1 ∨ B.length β = 2 ∧ ↑j = 1))

def TMB.NSMForBananaException {g : ℕ} (B : Banana g) (u v : B.graph.V) : Prop

Endpoint-safe exceptional alternatives in corrected Theorem 3.9.

Equations

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

def TMB.ThetaAllSubmodularCoordinates (B : Banana 2) (α β : Fin 3) (i : B.PathPosition α) (j : B.PathPosition β) : Prop

Coordinate alternatives for all-submodular theta markings.

Equations

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

def TMB.ThetaTransmissionSubTwoCase (B : Banana 2) (u : B.graph.V) (X : CFDiv B.graph) : Prop

The four exceptional transmission rows in genus two.

Equations

• TMB.ThetaTransmissionSubTwoCase B u X = TMB.linearEquiv B.graph X (2 • TMB.oneChip u)

def TMB.ThetaTransmissionSubOneCase (B : Banana 2) (u v : B.graph.V) (X : CFDiv B.graph) : Prop

The theta-graph case where X is equivalent to a chip at u plus a chip at some w, and the degree-zero differences from w to either mark are nonprincipal.

Equations

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

def TMB.ThetaTransmissionAddOneCase (B : Banana 2) (u v : B.graph.V) (X : CFDiv B.graph) : Prop

The theta-graph case where X is equivalent to a chip at v plus a chip at w, and neither marked two-chip divisor with w is canonical.

Equations

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

def TMB.ThetaTransmissionAddTwoCase (B : Banana 2) (u v : B.graph.V) (X : CFDiv B.graph) : Prop

The theta-graph case where X is equivalent to the canonical divisor shifted by a chip from u to v.

Equations

• TMB.ThetaTransmissionAddTwoCase B u v X = TMB.linearEquiv B.graph X (TMB.canonicalDivisor B.graph - TMB.oneChip u + TMB.oneChip v)

def TMB.NonRecurrent (M : TwiceMarked) (k : ℕ) : Prop

Concrete finite-residue nonrecurrence.

Equations

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

def TMB.ThetaKGeneralCoordinates {k : ℕ} (B : Banana 2) (alpha beta : Fin 3) (i : B.PathPosition alpha) (j : B.PathPosition beta) : Prop

The three coordinate families in the theta branch of Theorem 4.13.

Equations

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

def TMB.WedgeKGeneralPlacement (G H : CFGraph) (x : G.V) (y : H.V) (u v : (vertexWedge G H x y).V) (k : ℕ) : Prop

The six ordered placements that can have general transmission on a rigid wedge of two genus-one factors.

Equations

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

def TMB.BridgelessGenusTwoKGeneralCharacterization (G : CFGraph) (u v : G.V) (k : ℕ) : Prop

The isomorphism-invariant theta-or-wedge classification in genus two.

Equations

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

def TMB.CanonicalMarkedSupportsPairwiseDisjoint (M : TwiceMarked) (k : ℕ) : Prop

Pairwise disjointness of the canonical marked supports at the nonzero torsion residues.

Equations

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

noncomputable def TMB.degreeTwistInt (M : TwiceMarked) (D : CFDiv M.graph) (d b : ℤ) : CFDiv M.graph

Degree-d representative at a marked-difference index.

Equations

• TMB.degreeTwistInt M D d b = D + (d - TMB.deg D + b) • TMB.oneChip M.u - b • TMB.oneChip M.v

def TMB.effectiveDegreeOneTwistResidues (M : TwiceMarked) (D : CFDiv M.graph) (k : ℕ) : Set (Fin k)

Effective degree-one torsion residues.

Equations

• TMB.effectiveDegreeOneTwistResidues M D k = {b : Fin k | 0 ≤ TMB.rank M.graph (TMB.degreeTwistInt M D 1 ↑↑b)}

noncomputable def TMB.invTauCorrection (M : TwiceMarked) (D : CFDiv M.graph) : ℤ

Correction term in Lemma 4.10.

Equations

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

def TMB.southeastSet (τ : ℤ → ℤ) (m n : ℤ) : Set ℤ

Southeast and northwest quadrant index sets.

Equations

• TMB.southeastSet τ m n = {k : ℤ | n ≤ k ∧ τ k < m}

def TMB.northwestSet (τ : ℤ → ℤ) (m n : ℤ) : Set ℤ

The northwest quadrant of an integer function at thresholds (m, n): indices below n whose image is at least m.

Equations

• TMB.northwestSet τ m n = {k : ℤ | k < n ∧ m ≤ τ k}

noncomputable def TMB.rawInverse (τ : ℤ → ℤ) : ℤ → ℤ

Set-theoretic inverse of an integer function.

Equations

• TMB.rawInverse τ = Function.invFun τ

def TMB.rawAffineReflection (τ : ℤ → ℤ) : ℤ → ℤ

Conjugation by negation.

Equations

• TMB.rawAffineReflection τ n = -τ (-n)

noncomputable def TMB.swapTransmissionPermutation (τ : ℤ → ℤ) : ℤ → ℤ

Reflected inverse used when swapping marks.

Equations

• TMB.swapTransmissionPermutation τ = TMB.rawAffineReflection (TMB.rawInverse τ)

def TMB.transmissionDualDivisor {G : CFGraph} (u v : G.V) (D : CFDiv G) : CFDiv G

Riemann--Roch dual divisor with both marks restored.

Equations

• TMB.transmissionDualDivisor u v D = TMB.canonicalDivisor G - D + TMB.oneChip u + TMB.oneChip v

def TMB.sciSet (τ : ℤ → ℤ) : Set (ℤ × ℤ)

Sign-changing inversions and their number.

Equations

• TMB.sciSet τ = {p : ℤ × ℤ | p.1 < p.2 ∧ 0 < τ p.1 ∧ τ p.2 ≤ 0}

noncomputable def TMB.sci (τ : ℤ → ℤ) : ℕ

The natural cardinality of inversion pairs crossing zero in the images: the earlier image is positive and the later image is nonpositive.

Equations

• TMB.sci τ = (TMB.sciSet τ).ncard

structure TMB.MarkedPointAutomorphism (M : TwiceMarked) : Type

Mark-preserving and mark-swapping graph automorphisms.

• iso : CFGraphIso M.graph M.graph

  The graph automorphism whose vertex bijection preserves the set of the two marked vertices.

• preserves_marked_set (x : M.graph.V) : x = M.u ∨ x = M.v ↔ self.iso.vertexEquiv x = M.u ∨ self.iso.vertexEquiv x = M.v

structure TMB.MarkedPointSwap (M : TwiceMarked) extends TMB.MarkedPointAutomorphism M : Type

A marked-point automorphism that interchanges the two distinguished vertices.

• iso : CFGraphIso M.graph M.graph
• preserves_marked_set (x : M.graph.V) : x = M.u ∨ x = M.v ↔ self.iso.vertexEquiv x = M.u ∨ self.iso.vertexEquiv x = M.v
• map_u : self.iso.vertexEquiv M.u = M.v
• map_v : self.iso.vertexEquiv M.v = M.u

noncomputable def TMB.sectionFiveRankDropSum (M : TwiceMarked) (D : CFDiv M.graph) (k : ℕ) : ℤ

Finite rank-drop sum from Section 5.

Equations

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

def TMB.HasInversionLowerBound (M : TwiceMarked) (k q : ℕ) : Prop

A transmission permutation with a specified inversion lower bound.

Equations

• TMB.HasInversionLowerBound M k q = ∃ (D : TMB.CFDiv M.graph) (τ : ℤ → ℤ), TMB.IsTransmissionPermutation M D τ ∧ TMB.IsKAffine k τ ∧ (TMB.kInversions k τ).Finite ∧ q ≤ TMB.kInversionCount k τ

def TMB.crossOneOffCutoff (g n : ℕ) : ℕ

Arithmetic functions used by the one-off and cross-one-off blocks.

Equations

• TMB.crossOneOffCutoff g n = g + g / (n - 1)

def TMB.CrossOneOffLongEnough (g n₀ n₁ : ℕ) : Prop

The cross one-off length condition requiring n₀ to be at least g + 1 + g / (n₁ - 1), with natural-number division.

Equations

• TMB.CrossOneOffLongEnough g n₀ n₁ = (g + 1 + g / (n₁ - 1) ≤ n₀)

def TMB.oneOffRow (g n b : ℕ) : ℕ

The one-off row value at index b, computed separately for residues zero, n - 1, and all remaining residues modulo n.

Equations

• TMB.oneOffRow g n b = if b % n = 0 then b / n else if b % n = n - 1 then g + b / n + 1 else g + 2 * (b / n) + 1 - b

def TMB.crossOneOffRow (g n b : ℕ) : ℕ

The cross one-off row value at index b, with its extra unit in the zero-residue and interior-residue cases.

Equations

• TMB.crossOneOffRow g n b = if b % n = 0 then b / n + 1 else if b % n = n - 1 then g + b / n + 1 else g + 2 * (b / n) + 2 - b

def TMB.correctedCrossOneOffForcedCount (g n : ℕ) : ℕ

The corrected forced-count formula: choose g 2 at period two, and choose (g - 1) 2 + g / (n - 1) otherwise.

Equations

• TMB.correctedCrossOneOffForcedCount g n = if n = 2 then g.choose 2 else (g - 1).choose 2 + g / (n - 1)