Example 1.15: an explicit genus-eight Brill--Noether general chain

The five factors, in the order the paper lists them:

• the cycle B_{3,1} (torsion order k = 4);
• the evenly marked theta graph θ_{4,1,4}, marked at (x_1, z_1) (k = 4);
• the cycle B_{3,2} (k = 5);
• the evenly marked theta graph θ_{5,2,10}, marked at (x_2, z_4) (k = 5);
• the evenly marked theta graph θ_{6,2,3}, marked at (x_4, z_2) (k = 3).

Each factor's k-general transmission comes from cycle_kGeneralTransmission (Example 1.11, Bananas/CycleTorsionOrder.lean) or evenlyMarkedTheta_kGeneral (Bananas/EvenlyMarkedThetaKGeneral.lean). The genera are 1, 2, 1, 2, 2, summing to the paper's genus 8, and the minimum prefix/suffix budget of Corollary 6.16(2) checks out by direct computation: min(1,8) < 4, min(3,7) < 4, min(4,5) < 5, min(6,4) < 5, min(8,2) < 3. (FORMALIZATION_NOTES.md records that the paper's own displayed torsion orders 4,5,5,5,3 disagree with its per-factor computations 4,4,5,5,3; the k-values used here are the correct per-factor ones, and the conclusion is unaffected either way.)

The five factors

def Bananas.bngB31 : Banana 1

The cycle B_{3,1}.

Equations

• Bananas.bngB31 = Bananas.bananaOfLengths 1 ![3, 1] Bananas.bngB31._proof_1

def Bananas.bngTheta414 : Banana 2

The theta graph θ_{4,1,4}.

Equations

• Bananas.bngTheta414 = Bananas.bananaOfLengths 2 ![4, 1, 4] Bananas.bngTheta414._proof_1

def Bananas.bngB32 : Banana 1

The cycle B_{3,2}.

Equations

• Bananas.bngB32 = Bananas.bananaOfLengths 1 ![3, 2] Bananas.bngB32._proof_1

def Bananas.bngTheta5210 : Banana 2

The theta graph θ_{5,2,10}.

Equations

• Bananas.bngTheta5210 = Bananas.bananaOfLengths 2 ![5, 2, 10] Bananas.bngTheta5210._proof_1

def Bananas.bngTheta623 : Banana 2

The theta graph θ_{6,2,3}.

Equations

• Bananas.bngTheta623 = Bananas.bananaOfLengths 2 ![6, 2, 3] Bananas.bngTheta623._proof_1

def Bananas.bngX1 : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition bngTheta414 0

x_1 on θ_{4,1,4}: strand 0 (the n_0-strand), position 1.

Equations

• Bananas.bngX1 = ⟨1, Bananas.bngX1._proof_1⟩

def Bananas.bngZ1 : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition bngTheta414 2

z_1 on θ_{4,1,4}: strand 2 (the n_2-strand), position 1.

Equations

• Bananas.bngZ1 = ⟨1, Bananas.bngZ1._proof_1⟩

def Bananas.bngX2 : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition bngTheta5210 0

x_2 on θ_{5,2,10}.

Equations

• Bananas.bngX2 = ⟨2, Bananas.bngX2._proof_1⟩

def Bananas.bngZ4 : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition bngTheta5210 2

z_4 on θ_{5,2,10}.

Equations

• Bananas.bngZ4 = ⟨4, Bananas.bngZ4._proof_1⟩

def Bananas.bngX4 : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition bngTheta623 0

x_4 on θ_{6,2,3}.

Equations

• Bananas.bngX4 = ⟨4, Bananas.bngX4._proof_1⟩

def Bananas.bngZ2 : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition bngTheta623 2

z_2 on θ_{6,2,3}.

Equations

• Bananas.bngZ2 = ⟨2, Bananas.bngZ2._proof_1⟩

theorem Bananas.bngEvenlyMarked414 : EvenlyMarkedTheta bngTheta414 0 2 bngX1 bngZ1

theorem Bananas.bngEvenlyMarked5210 : EvenlyMarkedTheta bngTheta5210 0 2 bngX2 bngZ4

theorem Bananas.bngEvenlyMarked623 : EvenlyMarkedTheta bngTheta623 0 2 bngX4 bngZ2

noncomputable def Bananas.bngF1 : KGeneralChainFactor

Factor 1: the cycle B_{3,1}, torsion order 4.

Equations

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

noncomputable def Bananas.bngF2 : KGeneralChainFactor

Factor 2: the theta graph θ_{4,1,4}, marked at (x_1, z_1), torsion order 4.

Equations

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

noncomputable def Bananas.bngF3 : KGeneralChainFactor

Factor 3: the cycle B_{3,2}, torsion order 5.

Equations

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

noncomputable def Bananas.bngF4 : KGeneralChainFactor

Factor 4: the theta graph θ_{5,2,10}, marked at (x_2, z_4), torsion order 5.

Equations

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

noncomputable def Bananas.bngF5 : KGeneralChainFactor

Factor 5: the theta graph θ_{6,2,3}, marked at (x_4, z_2), torsion order 3.

Equations

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

theorem Bananas.bngF1_genus : bngF1.marked.graph.genus = 1

The genus of each factor, read off Spec.genus_graph.

theorem Bananas.bngF2_genus : bngF2.marked.graph.genus = 2

theorem Bananas.bngF3_genus : bngF3.marked.graph.genus = 1

theorem Bananas.bngF4_genus : bngF4.marked.graph.genus = 2

theorem Bananas.bngF5_genus : bngF5.marked.graph.genus = 2

theorem Bananas.bngChainMinBudget : ChainMinBudget [bngF1, bngF2, bngF3, bngF4, bngF5]

theorem Bananas.exampleBng_brillNoetherGeneral : BrillNoetherGeneral (bngF1.marked.chain (List.map KGeneralChainFactor.marked [bngF2, bngF3, bngF4, bngF5])).graph

Example 1.15 (eg:bng): the iterated vertex gluing of the five factors — cycle B_{3,1}, evenly marked θ_{4,1,4} at (x_1,z_1), cycle B_{3,2}, evenly marked θ_{5,2,10} at (x_2,z_4), evenly marked θ_{6,2,3} at (x_4,z_2) — is a genus-eight Brill--Noether general graph.

theorem Bananas.exampleBng_genus : (bngF1.marked.chain (List.map KGeneralChainFactor.marked [bngF2, bngF3, bngF4, bngF5])).graph.genus = 8