Challenge: the product formula on a smooth proper curve

This checked bridge preserves the exact residue-degree-weighted product-formula contract used by the degree-zero Picard consumer. Tau Ceti proves the result for its geometric order system; the bridge transports it to an abstract order system with the same order homomorphisms.

theorem MazurTheorem.Challenge.divisorProductFormula (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (π : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.IsProper π] [AlgebraicGeometry.SmoothOfRelativeDimension 1 π] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem (TauCeti.AlgebraicGeometry.CodimensionOnePoint X) (Additive (↑X.functionField)ˣ)) (hord : S.ord = TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderAt) : S.IsWeightedDegreeZero fun (x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X) => ↑(AlgebraicGeometry.Scheme.Hom.residueDegree π ↑x)

The exact residue-degree-weighted product formula required to transport divisor degree zero to the scheme Picard group. The equality hord pins the abstract order system to Mathlib's geometric orders of vanishing.