Exact torsion of two length-two midpoint marks #
The exceptional high-genus all-submodular marking has torsion order two. This is independent of the number of other strands: each midpoint doubles to the same endpoint pencil.
TorsionWitness for an explicitly marked graph, with the structure
projections reduced away. Rewriting with this before touching the witness
keeps every divisor typed at CFDiv G rather than at the defeq-but-distinct
CFDiv (mark G u v).graph; otherwise simp lemmas such as one_zsmul fail
to fire, because the SMul instance recorded in the term mentions
(mark G u v).graph.
Every combinatorial midpoint, not only the midpoint of a length-two strand, doubles to the degree-two endpoint pencil. This is the corrected torsion input needed after the length-two cross-strand submodularity exception: a length-two midpoint paired with the midpoint of an arbitrary even-length strand still has torsion order two.
Two distinct-strand midpoints have exact torsion order two. No length-two hypothesis is required for this torsion calculation.