def Hex.obstructionPrime : Nat

The fixed word-sized prime carrying the divisibility obstruction.

Any prime below 2 ^ 31 satisfies ZMod64.Bounds; 2 ^ 26 - 5 is large enough that an accidental zero remainder costs at most one exact division that would have been performed anyway, and small enough that its trial-division primality proof is cheap to check in the kernel.

Equations

• Hex.obstructionPrime = 67108859

instance Hex.boundsObstructionPrime : ZMod64.Bounds obstructionPrime

obstructionPrime fits the word-arithmetic bounds of ZMod64.

theorem Hex.obstructionPrime_prime : Nat.Prime obstructionPrime

obstructionPrime is prime, by kernel-checked trial division.

instance Hex.instPrimeModulusObstructionPrime : ZMod64.PrimeModulus obstructionPrime

ZMod64 arithmetic modulo obstructionPrime is arithmetic in a prime field, by obstructionPrime_prime.

def Hex.obstructionImage (f : ZPoly) : FpPoly obstructionPrime

The image of an integer polynomial in 𝔽_q[X].

Equations

• Hex.obstructionImage f = Hex.ZPoly.modP Hex.obstructionPrime f

def Hex.TargetImage (target : ZPoly) : Type

The recombination target's image in 𝔽_q[X], computed once for a whole subset-cardinality level rather than once per candidate.

The subtype proof pins the stored array to the reference reduction, so a traversal reading this is interchangeable with one reducing the target at every leaf.

Equations

• Hex.TargetImage target = { image : Hex.FpPoly Hex.obstructionPrime // image = Hex.obstructionImage target }

def Hex.targetImage (target : ZPoly) : TargetImage target

Reduce a recombination target once.

Equations

• Hex.targetImage target = ⟨Hex.obstructionImage target, ⋯⟩

def Hex.obstructionRemainder (target candidate : ZPoly) : FpPoly obstructionPrime

Reference form of the obstruction: the 𝔽_q[X] remainder of the reduced target by the reduced candidate.

Equations

• Hex.obstructionRemainder target candidate = Hex.DensePoly.mod (Hex.obstructionImage target) (Hex.obstructionImage candidate)

def Hex.obstructs {target : ZPoly} (cached : TargetImage target) (candidate : ZPoly) : Bool

The divisibility obstruction: true exactly when the reduced candidate leaves a nonzero remainder in the reduced target, which certifies that the candidate does not divide the target over ℤ.

The divisor's leading-coefficient inverse is computed once for the whole long-division pass, which is the only difference from obstructionRemainder.

Equations

• Hex.obstructs cached candidate = !Hex.DensePoly.isZero (cached.val.modCached (Hex.obstructionImage candidate))

theorem Hex.obstructs_eq {target : ZPoly} (cached : TargetImage target) (candidate : ZPoly) : obstructs cached candidate = !DensePoly.isZero (obstructionRemainder target candidate)

The optimized obstruction computes the reference remainder.

theorem Hex.obstructionRemainder_eq_zero_of_dvd {target candidate : ZPoly} (hdvd : candidate ∣ target) : obstructionRemainder target candidate = 0

Reduction modulo q carries integer divisibility into 𝔽_q[X], where division by the image leaves no remainder. This is the whole content of the obstruction: it fires only on candidates that cannot divide.

theorem Hex.obstructs_eq_false_of_dvd {target : ZPoly} (cached : TargetImage target) {candidate : ZPoly} (hdvd : candidate ∣ target) : obstructs cached candidate = false

No false rejection: a genuine divisor is never obstructed.

theorem Hex.not_dvd_of_obstructs {target : ZPoly} (cached : TargetImage target) {candidate : ZPoly} (hobstructs : obstructs cached candidate = true) : ¬candidate ∣ target

An obstructed candidate does not divide the target.

theorem Hex.exactQuotient?_eq_none_of_obstructs {target : ZPoly} (cached : TargetImage target) {candidate : ZPoly} (hobstructs : obstructs cached candidate = true) : exactQuotient? target candidate = none

An obstructed candidate would have failed exact division, so skipping the exact division changes nothing. This is the equation the traversal's leaf rewrites through.

def Hex.obstructedQuotient? {target : ZPoly} (cached : TargetImage target) (candidate : ZPoly) : Option ZPoly

Exact division, guarded by the obstruction.

This is the single production entry point for "reject over 𝔽_q, otherwise divide exactly": both recombination traversals reach exact division only through it, so obstructedQuotient?_eq is the one equation that has to hold for either of them to be unchanged.

Equations

• Hex.obstructedQuotient? cached candidate = if Hex.obstructs cached candidate = true then none else Hex.exactQuotient? target candidate

@[simp]

theorem Hex.obstructedQuotient?_eq {target : ZPoly} (cached : TargetImage target) (candidate : ZPoly) : obstructedQuotient? cached candidate = exactQuotient? target candidate

Guarding exact division by the obstruction does not change its value.