Paper coordinate representatives are q-reduced

This file supplies the concrete bridge left open by BananaJacobianReducedInjectivity.lean. An interior coordinate contributes the corresponding semibreak chip, a terminal coordinate contributes a chip at the right endpoint, and every nonzero coordinate contributes one unit of debt at the left endpoint.

def Bananas.IsPaperInteriorCoordinate {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (alpha : Fin (g + 1)) : Prop

The decidable numerical form of being an interior normalized position.

Equations

• Bananas.IsPaperInteriorCoordinate B p alpha = (0 < ↑(p alpha) ∧ ↑(p alpha) < B.length alpha)

noncomputable def Bananas.paperCoordinateChips {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (alpha : Fin (g + 1)) : Option (Fin (B.length alpha - 1))

The storage-oriented semibreak chips encoded by a vector of normalized strand positions.

Equations

• Bananas.paperCoordinateChips B p alpha = if h : 0 < ↑(p alpha) ∧ ↑(p alpha) < B.length alpha then some (Bananas.normalizedInteriorOffset B alpha (p alpha) h) else none

def Bananas.paperCoordinateLeftCoefficient {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) : ℤ

One unit of left-endpoint debt for every nonzero coordinate.

Equations

• Bananas.paperCoordinateLeftCoefficient B p = ∑ alpha : Fin (g + 1), if ↑(p alpha) = 0 then 0 else -1

def Bananas.paperCoordinateRightCoefficient {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) : ℤ

One right-endpoint chip for every terminal coordinate.

Equations

• Bananas.paperCoordinateRightCoefficient B p = ∑ alpha : Fin (g + 1), if ↑(p alpha) = B.length alpha then 1 else 0

noncomputable def Bananas.paperCoordinateSemibreak {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)

The semibreak part of the paper coordinate divisor.

Equations

• Bananas.paperCoordinateSemibreak B p = Bananas.semibreakDivisor B (Bananas.paperCoordinateChips B p)

theorem Bananas.isSemibreak_paperCoordinateSemibreak {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) : IsSemibreak B (paperCoordinateSemibreak B p)

theorem Bananas.bananaPositionCoordinateDivisor_eq_normalForm {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) : bananaPositionCoordinateDivisor B p = bananaNormalForm B (paperCoordinateLeftCoefficient B p) (paperCoordinateRightCoefficient B p) (paperCoordinateSemibreak B p)

The paper coordinate divisor is exactly an endpoint/semibreak normal form.

theorem Bananas.paperCoordinateRightCoefficient_add_degree_le_genus {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hPaper : IsPaperReducedPositionCoordinates B p) : paperCoordinateRightCoefficient B p + CFDiv.degree (paperCoordinateSemibreak B p) ≤ ↑g

The numerical normal-form bound follows from the required zero coordinate. The ordering clause in the paper's representative convention is not needed for this reducedness argument.

theorem Bananas.q_reduced_bananaPositionCoordinateDivisor_of_paperReduced {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hPaper : IsPaperReducedPositionCoordinates B p) : qReduced (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (bananaPositionCoordinateDivisor B p)

The paper's preferred coordinate representative is reduced at the common left endpoint.

theorem Bananas.bananaPositionCoordinates_eq_zero_of_paperReduced_of_mem_relations {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hPaper : IsPaperReducedPositionCoordinates B p) (hKernel : bananaPositionCoordinates B p ∈ bananaCoordinateRelations B) : bananaPositionCoordinates B p = 0

Full kernel-triviality statement for the paper's reduced coordinate representatives.