def Hex.NormRecovery.taylorShift (p : Array Int) (c : Int) : Array Int

p(X + c) for a dense ascending coefficient array, by the synthetic Taylor shift.

Equations

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

def Hex.NormRecovery.factorials (m : Nat) : Array Nat

The factorials 0!, …, m!.

Equations

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

def Hex.NormRecovery.seriesLog (a : Array Rat) (m : Nat) : Array Rat

The formal logarithm of a power series with constant term 1, to degree m.

Equations

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

def Hex.NormRecovery.logCoshCoeffs (m : Nat) : Array Rat

γ_k = [w^{2k}] log cosh w for k = 1, …, m; every one is nonzero.

Equations

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

def Hex.NormRecovery.powerSums (f : Array Int) (count : Nat) : Array Int

The power sums p_1, …, p_count of the roots of a monic dense integer polynomial, by Newton's identities.

Equations

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

def Hex.NormRecovery.integerRoots (coeffs : Array Int) (bound : Nat) : Option (Array Int)

The integer roots of a monic dense integer polynomial, all of absolute value at most bound; none when the search is abandoned.

Equations

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

def Hex.QuadraticNormCertificate.radicandBound : Nat

The largest radicand magnitude the integer-root search will chase.

Only the search is capped: a genuine certificate above the cap is declined, not mis-accepted.

Equations

• Hex.QuadraticNormCertificate.radicandBound = 1 <<< 20

def Hex.QuadraticNormCertificate.recover? (f : ZPoly) : Option QuadraticNormCertificate

Recover the certificate f would satisfy, if any.

Returns none as soon as any structural requirement fails, so a polynomial outside the class is refused after a few coefficient operations. A some result is a proposal: Hex.QuadraticNormCertificate.check is what decides it.

Equations

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

def Hex.QuadraticNormCertificate.widthFloor : Nat

Modular support width at or above which the certificate is attempted.

Recombination at width w walks up to 2 ^ (w - 1) supports, so the gate is stated as a width rather than as a node count: at the floor the walk is 2 ^ 15 = 32768 nodes, an eighth of the Hex.defaultSubsetBudget the recombination already carries, and it is the cost of that walk the certificate is worth attempting to replace. Below the floor a row pays exactly nothing, because nothing is constructed.

The floor is deliberately not defaultSubsetBudget itself. A width-16 walk sits far under that budget and would never trip it, yet width 16 is where the walk first costs tens of milliseconds -- three orders of magnitude above the worst measured cost of a certificate that fails to apply.

Equations

• Hex.QuadraticNormCertificate.widthFloor = 16

def Hex.QuadraticNormCertificate.certify? (f : ZPoly) : Option QuadraticNormCertificate

Recover a certificate for f and check it.

some cert means cert.check f = true, so f is a certified-irreducible iterated quadratic norm; none carries no claim either way.

Equations

• Hex.QuadraticNormCertificate.certify? f = match Hex.QuadraticNormCertificate.recover? f with | some cert => if cert.check f = true then some cert else none | none => none

theorem Hex.QuadraticNormCertificate.check_of_certify? {f : ZPoly} {cert : QuadraticNormCertificate} (h : certify? f = some cert) : cert.check f = true

A recovered certificate has passed its own check: this is the only property of the search anything downstream may use.

def Hex.quadraticNormCertified (core : ZPoly) (width : Nat) : Bool

Does the budget-gated iterated-quadratic-norm certificate prove core irreducible?

width is the number of modular factors, known once the modular factorization is in hand. Below Hex.QuadraticNormCertificate.widthFloor the answer is false with nothing constructed, so a row that recombines cheaply pays nothing for the attempt. Above it, Hex.QuadraticNormCertificate.recover? proposes a translation and radicands and Hex.QuadraticNormCertificate.check decides them; a failure at either step is an ordinary false carrying no state.

Normalization. Every F(c; d) is monic, so the certificate applies to core exactly when core has leading coefficient 1 or -1, and the only normalization is negation: -1 is a unit of ℤ[X], so core and -core are irreducible together. There is no scaling and no content division, because a primitive integer polynomial with leading coefficient outside {1, -1} is never ± F(c; d); Hex.ZPoly.normalizePrimitiveSign, inside the check, is that negation and nothing else.

Equations

• Hex.quadraticNormCertified core width = (decide (Hex.QuadraticNormCertificate.widthFloor ≤ width) && (Hex.QuadraticNormCertificate.certify? core).isSome)