`hex`'s dense polynomial storage: a non-injective refinement at `map2a` #

leanprover/hex's polynomial machinery (Berlekamp–Zassenhaus factoring, Hensel lifting) stores a polynomial as a dense coefficient list — the CoqEAL seqpoly representation. That storage is not injective as a refinement of the mathematical polynomial: trailing zeros are redundant, so [1,2] and [1,2,0] denote the same polynomial 2X + 1. This module builds that refinement and pins down the exact Param level it reaches (possibility 2): a non-bijective refinement lands at forward/backward map2a, the graded engine's sweet spot, and provably cannot reach map2b/map3/map4 — the levels an Equiv-based or univalent transfer would demand.

The refinement relation #

Two dense lists are related when their coefficient functions agree:

SameCoeff l l' := ∀ i, l.getD i 0 = l'.getD i 0.

This is exactly the seqpoly refinement (agree as polynomials). It is reflexive, symmetric, transitive, and strictly coarser than equality — the quotient by trailing zeros. The abstract polynomial is the SameCoeff-class; the two carrier types coincide (List ℤ) because the quotient lives in the relation, not the type. Reaching Mathlib's Polynomial ℤ as the abstract side (via Polynomial.coeff) is an orthogonal finite-support packaging and does not change the level analysis.

Why the level is exactly `map2a` #

seqPolyParam : Param .map2a .map2a carries SameCoeff with the identity map each way: map_in_R (map l = l' → SameCoeff l l') is reflexivity after subst, so map2a holds in both directions. But map2b's R_in_map (SameCoeff l l' → id l = l', i.e. SameCoeff l l' → l = l') is false: seqPoly_not_injective exhibits SameCoeff [1,2] [1,2,0] with [1,2] ≠ [1,2,0]. So the refinement stops at map2a; map3 (both inclusions) and map4 (univalent) are a fortiori unreachable. This is the structural reason the graded hierarchy is the right tool for hex's storage: a two-sided-equivalence framework would reject this refinement outright; map2a is precisely what forallTransfer/TransferDom consume.

The dense polynomial carrier and its coefficient view #

source

@[reducible, inline]

abbrev Transfer.Param.HexPoly :

Type

hex's dense polynomial storage: a coefficient list (low degree first).

Equations

Transfer.Param.HexPoly = List ℤ

Instances For

source

def Transfer.Param.coeffOf (l : HexPoly) (i : ℕ) :

ℤ

The coefficient at degree i (out-of-range degrees are 0).

Equations

Transfer.Param.coeffOf l i = List.getD l i 0

Instances For

source

def Transfer.Param.SameCoeff (l l' : HexPoly) :

Prop

The seqpoly refinement relation: two dense lists denote the same polynomial when all coefficients agree. Reflexive, and strictly coarser than equality (trailing zeros are identified).

Equations

Transfer.Param.SameCoeff l l' = ∀ (i : ℕ), Transfer.Param.coeffOf l i = Transfer.Param.coeffOf l' i

Instances For

source

theorem Transfer.Param.SameCoeff.refl (l : HexPoly) :

SameCoeff l l

The refinement witness — forward/backward `map2a`, no higher #

source

def Transfer.Param.seqPolyParam :

Param MapClass.map2a MapClass.map2a HexPoly HexPoly

The seqpoly refinement as a Param .map2a .map2a HexPoly HexPoly. Each direction uses the identity map with map_in_R discharged by reflexivity (map l = l' → SameCoeff l l' after subst). It reaches map2a both ways but not map2b (see seqPoly_not_injective).

Equations

Transfer.Param.seqPolyParam = { R := Transfer.Param.SameCoeff, fwd := { map := id, map_in_R := ⋯ }, bwd := { map := id, map_in_R := ⋯ } }

Instances For

The `map2a` boundary: non-injectivity refutes `map2b`/`map3` #

source

theorem Transfer.Param.sameCoeff_snoc_zero_pair :

SameCoeff [1, 2] [1, 2, 0]

[1,2] and [1,2,0] have identical coefficients (2X + 1): the trailing zero is redundant.

source

theorem Transfer.Param.seqPoly_not_injective :

∃ (l : HexPoly ), ∃ (l' : HexPoly ), SameCoeff l l' ∧ l ≠ l'

The refinement is non-injective: SameCoeff holds between distinct lists. This refutes map2b's inclusion R_in_map : SameCoeff l l' → l = l' (with the identity map), so the witness cannot be promoted past map2a. The non-bijectivity is forced by the representation (trailing zeros), not an artefact of the proof.

Transferring a coefficient-invariant property across the quotient #

The domain at the ∀-rule level (.map0, .map2a) forgets the forward map2a of seqPolyParam. param_transfer then moves any coefficient-invariant statement across trailing-zero padding — a property proved for one dense representation holds for every SameCoeff-equivalent one.

source

def Transfer.Param.seqPolyDom :

Param MapClass.map0 MapClass.map2a HexPoly HexPoly

The seqpoly refinement at the level forallTransfer/TransferDom consume.

Equations