From fa3aa4aa09b498b2e78b1d7b77c23420be455a66 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:26:26 -0400 Subject: [PATCH 1/7] feat(foundations): Galois rings, ring Lagrange interpolation and the p-adic valuation of Q[X]/(f) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit T2.2 of #1538 (Theorem D.1 of OpenAI2026ETH, §D.4.1, pp. 57-58). - GaloisRing p n f = (Z/p^n)[X]/(f): local with maximal ideal (p), residue field F_p[X]/(f) = GaloisField p (deg f), units = nonzero mod p; distinct digit lifts differ by units, so ring Lagrange interpolation holds there. - Lagrange.ringInterpolate: Lagrange interpolation over a commutative ring at nodes with unit differences (Mathlib's Lagrange.interpolate needs a field). - AdjoinRoot.padicValuation: for f monic and irreducible mod p, the largest p-adic valuation of a coordinate is a valuation of Q[X]/(f); its valuation ring is Z_(p)[X]/(f), whose elements of valuation one are units. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 3 + .../Data/Polynomial/RingLagrange.lean | 154 ++++++++ .../Padics/AdjoinRootValuation.lean | 303 +++++++++++++++ .../Foundations/RingTheory/GaloisRing.lean | 351 ++++++++++++++++++ .../Data/Polynomial/RingLagrange.lean | 54 +++ .../Padics/AdjoinRootValuation.lean | 98 +++++ .../Foundations/RingTheory/GaloisRing.lean | 111 ++++++ 7 files changed, 1074 insertions(+) create mode 100644 Complexity/Foundations/Data/Polynomial/RingLagrange.lean create mode 100644 Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean create mode 100644 Complexity/Foundations/RingTheory/GaloisRing.lean create mode 100644 ComplexityTests/Foundations/Data/Polynomial/RingLagrange.lean create mode 100644 ComplexityTests/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean create mode 100644 ComplexityTests/Foundations/RingTheory/GaloisRing.lean diff --git a/Complexity.lean b/Complexity.lean index 1cd97a4651..7ae579ac43 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2679,6 +2679,7 @@ public import Complexity.Foundations.Data.Polynomial.CoeffNorm1 public import Complexity.Foundations.Data.Polynomial.HermiteInterpolation public import Complexity.Foundations.Data.Polynomial.ParityAmplifier public import Complexity.Foundations.Data.Polynomial.ParityAmplifierDegree +public import Complexity.Foundations.Data.Polynomial.RingLagrange public import Complexity.Foundations.Data.Polynomial.SignQueries public import Complexity.Foundations.Data.Polynomial.StagedJetArithmetic public import Complexity.Foundations.Data.Rat.Basic @@ -2748,6 +2749,7 @@ public import Complexity.Foundations.NumberTheory.AKS.Criterion public import Complexity.Foundations.NumberTheory.AKS.Introspective public import Complexity.Foundations.NumberTheory.AKS.SmallR public import Complexity.Foundations.NumberTheory.Harmonic +public import Complexity.Foundations.NumberTheory.Padics.AdjoinRootValuation public import Complexity.Foundations.NumberTheory.PrimeCounting public import Complexity.Foundations.NumberTheory.PrimeWindow public import Complexity.Foundations.NumberTheory.SqrtPrimeWindow @@ -2777,6 +2779,7 @@ public import Complexity.Foundations.Relation.InductiveCounting public import Complexity.Foundations.Relation.RelatesWithinSteps public import Complexity.Foundations.RingTheory.CyclicIntRing public import Complexity.Foundations.RingTheory.CyclicIntRing.Coefficients +public import Complexity.Foundations.RingTheory.GaloisRing public import Complexity.Foundations.Semantics.Stateful.Amortized public import Complexity.Foundations.Semantics.Stateful.Basic public import Complexity.Foundations.Semantics.Stateful.Composition diff --git a/Complexity/Foundations/Data/Polynomial/RingLagrange.lean b/Complexity/Foundations/Data/Polynomial/RingLagrange.lean new file mode 100644 index 0000000000..2ee13b0100 --- /dev/null +++ b/Complexity/Foundations/Data/Polynomial/RingLagrange.lean @@ -0,0 +1,154 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate (Mathlib, `Mathlib/LinearAlgebra/Lagrange.lean`) + +public import Complexity.Init +public import Mathlib.LinearAlgebra.Lagrange + +/-! +# Lagrange interpolation over a commutative ring + +Mathlib's `Lagrange.interpolate` works over a field. Over a commutative ring `R`, interpolation at +nodes `v i`, `i ∈ s`, still works when the nodes have *unit differences*: every `v i - v j` with +`i ≠ j` is a unit. Galois rings such as `(ℤ / 2 ^ p)[U] / (f)` are the motivating example; they +are not domains, but lifts of distinct residue-field elements differ by units. + +The Lagrange basis polynomial at `i` is `∏_{j ∈ s, j ≠ i} (X - v j) / (v i - v j)`, where the +division is multiplication by `Ring.inverse (v i - v j)` (`Lagrange.ringBasis`). It is one at +`v i` and zero at the other nodes, so `Lagrange.ringInterpolate s v r = ∑ i ∈ s, r i • basis i` +takes the value `r i` at `v i`. A polynomial of degree less than `#s` that vanishes at all nodes is +zero, because the factors `X - v i` are pairwise coprime; hence every polynomial of degree less +than `#s` is the interpolant of its values (`Lagrange.eq_ringInterpolate`). Over a field these +are Mathlib's `Lagrange.basis` and `Lagrange.interpolate` +(`Lagrange.ringInterpolate_eq_interpolate`). + +## Main definitions + +* `Lagrange.ringBasis`: the Lagrange basis polynomial, with `Ring.inverse` for division. +* `Lagrange.ringInterpolate`: Lagrange interpolation over a commutative ring, as a linear map. + +## Main results + +* `Lagrange.eval_ringInterpolate_at_node`: the interpolant takes the prescribed values. +* `Lagrange.degree_ringInterpolate_lt`: it has degree less than the number of nodes. +* `Lagrange.eq_zero_of_degree_lt_of_eval_eq_zero`: uniqueness at nodes with unit differences. +* `Lagrange.eq_ringInterpolate`: a polynomial of degree less than `#s` is the interpolant of its + values. +* `Lagrange.ringInterpolate_eq_interpolate`: over a field, this is `Lagrange.interpolate`. +-/ + +public section + +namespace Lagrange + +open Polynomial Finset + +variable {R : Type*} [CommRing R] {ι : Type*} [DecidableEq ι] {s : Finset ι} {v : ι → R} + {i j : ι} + +/-- The Lagrange basis polynomial `∏_{j ∈ s, j ≠ i} (X - v j) / (v i - v j)` over a commutative +ring, where division by `v i - v j` is multiplication by `Ring.inverse (v i - v j)`. When the nodes +have unit differences it is one at `v i` and zero at the other nodes. -/ +@[expose] noncomputable def ringBasis (s : Finset ι) (v : ι → R) (i : ι) : R[X] := + ∏ j ∈ s.erase i, C (Ring.inverse (v i - v j)) * (X - C (v j)) + +/-- **Lagrange interpolation over a commutative ring**: `∑ i ∈ s, r i • ringBasis s v i`. At nodes +with unit differences, it is the unique polynomial of degree less than `#s` taking the value `r i` +at `v i`. -/ +@[expose] noncomputable def ringInterpolate (s : Finset ι) (v : ι → R) : (ι → R) →ₗ[R] R[X] where + toFun r := ∑ i ∈ s, C (r i) * ringBasis s v i + map_add' r r' := by + simp only [Pi.add_apply, C_add, add_mul, sum_add_distrib] + map_smul' c r := by + simp only [Pi.smul_apply, smul_eq_mul, C_mul, RingHom.id_apply, smul_sum, mul_assoc, + smul_eq_C_mul] + +theorem ringInterpolate_apply (s : Finset ι) (v : ι → R) (r : ι → R) : + ringInterpolate s v r = ∑ i ∈ s, C (r i) * ringBasis s v i := + rfl + +/-- The basis polynomial at `i` is one at its own node. -/ +theorem eval_ringBasis_self (hvs : (s : Set ι).Pairwise fun i j => IsUnit (v i - v j)) + (hi : i ∈ s) : (ringBasis s v i).eval (v i) = 1 := by + rw [ringBasis, eval_prod] + refine prod_eq_one fun j hj => ?_ + obtain ⟨hji, hj⟩ := mem_erase.mp hj + rw [eval_mul, eval_C, eval_sub, eval_X, eval_C] + exact Ring.inverse_mul_cancel _ (hvs hi hj (Ne.symm hji)) + +/-- The basis polynomial at `i` vanishes at every other node. -/ +theorem eval_ringBasis_of_ne (hij : i ≠ j) (hj : j ∈ s) : (ringBasis s v i).eval (v j) = 0 := by + rw [ringBasis, eval_prod] + refine prod_eq_zero (mem_erase.mpr ⟨Ne.symm hij, hj⟩) ?_ + simp only [eval_mul, eval_sub, eval_X, eval_C, sub_self, mul_zero] + +theorem natDegree_ringBasis_le (s : Finset ι) (v : ι → R) (i : ι) : + (ringBasis s v i).natDegree ≤ #(s.erase i) := by + refine (natDegree_prod_le _ _).trans + ((sum_le_sum fun j _ => ?_).trans_eq (card_eq_sum_ones _).symm) + exact (natDegree_C_mul_le _ _).trans (natDegree_X_sub_C_le _) + +/-- The basis polynomial at a node has degree less than the number of nodes. -/ +theorem degree_ringBasis_lt (hi : i ∈ s) : (ringBasis s v i).degree < #s := by + refine (degree_le_natDegree).trans_lt ?_ + have h := natDegree_ringBasis_le s v i + rw [card_erase_of_mem hi] at h + have hs : 0 < #s := card_pos.mpr ⟨i, hi⟩ + exact_mod_cast (show (ringBasis s v i).natDegree < #s by omega) + +/-- The interpolant has degree less than the number of nodes. -/ +theorem degree_ringInterpolate_lt (r : ι → R) : (ringInterpolate s v r).degree < #s := by + rw [← mem_degreeLT, ringInterpolate_apply] + refine Submodule.sum_mem _ fun i hi => ?_ + rw [← smul_eq_C_mul] + exact Submodule.smul_mem _ _ (mem_degreeLT.mpr (degree_ringBasis_lt hi)) + +/-- **The interpolant takes the prescribed values** at nodes with unit differences. -/ +theorem eval_ringInterpolate_at_node (hvs : (s : Set ι).Pairwise fun i j => IsUnit (v i - v j)) + (r : ι → R) (hi : i ∈ s) : (ringInterpolate s v r).eval (v i) = r i := by + rw [ringInterpolate_apply, eval_finsetSum, sum_eq_single_of_mem i hi, eval_mul, eval_C, + eval_ringBasis_self hvs hi, mul_one] + intro j _ hji + rw [eval_mul, eval_ringBasis_of_ne hji hi, mul_zero] + +omit [DecidableEq ι] in +/-- **Uniqueness of interpolation over a commutative ring.** A polynomial of degree less than +`#s` that vanishes at nodes with unit differences is zero: the factors `X - v i` are pairwise +coprime, so their product, of degree `#s`, divides it. -/ +theorem eq_zero_of_degree_lt_of_eval_eq_zero + (hvs : (s : Set ι).Pairwise fun i j => IsUnit (v i - v j)) {f : R[X]} (hf : f.degree < #s) + (h0 : ∀ i ∈ s, f.eval (v i) = 0) : f = 0 := by + nontriviality R + by_contra hne + have hdvd : nodal s v ∣ f := by + rw [nodal] + refine prod_dvd_of_coprime (fun i hi j hj hij => ?_) fun i hi => ?_ + · exact isCoprime_X_sub_C_of_isUnit_sub (hvs hi hj hij) + · exact dvd_iff_isRoot.mpr (h0 i hi) + exact nodal_monic.not_dvd_of_degree_lt hne (by rwa [degree_nodal]) hdvd + +/-- **Every polynomial of degree less than `#s` is the interpolant of its values** at nodes with +unit differences. -/ +theorem eq_ringInterpolate (hvs : (s : Set ι).Pairwise fun i j => IsUnit (v i - v j)) + {f : R[X]} (hf : f.degree < #s) : f = ringInterpolate s v (fun i => f.eval (v i)) := by + refine sub_eq_zero.mp (eq_zero_of_degree_lt_of_eval_eq_zero hvs + ((degree_sub_le _ _).trans_lt (max_lt hf (degree_ringInterpolate_lt _))) fun i hi => ?_) + rw [eval_sub, eval_ringInterpolate_at_node hvs _ hi, sub_self] + +/-- Over a field, `ringBasis` is Mathlib's `Lagrange.basis`. -/ +theorem ringBasis_eq_basis {F : Type*} [Field F] (s : Finset ι) (v : ι → F) (i : ι) : + ringBasis s v i = Lagrange.basis s v i := by + simp only [ringBasis, Lagrange.basis, basisDivisor, Ring.inverse_eq_inv'] + +/-- Over a field, `ringInterpolate` is Mathlib's `Lagrange.interpolate`. -/ +theorem ringInterpolate_eq_interpolate {F : Type*} [Field F] (s : Finset ι) (v : ι → F) : + ringInterpolate s v = interpolate s v := by + ext r : 1 + simp only [ringInterpolate_apply, interpolate_apply, ringBasis_eq_basis] + +end Lagrange diff --git a/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean b/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean new file mode 100644 index 0000000000..707dad117b --- /dev/null +++ b/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean @@ -0,0 +1,303 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate (Mathlib, `Mathlib/NumberTheory/Padics/`) + +public import Complexity.Init +public import Mathlib.NumberTheory.Padics.PadicNumbers +public import Mathlib.RingTheory.AdjoinRoot +public import Mathlib.RingTheory.Valuation.Integers +import Complexity.Foundations.RingTheory.GaloisRing +import Mathlib.Algebra.GCDMonoid.IntegrallyClosed +import Mathlib.Algebra.Polynomial.Eval.Irreducible +import Mathlib.RingTheory.Localization.Integral +import Mathlib.RingTheory.Polynomial.Content +import Mathlib.RingTheory.Polynomial.GaussLemma + +/-! +# The `p`-adic valuation of `ℚ[X] / (f)` for `f` irreducible modulo `p` + +Let `p` be a prime and `f` a monic integer polynomial that is irreducible modulo `p`. Then `f` is +irreducible over `ℚ` (`AdjoinRoot.irreducible_map_rat`), so `K = ℚ[X] / (f)` is a field. Give each +element of `K` its coordinates in the basis `1, X, …, X ^ (deg f - 1)`, and let `v x` be the +largest `p`-adic valuation `Rat.padicValuation p` of a coordinate; written additively, `v x` is the +least `p`-adic order of a coordinate. This file proves that `v` is a valuation of `K` +(`AdjoinRoot.padicValuation`): it is multiplicative and ultrametric. + +Multiplicativity is the substantial point. Every element of `K` is a rational multiple +`r • x₀` of the image `x₀` of an element of `ℤ[X] / (f)` that is nonzero modulo `p`, and such +`x₀` have `v x₀ = 1`. Reduction modulo `p` is a ring map into the field `𝔽_p[X] / (f)`, so a +product of two such elements is again nonzero modulo `p`. + +The valuation ring `O = {x | v x ≤ 1}` of `v` consists of the elements whose coordinates have no +`p` in their denominators, that is `ℤ_(p)[X] / (f)` (`AdjoinRoot.mem_integer_padicValuation_iff`), +and an element of `O` with `v x = 1`, one that is nonzero modulo `p`, is a unit of `O` +(`AdjoinRoot.isUnit_of_padicValuation_eq_one`). + +This is the 2-adic valuation `v₂` of the coefficient field `K = ℚ[U] / (f)` of [OpenAI2026ETH] +(§D.4.1, p. 57), with `v₂ x = n` corresponding to `v x = exp (-n)`. + +## Main definitions + +* `AdjoinRoot.padicValuation`: the `p`-adic valuation of `ℚ[X] / (f)`. + +## Main results + +* `AdjoinRoot.irreducible_map_rat`: `f` is irreducible over `ℚ`. +* `AdjoinRoot.padicValuation_apply`: `v x` is the largest valuation of a coordinate of `x`. +* `AdjoinRoot.padicValuation_algebraMap`: `v` extends `Rat.padicValuation p`. +* `AdjoinRoot.padicValuation_map_eq_one_iff`: an element of `ℤ[X] / (f)` has valuation one + exactly when it is nonzero modulo `p`. +* `AdjoinRoot.mem_integer_padicValuation_iff`: the valuation ring is `ℤ_(p)[X] / (f)`. +* `AdjoinRoot.isUnit_of_padicValuation_eq_one`: elements of valuation one are units of it. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.1, p. 57. +-/ + +public section + +open Polynomial +open scoped WithZero + +namespace AdjoinRoot + +variable (p : ℕ) [hp : Fact p.Prime] {f : ℤ[X]} + +/-- **Irreducible modulo `p` implies irreducible over `ℚ`**, for monic `f`. -/ +theorem irreducible_map_rat (hf : f.Monic) + (hirr : Irreducible (f.map (Int.castRingHom (ZMod p)))) : + Irreducible (f.map (Int.castRingHom ℚ)) := + (hf.irreducible_iff_irreducible_map_fraction_map (K := ℚ)).mp + (Monic.irreducible_of_irreducible_map _ _ hf hirr) + +variable {p} + +/-- The reduced representative has degree below `deg g`. -/ +private theorem degree_modByMonicHom_lt {R : Type*} [CommRing R] [Nontrivial R] {g : R[X]} + (hg : g.Monic) (x : AdjoinRoot g) : (modByMonicHom hg x).degree < g.degree := by + obtain ⟨Q, rfl⟩ := mk_surjective x + rw [modByMonicHom_mk] + exact degree_modByMonic_lt _ hg + +variable (p) in +/-- The largest `p`-adic valuation of a coordinate of `x` in the basis `1, X, …, X ^ (deg f - 1)`. +-/ +private noncomputable def coordVal (hf : f.Monic) (x : AdjoinRoot (f.map (Int.castRingHom ℚ))) : + ℤᵐ⁰ := + (Finset.range f.natDegree).sup fun i => + Rat.padicValuation p ((modByMonicHom (hf.map (Int.castRingHom ℚ)) x).coeff i) + +private theorem coordVal_smul_le (hf : f.Monic) (r : ℚ) + (x : AdjoinRoot (f.map (Int.castRingHom ℚ))) : + coordVal p hf (r • x) ≤ Rat.padicValuation p r * coordVal p hf x := by + refine Finset.sup_le fun i hi => ?_ + rw [LinearMap.map_smul_of_tower, coeff_smul, smul_eq_mul, map_mul] + exact mul_le_mul_right (Finset.le_sup (f := fun i => Rat.padicValuation p + ((modByMonicHom (hf.map (Int.castRingHom ℚ)) x).coeff i)) hi) _ + +/-- The coordinates scale with rational scalars. -/ +private theorem coordVal_smul (hf : f.Monic) (r : ℚ) + (x : AdjoinRoot (f.map (Int.castRingHom ℚ))) : + coordVal p hf (r • x) = Rat.padicValuation p r * coordVal p hf x := by + refine le_antisymm (coordVal_smul_le hf r x) ?_ + rcases eq_or_ne r 0 with rfl | hr + · simp + have h := coordVal_smul_le (p := p) hf r⁻¹ (r • x) + rw [inv_smul_smul₀ hr, map_inv₀] at h + calc + Rat.padicValuation p r * coordVal p hf x + ≤ Rat.padicValuation p r * ((Rat.padicValuation p r)⁻¹ * coordVal p hf (r • x)) := + mul_le_mul_right h _ + _ = coordVal p hf (r • x) := by + rw [← mul_assoc, mul_inv_cancel₀ ((Rat.padicValuation p).ne_zero_iff.mpr hr), one_mul] + +/-- The image of `ℤ[X] / (f)` in `ℚ[X] / (f)`. -/ +private noncomputable abbrev toRat (f : ℤ[X]) : + AdjoinRoot f →+* AdjoinRoot (f.map (Int.castRingHom ℚ)) := + map (Int.castRingHom ℚ) f _ dvd_rfl + +/-- Reduction of `ℤ[X] / (f)` modulo `p`. -/ +private noncomputable abbrev toZMod (p : ℕ) (f : ℤ[X]) : + AdjoinRoot f →+* AdjoinRoot (f.map (Int.castRingHom (ZMod p))) := + map (Int.castRingHom (ZMod p)) f _ dvd_rfl + +/-- The coordinates of the image of `ℤ[X] / (f)` are the integer coordinates. -/ +private theorem modByMonicHom_toRat (hf : f.Monic) (o : AdjoinRoot f) : + modByMonicHom (hf.map (Int.castRingHom ℚ)) (toRat f o) = + (modByMonicHom hf o).map (Int.castRingHom ℚ) := by + obtain ⟨Q, rfl⟩ := mk_surjective o + rw [toRat, map_mk, modByMonicHom_mk, modByMonicHom_mk, map_modByMonic _ hf] + +/-- **Images of `ℤ[X] / (f)` have valuation one exactly when they are nonzero modulo `p`**, and at +most one in any case. -/ +private theorem coordVal_toRat_eq_one_iff (hf : f.Monic) (o : AdjoinRoot f) : + coordVal p hf (toRat f o) ≤ 1 ∧ + (coordVal p hf (toRat f o) = 1 ↔ toZMod p f o ≠ 0) := by + set Q := modByMonicHom hf o + have hQdeg : ∀ i, f.natDegree ≤ i → Q.coeff i = 0 := fun i hi => + coeff_eq_zero_of_degree_lt ((degree_modByMonicHom_lt hf o).trans_le + ((degree_le_natDegree).trans (by exact_mod_cast hi))) + have hval : ∀ i, Rat.padicValuation p ((modByMonicHom (hf.map (Int.castRingHom ℚ)) + (toRat f o)).coeff i) = Int.padicValuation p (Q.coeff i) := fun i => by + rw [modByMonicHom_toRat, coeff_map, eq_intCast, Rat.padicValuation_cast] + have hle : coordVal p hf (toRat f o) ≤ 1 := + Finset.sup_le fun i _ => (hval i).trans_le (Int.padicValuation_le_one p _) + refine ⟨hle, ?_⟩ + rw [Ne, toZMod, map_eq_zero_iff _ hf dvd_rfl rfl] + simp only [eq_intCast, ZMod.intCast_zmod_eq_zero_iff_dvd] + constructor + · intro h1 hdvd + have hlt : coordVal p hf (toRat f o) < 1 := by + refine (Finset.sup_lt_iff (bot_lt_iff_ne_bot.mpr (by simp))).mpr fun i _ => ?_ + rw [hval] + exact Int.padicValuation_lt_one_iff.mpr (hdvd i) + exact hlt.ne h1 + · intro hndvd + obtain ⟨i, hi⟩ := not_forall.mp hndvd + have hie : i < f.natDegree := by + by_contra hie + exact hi (by rw [hQdeg i (not_lt.mp hie)]; exact dvd_zero _) + refine le_antisymm hle ?_ + rw [← Int.padicValuation_eq_one_iff.mpr hi, ← hval] + exact Finset.le_sup (f := fun i => Rat.padicValuation p + ((modByMonicHom (hf.map (Int.castRingHom ℚ)) (toRat f o)).coeff i)) (Finset.mem_range.mpr hie) + +/-- **Every element is a rational multiple of an integral element that is nonzero modulo `p`.** +Clear the denominators of the coordinates and divide by the content. -/ +private theorem exists_eq_smul_toRat (hf : f.Monic) + (hirr : Irreducible (f.map (Int.castRingHom (ZMod p)))) + (x : AdjoinRoot (f.map (Int.castRingHom ℚ))) : + ∃ r : ℚ, ∃ o : AdjoinRoot f, toZMod p f o ≠ 0 ∧ x = r • toRat f o := by + have := Fact.mk hirr + set P := modByMonicHom (hf.map (Int.castRingHom ℚ)) x + have hx : mk _ P = x := mk_leftInverse _ x + rcases eq_or_ne P 0 with hP | hP + · refine ⟨0, 1, by rw [map_one]; exact one_ne_zero, ?_⟩ + rw [zero_smul, ← hx, hP, map_zero] + obtain ⟨b, hb, hQ₀'⟩ := IsLocalization.integerNormalization_spec (nonZeroDivisors ℤ) P + set Q₀ := IsLocalization.integerNormalization (nonZeroDivisors ℤ) P + have hb0 : (b : ℚ) ≠ 0 := by exact_mod_cast nonZeroDivisors.ne_zero hb + have hQ₀ : Q₀.map (Int.castRingHom ℚ) = C (b : ℚ) * P := by + rw [← algebraMap_int_eq, hQ₀', ← Int.cast_smul_eq_zsmul ℚ, smul_eq_C_mul] + have hQ₀ne : Q₀ ≠ 0 := by + rintro h + rw [h, Polynomial.map_zero] at hQ₀ + exact mul_ne_zero (C_ne_zero.mpr hb0) hP hQ₀.symm + set Q₁ := Q₀.primPart + have hdeg : Q₁.degree < (f.map (Int.castRingHom (ZMod p))).degree := by + rw [hf.degree_map, degree_eq_natDegree (primPart_ne_zero Q₀), natDegree_primPart] + have hPdeg : P.degree < f.degree := + (hf.degree_map (Int.castRingHom ℚ)) ▸ degree_modByMonicHom_lt (hf.map _) x + have : Q₀.degree < f.degree := by + refine lt_of_le_of_lt ?_ hPdeg + rw [← degree_map_eq_of_injective (RingHom.injective_int (Int.castRingHom ℚ)) Q₀, hQ₀] + exact degree_mul_le_of_le (degree_C_le) le_rfl |>.trans (by simp) + rwa [degree_eq_natDegree hQ₀ne] at this + have hred : (Q₁.map (Int.castRingHom (ZMod p))) ≠ 0 := by + intro h0 + have hdvd : C (p : ℤ) ∣ Q₁ := (C_dvd_iff_dvd_coeff _ _).mpr fun i => by + rw [← ZMod.intCast_zmod_eq_zero_iff_dvd, ← eq_intCast (Int.castRingHom (ZMod p)), ← coeff_map, + h0, coeff_zero] + have hu := isPrimitive_primPart Q₀ (p : ℤ) hdvd + rw [Int.isUnit_iff_natAbs_eq, Int.natAbs_natCast] at hu + exact hp.out.one_lt.ne' hu + refine ⟨Q₀.content / b, mk f Q₁, ?_, ?_⟩ + · rw [toZMod, map_mk, Ne, mk_eq_zero] + exact (hf.map _).not_dvd_of_degree_lt hred ((degree_map_le).trans_lt hdeg) + · rw [toRat, map_mk, ← hx, Algebra.smul_def, algebraMap_eq, ← mk_C, ← map_mul] + congr 1 + have h := congrArg (Polynomial.map (Int.castRingHom ℚ)) (eq_C_content_mul_primPart Q₀) + rw [Polynomial.map_mul, map_C, hQ₀, eq_intCast] at h + calc + P = C (b : ℚ)⁻¹ * (C (b : ℚ) * P) := by + rw [← mul_assoc, ← C_mul, inv_mul_cancel₀ hb0, C_1, one_mul] + _ = C ((Q₀.content : ℚ) / b) * Q₁.map (Int.castRingHom ℚ) := by + rw [h, ← mul_assoc, ← C_mul, div_eq_inv_mul] + +variable (p) in +/-- **The `p`-adic valuation of `ℚ[X] / (f)`**, for `f` monic and irreducible modulo `p`: the +largest `p`-adic valuation of a coordinate in the basis `1, X, …, X ^ (deg f - 1)`. It extends +`Rat.padicValuation p` (`AdjoinRoot.padicValuation_algebraMap`). -/ +noncomputable def padicValuation (hf : f.Monic) + (hirr : Irreducible (f.map (Int.castRingHom (ZMod p)))) : + Valuation (AdjoinRoot (f.map (Int.castRingHom ℚ))) ℤᵐ⁰ where + toFun := coordVal p hf + map_zero' := by + simp only [coordVal, map_zero, coeff_zero] + exact Finset.sup_bot _ + map_one' := by + have := (coordVal_toRat_eq_one_iff (p := p) hf 1).2.mpr (by + have := Fact.mk hirr + rw [map_one]; exact one_ne_zero) + rwa [map_one] at this + map_mul' x y := by + have := Fact.mk hirr + obtain ⟨r, o, ho, rfl⟩ := exists_eq_smul_toRat hf hirr x + obtain ⟨r', o', ho', rfl⟩ := exists_eq_smul_toRat hf hirr y + rw [smul_mul_smul_comm, ← map_mul, coordVal_smul, coordVal_smul, coordVal_smul, map_mul, + (coordVal_toRat_eq_one_iff hf _).2.mpr (by rw [map_mul]; exact mul_ne_zero ho ho'), + (coordVal_toRat_eq_one_iff hf _).2.mpr ho, (coordVal_toRat_eq_one_iff hf _).2.mpr ho', + mul_one, mul_one, mul_one] + map_add_le_max' x y := by + refine Finset.sup_le fun i hi => ?_ + rw [map_add, coeff_add] + refine ((Rat.padicValuation p).map_add _ _).trans (max_le_max ?_ ?_) <;> + exact Finset.le_sup (f := fun i => Rat.padicValuation p _) hi + +variable (hf : f.Monic) (hirr : Irreducible (f.map (Int.castRingHom (ZMod p)))) + +/-- The valuation is the largest `p`-adic valuation of a coordinate. -/ +theorem padicValuation_apply (x : AdjoinRoot (f.map (Int.castRingHom ℚ))) : + padicValuation p hf hirr x = (Finset.range f.natDegree).sup fun i => + Rat.padicValuation p ((modByMonicHom (hf.map (Int.castRingHom ℚ)) x).coeff i) := by + simp only [padicValuation] + rfl + +/-- **The valuation extends the `p`-adic valuation of `ℚ`.** -/ +theorem padicValuation_algebraMap (r : ℚ) : + padicValuation p hf hirr (algebraMap ℚ _ r) = Rat.padicValuation p r := by + rw [Algebra.algebraMap_eq_smul_one, ← mul_one (Rat.padicValuation p r), + ← (padicValuation p hf hirr).map_one] + exact coordVal_smul hf r 1 + +/-- **An element of `ℤ[X] / (f)` has valuation one exactly when it is nonzero modulo `p`.** -/ +theorem padicValuation_map_eq_one_iff (o : AdjoinRoot f) : + padicValuation p hf hirr (map (Int.castRingHom ℚ) f _ dvd_rfl o) = 1 ↔ + map (Int.castRingHom (ZMod p)) f _ dvd_rfl o ≠ 0 := + (coordVal_toRat_eq_one_iff hf o).2 + +/-- Elements of `ℤ[X] / (f)` have valuation at most one. -/ +theorem padicValuation_map_le_one (o : AdjoinRoot f) : + padicValuation p hf hirr (map (Int.castRingHom ℚ) f _ dvd_rfl o) ≤ 1 := + (coordVal_toRat_eq_one_iff hf o).1 + +/-- **The valuation ring is `ℤ_(p)[X] / (f)`**: the elements whose coordinates have no `p` in their +denominators. -/ +theorem mem_integer_padicValuation_iff (x : AdjoinRoot (f.map (Int.castRingHom ℚ))) : + x ∈ (padicValuation p hf hirr).integer ↔ + ∀ i, Rat.padicValuation p ((modByMonicHom (hf.map (Int.castRingHom ℚ)) x).coeff i) ≤ 1 := by + rw [Valuation.mem_integer_iff, padicValuation_apply, Finset.sup_le_iff] + refine ⟨fun h i => ?_, fun h i _ => h i⟩ + rcases lt_or_ge i f.natDegree with hi | hi + · exact h i (Finset.mem_range.mpr hi) + · rw [coeff_eq_zero_of_degree_lt, map_zero] + · exact zero_le + refine (degree_modByMonicHom_lt (hf.map _) x).trans_le ?_ + rw [hf.degree_map] + exact (degree_le_natDegree).trans (by exact_mod_cast hi) + +/-- **Elements of the valuation ring that are nonzero modulo `p` are units of it**: an element of +valuation one has an inverse of valuation one. -/ +theorem isUnit_of_padicValuation_eq_one {x : AdjoinRoot (f.map (Int.castRingHom ℚ))} + (hx : x ∈ (padicValuation p hf hirr).integer) (h1 : padicValuation p hf hirr x = 1) : + IsUnit (⟨x, hx⟩ : (padicValuation p hf hirr).integer) := by + have := Fact.mk (irreducible_map_rat p hf hirr) + exact (Valuation.integer.integers _).isUnit_iff_valuation_eq_one.mpr h1 + +end AdjoinRoot diff --git a/Complexity/Foundations/RingTheory/GaloisRing.lean b/Complexity/Foundations/RingTheory/GaloisRing.lean new file mode 100644 index 0000000000..da9bc2de1e --- /dev/null +++ b/Complexity/Foundations/RingTheory/GaloisRing.lean @@ -0,0 +1,351 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate (Mathlib, Galois rings) + +public import Complexity.Init +public import Complexity.Foundations.Data.Polynomial.RingLagrange +public import Mathlib.FieldTheory.Finite.GaloisField +public import Mathlib.RingTheory.AdjoinRoot +public import Mathlib.RingTheory.LocalRing.ResidueField.Defs +import Mathlib.RingTheory.LocalRing.ResidueField.Basic +import Mathlib.RingTheory.Polynomial.Nilpotent + +/-! +# Galois rings + +For a prime `p`, an exponent `n ≠ 0` and an integer polynomial `f` that is monic and irreducible +modulo `p`, the *Galois ring* `GaloisRing p n f = (ℤ / p ^ n)[X] / (f)` is a local ring. Its maximal +ideal is `(p)`, and reduction modulo `p` identifies its residue field with `𝔽_p[X] / (f)`, the +finite field with `p ^ deg f` elements. In particular an element is a unit exactly when it is +nonzero modulo `p`. + +The *digit lifts* `∑ i, c i * X ^ i` with digits `c i ∈ {0, …, p - 1}` reduce to the `p ^ deg f` +distinct residue-field elements, so any two of them differ by a unit, and Lagrange interpolation +over the ring holds at any set of them (`GaloisRing.eq_ringInterpolate_digitLift`). + +This is the coefficient ring of the Boolean tensor contraction of [OpenAI2026ETH] (§D.4.1, +pp. 57–58), which takes `p = 2`, a degree `e = 4 ⌈log₂ s⌉` and the precision `n`; the manuscript's +binary-coordinate lifts are the digit lifts for `p = 2`. + +The argument is that of a surjection onto a field with nilpotent kernel +(`RingHom.isUnit_iff_ne_zero_of_isNilpotent`): reduction modulo `p` has kernel `(p)`, and +`p ^ n = 0`. The manuscript states the unit criterion for `ℤ_(2)[U] / (f)` and proves it with the +determinant of the multiplication matrix; at a finite precision the nilpotent kernel suffices. The +statement over `ℤ_(p)` is `AdjoinRoot.isUnit_of_padicValuation_eq_one`. + +## Main definitions + +* `GaloisRing`: the ring `(ℤ / p ^ n)[X] / (f)`. +* `GaloisRing.residue`: reduction modulo `p`, onto `𝔽_p[X] / (f)`. +* `GaloisRing.digitLift`: the lift `∑ i, c i * X ^ i` of a digit vector. + +## Main results + +* `RingHom.isLocalHom_of_isNilpotent`: a surjection with nilpotent kernel is a local + homomorphism. +* `AdjoinRoot.map_eq_zero_iff`: an element of `R[X] / (g)` vanishes in `S[X] / (g)` exactly when + the coefficients of its reduced representative do. +* `GaloisRing.ker_residue`: the kernel of reduction modulo `p` is `(p)`. +* `GaloisRing.isUnit_iff`: an element is a unit exactly when it is nonzero modulo `p`. +* `GaloisRing.instIsLocalRing`, `GaloisRing.maximalIdeal_eq`: the ring is local with maximal ideal + `(p)`. +* `GaloisRing.residueFieldEquiv`, `GaloisRing.algEquivGaloisField`: its residue field is + `𝔽_p[X] / (f) ≃ GaloisField p (deg f)`. +* `GaloisRing.isUnit_digitLift_sub`: distinct digit lifts differ by a unit. +* `GaloisRing.eq_ringInterpolate_digitLift`: Lagrange interpolation at digit lifts. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.1, pp. 57–58. +-/ + +public section + +open Polynomial IsLocalRing + +/-! ### Surjections with nilpotent kernel -/ + +namespace RingHom + +variable {R S : Type*} [CommRing R] [CommRing S] + +/-- A surjective ring homomorphism whose kernel consists of nilpotent elements is local: if `ψ x` +is a unit then `x y = 1 + n` for some `y` and nilpotent `n`. -/ +theorem isLocalHom_of_isNilpotent (ψ : R →+* S) (hψ : Function.Surjective ψ) + (hnil : ∀ x, ψ x = 0 → IsNilpotent x) : IsLocalHom ψ where + map_nonunit x hx := by + obtain ⟨u, hu⟩ := hx + obtain ⟨y, hy⟩ := hψ ↑u⁻¹ + have hn : IsNilpotent (x * y - 1) := + hnil _ (by rw [map_sub, map_mul, map_one, hy, ← hu, Units.mul_inv, sub_self]) + have h1 : IsUnit (x * y) := by + simpa only [add_sub_cancel] using hn.isUnit_one_add + exact isUnit_of_mul_isUnit_left h1 + +/-- Over a surjection onto a field with nilpotent kernel, an element is a unit exactly when its +image is nonzero. -/ +theorem isUnit_iff_ne_zero_of_isNilpotent {F : Type*} [Field F] (ψ : R →+* F) + (hψ : Function.Surjective ψ) (hnil : ∀ x, ψ x = 0 → IsNilpotent x) {x : R} : + IsUnit x ↔ ψ x ≠ 0 := by + have := ψ.isLocalHom_of_isNilpotent hψ hnil + exact ⟨fun h => (h.map ψ).ne_zero, fun h => isUnit_of_map_unit ψ x (Ne.isUnit h)⟩ + +end RingHom + +/-! ### Reducing the coefficients of `R[X] / (g)` -/ + +namespace AdjoinRoot + +variable {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S) {g : R[X]} + +/-- Reducing the coefficients maps the class of `P` to the class of `P.map φ`. -/ +theorem map_mk (q : S[X]) (h : q ∣ g.map φ) (P : R[X]) : + map φ g q h (mk g P) = mk q (P.map φ) := by + have : (map φ g q h).comp (mk g) = (mk q).comp (mapRingHom φ) := by + refine Polynomial.ringHom_ext (fun a => ?_) ?_ + · simp only [RingHom.comp_apply, mk_C, map_of, coe_mapRingHom, Polynomial.map_C] + · simp only [RingHom.comp_apply, mk_X, map_root, coe_mapRingHom, Polynomial.map_X] + exact congrArg (fun F : R[X] →+* AdjoinRoot q => F P) this + +/-- Reducing the coefficients is surjective when `φ` is. -/ +theorem map_surjective_of_surjective (q : S[X]) (h : q ∣ g.map φ) + (hφ : Function.Surjective φ) : Function.Surjective (map φ g q h) := by + intro y + obtain ⟨Q, rfl⟩ := mk_surjective y + obtain ⟨P, rfl⟩ := Polynomial.map_surjective φ hφ Q + exact ⟨mk g P, map_mk φ q h P⟩ + +/-- **An element vanishes after reducing the coefficients** of a monic `g` exactly when the +coefficients of its representative of degree below `deg g` do: that representative reduces to a +polynomial of degree below `deg (g.map φ)`, which `g.map φ` divides only when it is zero. -/ +theorem map_eq_zero_iff [Nontrivial S] (hg : g.Monic) {q : S[X]} (h : q ∣ g.map φ) + (hq : q = g.map φ) (x : AdjoinRoot g) : + map φ g q h x = 0 ↔ ∀ i, φ ((modByMonicHom hg x).coeff i) = 0 := by + subst hq + have := φ.domain_nontrivial + obtain ⟨Q, rfl⟩ := mk_surjective x + rw [modByMonicHom_mk] + set P := Q %ₘ g + have hx : mk g P = mk g Q := by + have := mk_leftInverse hg (mk g Q) + rwa [modByMonicHom_mk] at this + have hdeg : (P.map φ).degree < (g.map φ).degree := by + rw [hg.degree_map] + exact degree_map_le.trans_lt (degree_modByMonic_lt _ hg) + rw [← hx, map_mk, mk_eq_zero] + constructor + · intro hdvd i + by_contra hne + have h0 : P.map φ ≠ 0 := fun h0 => hne (by rw [← coeff_map, h0, coeff_zero]) + exact (hg.map φ).not_dvd_of_degree_lt h0 hdeg hdvd + · intro h + have : P.map φ = 0 := Polynomial.ext fun i => by rw [coeff_map, h, coeff_zero] + rw [this] + exact dvd_zero _ + +end AdjoinRoot + +/-! ### Galois rings -/ + +/-- The ring `(ℤ / p ^ n)[X] / (f)` presented by an integer polynomial `f`. For a prime `p`, +`n ≠ 0` and `f` monic and irreducible modulo `p`, it is the *Galois ring* of characteristic +`p ^ n` and rank `deg f`: a local ring with maximal ideal `(p)` and residue field +`𝔽_{p ^ deg f}`. -/ +abbrev GaloisRing (p n : ℕ) (f : ℤ[X]) : Type := + AdjoinRoot (f.map (Int.castRingHom (ZMod (p ^ n)))) + +namespace GaloisRing + +variable (p n : ℕ) (f : ℤ[X]) + +/-- Reducing integer coefficients modulo `m` and then modulo a divisor `d` of `m` is reducing +modulo `d`. -/ +theorem map_castHom_map {d m : ℕ} (h : d ∣ m) : + (f.map (Int.castRingHom (ZMod m))).map (ZMod.castHom h (ZMod d)) = + f.map (Int.castRingHom (ZMod d)) := by + rw [Polynomial.map_map] + congr 1 + exact RingHom.ext_int _ _ + +/-- The *digit lift* `∑ i, c i * X ^ i` of a digit vector `c`, with each digit `c i ∈ ZMod p` read +as an integer in `{0, …, p - 1}`. For `p = 2` these are the binary-coordinate lifts of +[OpenAI2026ETH] (§D.4.1, p. 58). -/ +@[expose] noncomputable def digitLift (c : Fin f.natDegree → ZMod p) : GaloisRing p n f := + ∑ i, ((c i).val : GaloisRing p n f) * AdjoinRoot.root _ ^ (i : ℕ) + +variable [NeZero n] + +/-- Reduction modulo `p`, from `(ℤ / p ^ n)[X] / (f)` onto `𝔽_p[X] / (f)`. -/ +noncomputable def residue : GaloisRing p n f →+* AdjoinRoot (f.map (Int.castRingHom (ZMod p))) := + AdjoinRoot.map (ZMod.castHom (dvd_pow_self p (NeZero.ne n)) (ZMod p)) _ _ + (map_castHom_map f _).symm.dvd + +@[simp] +theorem residue_mk (P : (ZMod (p ^ n))[X]) : + residue p n f (AdjoinRoot.mk _ P) = + AdjoinRoot.mk _ (P.map (ZMod.castHom (dvd_pow_self p (NeZero.ne n)) (ZMod p))) := + AdjoinRoot.map_mk _ _ _ P + +@[simp] +theorem residue_root : residue p n f (AdjoinRoot.root _) = AdjoinRoot.root _ := + AdjoinRoot.map_root _ _ _ _ + +@[simp] +theorem residue_of (a : ZMod (p ^ n)) : + residue p n f (AdjoinRoot.of _ a) = + AdjoinRoot.of _ (ZMod.castHom (dvd_pow_self p (NeZero.ne n)) (ZMod p) a) := + AdjoinRoot.map_of _ _ _ _ _ + +theorem residue_surjective : Function.Surjective (residue p n f) := + AdjoinRoot.map_surjective_of_surjective _ _ _ (ZMod.castHom_surjective _) + +variable {p n f} [Fact p.Prime] + +variable (p n f) in +/-- A digit lift reduces to `∑ i, c i * X ^ i` modulo `p`. -/ +theorem residue_digitLift (c : Fin f.natDegree → ZMod p) : + residue p n f (digitLift p n f c) = AdjoinRoot.mk _ (∑ i, C (c i) * X ^ (i : ℕ)) := by + simp only [digitLift, map_sum, map_mul, map_pow, map_natCast, residue_root, AdjoinRoot.mk_C, + AdjoinRoot.mk_X] + refine Finset.sum_congr rfl fun i _ => ?_ + rw [← map_natCast (AdjoinRoot.of _), ZMod.natCast_zmod_val] + +/-- Digit lifts reduce to distinct elements modulo `p`: the coordinates `1, X, …, X ^ (deg f - 1)` +are independent in `𝔽_p[X] / (f)` for monic `f`. -/ +theorem residue_digitLift_injective (hf : f.Monic) : + Function.Injective fun c : Fin f.natDegree → ZMod p => residue p n f (digitLift p n f c) := by + intro c c' h + simp only [residue_digitLift] at h + rw [AdjoinRoot.mk_eq_mk, ← Finset.sum_sub_distrib] at h + set P : (ZMod p)[X] := ∑ i, (C (c i) * X ^ (i : ℕ) - C (c' i) * X ^ (i : ℕ)) + have hcoeff : ∀ i : Fin f.natDegree, P.coeff i = c i - c' i := fun i => by + simp only [P, finsetSum_coeff, coeff_sub, coeff_C_mul, coeff_X_pow, mul_ite, mul_one, + mul_zero] + rw [Finset.sum_eq_single i (fun j _ hji => ?_) (by simp), ite_eq_left rfl, ite_eq_left rfl] + rw [ite_eq_right fun h => hji (Fin.ext h.symm), ite_eq_right fun h => hji (Fin.ext h.symm), + sub_zero] + have hP : P = 0 := by + by_contra h0 + refine (hf.map (Int.castRingHom (ZMod p))).not_dvd_of_degree_lt h0 ?_ h + rw [hf.degree_map, degree_eq_natDegree hf.ne_zero] + refine (degree_sum_le _ _).trans_lt + ((Finset.sup_lt_iff (WithBot.bot_lt_coe _)).mpr fun i _ => ?_) + refine (degree_sub_le _ _).trans_lt (max_lt ?_ ?_) <;> + exact (degree_C_mul_X_pow_le _ _).trans_lt (by exact_mod_cast i.isLt) + funext i + have := hcoeff i + rw [hP, coeff_zero] at this + exact (sub_eq_zero.mp this.symm) + + +/-- An element of `ℤ / p ^ n` that vanishes modulo `p` is a multiple of `p`. -/ +private theorem dvd_of_castHom_eq_zero {a : ZMod (p ^ n)} + (ha : ZMod.castHom (dvd_pow_self p (NeZero.ne n)) (ZMod p) a = 0) : (p : ZMod (p ^ n)) ∣ a := by + obtain ⟨k, rfl⟩ := ZMod.natCast_zmod_surjective a + rw [map_natCast, ZMod.natCast_eq_zero_iff] at ha + obtain ⟨m, rfl⟩ := ha + exact ⟨m, by push_cast; ring⟩ + +/-- **The kernel of reduction modulo `p` is `(p)`**, when `f` is monic. -/ +theorem ker_residue (hf : f.Monic) : + RingHom.ker (residue p n f) = Ideal.span {(p : GaloisRing p n f)} := by + ext x + rw [RingHom.mem_ker, Ideal.mem_span_singleton] + constructor + · intro hx + rw [residue, AdjoinRoot.map_eq_zero_iff _ (hf.map _) _ + (map_castHom_map f (dvd_pow_self p (NeZero.ne n))).symm] at hx + obtain ⟨Q, hQ⟩ := (C_dvd_iff_dvd_coeff (p : ZMod (p ^ n)) _).mpr fun i => + dvd_of_castHom_eq_zero (hx i) + refine ⟨AdjoinRoot.mk _ Q, ?_⟩ + rw [← AdjoinRoot.mk_leftInverse (hf.map _) x, hQ, map_mul, AdjoinRoot.mk_C, map_natCast] + · rintro ⟨y, rfl⟩ + rw [map_mul, map_natCast, ← map_natCast (AdjoinRoot.of _), ZMod.natCast_self, map_zero, + zero_mul] + +/-- `p ^ n = 0`, so elements that vanish modulo `p` are nilpotent. -/ +theorem isNilpotent_of_residue_eq_zero (hf : f.Monic) {x : GaloisRing p n f} + (hx : residue p n f x = 0) : IsNilpotent x := by + rw [← RingHom.mem_ker, ker_residue hf, Ideal.mem_span_singleton] at hx + obtain ⟨y, rfl⟩ := hx + refine ⟨n, ?_⟩ + rw [mul_pow, ← Nat.cast_pow, ← map_natCast (AdjoinRoot.of _), ZMod.natCast_self, map_zero, + zero_mul] + +variable (hf : f.Monic) (hirr : Irreducible (f.map (Int.castRingHom (ZMod p)))) +include hf hirr + +/-- **Units are the elements that are nonzero modulo `p`.** -/ +theorem isUnit_iff {x : GaloisRing p n f} : IsUnit x ↔ residue p n f x ≠ 0 := + have := Fact.mk hirr + (residue p n f).isUnit_iff_ne_zero_of_isNilpotent (residue_surjective p n f) fun _ => + isNilpotent_of_residue_eq_zero hf + +/-- **Distinct digit lifts differ by a unit.** -/ +theorem isUnit_digitLift_sub {c c' : Fin f.natDegree → ZMod p} (h : c ≠ c') : + IsUnit (digitLift p n f c - digitLift p n f c') := by + rw [isUnit_iff hf hirr, map_sub, sub_ne_zero] + exact fun h' => h (residue_digitLift_injective hf h') + +/-- **Lagrange interpolation at digit lifts.** A polynomial over a Galois ring of degree less than +`#s`, for a set `s` of digit vectors, is the interpolant of its values at their lifts; the lifts +have unit differences. -/ +theorem eq_ringInterpolate_digitLift {s : Finset (Fin f.natDegree → ZMod p)} + {P : (GaloisRing p n f)[X]} (hP : P.degree < s.card) : + P = Lagrange.ringInterpolate s (digitLift p n f) (fun c => P.eval (digitLift p n f c)) := + Lagrange.eq_ringInterpolate (fun _ _ _ _ h => isUnit_digitLift_sub hf hirr h) hP + +/-- **A Galois ring is local.** -/ +theorem isLocalRing : IsLocalRing (GaloisRing p n f) := + have := Fact.mk hirr + have := (residue p n f).isLocalHom_of_isNilpotent (residue_surjective p n f) fun _ => + isNilpotent_of_residue_eq_zero hf + (residue p n f).domain_isLocalRing + +omit hirr in +/-- `𝔽_p[X] / (f)` has `p ^ deg f` elements. -/ +theorem natCard_adjoinRoot : + Nat.card (AdjoinRoot (f.map (Int.castRingHom (ZMod p)))) = p ^ f.natDegree := by + let b := (AdjoinRoot.powerBasis' (hf.map (Int.castRingHom (ZMod p)))).basis + rw [Nat.card_congr b.equivFun.toEquiv, Nat.card_fun, Nat.card_zmod, Nat.card_eq_fintype_card, + Fintype.card_fin, AdjoinRoot.powerBasis'_dim, hf.natDegree_map] + +end GaloisRing + +/-! ### The residue field -/ + +namespace GaloisRing + +variable {p n : ℕ} {f : ℤ[X]} [NeZero n] [Fact p.Prime] [hf : Fact f.Monic] + [hirr : Fact (Irreducible (f.map (Int.castRingHom (ZMod p))))] + +instance instIsLocalRing : IsLocalRing (GaloisRing p n f) := + isLocalRing hf.out hirr.out + +/-- **The maximal ideal of a Galois ring is `(p)`.** -/ +theorem maximalIdeal_eq : maximalIdeal (GaloisRing p n f) = Ideal.span {(p : GaloisRing p n f)} := + by rw [← ker_residue hf.out, IsLocalRing.ker_eq_maximalIdeal _ (residue_surjective p n f)] + +/-- **The residue field of a Galois ring** is `𝔽_p[X] / (f)`, by reduction modulo `p`. -/ +noncomputable def residueFieldEquiv : + ResidueField (GaloisRing p n f) ≃+* AdjoinRoot (f.map (Int.castRingHom (ZMod p))) := + (Ideal.quotEquivOfEq (IsLocalRing.ker_eq_maximalIdeal _ (residue_surjective p n f)).symm).trans + (RingHom.quotientKerEquivOfSurjective (residue_surjective p n f)) + +@[simp] +theorem residueFieldEquiv_residue (x : GaloisRing p n f) : + residueFieldEquiv (IsLocalRing.residue _ x) = residue p n f x := by + simp only [residueFieldEquiv] + rfl + +/-- **The residue field is the Galois field** with `p ^ deg f` elements. -/ +noncomputable def algEquivGaloisField : + AdjoinRoot (f.map (Int.castRingHom (ZMod p))) ≃ₐ[ZMod p] GaloisField p f.natDegree := + GaloisField.algEquivGaloisField p f.natDegree (natCard_adjoinRoot hf.out) + +end GaloisRing diff --git a/ComplexityTests/Foundations/Data/Polynomial/RingLagrange.lean b/ComplexityTests/Foundations/Data/Polynomial/RingLagrange.lean new file mode 100644 index 0000000000..94333bd0bc --- /dev/null +++ b/ComplexityTests/Foundations/Data/Polynomial/RingLagrange.lean @@ -0,0 +1,54 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Foundations.Data.Polynomial.RingLagrange +import Mathlib.Data.ZMod.Basic +import Mathlib.Tactic.FinCases + +/-! Tests for Lagrange interpolation over a commutative ring. -/ + +namespace ComplexityTests.RingLagrange + +open Polynomial Lagrange + +/-! ### Interpolation over `ZMod 8`, which is not a domain -/ + +/-- The nodes `0` and `1` of `ZMod 8` differ by a unit. -/ +theorem pairwise_isUnit : + ((Finset.univ : Finset (Fin 2)) : Set (Fin 2)).Pairwise + fun i j => IsUnit ((![0, 1] : Fin 2 → ZMod 8) i - ![0, 1] j) := by + intro i _ j _ hij + fin_cases i <;> fin_cases j + · exact absurd rfl hij + · simp + · simp + · exact absurd rfl hij + +/-- The interpolant of the values `3, 5` at `0, 1` takes those values. -/ +example : (ringInterpolate Finset.univ (![0, 1] : Fin 2 → ZMod 8) ![3, 5]).eval 0 = 3 ∧ + (ringInterpolate Finset.univ (![0, 1] : Fin 2 → ZMod 8) ![3, 5]).eval 1 = 5 := + ⟨eval_ringInterpolate_at_node pairwise_isUnit _ (Finset.mem_univ (0 : Fin 2)), + eval_ringInterpolate_at_node pairwise_isUnit _ (Finset.mem_univ (1 : Fin 2))⟩ + +/-- A linear polynomial over `ZMod 8` is the interpolant of its values at `0` and `1`. -/ +example : (C 3 + C 2 * X : (ZMod 8)[X]) = + ringInterpolate Finset.univ (![0, 1] : Fin 2 → ZMod 8) + (fun i => (C 3 + C 2 * X : (ZMod 8)[X]).eval (![0, 1] i)) := + eq_ringInterpolate pairwise_isUnit ((degree_add_le _ _).trans_lt (max_lt + (degree_C_le.trans_lt (by decide)) ((degree_C_mul_X_le _).trans_lt (by decide)))) + +/-! ### Unit differences are needed -/ + +/-- Over `ZMod 4`, the nodes `0` and `2` differ by the non-unit `2`, and the nonzero polynomial +`2 X` of degree below two vanishes at both: uniqueness fails without unit differences. -/ +example : (C 2 * X : (ZMod 4)[X]).eval 0 = 0 ∧ (C 2 * X : (ZMod 4)[X]).eval 2 = 0 ∧ + (C 2 * X : (ZMod 4)[X]) ≠ 0 := by + refine ⟨by simp, by simp only [eval_mul, eval_C, eval_X]; decide, fun h => ?_⟩ + have := congrArg (coeff · 1) h + simp only [coeff_C_mul, coeff_X_one, mul_one, coeff_zero] at this + exact absurd this (by decide) + +end ComplexityTests.RingLagrange diff --git a/ComplexityTests/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean b/ComplexityTests/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean new file mode 100644 index 0000000000..1219f44ba2 --- /dev/null +++ b/ComplexityTests/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean @@ -0,0 +1,98 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Foundations.NumberTheory.Padics.AdjoinRootValuation +import Mathlib.Algebra.Field.ZMod +import Mathlib.Algebra.Polynomial.SpecificDegree +import Mathlib.Tactic.ComputeDegree +import Mathlib.Tactic.FinCases + +/-! Tests for the 2-adic valuation of `K = ℚ[U] / (U ^ 2 + U + 1)`, the case `e = 2` of the +coefficient field of [OpenAI2026ETH], §D.4.1. -/ + +namespace ComplexityTests.AdjoinRootValuation + +open Polynomial +open scoped WithZero + +/-- `U ^ 2 + U + 1`, irreducible modulo 2. -/ +noncomputable def f : ℤ[X] := X ^ 2 + X + 1 + +theorem f_monic : f.Monic := by unfold f; monicity! + +theorem f_irreducible : Irreducible (f.map (Int.castRingHom (ZMod 2))) := by + unfold f + simp only [Polynomial.map_add, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_one] + refine Polynomial.irreducible_of_degree_le_three_of_not_isRoot ?_ ?_ + · have : (X ^ 2 + X + 1 : (ZMod 2)[X]).natDegree = 2 := by compute_degree! + simp [this] + · intro x hx + rw [IsRoot.def, eval_add, eval_add, eval_pow, eval_X, eval_one] at hx + fin_cases x <;> revert hx <;> decide + +/-- The field `K = ℚ[U] / (U ^ 2 + U + 1)`. -/ +abbrev K : Type := AdjoinRoot (f.map (Int.castRingHom ℚ)) + +/-- The 2-adic valuation of `K`. -/ +noncomputable abbrev v : Valuation K ℤᵐ⁰ := AdjoinRoot.padicValuation 2 f_monic f_irreducible + +/-- The map `ℤ[U] / (f) → K`. -/ +noncomputable abbrev ι : AdjoinRoot f →+* K := AdjoinRoot.map (Int.castRingHom ℚ) f _ dvd_rfl + +instance : Fact (Irreducible (f.map (Int.castRingHom (ZMod 2)))) := ⟨f_irreducible⟩ + +/-- `U ^ 2 + U + 1 = 0` modulo `2`. -/ +theorem root_sq_add_root_add_one : + (AdjoinRoot.root (f.map (Int.castRingHom (ZMod 2)))) ^ 2 + AdjoinRoot.root _ + 1 = 0 := by + rw [← AdjoinRoot.mk_X, ← map_pow, ← map_add, ← map_one (AdjoinRoot.mk _), ← map_add, + AdjoinRoot.mk_eq_zero] + exact dvd_of_eq (by simp [f]) + +/-- `U` is nonzero modulo `2`: otherwise `f(0) = 1` would vanish. -/ +theorem root_ne_zero_mod_two : + AdjoinRoot.map (Int.castRingHom (ZMod 2)) f _ dvd_rfl (AdjoinRoot.root f) ≠ 0 := by + rw [AdjoinRoot.map_root] + intro h + have := root_sq_add_root_add_one + rw [h] at this + simp at this + +/-- `1 + U` is nonzero modulo `2`: it is `U²`, the square of a nonzero element of a field. -/ +theorem one_add_root_ne_zero_mod_two : + AdjoinRoot.map (Int.castRingHom (ZMod 2)) f _ dvd_rfl (1 + AdjoinRoot.root f) ≠ 0 := by + have hroot := root_ne_zero_mod_two + rw [AdjoinRoot.map_root] at hroot + rw [map_add, map_one, AdjoinRoot.map_root] + intro h1 + have h := root_sq_add_root_add_one + rw [add_assoc, add_comm (AdjoinRoot.root _), h1, add_zero] at h + exact pow_ne_zero 2 hroot h + +/-! ### The valuation on concrete elements -/ + +theorem padicValRat_two : padicValRat 2 (2 : ℚ) = 1 := by + exact_mod_cast padicValRat.self (p := 2) one_lt_two + +/-- `v (1 / 2) = exp 1`: the valuation extends that of `ℚ`. -/ +example : v (algebraMap ℚ K (1 / 2)) = WithZero.exp 1 := by + rw [AdjoinRoot.padicValuation_algebraMap] + simp [Rat.padicValuation, padicValRat_two] + +/-- `v (2 U) = v 2 * v U = exp (-1)`, by multiplicativity: `U` is nonzero modulo `2`. -/ +example : v (algebraMap ℚ K 2 * ι (AdjoinRoot.root f)) = WithZero.exp (-1) := by + rw [map_mul, AdjoinRoot.padicValuation_algebraMap, + (AdjoinRoot.padicValuation_map_eq_one_iff f_monic f_irreducible _).mpr root_ne_zero_mod_two, + mul_one] + simp [Rat.padicValuation, padicValRat_two] + +/-- `1 + U` is integral and nonzero modulo `2`, hence a unit of the valuation ring. -/ +example : ∃ h : ι (1 + AdjoinRoot.root f) ∈ v.integer, IsUnit (⟨_, h⟩ : v.integer) := + have h := AdjoinRoot.padicValuation_map_le_one f_monic f_irreducible (1 + AdjoinRoot.root f) + ⟨h, AdjoinRoot.isUnit_of_padicValuation_eq_one f_monic f_irreducible h + ((AdjoinRoot.padicValuation_map_eq_one_iff f_monic f_irreducible _).mpr + one_add_root_ne_zero_mod_two)⟩ + +end ComplexityTests.AdjoinRootValuation diff --git a/ComplexityTests/Foundations/RingTheory/GaloisRing.lean b/ComplexityTests/Foundations/RingTheory/GaloisRing.lean new file mode 100644 index 0000000000..c11fcc94d8 --- /dev/null +++ b/ComplexityTests/Foundations/RingTheory/GaloisRing.lean @@ -0,0 +1,111 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Foundations.RingTheory.GaloisRing +import Mathlib.Algebra.Polynomial.SpecificDegree +import Mathlib.Tactic.ComputeDegree +import Mathlib.Tactic.FinCases + +/-! Tests for Galois rings, on `(ℤ / 8)[U] / (U ^ 2 + U + 1)`: the case `p = 2`, `e = 2` and +precision `3` of the coefficient ring of [OpenAI2026ETH], §D.4.1. -/ + +namespace ComplexityTests.GaloisRing + +open Polynomial IsLocalRing + +/-- `U ^ 2 + U + 1`, irreducible modulo 2. -/ +noncomputable def f : ℤ[X] := X ^ 2 + X + 1 + +theorem f_monic : f.Monic := by unfold f; monicity! + +theorem f_natDegree : f.natDegree = 2 := by unfold f; compute_degree! + +theorem f_irreducible : Irreducible (f.map (Int.castRingHom (ZMod 2))) := by + unfold f + simp only [Polynomial.map_add, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_one] + refine Polynomial.irreducible_of_degree_le_three_of_not_isRoot ?_ ?_ + · have : (X ^ 2 + X + 1 : (ZMod 2)[X]).natDegree = 2 := by compute_degree! + simp [this] + · intro x hx + rw [IsRoot.def, eval_add, eval_add, eval_pow, eval_X, eval_one] at hx + fin_cases x <;> revert hx <;> decide + +instance : Fact f.Monic := ⟨f_monic⟩ + +instance : Fact (Irreducible (f.map (Int.castRingHom (ZMod 2)))) := ⟨f_irreducible⟩ + +/-- The ring `(ℤ / 8)[U] / (U ^ 2 + U + 1)`. -/ +abbrev A : Type := GaloisRing 2 3 f + +/-- The root `U`. -/ +noncomputable abbrev U : A := AdjoinRoot.root _ + +/-! ### Locality and units -/ + +/-- The residue field has characteristic two. -/ +theorem two_eq_zero : (2 : AdjoinRoot (f.map (Int.castRingHom (ZMod 2)))) = 0 := by + rw [← map_ofNat (AdjoinRoot.of _), show (OfNat.ofNat 2 : ZMod 2) = 0 by decide, map_zero] + +/-- The ring is local. -/ +example : IsLocalRing A := inferInstance + +/-- `2` is not a unit: it vanishes modulo `2`. -/ +example : ¬IsUnit (2 : A) := by + rw [GaloisRing.isUnit_iff f_monic f_irreducible, map_ofNat, not_not] + exact two_eq_zero + +/-- `1 + 2 U` is a unit: it is one modulo `2`. -/ +example : IsUnit (1 + 2 * U) := by + rw [GaloisRing.isUnit_iff f_monic f_irreducible] + simp only [map_add, map_mul, map_one, map_ofNat, two_eq_zero, zero_mul, add_zero] + exact one_ne_zero + +/-- `2` generates the maximal ideal. -/ +example : (2 : A) ∈ maximalIdeal A := by + rw [GaloisRing.maximalIdeal_eq] + exact_mod_cast Ideal.mem_span_singleton_self (2 : A) + +/-- The residue field has `2 ^ 2 = 4` elements. -/ +example : Nat.card (AdjoinRoot (f.map (Int.castRingHom (ZMod 2)))) = 4 := by + rw [GaloisRing.natCard_adjoinRoot f_monic, f_natDegree] + norm_num + +/-! ### Digit lifts and interpolation -/ + +/-- The digit vector `(0, 1)`. -/ +def c₀₁ : Fin f.natDegree → ZMod 2 := fun i => if (i : ℕ) = 1 then 1 else 0 + +/-- The digit vector `(1, 0)`. -/ +def c₁₀ : Fin f.natDegree → ZMod 2 := fun i => if (i : ℕ) = 0 then 1 else 0 + +/-- The lift of `(0, 1)` is `U`, and the lift of `(1, 0)` is `1`. -/ +theorem digitLift_c₀₁ : + GaloisRing.digitLift 2 3 f c₀₁ = U ∧ GaloisRing.digitLift 2 3 f c₁₀ = 1 := by + simp only [GaloisRing.digitLift, Fin.sum_univ_eq_sum_range + (fun i => (((if i = 1 then 1 else 0 : ZMod 2)).val : A) * AdjoinRoot.root _ ^ i), + Fin.sum_univ_eq_sum_range + (fun i => (((if i = 0 then 1 else 0 : ZMod 2)).val : A) * AdjoinRoot.root _ ^ i), + c₀₁, c₁₀, f_natDegree, Finset.sum_range_succ, Finset.sum_range_zero] + exact ⟨by simp [ZMod.val_one]; rfl, by simp [ZMod.val_one]⟩ + +/-- `U - 1` is a unit, as the difference of two distinct digit lifts. -/ +example : IsUnit (U - 1) := by + rw [← digitLift_c₀₁.1, ← digitLift_c₀₁.2] + refine GaloisRing.isUnit_digitLift_sub f_monic f_irreducible fun h => ?_ + have := congrFun h ⟨1, by rw [f_natDegree]; norm_num⟩ + simp [c₀₁, c₁₀] at this + +/-- There are `4` digit vectors, so a cubic over the ring is the interpolant of its values at the +four digit lifts. -/ +example (P : A[X]) (hP : P.natDegree ≤ 3) : + P = Lagrange.ringInterpolate Finset.univ (GaloisRing.digitLift 2 3 f) + (fun c => P.eval (GaloisRing.digitLift 2 3 f c)) := by + refine GaloisRing.eq_ringInterpolate_digitLift f_monic f_irreducible + ((degree_le_natDegree).trans_lt ?_) + rw [Finset.card_univ, Fintype.card_fun, ZMod.card, Fintype.card_fin, f_natDegree] + exact_mod_cast (show P.natDegree < 2 ^ 2 by omega) + +end ComplexityTests.GaloisRing From f9349461854369452a5b74f4698f350ab194f7a5 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:11:30 -0400 Subject: [PATCH 2/7] refactor(foundations): move AdjoinRoot coefficient reduction to its own module `AdjoinRoot.map_mk`, `AdjoinRoot.map_surjective_of_surjective` and `AdjoinRoot.map_eq_zero_iff` move unchanged from `GaloisRing.lean` to the new `Complexity/Foundations/RingTheory/AdjoinRoot.lean`. Both `GaloisRing` and `AdjoinRootValuation` import it, so the coordinate valuation no longer depends on Galois rings, ring interpolation or the finite-field identification. Names are unchanged; `GaloisRing` re-exports the module publicly. Addresses the placement finding of reviewer-codex-edemaine on #1859. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Padics/AdjoinRootValuation.lean | 3 +- .../Foundations/RingTheory/AdjoinRoot.lean | 85 +++++++++++++++++++ .../Foundations/RingTheory/GaloisRing.lean | 57 +------------ 4 files changed, 89 insertions(+), 57 deletions(-) create mode 100644 Complexity/Foundations/RingTheory/AdjoinRoot.lean diff --git a/Complexity.lean b/Complexity.lean index 7ae579ac43..6e48165717 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2777,6 +2777,7 @@ public import Complexity.Foundations.Probability.TrueSampleMeans public import Complexity.Foundations.Quantum.Measurement public import Complexity.Foundations.Relation.InductiveCounting public import Complexity.Foundations.Relation.RelatesWithinSteps +public import Complexity.Foundations.RingTheory.AdjoinRoot public import Complexity.Foundations.RingTheory.CyclicIntRing public import Complexity.Foundations.RingTheory.CyclicIntRing.Coefficients public import Complexity.Foundations.RingTheory.GaloisRing diff --git a/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean b/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean index 707dad117b..edb4016e1f 100644 --- a/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean +++ b/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean @@ -11,7 +11,8 @@ public import Complexity.Init public import Mathlib.NumberTheory.Padics.PadicNumbers public import Mathlib.RingTheory.AdjoinRoot public import Mathlib.RingTheory.Valuation.Integers -import Complexity.Foundations.RingTheory.GaloisRing +import Complexity.Foundations.RingTheory.AdjoinRoot +import Mathlib.Algebra.Field.ZMod import Mathlib.Algebra.GCDMonoid.IntegrallyClosed import Mathlib.Algebra.Polynomial.Eval.Irreducible import Mathlib.RingTheory.Localization.Integral diff --git a/Complexity/Foundations/RingTheory/AdjoinRoot.lean b/Complexity/Foundations/RingTheory/AdjoinRoot.lean new file mode 100644 index 0000000000..39bfed75e5 --- /dev/null +++ b/Complexity/Foundations/RingTheory/AdjoinRoot.lean @@ -0,0 +1,85 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate (Mathlib, `Mathlib/RingTheory/AdjoinRoot.lean`) + +public import Complexity.Init +public import Mathlib.RingTheory.AdjoinRoot + +/-! +# Reducing the coefficients of `R[X] / (g)` + +For a ring homomorphism `φ : R →+* S` and `q ∣ g.map φ`, Mathlib's `AdjoinRoot.map φ g q` sends +`R[X] / (g)` to `S[X] / (q)`. This file computes it on classes of polynomials, shows that it is +surjective when `φ` is, and characterizes its kernel when `g` is monic and `q = g.map φ`: an element +vanishes exactly when the coefficients of its reduced representative do. + +These facts are used both for Galois rings (`GaloisRing.residue`, reduction modulo `p`) and for the +`p`-adic valuation of `ℚ[X] / (f)` (`AdjoinRoot.padicValuation`). + +## Main results + +* `AdjoinRoot.map_mk`: the class of `P` maps to the class of `P.map φ`. +* `AdjoinRoot.map_surjective_of_surjective`: reducing the coefficients is surjective when `φ` is. +* `AdjoinRoot.map_eq_zero_iff`: an element of `R[X] / (g)` vanishes in `S[X] / (g.map φ)` exactly + when the coefficients of its reduced representative do. +-/ + +public section + +open Polynomial + +namespace AdjoinRoot + +variable {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S) {g : R[X]} + +/-- Reducing the coefficients maps the class of `P` to the class of `P.map φ`. -/ +theorem map_mk (q : S[X]) (h : q ∣ g.map φ) (P : R[X]) : + map φ g q h (mk g P) = mk q (P.map φ) := by + have : (map φ g q h).comp (mk g) = (mk q).comp (mapRingHom φ) := by + refine Polynomial.ringHom_ext (fun a => ?_) ?_ + · simp only [RingHom.comp_apply, mk_C, map_of, coe_mapRingHom, Polynomial.map_C] + · simp only [RingHom.comp_apply, mk_X, map_root, coe_mapRingHom, Polynomial.map_X] + exact congrArg (fun F : R[X] →+* AdjoinRoot q => F P) this + +/-- Reducing the coefficients is surjective when `φ` is. -/ +theorem map_surjective_of_surjective (q : S[X]) (h : q ∣ g.map φ) + (hφ : Function.Surjective φ) : Function.Surjective (map φ g q h) := by + intro y + obtain ⟨Q, rfl⟩ := mk_surjective y + obtain ⟨P, rfl⟩ := Polynomial.map_surjective φ hφ Q + exact ⟨mk g P, map_mk φ q h P⟩ + +/-- **An element vanishes after reducing the coefficients** of a monic `g` exactly when the +coefficients of its representative of degree below `deg g` do: that representative reduces to a +polynomial of degree below `deg (g.map φ)`, which `g.map φ` divides only when it is zero. -/ +theorem map_eq_zero_iff [Nontrivial S] (hg : g.Monic) {q : S[X]} (h : q ∣ g.map φ) + (hq : q = g.map φ) (x : AdjoinRoot g) : + map φ g q h x = 0 ↔ ∀ i, φ ((modByMonicHom hg x).coeff i) = 0 := by + subst hq + have := φ.domain_nontrivial + obtain ⟨Q, rfl⟩ := mk_surjective x + rw [modByMonicHom_mk] + set P := Q %ₘ g + have hx : mk g P = mk g Q := by + have := mk_leftInverse hg (mk g Q) + rwa [modByMonicHom_mk] at this + have hdeg : (P.map φ).degree < (g.map φ).degree := by + rw [hg.degree_map] + exact degree_map_le.trans_lt (degree_modByMonic_lt _ hg) + rw [← hx, map_mk, mk_eq_zero] + constructor + · intro hdvd i + by_contra hne + have h0 : P.map φ ≠ 0 := fun h0 => hne (by rw [← coeff_map, h0, coeff_zero]) + exact (hg.map φ).not_dvd_of_degree_lt h0 hdeg hdvd + · intro h + have : P.map φ = 0 := Polynomial.ext fun i => by rw [coeff_map, h, coeff_zero] + rw [this] + exact dvd_zero _ + +end AdjoinRoot diff --git a/Complexity/Foundations/RingTheory/GaloisRing.lean b/Complexity/Foundations/RingTheory/GaloisRing.lean index da9bc2de1e..79a1b2965e 100644 --- a/Complexity/Foundations/RingTheory/GaloisRing.lean +++ b/Complexity/Foundations/RingTheory/GaloisRing.lean @@ -9,8 +9,8 @@ module public import Complexity.Init public import Complexity.Foundations.Data.Polynomial.RingLagrange +public import Complexity.Foundations.RingTheory.AdjoinRoot public import Mathlib.FieldTheory.Finite.GaloisField -public import Mathlib.RingTheory.AdjoinRoot public import Mathlib.RingTheory.LocalRing.ResidueField.Defs import Mathlib.RingTheory.LocalRing.ResidueField.Basic import Mathlib.RingTheory.Polynomial.Nilpotent @@ -48,8 +48,6 @@ statement over `ℤ_(p)` is `AdjoinRoot.isUnit_of_padicValuation_eq_one`. * `RingHom.isLocalHom_of_isNilpotent`: a surjection with nilpotent kernel is a local homomorphism. -* `AdjoinRoot.map_eq_zero_iff`: an element of `R[X] / (g)` vanishes in `S[X] / (g)` exactly when - the coefficients of its reduced representative do. * `GaloisRing.ker_residue`: the kernel of reduction modulo `p` is `(p)`. * `GaloisRing.isUnit_iff`: an element is a unit exactly when it is nonzero modulo `p`. * `GaloisRing.instIsLocalRing`, `GaloisRing.maximalIdeal_eq`: the ring is local with maximal ideal @@ -97,59 +95,6 @@ theorem isUnit_iff_ne_zero_of_isNilpotent {F : Type*} [Field F] (ψ : R →+* F) end RingHom -/-! ### Reducing the coefficients of `R[X] / (g)` -/ - -namespace AdjoinRoot - -variable {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S) {g : R[X]} - -/-- Reducing the coefficients maps the class of `P` to the class of `P.map φ`. -/ -theorem map_mk (q : S[X]) (h : q ∣ g.map φ) (P : R[X]) : - map φ g q h (mk g P) = mk q (P.map φ) := by - have : (map φ g q h).comp (mk g) = (mk q).comp (mapRingHom φ) := by - refine Polynomial.ringHom_ext (fun a => ?_) ?_ - · simp only [RingHom.comp_apply, mk_C, map_of, coe_mapRingHom, Polynomial.map_C] - · simp only [RingHom.comp_apply, mk_X, map_root, coe_mapRingHom, Polynomial.map_X] - exact congrArg (fun F : R[X] →+* AdjoinRoot q => F P) this - -/-- Reducing the coefficients is surjective when `φ` is. -/ -theorem map_surjective_of_surjective (q : S[X]) (h : q ∣ g.map φ) - (hφ : Function.Surjective φ) : Function.Surjective (map φ g q h) := by - intro y - obtain ⟨Q, rfl⟩ := mk_surjective y - obtain ⟨P, rfl⟩ := Polynomial.map_surjective φ hφ Q - exact ⟨mk g P, map_mk φ q h P⟩ - -/-- **An element vanishes after reducing the coefficients** of a monic `g` exactly when the -coefficients of its representative of degree below `deg g` do: that representative reduces to a -polynomial of degree below `deg (g.map φ)`, which `g.map φ` divides only when it is zero. -/ -theorem map_eq_zero_iff [Nontrivial S] (hg : g.Monic) {q : S[X]} (h : q ∣ g.map φ) - (hq : q = g.map φ) (x : AdjoinRoot g) : - map φ g q h x = 0 ↔ ∀ i, φ ((modByMonicHom hg x).coeff i) = 0 := by - subst hq - have := φ.domain_nontrivial - obtain ⟨Q, rfl⟩ := mk_surjective x - rw [modByMonicHom_mk] - set P := Q %ₘ g - have hx : mk g P = mk g Q := by - have := mk_leftInverse hg (mk g Q) - rwa [modByMonicHom_mk] at this - have hdeg : (P.map φ).degree < (g.map φ).degree := by - rw [hg.degree_map] - exact degree_map_le.trans_lt (degree_modByMonic_lt _ hg) - rw [← hx, map_mk, mk_eq_zero] - constructor - · intro hdvd i - by_contra hne - have h0 : P.map φ ≠ 0 := fun h0 => hne (by rw [← coeff_map, h0, coeff_zero]) - exact (hg.map φ).not_dvd_of_degree_lt h0 hdeg hdvd - · intro h - have : P.map φ = 0 := Polynomial.ext fun i => by rw [coeff_map, h, coeff_zero] - rw [this] - exact dvd_zero _ - -end AdjoinRoot - /-! ### Galois rings -/ /-- The ring `(ℤ / p ^ n)[X] / (f)` presented by an integer polynomial `f`. For a prime `p`, From 5189108242a32270693556cd43044d989591fe1d Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:11:30 -0400 Subject: [PATCH 3/7] doc(foundations): scope GaloisRing to the manuscript's base ring O/(2^n) On p. 57 of the pinned manuscript, O = Z_(2)[U]/(f), A = O[V]/(V^l) and A_p = A/(2^p). `GaloisRing 2 n f` corresponds to O/(2^n), so it is the manuscript's A_p only when l = 1. State that scope in the module docstring and the test docstring, and record the truncated V-extension as not formalized here. Addresses the source-scope finding of reviewer-codex-edemaine on #1859. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity/Foundations/RingTheory/GaloisRing.lean | 10 +++++++--- ComplexityTests/Foundations/RingTheory/GaloisRing.lean | 3 ++- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/Complexity/Foundations/RingTheory/GaloisRing.lean b/Complexity/Foundations/RingTheory/GaloisRing.lean index 79a1b2965e..b9f21502ce 100644 --- a/Complexity/Foundations/RingTheory/GaloisRing.lean +++ b/Complexity/Foundations/RingTheory/GaloisRing.lean @@ -28,9 +28,13 @@ The *digit lifts* `∑ i, c i * X ^ i` with digits `c i ∈ {0, …, p - 1}` red distinct residue-field elements, so any two of them differ by a unit, and Lagrange interpolation over the ring holds at any set of them (`GaloisRing.eq_ringInterpolate_digitLift`). -This is the coefficient ring of the Boolean tensor contraction of [OpenAI2026ETH] (§D.4.1, -pp. 57–58), which takes `p = 2`, a degree `e = 4 ⌈log₂ s⌉` and the precision `n`; the manuscript's -binary-coordinate lifts are the digit lifts for `p = 2`. +This is the base coefficient ring of the Boolean tensor contraction of [OpenAI2026ETH] (§D.4.1, +pp. 57–58), with `p = 2`, a degree `e = 4 ⌈log₂ s⌉` and the precision `n`. The manuscript puts +`O = ℤ_(2)[U] / (f)` and `A = O[V] / (V ^ ℓ)`, and computes in `A / (2 ^ n)` (written `A_p` there, +with `p` the precision). `GaloisRing 2 n f` corresponds to `O / (2 ^ n)`, since +`ℤ_(2) / (2 ^ n) ≅ ℤ / 2 ^ n` (that identification is not formalized here). It is therefore the +manuscript's `A / (2 ^ n)` only when `ℓ = 1`; the truncated `V`-extension for general `ℓ` is not +formalized here. The manuscript's binary-coordinate lifts are the digit lifts for `p = 2`. The argument is that of a surjection onto a field with nilpotent kernel (`RingHom.isUnit_iff_ne_zero_of_isNilpotent`): reduction modulo `p` has kernel `(p)`, and diff --git a/ComplexityTests/Foundations/RingTheory/GaloisRing.lean b/ComplexityTests/Foundations/RingTheory/GaloisRing.lean index c11fcc94d8..9a4438a778 100644 --- a/ComplexityTests/Foundations/RingTheory/GaloisRing.lean +++ b/ComplexityTests/Foundations/RingTheory/GaloisRing.lean @@ -10,7 +10,8 @@ import Mathlib.Tactic.ComputeDegree import Mathlib.Tactic.FinCases /-! Tests for Galois rings, on `(ℤ / 8)[U] / (U ^ 2 + U + 1)`: the case `p = 2`, `e = 2` and -precision `3` of the coefficient ring of [OpenAI2026ETH], §D.4.1. -/ +precision `3` of the base coefficient ring `O / (2 ^ 3)` of [OpenAI2026ETH], §D.4.1, which is the +manuscript's `A_3` when `ℓ = 1`. -/ namespace ComplexityTests.GaloisRing From 99d9e0d69372a439fe89c955398c74361686e888 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:28:05 -0400 Subject: [PATCH 4/7] feat(PolyTime): arithmetic in (Z/2^p)[U]/(f) on coefficient lists Addition, multiplication by U and shift-and-add multiplication modulo 2^p and a monic f given by its lower coefficients, proved correct in AdjoinRoot (f mod 2^p) and certified polynomial-time with p in unary and coordinates in binary. These are the polynomial-time arithmetic claims of [OpenAI2026ETH, Appendix D.4.1] for addition and multiplication (l = 1). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../PolyTime/GaloisRingArithmetic.lean | 446 ++++++++++++++++++ ComplexityTests/GaloisRingArithmetic.lean | 59 +++ 3 files changed, 506 insertions(+) create mode 100644 Complexity/Computability/PolyTime/GaloisRingArithmetic.lean create mode 100644 ComplexityTests/GaloisRingArithmetic.lean diff --git a/Complexity.lean b/Complexity.lean index fdd3b220c6..566b83dcbd 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1985,6 +1985,7 @@ public import Complexity.Computability.PolyTime.CNF.SparsePolyCompile public import Complexity.Computability.PolyTime.CSP.ToCNF public import Complexity.Computability.PolyTime.CommonCountingAccum public import Complexity.Computability.PolyTime.FineGrained.ParameterCheck +public import Complexity.Computability.PolyTime.GaloisRingArithmetic public import Complexity.Computability.PolyTime.GreedyLabelSchedule public import Complexity.Computability.PolyTime.GreedySlotScore public import Complexity.Computability.PolyTime.Int.ExactDiv diff --git a/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean b/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean new file mode 100644 index 0000000000..b46df67660 --- /dev/null +++ b/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean @@ -0,0 +1,446 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Data.ZMod.Basic +public import Mathlib.RingTheory.AdjoinRoot +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Fold +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryDivision +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListLookup +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListMap +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeLoops +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Data.List.GetD +import Mathlib.Data.Nat.Size + +/-! +# Arithmetic modulo `2 ^ p` and a monic polynomial, on coefficient lists + +The coefficient rings of the contraction algorithm of [OpenAI2026ETH] (Appendix D.4.1, p. 57) are +`A_p = (ℤ / 2 ^ p)[U] / (f)` for a monic `f ∈ ℤ[U]` of degree `e`. An element is represented in the +basis `1, U, …, U ^ (e - 1)` by its list of coordinates, each an integer residue modulo `2 ^ p`. +The monic polynomial is given by the list `fl` of its coefficients below the leading one +(`GaloisRingArith.monicOf`), so `e` is the length of `fl`. With `f` irreducible modulo `2`, `A_p` is +the Galois ring `(ℤ / 2 ^ p)[U] / (f)`; nothing here needs irreducibility. + +The value of a coefficient list `c` is `∑ i < e, c i U ^ i` in `A_p` (`GaloisRingArith.val`). + +* **Addition** (`GaloisRingArith.add`) adds coordinates modulo `2 ^ p`. +* **Multiplication by `U`** (`GaloisRingArith.mulX`) shifts the coordinates up and subtracts the top + coordinate times `f`, reducing `U ^ e = -∑ i < e, fl i U ^ i`. +* **Multiplication** (`GaloisRingArith.mul`) is shift-and-add: `c d = ∑ i < e, c i (U ^ i d)`, + accumulating `c i` times the current `U ^ i d` and multiplying it by `U`, `e` times. + +Each operation is correct (`GaloisRingArith.val_add`, `GaloisRingArith.val_mulX`, +`GaloisRingArith.val_mul`) and polynomial-time, with the precision `p` in unary and the +coordinates and the coefficients of `f` in binary (`GaloisRingArith.computableInPolyTime_add`, +`GaloisRingArith.computableInPolyTime_mul`). Their outputs are reduced, with `e` coordinates below +`2 ^ p` (`GaloisRingArith.length_mul`, `GaloisRingArith.lt_of_mem_mul`). These are the +polynomial-time arithmetic claims of Appendix D.4.1 for addition and multiplication, in the case +`ℓ = 1` of the source, where `A = O` has no `V`-coordinates. Inversion of units, which the source +does by Newton lifting, is not covered here. + +## Main definitions + +* `Cslib.GaloisRingArith.monicOf`: the monic polynomial with given lower coefficients. +* `Cslib.GaloisRingArith.val`: the value of a coefficient list. +* `Cslib.GaloisRingArith.add`, `Cslib.GaloisRingArith.mulX`, `Cslib.GaloisRingArith.mul`: addition, + multiplication by `U` and multiplication. + +## Main results + +* `Cslib.GaloisRingArith.val_add`, `Cslib.GaloisRingArith.val_mulX`, + `Cslib.GaloisRingArith.val_mul`: correctness. +* `Cslib.GaloisRingArith.computableInPolyTime_add`, + `Cslib.GaloisRingArith.computableInPolyTime_mulX`, + `Cslib.GaloisRingArith.computableInPolyTime_mul`: polynomial time. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.4.1 (p. 57). +-/ + +@[expose] public section + +namespace Cslib.GaloisRingArith + +open Polynomial Finset + +/-- The monic polynomial `U ^ e + ∑ i < e, fl i U ^ i` of degree `e = fl.length`. -/ +noncomputable def monicOf (fl : List ℕ) : ℤ[X] := + X ^ fl.length + ∑ i ∈ range fl.length, C (fl.getD i 0 : ℤ) * X ^ i + +/-- `monicOf fl` is monic, of degree `fl.length`. -/ +theorem monic_monicOf (fl : List ℕ) : (monicOf fl).Monic := by + unfold monicOf + apply monic_X_pow_add + refine (degree_sum_le _ _).trans_lt ?_ + rw [Finset.sup_lt_iff (WithBot.bot_lt_coe _)] + intro i hi + exact (degree_C_mul_X_pow_le _ _).trans_lt (WithBot.coe_lt_coe.mpr (mem_range.mp hi)) + +/-- The ring `A_p = (ℤ / 2 ^ p)[U] / (f)` for `f = monicOf fl`. -/ +abbrev Ring (p : ℕ) (fl : List ℕ) : Type := + AdjoinRoot ((monicOf fl).map (Int.castRingHom (ZMod (2 ^ p)))) + +/-- The value `∑ i < e, c i U ^ i` of a coefficient list in `A_p`, with `e = fl.length`. +Coordinates past `e` are ignored and missing ones are zero. -/ +noncomputable def val (p : ℕ) (fl c : List ℕ) : Ring p fl := + ∑ i ∈ range fl.length, ((c.getD i 0 : ℕ) : Ring p fl) * AdjoinRoot.root _ ^ i + +/-- Coordinatewise sum modulo `2 ^ p`. -/ +def add (p : ℕ) (fl c d : List ℕ) : List ℕ := + (List.range fl.length).map fun i => (c.getD i 0 + d.getD i 0) % 2 ^ p + +/-- Add `k` times `d` to `c`, coordinatewise modulo `2 ^ p`. -/ +def addSmul (p : ℕ) (fl c : List ℕ) (k : ℕ) (d : List ℕ) : List ℕ := + (List.range fl.length).map fun i => (c.getD i 0 + k * d.getD i 0) % 2 ^ p + +/-- Multiplication by `U`: shift the coordinates up and subtract the top coordinate times the +lower coefficients of `f`, modulo `2 ^ p`. -/ +def mulX (p : ℕ) (fl c : List ℕ) : List ℕ := + (List.range fl.length).map fun i => + ((0 :: c).getD i 0 + (2 ^ p - c.getD (fl.length - 1) 0 * fl.getD i 0 % 2 ^ p)) % 2 ^ p + +/-- The zero element, with `e` coordinates. -/ +def zero (fl : List ℕ) : List ℕ := (List.range fl.length).map fun _ => 0 + +/-- One step of shift-and-add multiplication by `c`: from `(U ^ i d, ∑ j < i, c j U ^ j d)`, +add `c i U ^ i d` to the accumulator and multiply the current power by `U`. -/ +def mulStep (p : ℕ) (fl c : List ℕ) (s : List ℕ × List ℕ) (i : ℕ) : List ℕ × List ℕ := + (mulX p fl s.1, addSmul p fl s.2 (c.getD i 0) s.1) + +/-- **Multiplication** by shift-and-add. -/ +def mul (p : ℕ) (fl c d : List ℕ) : List ℕ := + ((List.range fl.length).foldl (mulStep p fl c) (d, zero fl)).2 + +/-! ### Correctness -/ + +section Correctness + +variable {p : ℕ} {fl : List ℕ} + +theorem natCast_two_pow : ((2 ^ p : ℕ) : Ring p fl) = 0 := by + rw [← map_natCast (algebraMap (ZMod (2 ^ p)) (Ring p fl)), ZMod.natCast_self, map_zero] + +theorem natCast_mod_two_pow (x : ℕ) : ((x % 2 ^ p : ℕ) : Ring p fl) = (x : Ring p fl) := by + conv_rhs => rw [← Nat.mod_add_div x (2 ^ p)] + rw [Nat.cast_add, Nat.cast_mul, natCast_two_pow, zero_mul, add_zero] + +/-- The root satisfies `U ^ e = -∑ i < e, fl i U ^ i`. -/ +theorem root_pow_length : + (AdjoinRoot.root _ : Ring p fl) ^ fl.length = + -∑ i ∈ range fl.length, ((fl.getD i 0 : ℕ) : Ring p fl) * AdjoinRoot.root _ ^ i := by + have hmap : (monicOf fl).map (Int.castRingHom (ZMod (2 ^ p))) = X ^ fl.length + + ∑ i ∈ range fl.length, C ((fl.getD i 0 : ℕ) : ZMod (2 ^ p)) * X ^ i := by + simp [monicOf, Polynomial.map_sum] + have h := AdjoinRoot.eval₂_root ((monicOf fl).map (Int.castRingHom (ZMod (2 ^ p)))) + conv at h => lhs; arg 3; rw [hmap] + simp only [eval₂_add, eval₂_finsetSum, eval₂_mul, eval₂_natCast, eval₂_X_pow, + map_natCast] at h + exact eq_neg_of_add_eq_zero_left h + +@[simp] theorem val_zero : val p fl (zero fl) = 0 := by + refine sum_eq_zero fun i hi => ?_ + rw [zero, List.getD_eq_getElem _ _ (by simpa using hi)] + simp + +/-- **Addition is correct.** -/ +theorem val_add (c d : List ℕ) : val p fl (add p fl c d) = val p fl c + val p fl d := by + rw [val, val, val, ← sum_add_distrib] + refine sum_congr rfl fun i hi => ?_ + rw [add, List.getD_eq_getElem _ _ (by simpa using hi)] + simp only [List.getElem_map, List.getElem_range, natCast_mod_two_pow, Nat.cast_add, add_mul] + +/-- **Adding a multiple is correct.** -/ +theorem val_addSmul (c : List ℕ) (k : ℕ) (d : List ℕ) : + val p fl (addSmul p fl c k d) = val p fl c + (k : Ring p fl) * val p fl d := by + rw [val, val, val, mul_sum, ← sum_add_distrib] + refine sum_congr rfl fun i hi => ?_ + rw [addSmul, List.getD_eq_getElem _ _ (by simpa using hi)] + simp only [List.getElem_map, List.getElem_range, natCast_mod_two_pow, Nat.cast_add, + Nat.cast_mul] + ring + +/-- Shifting coordinates and subtracting the top one times the lower coefficients of `f` is +multiplication by a root of `f`, in any commutative ring. -/ +private theorem shift_sub_mul_sum {R : Type*} [CommRing R] (r : R) (cs fs : ℕ → R) (e : ℕ) + (hroot : r ^ (e + 1) = -∑ i ∈ range (e + 1), fs i * r ^ i) : + ∑ i ∈ range (e + 1), ((if i = 0 then 0 else cs (i - 1)) - cs e * fs i) * r ^ i = + r * ∑ i ∈ range (e + 1), cs i * r ^ i := by + simp only [sub_mul, sum_sub_distrib] + rw [sum_range_succ' (fun i => (if i = 0 then 0 else cs (i - 1)) * r ^ i)] + simp only [Nat.add_sub_cancel, Nat.succ_ne_zero, ite_false, ite_true, zero_mul, add_zero] + rw [mul_sum, sum_range_succ (fun i => r * (cs i * r ^ i)), + show r * (cs e * r ^ e) = cs e * r ^ (e + 1) by ring, hroot, mul_neg, mul_sum, + ← sub_eq_add_neg] + congr 1 + · exact sum_congr rfl fun i _ => by ring + · exact sum_congr rfl fun i _ => by ring + +/-- **Multiplication by `U` is correct.** -/ +theorem val_mulX (c : List ℕ) : + val p fl (mulX p fl c) = AdjoinRoot.root _ * val p fl c := by + -- Each coordinate is the shifted coordinate minus the top coordinate times `fl i`. + have hcoord (i : ℕ) (hi : i < fl.length) : (((mulX p fl c).getD i 0 : ℕ) : Ring p fl) = + (if i = 0 then 0 else (c.getD (i - 1) 0 : Ring p fl)) - + (c.getD (fl.length - 1) 0 : Ring p fl) * (fl.getD i 0 : Ring p fl) := by + rw [mulX, List.getD_eq_getElem _ _ (by simpa using hi)] + simp only [List.getElem_map, List.getElem_range, natCast_mod_two_pow, Nat.cast_add] + rw [Nat.cast_sub (Nat.mod_lt _ (Nat.two_pow_pos p)).le, natCast_two_pow, natCast_mod_two_pow, + Nat.cast_mul] + rcases i with _ | i <;> simp [sub_eq_add_neg] + rcases Nat.eq_zero_or_pos fl.length with he | he + · simp [val, he] + obtain ⟨e, he'⟩ := Nat.exists_eq_add_of_lt he + rw [Nat.zero_add] at he' + have hroot := root_pow_length (p := p) (fl := fl) + rw [val, val, sum_congr rfl fun i hi => by rw [hcoord i (mem_range.mp hi)]] + rw [he', Nat.add_sub_cancel] at * + exact shift_sub_mul_sum _ (fun i => (c.getD i 0 : Ring p fl)) (fun i => (fl.getD i 0 : Ring p fl)) + e hroot + +/-- **Multiplication is correct.** -/ +theorem val_mul (c d : List ℕ) : val p fl (mul p fl c d) = val p fl c * val p fl d := by + -- After `j` steps the state is `(U ^ j d, ∑ i < j, c i U ^ i d)`. + have hinv (j : ℕ) : + val p fl ((List.range j).foldl (mulStep p fl c) (d, zero fl)).1 = + AdjoinRoot.root _ ^ j * val p fl d ∧ + val p fl ((List.range j).foldl (mulStep p fl c) (d, zero fl)).2 = + (∑ i ∈ range j, ((c.getD i 0 : ℕ) : Ring p fl) * AdjoinRoot.root _ ^ i) * val p fl d := by + induction j with + | zero => simp + | succ j ih => + rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, mulStep] + refine ⟨?_, ?_⟩ + · rw [val_mulX, ih.1, pow_succ]; ring + · rw [val_addSmul, ih.1, ih.2, sum_range_succ]; ring + rw [mul, (hinv fl.length).2] + rfl + +end Correctness + +/-! ### Reduced outputs -/ + +@[simp] theorem length_add (p : ℕ) (fl c d : List ℕ) : (add p fl c d).length = fl.length := by + simp [add] + +@[simp] theorem length_addSmul (p : ℕ) (fl c : List ℕ) (k : ℕ) (d : List ℕ) : + (addSmul p fl c k d).length = fl.length := by + simp [addSmul] + +@[simp] theorem length_mulX (p : ℕ) (fl c : List ℕ) : (mulX p fl c).length = fl.length := by + simp [mulX] + +@[simp] theorem length_zero (fl : List ℕ) : (zero fl).length = fl.length := by simp [zero] + +theorem lt_of_mem_add {p : ℕ} {fl c d : List ℕ} {x : ℕ} (hx : x ∈ add p fl c d) : x < 2 ^ p := by + obtain ⟨i, -, rfl⟩ := List.mem_map.mp hx + exact Nat.mod_lt _ (Nat.two_pow_pos p) + +theorem lt_of_mem_addSmul {p : ℕ} {fl c : List ℕ} {k : ℕ} {d : List ℕ} {x : ℕ} + (hx : x ∈ addSmul p fl c k d) : x < 2 ^ p := by + obtain ⟨i, -, rfl⟩ := List.mem_map.mp hx + exact Nat.mod_lt _ (Nat.two_pow_pos p) + +theorem lt_of_mem_mulX {p : ℕ} {fl c : List ℕ} {x : ℕ} (hx : x ∈ mulX p fl c) : x < 2 ^ p := by + obtain ⟨i, -, rfl⟩ := List.mem_map.mp hx + exact Nat.mod_lt _ (Nat.two_pow_pos p) + +theorem length_mul (p : ℕ) (fl c d : List ℕ) : (mul p fl c d).length = fl.length := by + rcases Nat.eq_zero_or_pos fl.length with he | he + · simp [mul, he, zero] + obtain ⟨e, he'⟩ := Nat.exists_eq_add_of_lt he + rw [mul, Nat.zero_add] at * + rw [he', List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, mulStep, + length_addSmul, he'] + +theorem lt_of_mem_mul {p : ℕ} {fl c d : List ℕ} {x : ℕ} (hx : x ∈ mul p fl c d) : x < 2 ^ p := by + rcases Nat.eq_zero_or_pos fl.length with he | he + · simp [mul, he, zero] at hx + obtain ⟨e, he'⟩ := Nat.exists_eq_add_of_lt he + rw [Nat.zero_add] at he' + rw [mul, he', List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, + mulStep] at hx + exact lt_of_mem_addSmul hx + +/-! ### Polynomial time -/ + +section PolyTime + +open Turing.MultiTapeTM + +variable {α : Type} {encIn : α ↪ List Bool} + +/-- Reduction modulo `2 ^ p`, with `p` in unary. -/ +@[fun_prop] +theorem computableInPolyTime_mod_two_pow {x p : α → ℕ} + (hx : ComputableInPolyTime x encIn encNat) (hp : ComputableInPolyTime p encIn encUnary) : + ComputableInPolyTime (fun a => x a % 2 ^ p a) encIn encNat := + ComputableInPolyTime.binary_mod.comp (hx.prod (ComputableInPolyTime.binary_two_pow.comp hp)) + +/-- A coordinate, at a unary index. -/ +theorem computableInPolyTime_getD {c : α → List ℕ} {i : α → ℕ} + (hc : ComputableInPolyTime c encIn (encList encNat)) + (hi : ComputableInPolyTime i encIn encUnary) : + ComputableInPolyTime (fun a => (c a).getD (i a) 0) encIn encNat := + (ComputableInPolyTime.listGetD (encA := encNat) 0).comp (hc.prod hi) + +/-- Tabulating `e` coordinates, for a unary `e`. -/ +theorem computableInPolyTime_tabulate {n : α → ℕ} {g : α → ℕ → ℕ} + (hn : ComputableInPolyTime n encIn encUnary) + (hg : ComputableInPolyTime (fun q : α × ℕ => g q.1 q.2) (encPair encIn encUnary) encNat) : + ComputableInPolyTime (fun x => (List.range (n x)).map (g x)) encIn (encList encNat) := + ComputableInPolyTime.mapWithInput (ComputableInPolyTime.range.comp hn) hg + +private theorem length_polyTime {fl : α → List ℕ} + (hfl : ComputableInPolyTime fl encIn (encList encNat)) : + ComputableInPolyTime (fun x => (fl x).length) encIn encUnary := + (ComputableInPolyTime.length_list encNat).comp hfl + +/-- **Addition is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_add {p : α → ℕ} {fl c d : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) + (hd : ComputableInPolyTime d encIn (encList encNat)) : + ComputableInPolyTime (fun x => add (p x) (fl x) (c x) (d x)) encIn (encList encNat) := by + have h1 := ComputableInPolyTime.fst encIn encUnary + have h2 := ComputableInPolyTime.snd encIn encUnary + exact computableInPolyTime_tabulate (length_polyTime hfl) + (computableInPolyTime_mod_two_pow (ComputableInPolyTime.binary_add.comp + ((computableInPolyTime_getD (hc.comp h1) h2).prod + (computableInPolyTime_getD (hd.comp h1) h2))) (hp.comp h1)) + +/-- **Adding a multiple is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_addSmul {p k : α → ℕ} {fl c d : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) + (hk : ComputableInPolyTime k encIn encNat) + (hd : ComputableInPolyTime d encIn (encList encNat)) : + ComputableInPolyTime (fun x => addSmul (p x) (fl x) (c x) (k x) (d x)) encIn + (encList encNat) := by + have h1 := ComputableInPolyTime.fst encIn encUnary + have h2 := ComputableInPolyTime.snd encIn encUnary + exact computableInPolyTime_tabulate (length_polyTime hfl) + (computableInPolyTime_mod_two_pow (ComputableInPolyTime.binary_add.comp + ((computableInPolyTime_getD (hc.comp h1) h2).prod + (ComputableInPolyTime.binary_mul' (hk.comp h1) + (computableInPolyTime_getD (hd.comp h1) h2)))) (hp.comp h1)) + +/-- **Multiplication by `U` is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_mulX {p : α → ℕ} {fl c : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) : + ComputableInPolyTime (fun x => mulX (p x) (fl x) (c x)) encIn (encList encNat) := by + have h1 := ComputableInPolyTime.fst encIn encUnary + have h2 := ComputableInPolyTime.snd encIn encUnary + have hshift := computableInPolyTime_getD + (ComputableInPolyTime.cons' (ComputableInPolyTime.const 0) (hc.comp h1)) h2 + have htop := computableInPolyTime_getD (hc.comp h1) + (ComputableInPolyTime.unary_sub' (length_polyTime (hfl.comp h1)) + (ComputableInPolyTime.const 1)) + have hsub := computableInPolyTime_mod_two_pow + (ComputableInPolyTime.binary_mul' htop (computableInPolyTime_getD (hfl.comp h1) h2)) + (hp.comp h1) + exact computableInPolyTime_tabulate (length_polyTime hfl) + (computableInPolyTime_mod_two_pow (ComputableInPolyTime.binary_add.comp (hshift.prod + (ComputableInPolyTime.binary_sub' (ComputableInPolyTime.binary_two_pow.comp (hp.comp h1)) + hsub))) (hp.comp h1)) + +/-- A reduced coefficient list, with `e` coordinates below `2 ^ p`, is at most +`e (2 p + 1)` long in binary. -/ +theorem length_encList_le {p e : ℕ} {c : List ℕ} (hlen : c.length = e) + (hlt : ∀ x ∈ c, x < 2 ^ p) : (encList encNat c).length ≤ e * (2 * p + 1) := by + rw [length_encList] + calc (c.map fun x => 2 * (encNat x).length + 1).sum + ≤ (c.map fun x => 2 * (encNat x).length + 1).length • (2 * p + 1) := + List.sum_le_length_nsmul _ _ fun n hn => by + obtain ⟨x, hx, rfl⟩ := List.mem_map.mp hn + have : (encNat x).length ≤ p := by + change x.bits.length ≤ p + rw [Nat.size_eq_bits_len] at * + exact (Nat.size_eq_bits_len x ▸ Nat.size_le.mpr (hlt x hx)) + omega + _ = e * (2 * p + 1) := by rw [List.length_map, hlen, smul_eq_mul] + +/-- **Multiplication is polynomial-time**, with the precision in unary. Every intermediate pair is +reduced after its first step, so its length is bounded by the precision and the degree. -/ +@[fun_prop] +theorem computableInPolyTime_mul {p : α → ℕ} {fl c d : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) + (hd : ComputableInPolyTime d encIn (encList encNat)) : + ComputableInPolyTime (fun x => mul (p x) (fl x) (c x) (d x)) encIn (encList encNat) := by + let encS := encPair (encList encNat) (encList encNat) + have hinit : ComputableInPolyTime (fun x => (d x, zero (fl x))) encIn encS := + hd.prod (computableInPolyTime_tabulate (g := fun _ _ => 0) (length_polyTime hfl) + (ComputableInPolyTime.const 0)) + have hrange : ComputableInPolyTime (fun x => List.range (fl x).length) encIn + (encList encUnary) := + ComputableInPolyTime.range.comp (length_polyTime hfl) + -- The step, on the input, the state and the unary index. + have hstep : ComputableInPolyTime + (fun q : (α × (List ℕ × List ℕ)) × ℕ => mulStep (p q.1.1) (fl q.1.1) (c q.1.1) q.1.2 q.2) + (encPair (encPair encIn encS) encUnary) encS := by + have hq := ComputableInPolyTime.fst (encPair encIn encS) encUnary + have hx := (ComputableInPolyTime.fst encIn encS).comp hq + have hs := (ComputableInPolyTime.snd encIn encS).comp hq + have hi := ComputableInPolyTime.snd (encPair encIn encS) encUnary + have hcur := (ComputableInPolyTime.fst (encList encNat) (encList encNat)).comp hs + have hacc := (ComputableInPolyTime.snd (encList encNat) (encList encNat)).comp hs + exact (computableInPolyTime_mulX (hp.comp hx) (hfl.comp hx) hcur).prod + (computableInPolyTime_addSmul (hp.comp hx) (hfl.comp hx) hacc + (computableInPolyTime_getD (hc.comp hx) hi) hcur) + -- Every step's output is reduced, hence of bounded length. + have hgrowth : PolyBounded (fun x => (encIn x).length) + (fun x => 3 * ((fl x).length * (2 * p x + 1)) + 1) := by + have hpl := (ComputableInPolyTime.polyBounded_length hp) + have hfll := (ComputableInPolyTime.polyBounded_length hfl) + refine (((PolyBounded.const 3).mul (hfll.mul (((PolyBounded.const 2).mul hpl).add + (PolyBounded.const 1)))).add (PolyBounded.const 1)).mono fun x => ?_ + have h1 : p x ≤ (encUnary (p x)).length := by simp + have h2 : (fl x).length ≤ (encList encNat (fl x)).length := by + rw [length_encList] + calc (fl x).length = ((fl x).map fun _ => 1).sum := by simp + _ ≤ ((fl x).map fun a => 2 * (encNat a).length + 1).sum := + List.sum_le_sum fun a _ => by omega + have := Nat.mul_le_mul h2 (Nat.add_le_add_right (Nat.mul_le_mul_left 2 h1) 1) + omega + have hfold := ComputableInPolyTime.foldlWithInput_of_bounded_growth + (encA := encUnary) (encL := encList encUnary) + (step := fun x s i => mulStep (p x) (fl x) (c x) s i) hinit + ⟨hrange, hstep, inferInstance, inferInstance⟩ ⟨hgrowth, fun x s i _ => ?_⟩ + · exact (ComputableInPolyTime.snd (encList encNat) (encList encNat)).comp hfold + · have hcur := length_encList_le (length_mulX (p x) (fl x) s.1) fun _ h => lt_of_mem_mulX h + have hacc := length_encList_le (length_addSmul (p x) (fl x) s.2 ((c x).getD i 0) s.1) + fun _ h => lt_of_mem_addSmul h + simp only [mulStep, encS, length_encPair] + omega + +end PolyTime + +end Cslib.GaloisRingArith diff --git a/ComplexityTests/GaloisRingArithmetic.lean b/ComplexityTests/GaloisRingArithmetic.lean new file mode 100644 index 0000000000..566fca586f --- /dev/null +++ b/ComplexityTests/GaloisRingArithmetic.lean @@ -0,0 +1,59 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.PolyTime.GaloisRingArithmetic + +/-! # Arithmetic in `(ℤ / 2 ^ p)[U] / (f)` on coefficient lists + +Concrete products in the Galois ring `(ℤ / 8)[U] / (U ^ 2 + U + 1)` (`p = 3`, `fl = [1, 1]`), the +correctness statements, and the polynomial-time certificates in closed form, with the precision +in unary and the coordinates in binary. -/ + +namespace ComplexityTests.GaloisRingArithmetic + +open Cslib.GaloisRingArith Turing.MultiTapeTM + +-- `U * U = U ^ 2 = -1 - U`, that is `7 + 7 U` modulo `8`. +example : mulX 3 [1, 1] [0, 1] = [7, 7] := by decide + +-- `(1 + 2 U) (3 + U) = 3 + 7 U + 2 U ^ 2 = 1 + 5 U` modulo `8` and `U ^ 2 + U + 1`. +example : mul 3 [1, 1] [1, 2] [3, 1] = [1, 5] := by decide + +-- Addition reduces each coordinate: `(7 + 5 U) + (3 + 6 U) = 2 + 3 U` modulo `8`. +example : add 3 [1, 1] [7, 5] [3, 6] = [2, 3] := by decide + +-- `U` has order `3` here: `U ^ 3 = 1`. +example : mul 3 [1, 1] [0, 1] (mul 3 [1, 1] [0, 1] [0, 1]) = [1, 0] := by decide + +-- Unreduced inputs are reduced: missing coordinates are zero, extra ones ignored. +example : mul 3 [1, 1] [9] [3, 1, 4] = [3, 1] := by decide + +-- Degree three, `f = U ^ 3 + U + 1`, modulo `16`: `U ^ 2 * U = U ^ 3 = -1 - U`. +example : mulX 4 [1, 1, 0] [0, 0, 1] = [15, 15, 0] := by decide + +/-- The defining polynomial is monic. -/ +example : (monicOf [1, 1]).Monic := monic_monicOf _ + +/-- Multiplication is correct in the ring itself. -/ +example (c d : List ℕ) : val 3 [1, 1] (mul 3 [1, 1] c d) = val 3 [1, 1] c * val 3 [1, 1] d := + val_mul c d + +/-- **Multiplication in polynomial time**, on the ring description `(p, fl)` with `p` in unary +and the two coefficient lists in binary. -/ +example : ComputableInPolyTime + (fun q : (ℕ × List ℕ) × (List ℕ × List ℕ) => mul q.1.1 q.1.2 q.2.1 q.2.2) + (encPair (encPair encUnary (encList encNat)) (encPair (encList encNat) (encList encNat))) + (encList encNat) := by + fun_prop + +/-- **Addition in polynomial time**, in the same encoding. -/ +example : ComputableInPolyTime + (fun q : (ℕ × List ℕ) × (List ℕ × List ℕ) => add q.1.1 q.1.2 q.2.1 q.2.2) + (encPair (encPair encUnary (encList encNat)) (encPair (encList encNat) (encList encNat))) + (encList encNat) := by + fun_prop + +end ComplexityTests.GaloisRingArithmetic From b9caee50441cd14c22ce4d3f0285c1f20bed8e32 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:36:29 -0400 Subject: [PATCH 5/7] feat(PolyTime): unit and powers in (Z/2^p)[U]/(f) Powers c^k by k multiplications, with k in unary (the mode exponents of [OpenAI2026ETH, Appendix D.4.6] are below the precision). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../PolyTime/GaloisRingArithmetic.lean | 93 ++++++++++++++++++- ComplexityTests/GaloisRingArithmetic.lean | 17 ++++ 2 files changed, 106 insertions(+), 4 deletions(-) diff --git a/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean b/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean index b46df67660..8a9bfcd2a5 100644 --- a/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean +++ b/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean @@ -47,6 +47,9 @@ The value of a coefficient list `c` is `∑ i < e, c i U ^ i` in `A_p` (`GaloisR coordinate times `f`, reducing `U ^ e = -∑ i < e, fl i U ^ i`. * **Multiplication** (`GaloisRingArith.mul`) is shift-and-add: `c d = ∑ i < e, c i (U ^ i d)`, accumulating `c i` times the current `U ^ i d` and multiplying it by `U`, `e` times. +* **Powers** (`GaloisRingArith.pow`) `c ^ k` take `k` multiplications from `GaloisRingArith.one`, + with `k` in unary. In the source the exponents of the mode substitutions are below the + precision (Appendix D.4.6, p. 63), so they are polynomial. Each operation is correct (`GaloisRingArith.val_add`, `GaloisRingArith.val_mulX`, `GaloisRingArith.val_mul`) and polynomial-time, with the precision `p` in unary and the @@ -61,16 +64,19 @@ does by Newton lifting, is not covered here. * `Cslib.GaloisRingArith.monicOf`: the monic polynomial with given lower coefficients. * `Cslib.GaloisRingArith.val`: the value of a coefficient list. -* `Cslib.GaloisRingArith.add`, `Cslib.GaloisRingArith.mulX`, `Cslib.GaloisRingArith.mul`: addition, - multiplication by `U` and multiplication. +* `Cslib.GaloisRingArith.add`, `Cslib.GaloisRingArith.mulX`, `Cslib.GaloisRingArith.mul`, + `Cslib.GaloisRingArith.one`, `Cslib.GaloisRingArith.pow`: addition, multiplication by `U`, + multiplication, the unit and powers. ## Main results * `Cslib.GaloisRingArith.val_add`, `Cslib.GaloisRingArith.val_mulX`, - `Cslib.GaloisRingArith.val_mul`: correctness. + `Cslib.GaloisRingArith.val_mul`, `Cslib.GaloisRingArith.val_one`, + `Cslib.GaloisRingArith.val_pow`: correctness. * `Cslib.GaloisRingArith.computableInPolyTime_add`, `Cslib.GaloisRingArith.computableInPolyTime_mulX`, - `Cslib.GaloisRingArith.computableInPolyTime_mul`: polynomial time. + `Cslib.GaloisRingArith.computableInPolyTime_mul`, + `Cslib.GaloisRingArith.computableInPolyTime_pow`: polynomial time. ## References @@ -131,6 +137,13 @@ def mulStep (p : ℕ) (fl c : List ℕ) (s : List ℕ × List ℕ) (i : ℕ) : L def mul (p : ℕ) (fl c d : List ℕ) : List ℕ := ((List.range fl.length).foldl (mulStep p fl c) (d, zero fl)).2 +/-- The unit element `1`, with `e` coordinates. -/ +def one (fl : List ℕ) : List ℕ := (List.range fl.length).map fun i => if i = 0 then 1 else 0 + +/-- **Powers** `c ^ k`, by `k` multiplications; the exponent is read in unary. -/ +def pow (p : ℕ) (fl c : List ℕ) (k : ℕ) : List ℕ := + (List.range k).foldl (fun acc _ => mul p fl acc c) (one fl) + /-! ### Correctness -/ section Correctness @@ -235,6 +248,34 @@ theorem val_mul (c d : List ℕ) : val p fl (mul p fl c d) = val p fl c * val p rw [mul, (hinv fl.length).2] rfl +/-- **The unit is correct.** -/ +@[simp] theorem val_one : val p fl (one fl) = 1 := by + rcases Nat.eq_zero_or_pos fl.length with he | he + · -- The defining polynomial is `1`, so the ring is trivial. + have h1 : (monicOf fl).map (Int.castRingHom (ZMod (2 ^ p))) = 1 := by + simp [monicOf, he] + have h : (1 : Ring p fl) = 0 := by + rw [← map_one (AdjoinRoot.mk ((monicOf fl).map (Int.castRingHom (ZMod (2 ^ p))))), + AdjoinRoot.mk_eq_zero, h1] + simp [val, he, h] + · obtain ⟨e, he'⟩ := Nat.exists_eq_add_of_lt he + rw [Nat.zero_add] at he' + rw [val, he', sum_range_succ'] + simp only [one, he'] + rw [sum_eq_zero fun i hi => by + rw [List.getD_eq_getElem _ _ (by simp at hi ⊢; omega)] + simp] + rw [List.getD_eq_getElem _ _ (by simp)] + simp + +/-- **Powers are correct.** -/ +theorem val_pow (c : List ℕ) (k : ℕ) : val p fl (pow p fl c k) = val p fl c ^ k := by + rw [pow] + induction k with + | zero => simp + | succ k ih => rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, + val_mul, ih, pow_succ] + end Correctness /-! ### Reduced outputs -/ @@ -441,6 +482,50 @@ theorem computableInPolyTime_mul {p : α → ℕ} {fl c d : α → List ℕ} simp only [mulStep, encS, length_encPair] omega +/-- **Powers are polynomial-time**, with the precision and the exponent in unary. -/ +@[fun_prop] +theorem computableInPolyTime_pow {p k : α → ℕ} {fl c : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) + (hk : ComputableInPolyTime k encIn encUnary) : + ComputableInPolyTime (fun x => pow (p x) (fl x) (c x) (k x)) encIn (encList encNat) := by + have hone : ComputableInPolyTime (fun x => one (fl x)) encIn (encList encNat) := by + have h2 := ComputableInPolyTime.snd encIn encUnary + refine computableInPolyTime_tabulate (g := fun _ i => if i = 0 then 1 else 0) + (length_polyTime hfl) ?_ + refine (ComputableInPolyTime.ite (encMid := encNat) (c := fun q : α × ℕ => q.2 == 0) + ((ComputableInPolyTime.beq (h2) (ComputableInPolyTime.const 0))) + (ComputableInPolyTime.const 1) (ComputableInPolyTime.const 0)).of_enc_eq fun q => ?_ + by_cases h : q.2 = 0 <;> simp [h] + have hstep : ComputableInPolyTime (fun q : (α × List ℕ) × ℕ => mul (p q.1.1) (fl q.1.1) q.1.2 + (c q.1.1)) (encPair (encPair encIn (encList encNat)) encUnary) (encList encNat) := by + have hq := ComputableInPolyTime.fst (encPair encIn (encList encNat)) encUnary + have hx := (ComputableInPolyTime.fst encIn (encList encNat)).comp hq + have hacc := (ComputableInPolyTime.snd encIn (encList encNat)).comp hq + exact computableInPolyTime_mul (hp.comp hx) (hfl.comp hx) hacc (hc.comp hx) + have hgrowth : PolyBounded (fun x => (encIn x).length) + (fun x => (fl x).length * (2 * p x + 1)) := by + have hpl := (ComputableInPolyTime.polyBounded_length hp) + have hfll := (ComputableInPolyTime.polyBounded_length hfl) + refine (hfll.mul (((PolyBounded.const 2).mul hpl).add (PolyBounded.const 1))).mono + fun x => ?_ + have h1 : p x ≤ (encUnary (p x)).length := by simp + have h2 : (fl x).length ≤ (encList encNat (fl x)).length := by + rw [length_encList] + calc (fl x).length = ((fl x).map fun _ => 1).sum := by simp + _ ≤ ((fl x).map fun a => 2 * (encNat a).length + 1).sum := + List.sum_le_sum fun a _ => by omega + exact Nat.mul_le_mul h2 (Nat.add_le_add_right (Nat.mul_le_mul_left 2 h1) 1) + have hfold := ComputableInPolyTime.foldlWithInput_of_bounded_growth + (encA := encUnary) (encL := encList encUnary) + (step := fun x acc _ => mul (p x) (fl x) acc (c x)) hone + ⟨ComputableInPolyTime.range.comp hk, hstep, inferInstance, inferInstance⟩ + ⟨hgrowth, fun x acc _ _ => ?_⟩ + · exact hfold + · have := length_encList_le (length_mul (p x) (fl x) acc (c x)) fun _ h => lt_of_mem_mul h + omega + end PolyTime end Cslib.GaloisRingArith diff --git a/ComplexityTests/GaloisRingArithmetic.lean b/ComplexityTests/GaloisRingArithmetic.lean index 566fca586f..f0e7710ba4 100644 --- a/ComplexityTests/GaloisRingArithmetic.lean +++ b/ComplexityTests/GaloisRingArithmetic.lean @@ -34,6 +34,16 @@ example : mul 3 [1, 1] [9] [3, 1, 4] = [3, 1] := by decide -- Degree three, `f = U ^ 3 + U + 1`, modulo `16`: `U ^ 2 * U = U ^ 3 = -1 - U`. example : mulX 4 [1, 1, 0] [0, 0, 1] = [15, 15, 0] := by decide +-- The unit, and `U ^ 3 = 1` as a power. +example : one [1, 1] = [1, 0] ∧ pow 3 [1, 1] [0, 1] 3 = [1, 0] := by decide + +-- `(1 + U) ^ 2 = 1 + 2 U + U ^ 2 = U`. +example : pow 3 [1, 1] [1, 1] 2 = [0, 1] := by decide + +/-- Powers are correct. -/ +example (c : List ℕ) (k : ℕ) : val 3 [1, 1] (pow 3 [1, 1] c k) = val 3 [1, 1] c ^ k := + val_pow c k + /-- The defining polynomial is monic. -/ example : (monicOf [1, 1]).Monic := monic_monicOf _ @@ -56,4 +66,11 @@ example : ComputableInPolyTime (encList encNat) := by fun_prop +/-- **Powers in polynomial time**, with the exponent in unary. -/ +example : ComputableInPolyTime + (fun q : (ℕ × List ℕ) × (List ℕ × ℕ) => pow q.1.1 q.1.2 q.2.1 q.2.2) + (encPair (encPair encUnary (encList encNat)) (encPair (encList encNat) encUnary)) + (encList encNat) := by + fun_prop + end ComplexityTests.GaloisRingArithmetic From dc4824e4e3a12d05ae3527e90eb88b985f9c6525 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:41:30 -0400 Subject: [PATCH 6/7] feat(PolyTime): negation, subtraction and Newton inversion in (Z/2^p)[U]/(f) The seed x^(2^e - 2) by e - 1 squarings, then p Newton steps y(2 - xy); correct whenever the seed inverts x modulo 2, which holds for units of a Galois ring. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../PolyTime/GaloisRingArithmetic.lean | 287 +++++++++++++++--- ComplexityTests/GaloisRingArithmetic.lean | 20 ++ 2 files changed, 266 insertions(+), 41 deletions(-) diff --git a/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean b/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean index 8a9bfcd2a5..123a3cfdb2 100644 --- a/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean +++ b/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean @@ -50,6 +50,12 @@ The value of a coefficient list `c` is `∑ i < e, c i U ^ i` in `A_p` (`GaloisR * **Powers** (`GaloisRingArith.pow`) `c ^ k` take `k` multiplications from `GaloisRingArith.one`, with `k` in unary. In the source the exponents of the mode substitutions are below the precision (Appendix D.4.6, p. 63), so they are polynomial. +* **Inversion** (`GaloisRingArith.inv`) starts from the seed `x ^ (2 ^ e - 2)`, a product of `e - 1` + repeated squares (`GaloisRingArith.seed`), and takes `p` Newton steps `y ↦ y (2 - x y)`, each + squaring the defect `x y - 1` (`GaloisRingArith.val_mul_newton`). When the seed inverts `x` + modulo `2`, the result is the inverse (`GaloisRingArith.val_mul_inv`). In a Galois ring, with + `f` irreducible modulo `2`, this holds for every unit, since the residue field has `2 ^ e` + elements; that bridge is not made here. Each operation is correct (`GaloisRingArith.val_add`, `GaloisRingArith.val_mulX`, `GaloisRingArith.val_mul`) and polynomial-time, with the precision `p` in unary and the @@ -57,26 +63,32 @@ coordinates and the coefficients of `f` in binary (`GaloisRingArith.computableIn `GaloisRingArith.computableInPolyTime_mul`). Their outputs are reduced, with `e` coordinates below `2 ^ p` (`GaloisRingArith.length_mul`, `GaloisRingArith.lt_of_mem_mul`). These are the polynomial-time arithmetic claims of Appendix D.4.1 for addition and multiplication, in the case -`ℓ = 1` of the source, where `A = O` has no `V`-coordinates. Inversion of units, which the source -does by Newton lifting, is not covered here. +`ℓ = 1` of the source, where `A = O` has no `V`-coordinates, together with the inversion of units +by inversion modulo two and Newton lifting that the source names (Appendix D.4.1, p. 58). ## Main definitions * `Cslib.GaloisRingArith.monicOf`: the monic polynomial with given lower coefficients. * `Cslib.GaloisRingArith.val`: the value of a coefficient list. * `Cslib.GaloisRingArith.add`, `Cslib.GaloisRingArith.mulX`, `Cslib.GaloisRingArith.mul`, - `Cslib.GaloisRingArith.one`, `Cslib.GaloisRingArith.pow`: addition, multiplication by `U`, - multiplication, the unit and powers. + `Cslib.GaloisRingArith.one`, `Cslib.GaloisRingArith.pow`, `Cslib.GaloisRingArith.neg`, + `Cslib.GaloisRingArith.sub`: addition, multiplication by `U`, multiplication, the unit, powers, + negation and subtraction. +* `Cslib.GaloisRingArith.seed`, `Cslib.GaloisRingArith.newton`, `Cslib.GaloisRingArith.inv`: + inversion. ## Main results * `Cslib.GaloisRingArith.val_add`, `Cslib.GaloisRingArith.val_mulX`, `Cslib.GaloisRingArith.val_mul`, `Cslib.GaloisRingArith.val_one`, - `Cslib.GaloisRingArith.val_pow`: correctness. + `Cslib.GaloisRingArith.val_pow`, `Cslib.GaloisRingArith.val_neg`, + `Cslib.GaloisRingArith.val_sub`, `Cslib.GaloisRingArith.val_seed`, + `Cslib.GaloisRingArith.val_mul_inv`: correctness. * `Cslib.GaloisRingArith.computableInPolyTime_add`, `Cslib.GaloisRingArith.computableInPolyTime_mulX`, `Cslib.GaloisRingArith.computableInPolyTime_mul`, - `Cslib.GaloisRingArith.computableInPolyTime_pow`: polynomial time. + `Cslib.GaloisRingArith.computableInPolyTime_pow`, + `Cslib.GaloisRingArith.computableInPolyTime_inv`: polynomial time. ## References @@ -144,6 +156,33 @@ def one (fl : List ℕ) : List ℕ := (List.range fl.length).map fun i => if i = def pow (p : ℕ) (fl c : List ℕ) (k : ℕ) : List ℕ := (List.range k).foldl (fun acc _ => mul p fl acc c) (one fl) +/-- Negation, coordinatewise modulo `2 ^ p`. -/ +def neg (p : ℕ) (fl c : List ℕ) : List ℕ := + (List.range fl.length).map fun i => (2 ^ p - c.getD i 0 % 2 ^ p) % 2 ^ p + +/-- Subtraction. -/ +def sub (p : ℕ) (fl c d : List ℕ) : List ℕ := add p fl c (neg p fl d) + +/-- One step of the seed of inversion: from `(x ^ 2 ^ j, x ^ (2 ^ (j + 1) - 2))`, square the power +and multiply it in. -/ +def seedStep (p : ℕ) (fl : List ℕ) (s : List ℕ × List ℕ) : List ℕ × List ℕ := + (mul p fl s.1 s.1, mul p fl s.2 (mul p fl s.1 s.1)) + +/-- The seed `x ^ (2 ^ e - 2) = x ^ 2 x ^ 4 ⋯ x ^ (2 ^ (e - 1))` of inversion, by `e - 1` +squarings. In a Galois ring it inverts `x` modulo `2`, since the residue field has `2 ^ e` +elements. -/ +def seed (p : ℕ) (fl x : List ℕ) : List ℕ := + ((List.range (fl.length - 1)).foldl (fun s _ => seedStep p fl s) (x, one fl)).2 + +/-- One Newton step `y (2 - x y)` towards the inverse of `x`. -/ +def newton (p : ℕ) (fl x y : List ℕ) : List ℕ := + mul p fl y (sub p fl (add p fl (one fl) (one fl)) (mul p fl x y)) + +/-- **Inversion**: `p` Newton steps from the seed. It is the inverse of `x` whenever the seed +inverts `x` modulo `2` (`val_mul_inv`), in particular for every unit of a Galois ring. -/ +def inv (p : ℕ) (fl x : List ℕ) : List ℕ := + (List.range p).foldl (fun y _ => newton p fl x y) (seed p fl x) + /-! ### Correctness -/ section Correctness @@ -276,6 +315,78 @@ theorem val_pow (c : List ℕ) (k : ℕ) : val p fl (pow p fl c k) = val p fl c | succ k ih => rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, val_mul, ih, pow_succ] +/-- **Negation is correct.** -/ +theorem val_neg (c : List ℕ) : val p fl (neg p fl c) = -val p fl c := by + rw [val, val, ← sum_neg_distrib] + refine sum_congr rfl fun i hi => ?_ + rw [neg, List.getD_eq_getElem _ _ (by simpa using hi)] + simp only [List.getElem_map, List.getElem_range, natCast_mod_two_pow] + rw [Nat.cast_sub (Nat.mod_lt _ (Nat.two_pow_pos p)).le, natCast_two_pow, natCast_mod_two_pow] + ring + +/-- **Subtraction is correct.** -/ +theorem val_sub (c d : List ℕ) : val p fl (sub p fl c d) = val p fl c - val p fl d := by + rw [sub, val_add, val_neg, sub_eq_add_neg] + +/-- **The seed is the power `x ^ (2 ^ e - 2)`.** -/ +theorem val_seed (x : List ℕ) : val p fl (seed p fl x) = val p fl x ^ (2 ^ fl.length - 2) := by + have hinv (j : ℕ) : + val p fl ((List.range j).foldl (fun s _ => seedStep p fl s) (x, one fl)).1 = + val p fl x ^ 2 ^ j ∧ + val p fl ((List.range j).foldl (fun s _ => seedStep p fl s) (x, one fl)).2 = + val p fl x ^ (2 ^ (j + 1) - 2) := by + induction j with + | zero => simp + | succ j ih => + rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, seedStep] + refine ⟨?_, ?_⟩ + · rw [val_mul, ih.1, ← pow_add, ← two_mul, ← pow_succ'] + · rw [val_mul, val_mul, ih.1, ih.2, ← pow_add, ← pow_add] + congr 1 + have : 2 ≤ 2 ^ (j + 1) := by + calc 2 = 2 ^ 1 := rfl + _ ≤ 2 ^ (j + 1) := Nat.pow_le_pow_right (by norm_num) (by omega) + rw [pow_succ 2 (j + 1)] + omega + rw [seed, (hinv _).2] + rcases Nat.eq_zero_or_pos fl.length with he | he + · simp [he] + · rw [Nat.sub_add_cancel he] + +/-- **Newton's step squares the defect**: if `x y = 1 + 2 ^ m w` then +`x (y (2 - x y)) = 1 + 2 ^ (2 m) (-w ^ 2)`. -/ +theorem val_mul_newton (x y : List ℕ) {m : ℕ} {w : Ring p fl} + (h : val p fl x * val p fl y = 1 + 2 ^ m * w) : + val p fl x * val p fl (newton p fl x y) = 1 + 2 ^ (2 * m) * -w ^ 2 := by + rw [newton, val_mul, val_sub, val_add, val_mul, val_one] + have : val p fl x * (val p fl y * (1 + 1 - val p fl x * val p fl y)) = + (val p fl x * val p fl y) * (2 - val p fl x * val p fl y) := by ring + rw [this, h, show (2 : Ring p fl) ^ (2 * m) = 2 ^ m * 2 ^ m by rw [two_mul, pow_add]] + ring + +/-- **Inversion is correct** when the seed inverts `x` modulo `2`. -/ +theorem val_mul_inv (x : List ℕ) {w : Ring p fl} + (h : val p fl x * val p fl x ^ (2 ^ fl.length - 2) = 1 + 2 * w) : + val p fl x * val p fl (inv p fl x) = 1 := by + have hstep (k : ℕ) : ∃ w' : Ring p fl, val p fl x * + val p fl ((List.range k).foldl (fun y _ => newton p fl x y) (seed p fl x)) = + 1 + 2 ^ 2 ^ k * w' := by + induction k with + | zero => exact ⟨w, by rw [List.range_zero, List.foldl_nil, val_seed, h, pow_zero, pow_one]⟩ + | succ k ih => + obtain ⟨w', hw'⟩ := ih + refine ⟨-w' ^ 2, ?_⟩ + rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, + val_mul_newton _ _ hw', show 2 ^ (k + 1) = 2 * 2 ^ k by ring] + obtain ⟨w', hw'⟩ := hstep p + rw [inv, hw'] + have hp : (2 : Ring p fl) ^ 2 ^ p = 0 := by + have h2p : (2 : Ring p fl) ^ p = 0 := by + rw [show (2 : Ring p fl) ^ p = ((2 ^ p : ℕ) : Ring p fl) by push_cast; rfl, + natCast_two_pow] + exact pow_eq_zero_of_le Nat.lt_two_pow_self.le h2p + rw [hp, zero_mul, add_zero] + end Correctness /-! ### Reduced outputs -/ @@ -427,6 +538,38 @@ theorem length_encList_le {p e : ℕ} {c : List ℕ} (hlen : c.length = e) omega _ = e * (2 * p + 1) := by rw [List.length_map, hlen, smul_eq_mul] +/-- The unit is polynomial-time. -/ +@[fun_prop] +theorem computableInPolyTime_one {fl : α → List ℕ} + (hfl : ComputableInPolyTime fl encIn (encList encNat)) : + ComputableInPolyTime (fun x => one (fl x)) encIn (encList encNat) := by + have h2 := ComputableInPolyTime.snd encIn encUnary + refine computableInPolyTime_tabulate (g := fun _ i => if i = 0 then 1 else 0) + (length_polyTime hfl) ?_ + refine (ComputableInPolyTime.ite (encMid := encNat) (c := fun q : α × ℕ => q.2 == 0) + ((ComputableInPolyTime.beq (h2) (ComputableInPolyTime.const 0))) + (ComputableInPolyTime.const 1) (ComputableInPolyTime.const 0)).of_enc_eq fun q => ?_ + by_cases h : q.2 = 0 <;> simp [h] + +/-- The length bound shared by the folds below: a pair of reduced lists. -/ +private theorem polyBounded_reduced {p : α → ℕ} {fl : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) : + PolyBounded (fun x => (encIn x).length) + (fun x => 3 * ((fl x).length * (2 * p x + 1)) + 1) := by + have hpl := (ComputableInPolyTime.polyBounded_length hp) + have hfll := (ComputableInPolyTime.polyBounded_length hfl) + refine (((PolyBounded.const 3).mul (hfll.mul (((PolyBounded.const 2).mul hpl).add + (PolyBounded.const 1)))).add (PolyBounded.const 1)).mono fun x => ?_ + have h1 : p x ≤ (encUnary (p x)).length := by simp + have h2 : (fl x).length ≤ (encList encNat (fl x)).length := by + rw [length_encList] + calc (fl x).length = ((fl x).map fun _ => 1).sum := by simp + _ ≤ ((fl x).map fun a => 2 * (encNat a).length + 1).sum := + List.sum_le_sum fun a _ => by omega + have := Nat.mul_le_mul h2 (Nat.add_le_add_right (Nat.mul_le_mul_left 2 h1) 1) + omega + /-- **Multiplication is polynomial-time**, with the precision in unary. Every intermediate pair is reduced after its first step, so its length is bounded by the precision and the degree. -/ @[fun_prop] @@ -457,20 +600,7 @@ theorem computableInPolyTime_mul {p : α → ℕ} {fl c d : α → List ℕ} (computableInPolyTime_addSmul (hp.comp hx) (hfl.comp hx) hacc (computableInPolyTime_getD (hc.comp hx) hi) hcur) -- Every step's output is reduced, hence of bounded length. - have hgrowth : PolyBounded (fun x => (encIn x).length) - (fun x => 3 * ((fl x).length * (2 * p x + 1)) + 1) := by - have hpl := (ComputableInPolyTime.polyBounded_length hp) - have hfll := (ComputableInPolyTime.polyBounded_length hfl) - refine (((PolyBounded.const 3).mul (hfll.mul (((PolyBounded.const 2).mul hpl).add - (PolyBounded.const 1)))).add (PolyBounded.const 1)).mono fun x => ?_ - have h1 : p x ≤ (encUnary (p x)).length := by simp - have h2 : (fl x).length ≤ (encList encNat (fl x)).length := by - rw [length_encList] - calc (fl x).length = ((fl x).map fun _ => 1).sum := by simp - _ ≤ ((fl x).map fun a => 2 * (encNat a).length + 1).sum := - List.sum_le_sum fun a _ => by omega - have := Nat.mul_le_mul h2 (Nat.add_le_add_right (Nat.mul_le_mul_left 2 h1) 1) - omega + have hgrowth := polyBounded_reduced hp hfl have hfold := ComputableInPolyTime.foldlWithInput_of_bounded_growth (encA := encUnary) (encL := encList encUnary) (step := fun x s i => mulStep (p x) (fl x) (c x) s i) hinit @@ -490,33 +620,14 @@ theorem computableInPolyTime_pow {p k : α → ℕ} {fl c : α → List ℕ} (hc : ComputableInPolyTime c encIn (encList encNat)) (hk : ComputableInPolyTime k encIn encUnary) : ComputableInPolyTime (fun x => pow (p x) (fl x) (c x) (k x)) encIn (encList encNat) := by - have hone : ComputableInPolyTime (fun x => one (fl x)) encIn (encList encNat) := by - have h2 := ComputableInPolyTime.snd encIn encUnary - refine computableInPolyTime_tabulate (g := fun _ i => if i = 0 then 1 else 0) - (length_polyTime hfl) ?_ - refine (ComputableInPolyTime.ite (encMid := encNat) (c := fun q : α × ℕ => q.2 == 0) - ((ComputableInPolyTime.beq (h2) (ComputableInPolyTime.const 0))) - (ComputableInPolyTime.const 1) (ComputableInPolyTime.const 0)).of_enc_eq fun q => ?_ - by_cases h : q.2 = 0 <;> simp [h] + have hone := computableInPolyTime_one hfl have hstep : ComputableInPolyTime (fun q : (α × List ℕ) × ℕ => mul (p q.1.1) (fl q.1.1) q.1.2 (c q.1.1)) (encPair (encPair encIn (encList encNat)) encUnary) (encList encNat) := by have hq := ComputableInPolyTime.fst (encPair encIn (encList encNat)) encUnary have hx := (ComputableInPolyTime.fst encIn (encList encNat)).comp hq have hacc := (ComputableInPolyTime.snd encIn (encList encNat)).comp hq exact computableInPolyTime_mul (hp.comp hx) (hfl.comp hx) hacc (hc.comp hx) - have hgrowth : PolyBounded (fun x => (encIn x).length) - (fun x => (fl x).length * (2 * p x + 1)) := by - have hpl := (ComputableInPolyTime.polyBounded_length hp) - have hfll := (ComputableInPolyTime.polyBounded_length hfl) - refine (hfll.mul (((PolyBounded.const 2).mul hpl).add (PolyBounded.const 1))).mono - fun x => ?_ - have h1 : p x ≤ (encUnary (p x)).length := by simp - have h2 : (fl x).length ≤ (encList encNat (fl x)).length := by - rw [length_encList] - calc (fl x).length = ((fl x).map fun _ => 1).sum := by simp - _ ≤ ((fl x).map fun a => 2 * (encNat a).length + 1).sum := - List.sum_le_sum fun a _ => by omega - exact Nat.mul_le_mul h2 (Nat.add_le_add_right (Nat.mul_le_mul_left 2 h1) 1) + have hgrowth := polyBounded_reduced hp hfl have hfold := ComputableInPolyTime.foldlWithInput_of_bounded_growth (encA := encUnary) (encL := encList encUnary) (step := fun x acc _ => mul (p x) (fl x) acc (c x)) hone @@ -526,6 +637,100 @@ theorem computableInPolyTime_pow {p k : α → ℕ} {fl c : α → List ℕ} · have := length_encList_le (length_mul (p x) (fl x) acc (c x)) fun _ h => lt_of_mem_mul h omega +/-- **Negation is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_neg {p : α → ℕ} {fl c : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) : + ComputableInPolyTime (fun x => neg (p x) (fl x) (c x)) encIn (encList encNat) := by + have h1 := ComputableInPolyTime.fst encIn encUnary + have h2 := ComputableInPolyTime.snd encIn encUnary + exact computableInPolyTime_tabulate (length_polyTime hfl) + (computableInPolyTime_mod_two_pow (ComputableInPolyTime.binary_sub' + (ComputableInPolyTime.binary_two_pow.comp (hp.comp h1)) + (computableInPolyTime_mod_two_pow (computableInPolyTime_getD (hc.comp h1) h2) + (hp.comp h1))) (hp.comp h1)) + +/-- **Subtraction is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_sub {p : α → ℕ} {fl c d : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) + (hd : ComputableInPolyTime d encIn (encList encNat)) : + ComputableInPolyTime (fun x => sub (p x) (fl x) (c x) (d x)) encIn (encList encNat) := + computableInPolyTime_add hp hfl hc (computableInPolyTime_neg hp hfl hd) + +/-- **A Newton step is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_newton {p : α → ℕ} {fl x y : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hx : ComputableInPolyTime x encIn (encList encNat)) + (hy : ComputableInPolyTime y encIn (encList encNat)) : + ComputableInPolyTime (fun a => newton (p a) (fl a) (x a) (y a)) encIn (encList encNat) := + computableInPolyTime_mul hp hfl hy (computableInPolyTime_sub hp hfl + (computableInPolyTime_add hp hfl (computableInPolyTime_one hfl) + (computableInPolyTime_one hfl)) (computableInPolyTime_mul hp hfl hx hy)) + +/-- **The seed of inversion is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_seed {p : α → ℕ} {fl x : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hx : ComputableInPolyTime x encIn (encList encNat)) : + ComputableInPolyTime (fun a => seed (p a) (fl a) (x a)) encIn (encList encNat) := by + let encS := encPair (encList encNat) (encList encNat) + have hstep : ComputableInPolyTime + (fun q : (α × (List ℕ × List ℕ)) × ℕ => seedStep (p q.1.1) (fl q.1.1) q.1.2) + (encPair (encPair encIn encS) encUnary) encS := by + have hq := ComputableInPolyTime.fst (encPair encIn encS) encUnary + have ha := (ComputableInPolyTime.fst encIn encS).comp hq + have hs := (ComputableInPolyTime.snd encIn encS).comp hq + have h1 := (ComputableInPolyTime.fst (encList encNat) (encList encNat)).comp hs + have h2 := (ComputableInPolyTime.snd (encList encNat) (encList encNat)).comp hs + have hsq := computableInPolyTime_mul (hp.comp ha) (hfl.comp ha) h1 h1 + exact hsq.prod (computableInPolyTime_mul (hp.comp ha) (hfl.comp ha) h2 hsq) + have hfold := ComputableInPolyTime.foldlWithInput_of_bounded_growth + (encA := encUnary) (encL := encList encUnary) + (step := fun a s _ => seedStep (p a) (fl a) s) + (hx.prod (computableInPolyTime_one hfl)) + ⟨ComputableInPolyTime.range.comp (ComputableInPolyTime.unary_sub' (length_polyTime hfl) + (ComputableInPolyTime.const 1)), hstep, inferInstance, inferInstance⟩ + ⟨polyBounded_reduced hp hfl, fun a s _ _ => ?_⟩ + · exact (ComputableInPolyTime.snd (encList encNat) (encList encNat)).comp hfold + · have h1 := length_encList_le (length_mul (p a) (fl a) s.1 s.1) fun _ h => lt_of_mem_mul h + have h2 := length_encList_le (length_mul (p a) (fl a) s.2 (mul (p a) (fl a) s.1 s.1)) + fun _ h => lt_of_mem_mul h + simp only [seedStep, length_encPair] + omega + +/-- **Inversion is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_inv {p : α → ℕ} {fl x : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hx : ComputableInPolyTime x encIn (encList encNat)) : + ComputableInPolyTime (fun a => inv (p a) (fl a) (x a)) encIn (encList encNat) := by + have hstep : ComputableInPolyTime + (fun q : (α × List ℕ) × ℕ => newton (p q.1.1) (fl q.1.1) (x q.1.1) q.1.2) + (encPair (encPair encIn (encList encNat)) encUnary) (encList encNat) := by + have hq := ComputableInPolyTime.fst (encPair encIn (encList encNat)) encUnary + have ha := (ComputableInPolyTime.fst encIn (encList encNat)).comp hq + have hy := (ComputableInPolyTime.snd encIn (encList encNat)).comp hq + exact computableInPolyTime_newton (hp.comp ha) (hfl.comp ha) (hx.comp ha) hy + exact ComputableInPolyTime.foldlWithInput_of_bounded_growth + (encA := encUnary) (encL := encList encUnary) + (step := fun a y _ => newton (p a) (fl a) (x a) y) (computableInPolyTime_seed hp hfl hx) + ⟨ComputableInPolyTime.range.comp hp, hstep, inferInstance, inferInstance⟩ + ⟨polyBounded_reduced hp hfl, fun a y _ _ => by + have := length_encList_le (length_mul (p a) (fl a) y + (sub (p a) (fl a) (add (p a) (fl a) (one (fl a)) (one (fl a))) (mul (p a) (fl a) (x a) y))) + fun _ h => lt_of_mem_mul h + simp only [newton] + omega⟩ + end PolyTime end Cslib.GaloisRingArith diff --git a/ComplexityTests/GaloisRingArithmetic.lean b/ComplexityTests/GaloisRingArithmetic.lean index f0e7710ba4..c3f7705e26 100644 --- a/ComplexityTests/GaloisRingArithmetic.lean +++ b/ComplexityTests/GaloisRingArithmetic.lean @@ -44,6 +44,20 @@ example : pow 3 [1, 1] [1, 1] 2 = [0, 1] := by decide example (c : List ℕ) (k : ℕ) : val 3 [1, 1] (pow 3 [1, 1] c k) = val 3 [1, 1] c ^ k := val_pow c k +-- Inversion of units: `U⁻¹ = U ^ 2 = 7 + 7 U`, and `(1 + 2 U)⁻¹`, `(3 + 5 U)⁻¹` are inverses. +example : inv 3 [1, 1] [0, 1] = [7, 7] := by decide +example : mul 3 [1, 1] [1, 2] (inv 3 [1, 1] [1, 2]) = [1, 0] := by decide +example : mul 3 [1, 1] [3, 5] (inv 3 [1, 1] [3, 5]) = [1, 0] := by decide + +-- `2` is not a unit, and inversion does not invert it. +example : mul 3 [1, 1] [2, 0] (inv 3 [1, 1] [2, 0]) ≠ [1, 0] := by decide + +/-- Inversion is correct when the seed inverts modulo `2`. -/ +example (x : List ℕ) {w : Ring 3 [1, 1]} + (h : val 3 [1, 1] x * val 3 [1, 1] x ^ (2 ^ 2 - 2) = 1 + 2 * w) : + val 3 [1, 1] x * val 3 [1, 1] (inv 3 [1, 1] x) = 1 := + val_mul_inv x h + /-- The defining polynomial is monic. -/ example : (monicOf [1, 1]).Monic := monic_monicOf _ @@ -73,4 +87,10 @@ example : ComputableInPolyTime (encList encNat) := by fun_prop +/-- **Inversion in polynomial time.** -/ +example : ComputableInPolyTime + (fun q : (ℕ × List ℕ) × List ℕ => inv q.1.1 q.1.2 q.2) + (encPair (encPair encUnary (encList encNat)) (encList encNat)) (encList encNat) := by + fun_prop + end ComplexityTests.GaloisRingArithmetic From c1407c7afcd472e9346d40afc65f261bf8976085 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 23:37:40 -0400 Subject: [PATCH 7/7] feat(PolyTime): Newton inversion inverts every unit of a Galois ring GaloisRingArith.inv's correctness assumed that the seed x^(2^e-2) inverts x modulo 2. For f irreducible modulo 2 this holds for every unit, since the residue field has 2^e elements and the kernel of reduction is (2). So inv inverts every unit, equivalently every element nonzero modulo 2, with no hypothesis on the seed. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../PolyTime/GaloisRingUnits.lean | 127 ++++++++++++++++++ ComplexityTests/GaloisRingUnits.lean | 51 +++++++ 3 files changed, 179 insertions(+) create mode 100644 Complexity/Computability/PolyTime/GaloisRingUnits.lean create mode 100644 ComplexityTests/GaloisRingUnits.lean diff --git a/Complexity.lean b/Complexity.lean index de719dda8e..6175ed3d3b 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1997,6 +1997,7 @@ public import Complexity.Computability.PolyTime.CSP.ToCNF public import Complexity.Computability.PolyTime.CommonCountingAccum public import Complexity.Computability.PolyTime.FineGrained.ParameterCheck public import Complexity.Computability.PolyTime.GaloisRingArithmetic +public import Complexity.Computability.PolyTime.GaloisRingUnits public import Complexity.Computability.PolyTime.GreedyLabelSchedule public import Complexity.Computability.PolyTime.GreedySlotScore public import Complexity.Computability.PolyTime.Int.ExactDiv diff --git a/Complexity/Computability/PolyTime/GaloisRingUnits.lean b/Complexity/Computability/PolyTime/GaloisRingUnits.lean new file mode 100644 index 0000000000..fb25f4ca24 --- /dev/null +++ b/Complexity/Computability/PolyTime/GaloisRingUnits.lean @@ -0,0 +1,127 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.PolyTime.GaloisRingArithmetic +public import Complexity.Foundations.RingTheory.GaloisRing +import Mathlib.FieldTheory.Finite.Basic + +/-! +# Newton inversion inverts every unit of a Galois ring + +`Complexity/Computability/PolyTime/GaloisRingArithmetic.lean` computes in +`A_p = (ℤ / 2 ^ p)[U] / (f)` on coefficient lists, and inverts by `p` Newton steps from the seed +`x ^ (2 ^ e - 2)`, `e = deg f` (`GaloisRingArith.inv`). Its correctness +(`GaloisRingArith.val_mul_inv`) assumes that the seed inverts `x` modulo `2`. This file discharges +that assumption when `f` is irreducible modulo `2`, so that `A_p` is the Galois ring +`GaloisRing 2 p f`. + +Reduction modulo `2` maps `A_p` onto the field `𝔽_2[U] / (f)` with `2 ^ e` elements, where every +nonzero `r` has `r ^ (2 ^ e - 1) = 1`. A unit `y` reduces to a nonzero element, so +`y y ^ (2 ^ e - 2) - 1` lies in the kernel `(2)` of reduction (`GaloisRing.ker_residue`). The seed +is computed natively (`GaloisRingArith.seed`), so no inversion modulo `2` is needed separately. + +So `GaloisRingArith.inv` inverts every unit, that is every element that is nonzero modulo `2` +(`GaloisRing.isUnit_iff`), in polynomial time (`GaloisRingArith.computableInPolyTime_inv`). This +is the inversion of units by inversion modulo two and Newton lifting of [OpenAI2026ETH] +(Appendix D.4.1, p. 58), with `ℓ = 1`. + +## Main results + +* `Cslib.GaloisRingArith.natDegree_monicOf`: `monicOf fl` has degree `fl.length`. +* `Cslib.GaloisRingArith.exists_mul_pow_eq_one_add_two_mul`: the seed inverts a unit modulo `2`. +* `Cslib.GaloisRingArith.val_mul_inv_of_isUnit`, `Cslib.GaloisRingArith.val_inv_of_isUnit`: + Newton inversion inverts every unit. +* `Cslib.GaloisRingArith.val_mul_inv_of_residue_ne_zero`: it inverts every element that is nonzero + modulo `2`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.4.1 (pp. 57–58). +-/ + +public section + +namespace Cslib.GaloisRingArith + +open Polynomial Finset + +/-- `monicOf fl` has degree `fl.length`. -/ +theorem natDegree_monicOf (fl : List ℕ) : (monicOf fl).natDegree = fl.length := by + unfold monicOf + rw [natDegree_add_eq_left_of_degree_lt, natDegree_X_pow] + rw [degree_X_pow] + refine (degree_sum_le _ _).trans_lt ?_ + rw [Finset.sup_lt_iff (WithBot.bot_lt_coe _)] + intro i hi + exact (degree_C_mul_X_pow_le _ _).trans_lt (WithBot.coe_lt_coe.mpr (mem_range.mp hi)) + +variable {p : ℕ} {fl : List ℕ} + +/-- `A_p` is the Galois ring `GaloisRing 2 p (monicOf fl)`. -/ +theorem ring_eq_galoisRing : Ring p fl = GaloisRing 2 p (monicOf fl) := rfl + +/-- **The seed inverts a unit modulo `2`.** In a Galois ring of rank `e`, the residue field has +`2 ^ e` elements, so a unit `y` satisfies `y y ^ (2 ^ e - 2) = 1 + 2 w`. -/ +theorem exists_mul_pow_eq_one_add_two_mul [NeZero p] + (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2)))) {y : Ring p fl} + (hy : IsUnit y) : ∃ w : Ring p fl, y * y ^ (2 ^ fl.length - 2) = 1 + 2 * w := by + set F := AdjoinRoot ((monicOf fl).map (Int.castRingHom (ZMod 2))) + have : Fact (Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2)))) := ⟨hirr⟩ + have hcard : Nat.card F = 2 ^ fl.length := by + rw [GaloisRing.natCard_adjoinRoot (monic_monicOf fl), natDegree_monicOf] + have : Finite F := Nat.finite_of_card_ne_zero (by rw [hcard]; positivity) + let : Fintype F := Fintype.ofFinite F + have he : 1 ≤ fl.length := by + have := natDegree_pos_iff_degree_pos.mpr (degree_pos_of_irreducible hirr) + rwa [(monic_monicOf fl).natDegree_map, natDegree_monicOf] at this + have h2 : 2 ≤ 2 ^ fl.length := by + calc 2 = 2 ^ 1 := rfl + _ ≤ 2 ^ fl.length := Nat.pow_le_pow_right (by norm_num) he + -- The residue of `y` is nonzero, so its `(2 ^ e - 1)`-th power is `1`. + have hr : GaloisRing.residue 2 p (monicOf fl) y ≠ 0 := + (GaloisRing.isUnit_iff (monic_monicOf fl) hirr).mp hy + have hpow : GaloisRing.residue 2 p (monicOf fl) y ^ (2 ^ fl.length - 1) = 1 := by + have := FiniteField.pow_card_sub_one_eq_one _ hr + rwa [Fintype.card_eq_nat_card, hcard] at this + have hker : y * y ^ (2 ^ fl.length - 2) - 1 ∈ + RingHom.ker (GaloisRing.residue 2 p (monicOf fl)) := by + rw [RingHom.mem_ker, map_sub, map_mul, map_pow, map_one, ← pow_succ', + show 2 ^ fl.length - 2 + 1 = 2 ^ fl.length - 1 by omega, hpow, sub_self] + rw [GaloisRing.ker_residue (monic_monicOf fl), Ideal.mem_span_singleton] at hker + obtain ⟨w, hw⟩ := hker + exact ⟨w, by rw [← sub_eq_iff_eq_add', hw]; push_cast; rfl⟩ + +/-- **Newton inversion inverts every unit** of the Galois ring `A_p`, `f` irreducible modulo +`2`. -/ +theorem val_mul_inv_of_isUnit (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2)))) + {x : List ℕ} (hx : IsUnit (val p fl x)) : val p fl x * val p fl (inv p fl x) = 1 := by + rcases Nat.eq_zero_or_pos p with rfl | hp + · -- `A_0` is the zero ring. + have : Subsingleton (ZMod (2 ^ 0)) := by rw [pow_zero]; infer_instance + have := (AdjoinRoot.of ((monicOf fl).map (Int.castRingHom (ZMod (2 ^ 0))))).codomain_trivial + exact Subsingleton.elim _ _ + · have : NeZero p := ⟨hp.ne'⟩ + obtain ⟨w, hw⟩ := exists_mul_pow_eq_one_add_two_mul hirr hx + exact val_mul_inv x hw + +/-- **Newton inversion computes the inverse of a unit.** -/ +theorem val_inv_of_isUnit (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2)))) + {x : List ℕ} (hx : IsUnit (val p fl x)) : + val p fl (inv p fl x) = _root_.Ring.inverse (val p fl x) := by + rw [← _root_.Ring.inverse_mul_cancel_left _ (val p fl (inv p fl x)) hx, + val_mul_inv_of_isUnit hirr hx, mul_one] + +/-- **Newton inversion inverts every element that is nonzero modulo `2`.** -/ +theorem val_mul_inv_of_residue_ne_zero [NeZero p] + (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2)))) {x : List ℕ} + (hx : GaloisRing.residue 2 p (monicOf fl) (val p fl x) ≠ 0) : + val p fl x * val p fl (inv p fl x) = 1 := + val_mul_inv_of_isUnit hirr ((GaloisRing.isUnit_iff (monic_monicOf fl) hirr).mpr hx) + +end Cslib.GaloisRingArith diff --git a/ComplexityTests/GaloisRingUnits.lean b/ComplexityTests/GaloisRingUnits.lean new file mode 100644 index 0000000000..7325e3bcaf --- /dev/null +++ b/ComplexityTests/GaloisRingUnits.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.PolyTime.GaloisRingUnits +import Mathlib.Algebra.Polynomial.SpecificDegree + +/-! # Newton inversion of units in a Galois ring + +For `f = U ^ 2 + U + 1`, irreducible modulo `2`, Newton inversion inverts every unit of +`(ℤ / 8)[U] / (f)` (`p = 3`, `fl = [1, 1]`) with no hypothesis on the seed. -/ + +namespace ComplexityTests.GaloisRingUnits + +open Cslib.GaloisRingArith Polynomial + +/-- `U ^ 2 + U + 1` is irreducible modulo `2`: it has degree two and no root in `𝔽_2`. -/ +theorem irreducible_monicOf_one_one : + Irreducible ((monicOf [1, 1]).map (Int.castRingHom (ZMod 2))) := by + have hmap : (monicOf [1, 1]).map (Int.castRingHom (ZMod 2)) = X ^ 2 + X + 1 := by + simp [monicOf, Finset.sum_range_succ] + ring + have hmon : ((monicOf [1, 1]).map (Int.castRingHom (ZMod 2))).Monic := + (monic_monicOf _).map _ + have hdeg : ((monicOf [1, 1]).map (Int.castRingHom (ZMod 2))).natDegree = 2 := by + rw [(monic_monicOf _).natDegree_map, natDegree_monicOf]; rfl + rw [hmon.irreducible_iff_roots_eq_zero_of_degree_le_three (by omega) (by omega)] + refine Multiset.eq_zero_of_forall_notMem fun x hx => ?_ + rw [mem_roots hmon.ne_zero, IsRoot, hmap] at hx + simp only [eval_add, eval_pow, eval_X, eval_one] at hx + fin_cases x <;> exact absurd hx (by decide) + +/-- **Every unit is inverted**, with no hypothesis on the seed. -/ +example (x : List ℕ) (hx : IsUnit (val 3 [1, 1] x)) : + val 3 [1, 1] x * val 3 [1, 1] (inv 3 [1, 1] x) = 1 := + val_mul_inv_of_isUnit irreducible_monicOf_one_one hx + +/-- Every element that is nonzero modulo `2` is inverted. -/ +example (x : List ℕ) (hx : GaloisRing.residue 2 3 (monicOf [1, 1]) (val 3 [1, 1] x) ≠ 0) : + val 3 [1, 1] x * val 3 [1, 1] (inv 3 [1, 1] x) = 1 := + val_mul_inv_of_residue_ne_zero irreducible_monicOf_one_one hx + +/-- The seed inverts every unit modulo `2`: here `e = 2`, so the seed is `x ^ 2`. -/ +example (y : Ring 3 [1, 1]) (hy : IsUnit y) : ∃ w, y * y ^ (2 ^ 2 - 2) = 1 + 2 * w := + exists_mul_pow_eq_one_add_two_mul irreducible_monicOf_one_one hy + +example : (monicOf [1, 1]).natDegree = 2 := natDegree_monicOf _ + +end ComplexityTests.GaloisRingUnits