Verified local input for theta torsion

The segment-reflection script gives the one-strand canonical-divisor identity used in the paper's evenly-marked theta argument. The stronger identity for multiples of two marks is recorded below as an explicit remaining interface; it is not assumed here.

The raw prefix calculation behind the paper's eq:multDiffMarkedPts is available from ThetaPrefix. Its forward-oriented normalized adapter is verified there; reversed slots still require the corresponding reflected endpoint calculation.

theorem Bananas.path_reflection_linear_equiv (B : Banana 2) (α : Fin 3) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (canonicalDivisor (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (oneChip (strandVertex B α p) + oneChip (strandVertex B α (strandMirror B α p)))

Paper source: reflection ingredient behind eq:multDiffMarkedPts.

A path position and its reflection add to the banana canonical divisor.

Normalized strand coordinates must be translated before applying any raw-path firing identity. In the reversed orientation, normalized position i is stored at raw position length - i. The adapter for this (normalizedPathPosition, strandVertex_eq_pathVertex_normalized, normalizedPathPosition_isInterior) lives in BananaBasics.lean; nothing below this point ended up needing it directly.

def Bananas.EvenlyMarkedThetaMultiplePrincipalContract : Prop

Paper source: eq:multDiffMarkedPts and cor:evenlyMarkedKGT; this is an explicit contract for the currently missing graph-specific firing identity.

The exact graph lemma needed to finish the evenly-marked torsion proof.

For B : Banana 2, distinct strands α ≠ β, and interior positions i,j with common rational ratio, put k = B.length α / gcd (B.length α) i.val. The paper's equation K - n(u-v) ~ reflected(ni) + (nj) implies the following endpoint case at n = k, hence the desired torsion witness.

This was originally a specification of a then-missing multi-strand firing-script lemma. It is now discharged by ThetaResidue.evenlyMarkedTheta_multiple_principal, and Statements.evenlyMarkedTheta_torsion is unconditional. The named Prop is kept only as the interface through which that discharge is routed.

Equations

• One or more equations did not get rendered due to their size.

theorem Bananas.torsionWitness_of_evenlyMarkedTheta_contract (hContract : EvenlyMarkedThetaMultiplePrincipalContract) (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hEven : EvenlyMarkedTheta B α β i j) : TorsionWitness (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) (B.length α / (B.length α).gcd ↑i)

The missing multi-strand firing identity immediately yields the positive torsion witness used by the transmission API. This adapter deliberately does not claim minimality of the period.