Theta Principal

Firing-script values and slopes in the normalized strand coordinates.

def Bananas.normalizedPathValue (B : Banana 2) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin 3) (r : ℕ) : ℤ

The firing-script value at a normalized strand position, extended by zero beyond the strand.

Equations

• Bananas.normalizedPathValue B script α r = if hr : r ≤ B.length α then script (Bananas.strandVertex B α ⟨r, ⋯⟩) else 0

def Bananas.normalizedStepSlope (B : Banana 2) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin 3) (k : ℕ) : ℤ

The difference of firing-script values at consecutive normalized strand positions.

Equations

• Bananas.normalizedStepSlope B script α k = Bananas.normalizedPathValue B script α (k + 1) - Bananas.normalizedPathValue B script α k

theorem Bananas.normalizedPathValue_eq (B : Banana 2) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin 3) (r : ℕ) (hr : r ≤ B.length α) : normalizedPathValue B script α r = script (strandVertex B α ⟨r, ⋯⟩)

theorem Bananas.normalizedStepSlope_eq (B : Banana 2) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin 3) (k : ℕ) (hk : k < B.length α) : normalizedStepSlope B script α k = script (strandVertex B α ⟨k + 1, ⋯⟩) - script (strandVertex B α ⟨k, ⋯⟩)

theorem Bananas.sum_normalizedStepSlope (B : Banana 2) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin 3) : ∑ k ∈ Finset.range (B.length α), normalizedStepSlope B script α k = script (rightEndpoint B) - script (leftEndpoint B)

IsStepSlope follows the stored orientation of each core edge, whereas normalizedStepSlope always follows the common coordinate from core vertex 0 to core vertex 1. Thus a reversed stored edge needs both a sign and an index reversal.

def Bananas.storageStepSlope (B : Banana 2) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin 3) (k : ℕ) : ℤ

The strand slope in the stored edge orientation, reversing its index and sign when the strand orientation is reversed.

Equations

• Bananas.storageStepSlope B script α k = if B.core.tail α = 0 then Bananas.normalizedStepSlope B script α k else -Bananas.normalizedStepSlope B script α (B.length α - 1 - k)

theorem Bananas.storageStepSlope_isStepSlope (B : Banana 2) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : Utilities.Certificate.SubdivisionGraph.Spec.IsStepSlope B script (storageStepSlope B script)

theorem Bananas.prin_normalized_interior (B : Banana 2) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin 3) (r : Fin (B.length α - 1)) : (prin (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) script (strandVertex B α ⟨↑r + 1, ⋯⟩) = normalizedStepSlope B script α (↑r + 1) - normalizedStepSlope B script α ↑r

theorem Bananas.interiorMoment_prin (B : Banana 2) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin 3) : interiorMoment B α ((prin (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) script) = ↑(B.length α) * normalizedStepSlope B script α (B.length α - 1) - (script (rightEndpoint B) - script (leftEndpoint B))

theorem Bananas.prin_rightEndpoint_eq (B : Banana 2) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : (prin (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) script (rightEndpoint B) = -∑ α : Fin 3, normalizedStepSlope B script α (B.length α - 1)

theorem Bananas.thetaJacobianMoment_prin_mem (B : Banana 2) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : thetaJacobianMoment B ((prin (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) script) ∈ thetaLattice (B.length 0) (B.length 1) (B.length 2)