def Hex.ECPP.CM.jacobi : Nat → Nat → Nat → Int → Int

Binary Jacobi algorithm; fuel bounds every halving and reciprocity step.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.CM.jacobi 0 x✝² x✝¹ x✝ = 0

def Hex.ECPP.CM.symbol (a n : Nat) : Int

Fuel is linear in input bits; exhaustion conservatively returns zero.

Equations

• Hex.ECPP.CM.symbol a n = Hex.ECPP.CM.jacobi (4 * HexArith.bitLength n + 4) (a % n) n 1

def Hex.ECPP.CM.rootValid (n a r : Nat) : Bool

Check a canonical root proposal before using it.

Equations

• Hex.ECPP.CM.rootValid n a r = (decide (1 < n) && decide (r < n) && r * r % n == a % n)

def Hex.ECPP.CM.sqrt? (n z a : Nat) : Option Nat

Bounded Tonelli–Shanks with a caller-supplied nonresidue. Even for a composite modulus, success requires the actual root equation.

Equations

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

structure Hex.ECPP.CM.Invariant : Type

A class number one discriminant and its integer singular j-invariant.

• d : Nat

  Absolute value of the negative discriminant.

• j : Int

  Integer singular j-invariant of the discriminant.

@[instance_reducible]

instance Hex.ECPP.CM.instReprInvariant : Repr Invariant

Equations

• Hex.ECPP.CM.instReprInvariant = { reprPrec := Hex.ECPP.CM.instReprInvariant.repr }

def Hex.ECPP.CM.instReprInvariant.repr : Invariant → Nat → Std.Format

Equations

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

def Hex.ECPP.CM.portfolio : List Invariant

A fixed portfolio; no subject-specific trace or factorization is stored.

Equations

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

def Hex.ECPP.CM.normValid (n d t v : Nat) : Bool

Check the exact Cornacchia norm equation, independently of the search.

Equations

• Hex.ECPP.CM.normValid n d t v = (t * t + d * v * v == 4 * n)

def Hex.ECPP.CM.norm? (n d root : Nat) : Option (Nat × Nat)

Solve t² + d*v² = 4*n from a checked modular root. Odd discriminants also try x² + d*y² = n, since a solution can have both coordinates even. Even discriminants use the equivalent norm equation modulo n.

Equations

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

def Hex.ECPP.CM.traces (d t v : Nat) : List Int

Candidate traces, including all extra associates for j=0 and j=1728.

Equations

• Hex.ECPP.CM.traces d t v = List.flatMap (fun (a : Int) => [a, -a]) (if (d == 3) = true then [↑t, (↑t + 3 * ↑v) / 2, (↑t - 3 * ↑v) / 2] else if (d == 4) = true then [↑t, 2 * ↑v] else [↑t])

def Hex.ECPP.CM.curves (n : Nat) (inv : Invariant) (g : Nat) : List (Nat × Nat)

All exceptional twist classes use powers of a sextic/quartic nonresidue. Ordinary invariants use the curve and its quadratic twist.

Equations

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