Theta Moment

Interior path moments in normalized strand coordinates. Endpoints are omitted; this is the coordinate part of the theta Jacobian invariant.

def Bananas.interiorMoment (B : Banana 2) (α : Fin 3) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : ℤ

The position-weighted sum of divisor coefficients at the interior vertices of one strand.

Equations

• Bananas.interiorMoment B α D = ∑ r ∈ Finset.range (B.length α - 1), if h : r + 1 < B.length α then ↑(r + 1) * D (Bananas.strandVertex B α ⟨r + 1, ⋯⟩) else 0

def Bananas.thetaMoment (B : Banana 2) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : ℤ × ℤ

The differences of the second and third interior strand moments from the first.

Equations

• Bananas.thetaMoment B D = (Bananas.interiorMoment B 1 D - Bananas.interiorMoment B 0 D, Bananas.interiorMoment B 2 D - Bananas.interiorMoment B 0 D)

The raw difference of the three interior moments is useful for evaluating marked divisors, but it is not itself the Jacobian coordinate: a principal divisor can have nonzero endpoint contribution. The following asymmetric coordinate is the one compatible with the paper's presentation, taking v_{0,0} as basepoint.

def Bananas.thetaCoordinate (B : Banana 2) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : ℤ × ℤ × ℤ

The three strand moments, with the right-endpoint contribution included in the first coordinate.

Equations

• Bananas.thetaCoordinate B D = (Bananas.interiorMoment B 0 D + ↑(B.length 0) * D (Bananas.rightEndpoint B), Bananas.interiorMoment B 1 D, Bananas.interiorMoment B 2 D)

The two-coordinate projection used by the paper's theta presentation.

def Bananas.thetaJacobianMoment (B : Banana 2) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : ℤ × ℤ

The two Jacobian coordinates obtained by subtracting the third moment from the endpoint-corrected first and second moments.

Equations

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

theorem Bananas.interiorMoment_one_chip (B : Banana 2) (α β : Fin 3) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) : interiorMoment B α (oneChip (strandVertex B β j)) = if α = β then ↑↑j else 0

theorem Bananas.thetaMoment_marked_difference (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hi : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α i) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) : thetaMoment B (oneChip (strandVertex B α i) - oneChip (strandVertex B β j)) = (((if α = 1 then ↑↑i else 0) - if β = 1 then ↑↑j else 0) - ((if α = 0 then ↑↑i else 0) - if β = 0 then ↑↑j else 0), ((if α = 2 then ↑↑i else 0) - if β = 2 then ↑↑j else 0) - ((if α = 0 then ↑↑i else 0) - if β = 0 then ↑↑j else 0))

theorem Bananas.thetaCoordinate_marked_difference (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hi : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α i) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) : thetaCoordinate B (oneChip (strandVertex B α i) - oneChip (strandVertex B β j)) = (((if α = 0 then ↑↑i else 0) - if β = 0 then ↑↑j else 0) - ↑(B.length 0) * ((if strandVertex B α i = rightEndpoint B then 1 else 0) - if strandVertex B β j = rightEndpoint B then 1 else 0), (if α = 1 then ↑↑i else 0) - if β = 1 then ↑↑j else 0, (if α = 2 then ↑↑i else 0) - if β = 2 then ↑↑j else 0)

theorem Bananas.thetaJacobianMoment_marked_difference_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) : thetaJacobianMoment B (oneChip (strandVertex B 0 i) - oneChip (strandVertex B 1 j)) = (↑↑i, -↑↑j)