theorem Hex.FpPoly.Quotient.add_eq_reduce_val {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (a b : g.Quotient hmonic hg_pos) : a + b = reduce (a.val + b.val)

A quotient sum equals the reduction of the underlying polynomial sum.

theorem Hex.FpPoly.Quotient.mul_eq_reduce_val {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (a b : g.Quotient hmonic hg_pos) : a * b = reduce (a.val * b.val)

A quotient product equals the reduction of the underlying polynomial product.

theorem Hex.FpPoly.Quotient.mul_pow {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (a b : g.Quotient hmonic hg_pos) (n : Nat) : (a * b) ^ n = a ^ n * b ^ n

Power of a product factors out in the quotient.

theorem Hex.FpPoly.Quotient.pow_eq_reduce_linearPow {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (a : g.Quotient hmonic hg_pos) (n : Nat) : a ^ n = reduce (a.val.linearPow n)

For any quotient element a and exponent n, the nth power of a equals the reduction of the polynomial-level nth power of its representative.

theorem Hex.FpPoly.Quotient.reduce_powModMonicLinear_eq_pow {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (base : FpPoly p) (n : Nat) : reduce (base.powModMonicLinear g hmonic n) = reduce base ^ n

Structural modular exponentiation represents ordinary powering in the quotient.

The executable loop reduces after every multiplication; quotient reduction forgets those intermediate choices and returns the power of the base class.

theorem Hex.FpPoly.Quotient.add_pow_prime {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (a b : g.Quotient hmonic hg_pos) : (a + b) ^ p = a ^ p + b ^ p

Freshman's dream on the quotient (prime case): raising a sum to the characteristic distributes additively.

theorem Hex.FpPoly.Quotient.add_pow_pPow {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (a b : g.Quotient hmonic hg_pos) (k : Nat) : (a + b) ^ p ^ k = a ^ p ^ k + b ^ p ^ k

Freshman's dream on the quotient, iterated: raising a sum to p ^ k distributes additively for every k.

theorem Hex.FpPoly.Quotient.linearPow_C_pow_prime {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (c : ZMod64 p) : linearPow (DensePoly.C c) p = DensePoly.C c

linearPow (C c) p = C c over F_p: Fermat for constants in characteristic p.

theorem Hex.FpPoly.Quotient.reduce_C_pow_prime_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (c : ZMod64 p) : reduce (DensePoly.C c) ^ p = reduce (DensePoly.C c)

Constants are fixed by the prime-power Frobenius on the quotient.

theorem Hex.FpPoly.Quotient.reduce_C_pow_pPow_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (c : ZMod64 p) (k : Nat) : reduce (DensePoly.C c) ^ p ^ k = reduce (DensePoly.C c)

Constants are fixed by every iterate of the Frobenius on the quotient.

theorem Hex.FpPoly.Quotient.X_pow_pPowN {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (hp_pos : 0 < p) {n : Nat} (hX : X ^ p ^ n = X) (m : Nat) : (X ^ m) ^ p ^ n = X ^ m

Iterated Frobenius is the identity on Quotient.X powers, given a fixed point at Quotient.X itself.

theorem Hex.FpPoly.Quotient.reduce_monomial_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (m : Nat) (c : ZMod64 p) : reduce (DensePoly.monomial m c) = reduce (DensePoly.C c) * X ^ m

A monomial in the quotient equals reduce (C c) * X^m.

theorem Hex.FpPoly.Quotient.Internal.evalCoeffList_pow_prime {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (β : g.Quotient hmonic hg_pos) (cs : List (ZMod64 p)) : evalCoeffList (List.map (fun (c : ZMod64 p) => reduce (DensePoly.C c)) cs) (β ^ p) = evalCoeffList (List.map (fun (c : ZMod64 p) => reduce (DensePoly.C c)) cs) β ^ p

Evaluation commutes with the Frobenius.

g(β^p) = g(β)^p in characteristic p: freshman's dream distributes the power over the Horner sum, and Fermat fixes each coefficient, since the coefficients live in the prime field. This is the step that identifies composing with x^p mod f as the p-th power map on residues, which is what makes the Conway norm computable by Frobenius iteration rather than by modular exponentiation.

theorem Hex.FpPoly.Quotient.Internal.eval_pow_prime {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (f : FpPoly p) (β : g.Quotient hmonic hg_pos) : eval f (β ^ p) = eval f β ^ p

The FpPoly-level form of Hex.FpPoly.Quotient.Internal.evalCoeffList_pow_prime.

theorem Hex.FpPoly.Quotient.pow_pPowN_eq_self_of_pow_pPowN_X_eq_X {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} {hmonic : DensePoly.Monic g} {hg_pos : 0 < DensePoly.natDegree g} (_hg_irr : g.Irreducible) {n : Nat} (hX : X ^ p ^ n = X) (β : g.Quotient hmonic hg_pos) : β ^ p ^ n = β

If the Frobenius iterate β ↦ β ^ (p ^ n) fixes Quotient.X, it fixes every quotient element.

The irreducibility hypothesis is recorded for downstream callers but is not used in the proof: the X-generation argument is purely an algebra fact about F_p[X]/(g) for any monic positive-degree g.