The specified Pell function has exactly the original two-point divisor

Proved

MazurTransfer.Order13PellPrincipalDivisor.pellDivisor_coefficient

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

algebraic-geometryarithmetic-geometrymazur-theorem

For every place $v$ of the existing rational scheme function field of the literal order-13 curve, the specified divisor $D=19[v_-]-19[v_+]$ and original Pell function $f$ satisfy

D(v)=\operatorname{ord}_v(f).

This gives the complete divisor formula for that actual function, with its canonical infinity places.

Preamble

/-
Copyright (c) 2026 Vas and contributors. Released under Apache-2.0.
Design boundary: the exact two-point principal divisor of the explicit Pell
function in the actual rational scheme function field. Named downstream
consumer: nineteen annihilates the difference of the infinity Picard classes.
-/
import Definitions.Def_MazurTransfer_Order13PellPrincipalDivisorData
import Definitions.Def_MazurTransfer_Order13PellChartOverlapIdentities
import Theorems.Thm_MazurTransfer_Order13PellPrincipalDivisor_pellFunction_ord_away_infinity
import Theorems.Thm_MazurTransfer_Order13PellActualOrdinaryChart_pellFunction_eq_ordinaryPlus
noncomputable section
open MazurTransfer
open Order13PellPrincipalDivisor
open AlgebraicGeometry AlgebraicCurve
open MazurTorsion.XOneThirteenProjectiveCurve
open GoodCharacteristicGeometryPublicProof.MazurTransfer.Order13GoodCharacteristicCurveModel
open Order13IntegralSections Order13RationalSectionPicardInjection Order13ActualInfinityPlaceCenters
open Order13PellActualInfinityValuations
local instance : Fact ((104 : ℚ) ≠ 0) := ⟨by norm_num⟩

Formal statement

theorem MazurTransfer.Order13PellPrincipalDivisor.pellDivisor_coefficient (v : Place ℚ (actualCurveFunctionField ℚ)) :
    pellDivisor v = v.ord pellFunction := by sorry

Source

Original complete pellDivisor_coefficient statement and proof from MazurTheorem Order13PellPrincipalDivisor.lean, Apache-2.0, Vas and contributors. The unchanged original divisor and Pell function constructors are supplied by published Definitions. Public proved infinity orders and global orders away from infinity supply the complete valuation input. The full original closed type is kernel-compared. Named downstream consumer: the original Pell principal-divisor certificate and exact order nineteen of the actual infinity class.

View graph