Exact torsion order for normalized evenly marked theta marks.

theorem Bananas.interiorMoment_zsmul (B : Banana 2) (alpha : Fin 3) (n : ℤ) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : interiorMoment B alpha (n • D) = n * interiorMoment B alpha D

theorem Bananas.thetaJacobianMoment_zsmul (B : Banana 2) (n : ℤ) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : thetaJacobianMoment B (n • D) = n • thetaJacobianMoment B D

theorem Bananas.torsionWitness_coordinate_mem_thetaLattice_01 (B : Banana 2) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B 0) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B 1) (hi : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B 0 i) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B 1 j) (m : ℕ) (hm : TorsionWitness (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B 0 i) (strandVertex B 1 j)) m) : (↑(m * ↑i), -↑(m * ↑j)) ∈ thetaLattice (B.length 0) (B.length 1) (B.length 2)

theorem Bananas.evenlyMarkedTheta_isTorsionOrder_01 (B : Banana 2) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B 0) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B 1) (hEven : EvenlyMarkedTheta B 0 1 i j) : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B 0 i) (strandVertex B 1 j)) (B.length 0 / (B.length 0).gcd ↑i)