The literal arithmetic Picard diamond satisfies its cyclotomic relation
ProvedMazurTransfer.Order13ActualPicardCyclotomicNorm.rho_cyclotomicalgebraic-geometryarithmetic-geometrymazur-theorem
The actual diamond endomorphism rho of the arithmetic degree-zero Picard group of the order-thirteen curve over Q satisfies rho^2-rho+1=0 as an equality in its additive endomorphism ring. This is the complete original endomorphism-ring statement.
Preamble
import Definitions.Def_MazurTransfer_Order13ActualDiamondPicardEndomorphismsExplicitPublicOrderCertificate20261017
Formal statement
theorem MazurTransfer.Order13ActualPicardCyclotomicNorm.rho_cyclotomic : MazurTransfer.Order13ActualDiamondPicardEndomorphisms.rho ^ 2 - MazurTransfer.Order13ActualDiamondPicardEndomorphisms.rho + 1 = 0 := by sorry
Source
Complete original MazurTheorem Order13ActualPicardCyclotomicNorm.rho_cyclotomic proof and its four intermediate calculations. Official Anthropic FLT arithmetic Pic0 interfaces at 6e837e75355538c7f80bab5b956861e86c4eacc2, Apache-2.0.