The exact genus-two inversion formula, with its correction term #
ThetaGenusTwoCornerSum.lean reduces inv_k(τ_D) to three finite degree
slices and then evaluates them under the rigidity hypothesis u + v ≁ K_G,
which makes the residual degree-two product vanish pointwise. This file
evaluates that residual product instead of discarding it, and so proves the
paper's Lemma 4.10 (lem:invtau) as stated:
inv_k(τ_D) = # {[D'] ∈ T¹_D : |D'| ≠ ∅} + δ(0 ∈ T⁰_D and u + v ∼ K_G).
The correction term is invTauCorrection. Two facts pin it down: each
factor of the residual product is the principality indicator of a
degree-zero divisor, and exact torsion makes at most one residue in a
fundamental period principal. The upshot is that the whole cyclic sum of
residual products is 0 or 1, and is 1 exactly under the paper's
conjunction.
The converse half of thm:kgtThetas (Theorem 4.8) is then immediate: apply
the formula to D = w for a vertex w and read the bound inv_k ≤ g = 2
backwards.
Generic divisor bookkeeping #
Everything in this section is stated for an abstract {G : CFGraph} with
abstract divisors, so that no downstream use has to run divisor algebra on a
concrete banana.
fixedDegreeTwist and degreeTwistInt are the same twist family, the
former carrying its marks as separate arguments.
The degree-two twist is the next degree-zero twist with both marks added back.
A degree twist may be replaced by its Euclidean residue index modulo any torsion witness.
Principality of a degree twist depends only on the index modulo a torsion witness.
Every twist D + a·u - b·v of degree d is the degree-d twist family
member at index b. Together with the next lemma and
degreeTwistInt_injective_on_fundamental_period this says that the finite
family degreeTwistInt M D d · on Fin k is a system of representatives for
the paper's set T^d_D of degree-d twist classes.
Every degree-d twist index is represented in one fundamental period.
With A principal, the canonical complement of A + u + v is principal
exactly when the marked pair is canonical. This is the pointwise content of
the paper's correction term.
A product of two degree-zero multiplicities is one when both divisors are principal and zero otherwise.
If either factor of a degree-zero multiplicity product is nonprincipal, the product vanishes.
The correction term #
Paper source: the second summand of lem:invtau (Lemma 4.10),
δ(0 ∈ T⁰_D and u + v ∼ K_G).
0 ∈ T⁰_D says some degree-zero twist of D is principal; the second
conjunct is the failure of the paper's rigidity condition (in genus two,
r(u+v) = 0 is equivalent to u + v ≁ K_G).
Equations
- One or more equations did not get rendered due to their size.
Instances For
rfl-wrapper: the correction term at an explicitly marked graph, stated
without the TwiceMarked projections so that rw fires on it.
Rigid markings have no correction.
The canonical complement of a degree-two twist has degree zero.
Two principal degree-zero twists in one fundamental period, at indices shifted by one, have the same index.
The residual degree-two products of the genus-two telescoping sum add up to exactly the paper's correction term.
Paper source: lem:invtau (Lemma 4.10), in full, with its correction
term.
For a theta graph with any two marks, an exact torsion order k and any
divisor D admitting a k-affine transmission permutation, the number of
k-inversions is the number of effective degree-one twists of D in one
torsion period, plus δ(0 ∈ T⁰_D and u + v ∼ K_G).
The converse half of Theorem 4.8 #
The effective degree-one twists of a single chip are exactly the non-recurrence indices.
Paper source: thm:kgtThetas (Theorem 4.8), the "only if" direction.
For a rigidly marked theta graph, k-general transmission forces the marked
difference class to be non-recurrent. The proof is the paper's: apply the
exact formula of Lemma 4.10 to D = w for each vertex w, note that the
zero residue is always effective, and read the inversion bound inv_k ≤ 2
backwards.
Paper source: thm:kgtThetas (Theorem 4.8), both directions.
A rigidly marked theta graph of exact torsion order k has k-general
transmission if and only if the marked difference class is non-recurrent.