Arithmetic form of the theta exceptional-position condition #
This file separates the finite interval calculation in paper Theorem 3.4
from its divisor-rank content. Coordinates here are the normalized
coordinates used by strandVertex, measured from core vertex 0.
Distinct vertices on a nontrivial banana give a degree-zero divisor of
rank -1.
Paper source: thm-NonSubmodGenus2, with the exceptional support
construction used in lem-SameStrand.
Every two distinct interior normalized positions on one theta strand admit an explicit negative rank-difference witness.
Paper source: the boundary cases in thm-NonSubmodGenus2 and the
support formulation cor:suppUV.
The exceptional-position set is empty exactly in the three boundary
markings listed in Corollary 3.6 of the paper. Writing j + 1 = length
avoids truncated subtraction in the formal version of j = length - 1.
Paper source: thm-NonSubmodGenus2 (Theorem 3.4).
Complete theta classification for two interior marks on the same strand, valid for either stored orientation of that strand.
Reversing the strand coordinate and swapping the ordered marks preserves
nonemptiness of the exceptional-position set. This is the arithmetic
transport needed when a subdivision slot is stored from core vertex 1
rather than from core vertex 0.
A raw-coordinate classification implies the normalized theorem used in
Statements.lean. This checked wrapper isolates the sole remaining
divisor-rank result: the hypothesis hRaw.