Monotonicity ingredients for the length-two cross exception #
This file records the slightly enlarged midpoint base-point calculation needed
after a chip on another strand is put back into banana normal form. That
operation can lower one endpoint coefficient from 0 to -1; the original
low-degree lemma only covered nonnegative endpoint coefficients.
Elaboration cost #
All divisor algebra used below is proved once in the Generic section, for an
abstract CFGraph and abstract divisors. This is a performance requirement,
not a stylistic preference. change, convert and abel applied to divisors
of a concrete banana graph let the unifier fall back on comparing divisors
pointwise: it then unfolds oneChip into if v = w then 1 else 0 and starts
evaluating DecidableEq on the subdivision vertex type (a nested Sum of
Fins built out of pathVertex/strandVertex dite-chains). A single such
change costs minutes. With abstract divisors the same steps are instant, and
every use downstream is a syntactic rw/exact.
The loss of rank on deleting one chip is always either zero or one.
Graph-generic divisor algebra #
See the note on elaboration cost in the module docstring: every statement in this section is about an abstract graph, so that no use of it ever forces the unifier to look inside a banana divisor.
Linear equivalence is stable under subtracting a fixed divisor.
The workhorse: to see that a divisor is not a base point for u, move it
by a linear equivalence to a divisor where the rank comparison is known.
The two endpoints play symmetric roles in the reflection identity.
Reflection in the strand midpoint followed by a slide of the old chip
towards the tail endpoint L.
Variant of linear_equiv_pair_of_reflect_slide for the head-excess slide,
whose statement lists the endpoint chip second.
Boundary case: the old chip and the reflected mark are themselves a reflected pair, so both endpoint chips cancel.
Normal-form bookkeeping: paying one chip at R moves the deleted mark P
to the new slot X and removes the old chip Q.
Reflection alone: the deleted mark P is replaced by its mirror P' at
the cost of one chip at each endpoint.
Banana normal form as an explicit sum #
Definitional unfolding of bananaNormalForm, as a rewrite rule. Stated
for a variable banana, so proving it costs nothing.
Raw path-coordinate version of reflection in the midpoint of a strand.
An empty semibreak strand can be filled at any interior slot.
Moving the unique chip on a semibreak strand to another interior slot preserves semibreakness.
A length-two midpoint is represented by the same raw path position in either stored orientation.
Removing an occupied length-two midpoint does not change rank in the
low-degree normal-form range even when one (but not both) endpoint
coefficients is -1.
The two separate endpoint-degree bounds are exactly what is produced by normalizing the deletion of a vertex on a different strand.
If the other marked strand is empty in the semibreak part, deleting its
marked point preserves the base-point status of an occupied length-two
midpoint. This includes the boundary case a = b = 0, where the reflected
normal form has two endpoint debts and the rank formula does not apply.
Occupied-strand branch in which the old chip and the reflected marked point slide to the raw tail endpoint.
Occupied-strand branch in which the old chip and the reflected marked point slide to the raw head endpoint.
Occupied-strand boundary branch: the old chip and the reflected marked point form a reflected pair, so both endpoint contributions cancel and the old chip is simply removed from the semibreak part.
The marked rank second difference is nonnegative for every low-degree banana normal form in the length-two cross configuration.
Every divisor has nonnegative marked rank second difference when one mark is a length-two midpoint and the other is an interior point of a distinct strand (in raw path coordinates).
TeX label: thm-NSMForBanana (Theorem 3.9), corrected length-two
exception.
The extra all-submodular family identified by the external computational
audit: a midpoint on a length-two strand may be paired with any strictly
interior point on a different strand. This is a correction to Theorem 3.9,
whose published proof handles the distinct-strand case by the divisor
D = v_{α,1} + v_{α,i} + v_{β,n_β-1} and asserts
D ∼ v_{α,0} + v_{α,i+1} + v_{β,n_β-1} is v_{α,n_α}-reduced of rank 0.
When n_α = 2 and i = 1 this fails: v_{α,i+1} = v_{α,n_α} is
multivalent, so D ∼ v_{α,0} + v_{α,n_α} + v_{β,n_β-1} has rank 1 by
lem:g12.
The all-divisors rank argument is supplied by
rankDelta_lengthTwoCross_path_nonneg: after canonical duality and banana
normal-form reduction, deleting the second mark is normalized by one of the
empty, tail-sum, head-excess, or reflected-pair semibreak calculations.