A generic cross-strand far-mark rank witness #
The corrected high-genus ledger separates the local rank calculation from the
global far-mark classification. This file records the local calculation in
the coordinate language currently supported by SameStrand: two positive
chips are interior points on distinct strands, and the third position is an
explicit interior vertex distinct from both.
The conclusion is deliberately a rank pattern, not a rankDelta theorem.
The two-chip divisor has rank zero, while deleting the third chip from it
leaves a degree-one divisor of rank -1. This is the verified generic
cross-strand ingredient; selecting that third position from a normalized
"far" hypothesis is a separate orientation/mark-selection bridge.
Graph-generic ingredients #
Stated for an abstract CFGraph. Doing the rank bookkeeping here rather than
on a concrete banana keeps the unifier away from comparing divisors pointwise
(which unfolds oneChip and evaluates DecidableEq on the subdivision vertex
type); see the module docstring of LengthTwoCrossMonotonicity.lean.
A cross-strand two-chip divisor has rank zero when an explicit third interior vertex makes its one-chip deletion reduced with debt.
The divisor in the second conjunct has two positive chips and one deleted chip, i.e. it is the three-term witness used by the far-mark argument. The hypotheses name all vertex distinctness needed by the reducedness theorem; no endpoint coordinate pair is treated as unique.