theorem HexPolyTheory.Interpret.pseudo_multiplier {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b) (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p q : Hex.DensePoly E) : f (p.pseudoDiv q).multiplier = f q.leadingCoeff ^ p.pseudoExponent q

The multiplier agrees with the fixed leading-coefficient power after interpretation.

theorem HexPolyTheory.Interpret.pseudo_multiplier_ne_zero {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b) (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p q : Hex.DensePoly E) (hq : q ≠ 0) : f (p.pseudoDiv q).multiplier ≠ 0

Every nonzero divisor has a nonzero recorded multiplier.

theorem HexPolyTheory.Interpret.pseudo_reconstruct {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b) (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p q : Hex.DensePoly E) : Polynomial.C (f (p.pseudoDiv q).multiplier) * interpret f hz p = interpret f hz (p.pseudoDiv q).quotient * interpret f hz q + interpret f hz (p.pseudoDiv q).remainder

Reconstruction is an identity of interpreted polynomials, not stored representatives.

theorem HexPolyTheory.Interpret.pseudo_remainder_degree {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (p q : Hex.DensePoly E) (hq : q ≠ 0) : interpret f hz (p.pseudoDiv q).remainder = 0 ∨ (interpret f hz (p.pseudoDiv q).remainder).natDegree < (interpret f hz q).natDegree

Interpreted remainders have strictly smaller degree, with zero recorded separately.

theorem HexPolyTheory.Interpret.pseudo_rem {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b) (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p q : Hex.DensePoly E) : interpret f hz (p.pseudoDiv q).remainder = Polynomial.C (f (p.pseudoDiv q).multiplier) * (interpret f hz p % interpret f hz q)

The pseudo-remainder is the field remainder times its recorded nonzero scalar.

theorem HexPolyTheory.Interpret.pseudo_divMod {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b) (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p q : Hex.DensePoly E) : (interpret f hz (p.pseudoDiv q).quotient, interpret f hz (p.pseudoDiv q).remainder) = (Polynomial.C (f (p.pseudoDiv q).multiplier) * (interpret f hz p / interpret f hz q), Polynomial.C (f (p.pseudoDiv q).multiplier) * (interpret f hz p % interpret f hz q))

Both pseudo-division outputs agree with field division after scaling by the recorded multiplier; no inverse operation is required on the source carrier.

theorem HexPolyTheory.Interpret.dvd_pseudoGcd {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b) (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p q : Hex.DensePoly E) (d : Polynomial K) : d ∣ interpret f hz (p.pseudoGcd q) ↔ d ∣ interpret f hz p ∧ d ∣ interpret f hz q

The actual fraction-free gcd has precisely the common divisors of the inputs in the semantic field. It need not be a polynomial gcd over the stored domain.

theorem HexPolyTheory.Interpret.interpret_pseudoGcd {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b) (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p q : Hex.DensePoly E) : Associated (interpret f hz (p.pseudoGcd q)) (EuclideanDomain.gcd (interpret f hz p) (interpret f hz q))

Plain pseudo-gcd agrees with field gcd up to a nonzero scalar, including zero inputs.

theorem HexPolyTheory.Interpret.positive_reconstruct {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b) (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) [Neg E] (hn : ∀ (a : E), f (-a) = -f a) (sign : E → ℤ) (p q : Hex.DensePoly E) : Polynomial.C (f (Hex.DensePoly.positivePseudoDiv sign p q).multiplier) * interpret f hz p = interpret f hz (Hex.DensePoly.positivePseudoDiv sign p q).quotient * interpret f hz q + interpret f hz (Hex.DensePoly.positivePseudoDiv sign p q).remainder

Correcting a negative multiplier negates the quotient and remainder too.

theorem HexPolyTheory.Interpret.positive_remainder_degree {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (hs : ∀ (a b : E), f (a - b) = f a - f b) [Neg E] (sign : E → ℤ) (p q : Hex.DensePoly E) (hq : q ≠ 0) : interpret f hz (Hex.DensePoly.positivePseudoDiv sign p q).remainder = 0 ∨ (interpret f hz (Hex.DensePoly.positivePseudoDiv sign p q).remainder).natDegree < (interpret f hz q).natDegree

Sign correction preserves the strict interpreted remainder-degree bound.

theorem HexPolyTheory.Interpret.positive_multiplier {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b) (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) [Neg E] [LinearOrder K] [IsStrictOrderedRing K] (hn : ∀ (a : E), f (-a) = -f a) (sign : E → ℤ) (hsign : ∀ (a : E), sign a < 0 ↔ f a < 0) (p q : Hex.DensePoly E) (hq : q ≠ 0) : 0 < f (Hex.DensePoly.positivePseudoDiv sign p q).multiplier

The signed variant returns a strictly positive interpreted multiplier.