The four-alternative same-strand lemma #
This is the invariant form of paper Lemma 3.5 (lem-SameStrand). The paper
writes vertex equalities as equalities of strand coordinates. That is false
at either multivalent endpoint, because an endpoint has a coordinate on every
strand. We state the first three alternatives as physical vertex equalities
and the fourth as the existence of one strand containing all three physical
vertices.
The argument is needed only in the paper's standing banana range g ≥ 2.
That hypothesis is mathematically essential: in genus one every degree-one
divisor has rank zero, so the displayed four-alternative claim fails for
three suitable points on a cycle.
A physical vertex lies on the normalized strand alpha. Unlike a raw
coordinate equality, this treats the two common endpoints invariantly.
Equations
- Bananas.VertexOnBananaStrand B alpha x = ∃ (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha), x = Bananas.strandVertex B alpha p
Instances For
Three physical vertices lie on one common banana strand.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A noninterior normalized position is one of the two physical endpoints.
Either physical endpoint lies on every normalized banana strand.
A non-reflected pair, expressed invariantly by inequality of physical vertices, has rank zero.
Generic-genus form of the core-plus-interior Dhar calculation. The
theta-only theorem in SameStrand.lean predates the generic reduced-divisor
lemma which its proof actually uses.
A raw-coordinate reflected pair has rank one in every banana of genus at
least two. The older theorem in SameStrand.lean proves only the theta case;
the generic endpoint-pencil rank formula supplies exactly the missing step.
Generic-genus form of the same-positive-strand / distinct-negative-strand Dhar calculation.
Normalized-coordinate wrapper for the core-plus-interior Dhar
calculation in SameStrand.lean.
Two normalized interior chips on distinct strands cannot retain rank zero after deleting a core vertex.
Normalized-coordinate wrapper for the same-positive-strand / distinct negative-strand part of the Dhar calculation.
Corrected Lemma 3.5 (lem-SameStrand).
If rank(x + y - z) = 0 on a banana of genus at least two, then z equals
one of the two positive vertices, the two positive vertices are strand
reflections, or the three physical vertices lie on a common strand.
The paper appends coordinate equalities to the first, second, and fourth alternatives. Those parentheticals are invalid at the common endpoints; the vertex/common-strand formulation here is the faithful invariant claim.