theorem Hex.NumberTower.Norm.rawPoly_resultant (level : Level) (lower : List Level) (hlower : LevelsValid lower) (hinjective : LevelSemantics.DenoteInjective lower) (hinv : ∀ (a : Arithmetic.Coeff lower), LevelSemantics.coeffDenote lower a⁻¹ = (LevelSemantics.coeffDenote lower a)⁻¹) (f : Array (Array ℚ)) (c : ℤ) : Factor.rawPoly lower (oneLevel level lower f c) = (definingOuter level lower).resultant (shiftedOuter level lower f c)

The decoded executable norm agrees with the dense resultant over a validated lower field. The quadratic branch uses algebraic equivalence, followed by the same exact coordinate round trip as the general fallback.

theorem Hex.NumberTower.Norm.oneLevel_resultant (level : Level) (lower : List Level) (hlower : LevelsValid lower) (hinjective : LevelSemantics.DenoteInjective lower) (hinv : ∀ (a : Arithmetic.Coeff lower), LevelSemantics.coeffDenote lower a⁻¹ = (LevelSemantics.coeffDenote lower a)⁻¹) (f : Array (Array ℚ)) (c : ℤ) : rawPolynomial lower (DensePoly.ofCoeffs (Array.map (Arithmetic.Coeff.ofData lower) (oneLevel level lower f c))) = (rawOuter lower (definingOuter level lower)).resultant (rawOuter lower (shiftedOuter level lower f c)) (definingOuter level lower).natDegree (shiftedOuter level lower f c).natDegree

One executable Trager elimination step is the corresponding polynomial resultant after semantic interpretation of the lower tower.

theorem Hex.NumberTower.Norm.oneLevel_shift_zero (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (f : Array (Array ℚ)) (c : ℤ) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; Factor.rawPoly lower (oneLevel level lower (Factor.shiftTop level lower f c) 0) = Factor.rawPoly lower (oneLevel level lower f c)

Shifting a current-level polynomial first and then eliminating with zero shift gives the same lower-field norm as eliminating with that shift.

theorem Hex.NumberTower.Norm.shifted_dvd_norm (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (f : Array (Array ℚ)) (c : ℤ) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) (Factor.shiftTop level lower f c)) ∣ Polynomial.map (lowerHom level lower hvalid hinjectiveTop) (HexPolyMathlib.toPolynomial (Factor.rawPoly lower (oneLevel level lower f c)))

The shifted current-level polynomial divides the lifted one-level norm. This is the Bézout divisibility direction behind Trager recovery.

theorem Hex.NumberTower.Norm.oneLevel_ne_zero (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (f : Array (Array ℚ)) (c : ℤ) (hf : Factor.rawPoly (level :: lower) f ≠ 0) : Factor.rawPoly lower (oneLevel level lower f c) ≠ 0

A one-level Trager norm of a nonzero current-level polynomial is nonzero.

theorem Hex.NumberTower.Norm.iterated_ne_zero (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (f : Array (Array ℚ)) (hf : Factor.rawPoly levels f ≠ 0) : Factor.rawPoly [] (iterated levels f) ≠ 0

Eliminating every validated tower level preserves nonzeroness.

theorem Hex.NumberTower.Norm.oneLevel_mul (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (a b : DensePoly (Arithmetic.Coeff (level :: lower))) (c : ℤ) : Factor.rawPoly lower (oneLevel level lower (Factor.polyCoords (a * b)) c) = Factor.rawPoly lower (oneLevel level lower (Factor.polyCoords a) c) * Factor.rawPoly lower (oneLevel level lower (Factor.polyCoords b) c)

The one-level Trager norm is multiplicative on canonically encoded current-level polynomials.

theorem Hex.NumberTower.Norm.oneLevel_lift (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (q : DensePoly (Arithmetic.Coeff lower)) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; have lifted := HexPolyMathlib.ofPolynomial (Polynomial.map (lowerHom level lower hvalid hinjectiveTop) (HexPolyMathlib.toPolynomial q)); HexPolyMathlib.toPolynomial (Factor.rawPoly lower (oneLevel level lower (Factor.polyCoords lifted) 0)) = HexPolyMathlib.toPolynomial q ^ level.degree

The norm of a coefficientwise lower-field lift is the expected power by the relative degree.

theorem Hex.NumberTower.Norm.findSquarefreeShift_isSome_of_injective (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (f : Array (Array ℚ)) (hdegree : 0 < f.size - 1) (hsquarefree : Squarefree (rawPolynomial (level :: lower) (DensePoly.ofCoeffs (Array.map (Arithmetic.Coeff.ofData (level :: lower)) f)))) : (findSquarefreeShift level lower f).isSome = true

The finite characteristic-zero collision bound finds a squarefree norm for a squarefree positive-degree component whenever the current canonical coefficient interpretation is injective. This parameterized form is the one used by the level-by-level Trager induction.