Coordinate hygiene for the same-strand argument #
The paper's SameStrand lemma is a statement about vertices, not about
the non-unique path-slot descriptions of the two common endpoints. This
file starts the formal version by recording the injectivity fact needed to
turn vertex equalities into slot equalities when the positions concerned are
genuinely interior.
The generic form of the subinterval-reflection identity. The reusable
construction in GenusFourCore097 is polymorphic in the subdivision spec;
its original packaged equality was specialized only because that file's
application has six core vertices and nine slots.
Two interior chips whose raw path coordinates sum to less than the slot length slide to the tail endpoint and the point at their coordinate sum.
Two interior chips whose raw path coordinates sum past the slot length slide to the head endpoint and the point at their excess coordinate.
On a theta, two raw path coordinates summing to the strand length form the reflected (hence canonical) pair and have rank one.
Interior vertices on distinct banana strands are distinct. In particular, the slot label of an interior vertex is intrinsic, whereas the two endpoint descriptions deliberately are not.
If a path vertex agrees with an interior vertex on another strand, then the first path position is interior as well and the two strand labels agree. This is useful for identifying the inside endpoint of a crossing step.
The endpoint coordinate aliases that make the paper's parenthetical
i.e. clauses invalid without an interior hypothesis.
Concrete witness to the endpoint-alias issue in the paper's coordinate
parentheticals: already on a theta, the zero positions of slots 0 and 1
are equal vertices although their coordinate pairs differ.
A pointwise form of the last step in the reduced-divisor strategy: a
q-reduced divisor with a debt at q is not winnable and hence has rank
-1. It is kept separate from the banana interval calculation.
The pointwise version of the reduced-divisor calculation required in the
paper's SameStrand proof. For a two-chip divisor with debt at q, the
ordinary two-edge-cut condition handles every cut of size at least three.
Thus it remains only to burn the exceptional multiplicity-two cuts. This is
strictly weaker (and correct) than requiring every such cut containing both
chips to have size at least three.
If a cut fails the pointwise burning test for x+y-q, then every source
of a boundary edge is one of the two chip locations. This is the local
form in which a multiplicity-two cut can be fed to crossingSteps geometry.
Turn a positive boundary multiplicity into the crossing unit step used by the subdivision cut lemmas.
An excluded interior point whose two strand endpoints are on the cut side forces two different crossing steps on that strand.
The two directed boundary sources on opposite sides of an excluded path position cannot both be the same vertex of that path. This is the remaining one-strand arithmetic contradiction in the two-cut burning argument.
Exact Dhar calculation for three interior path coordinates: if the two positive chips lie on distinct strands, then subtracting a different interior vertex produces a reduced divisor at that vertex.
Core-endpoint case of the same Dhar calculation. With either core endpoint and an interior chip on one strand positive, subtracting an interior point of a different strand is reduced at the latter point.
If the debt lies strictly to the right of the non-endpoint chip on one
banana strand, the divisor consisting of the tail chip, the interior chip,
and that debt is reduced at the debt. No interior hypothesis is needed for
p: the case p = 0 simply puts both positive chips at the tail endpoint.
If the debt lies strictly to the left of the non-endpoint chip on one
banana strand, the divisor consisting of the interior chip, the head chip,
and that debt is reduced at the debt. This is the head-endpoint counterpart
of q_reduced_path_zero_add_same_strand_of_lt.
Rank form of the two endpoint reducedness lemmas.
General-coordinate version of the same-strand interval implication.
For interior marks, a rank-zero normal-form auxiliary vertex must lie on the marked strand; off-strand interior auxiliaries are ruled out by the distinct-strand reducedness theorem.
Left-endpoint specialization of the core-endpoint Dhar calculation.
Right-endpoint specialization of the core-endpoint Dhar calculation.
In particular, the left endpoint cannot be the auxiliary vertex in a
rank-zero w + u - v configuration with distinct interior marked strands.
The right endpoint likewise cannot be the auxiliary vertex in a
rank-zero w + u - v configuration with distinct interior marked strands.
Coordinate-free core-endpoint version used when decomposing an arbitrary auxiliary vertex into core and interior cases.
The remaining on-strand case of SameStrand. If the two positive
vertices are interior points of one theta strand and their pair has rank
zero, then subtracting an interior point of a different strand cannot leave
rank zero. The rank-zero hypothesis is essential: it excludes the reflected
pair, whose coordinate sum is the strand length.
Full auxiliary-vertex form needed by the negative-rankDelta bridge.
For distinct interior theta marks u and v, a rank-zero positive pair
w+u with w ≠ v cannot still have rank zero after subtracting v.