24.1. Introduction🔗

HexResultant computes polynomial resultants and discriminants without constructing a Sylvester matrix. Its Brown subresultant pseudo-remainder sequence stays in the coefficient ring and uses exact division only at the points where the recurrence proves divisibility. This matters for the tower algorithms later in the manual: their coefficient rings are executable number-field presentations, not Mathlib fields.

The computational library is Mathlib-free. HexResultantMathlib states the correspondence between the final executable value and Polynomial.resultant, including specialization and discriminant conventions.

Exact division is governed by the algebraic law ExactDivLaws, which the correctness proofs discharge rather than assuming laws for the total / operation. The executable carries no runtime divisibility check; the algorithm only invokes division at factors whose divisibility the Brown recurrence has established:

Hex.ExactDivLaws.{u} (R : Type u) [Zero R] [Mul R] [Div R] : Prop
Hex.ExactDivLaws.{u} (R : Type u) [Zero R]
  [Mul R] [Div R] : Prop

Hex.ExactDivLaws.mk.{u}

mul_div_cancel_right : ∀ (a b : R), b ≠ 0 → a * b / b = a