The original actual infinity divisor class has exact additive order nineteen

Proved

MazurTransfer.Order13InfinityPicardClassOrder.infinityClass_order

by Vas · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometryarithmetic-geometrymazur-theorem

The original arithmetic Picard class of the difference between the two canonical rational infinity places of the literal order-13 curve has exact additive order

\operatorname{ord}(c)=19.

It therefore generates a cyclic subgroup of order nineteen in arithmetic $\operatorname{Pic}^0$ , supplying the lower bound to match the proved rational torsion bound.

Preamble

/-
Copyright (c) 2026 Vas and contributors. Released under Apache-2.0.
Design boundary: the explicit principal divisor makes the nonzero difference
of the actual infinity section classes an element of exact order nineteen.
Named downstream consumer: the lower bound matching the rational arithmetic
Picard torsion bound from the two good reductions.
-/
import Definitions.Def_MazurTransfer_Order13InfinityDivisorClassData
import Theorems.Thm_MazurTransfer_Order13PellPrincipalDivisor_pellDivisor_isPrincipal
import Theorems.Thm_MazurTransfer_Order13InfinityPicardClassOrder_infinityClass_ne_zero
noncomputable section
open MazurTransfer
open Order13InfinityPicardClassOrder
open AlgebraicGeometry AlgebraicCurve
open MazurTorsion.XOneThirteenProjectiveCurve
open GoodCharacteristicGeometryPublicProof.MazurTransfer.Order13GoodCharacteristicCurveModel
open Order13IntegralSections Order13RationalSectionPicardInjection
open Order13PellPrincipalDivisor Order13ActualInfinityPlaceCenters
local instance : Fact ((104 : ℚ) ≠ 0) := ⟨by norm_num⟩

Formal statement

theorem MazurTransfer.Order13InfinityPicardClassOrder.infinityClass_order : addOrderOf infinityClass = 19 := by sorry

Source

Original complete infinityClass_order statement and main proof, with original nineteen_divisor_eq_pellDivisor and nineteen_smul_infinityClass helper proofs, from MazurTheorem Order13InfinityPicardClassOrder.lean, Apache-2.0, Vas and contributors. The unchanged original actual divisor/class constructors are supplied by their published Definition. The actual principal-divisor theorem and the exact original nonzero contract, proved directly by the genus obstruction, are public proved dependencies. The complete original closed type is kernel-compared. Named downstream consumer: the exact lower bound matching the rational arithmetic Picard torsion bound.

View graph