feat(Coding Theory): Add Gao decoder and correctness (#249)

* Add `ReedSolomon.lean` under `Data/CodingTheory`

* Add `GaoDecoder.lean`

* Add `ToMathlib/Polynomial/Roots.lean`

* Add `ToMathlib/Order/WithBot.lean`

* `EuclideanAlgorithm.lean`: Add Bézout invariants for `xgcd`

* `DivisionCorrectness.lean`: add `exactDiv_toPoly_iff`

* Add `GaoCorrectness.lean`

* `CompPoly.lean`: update imports

* Place encoder-only results in `ReedSolomon.lean`

* chore(coding-theory): address review nits on Gao decoder

Cosmetic cleanups to the Gao decoder formalization, no change to
statements or proof terms (axioms remain [propext, Classical.choice,
Quot.sound]; full build + lint-style pass):

- Convert bare `simp`/`simp [...]` to explicit `simp only [...]` at the
  seven sites in `GaoCorrectness.lean`/`ReedSolomon.lean`, per the repo's
  performance guidance (bare `simp` pulls in the full simp set).
- Rename lemmas mixing camelCase `errorLocator` into snake_case names:
  `disagreement_subset_errorLocator_zeros`,
  `disagreement_card_le_errorLocator_natDegree`,
  `hammingDist_le_errorLocator_natDegree` -> `*_error_locator_*`.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* refactor(coding-theory): move RS/Gao under Univariate/ReedSolomon

Relocate the Reed-Solomon code and Gao decoder from Data/CodingTheory/
to Univariate/ReedSolomon/, matching how the Guruswami-Sudan decoder
sits under its representation family (Bivariate/GuruswamiSudan/). Data/
is documented as helper lemmas and support definitions, not user-facing
decoders. Namespaces (CompPoly.ReedSolomon[.Gao]) are unchanged; only
file paths and the two internal imports move. CompPoly.lean regenerated
via update-lib.sh.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------


Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-authored-by: Alexander Hicks <25369263+alexanderlhicks@users.noreply.github.com>

Author: 3 people

CompPoly.lean

@@ -154,11 +154,13 @@ import CompPoly.Multivariate.VarsDegrees
 import CompPoly.Multivariate.Wheels
 import CompPoly.ToMathlib.Finsupp.Fin
 import CompPoly.ToMathlib.MvPolynomial.Equiv
+import CompPoly.ToMathlib.Order.WithBot
 import CompPoly.ToMathlib.Polynomial.BivariateDegree
 import CompPoly.ToMathlib.Polynomial.BivariateEvaluation
 import CompPoly.ToMathlib.Polynomial.BivariateMultiplicity
 import CompPoly.ToMathlib.Polynomial.BivariateWeightedDegree
 import CompPoly.ToMathlib.Polynomial.Div
+import CompPoly.ToMathlib.Polynomial.Roots
 import CompPoly.Univariate.Barycentric
 import CompPoly.Univariate.Basic
 import CompPoly.Univariate.BatchEval
@@ -211,6 +213,9 @@ import CompPoly.Univariate.Raw.Division
 import CompPoly.Univariate.Raw.Modular
 import CompPoly.Univariate.Raw.Ops
 import CompPoly.Univariate.Raw.Proofs
+import CompPoly.Univariate.ReedSolomon
+import CompPoly.Univariate.ReedSolomon.GaoCorrectness
+import CompPoly.Univariate.ReedSolomon.GaoDecoder
 import CompPoly.Univariate.Roots
 import CompPoly.Univariate.Roots.Backend
 import CompPoly.Univariate.Roots.Context

CompPoly/ToMathlib/Order/WithBot.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Conejero
+-/
+import Mathlib.Algebra.Order.Monoid.WithTop
+
+/-!
+# Strict additive monotonicity on `WithBot ℕ`
+
+Mathlib's `WithBot.add_lt_add_of_le_of_lt` / `WithBot.add_lt_add_of_lt_of_le` carry `≠ ⊥`
+side conditions; the fully strict version below needs none of them over `ℕ`.
+Upstreaming candidate.
+-/
+
+namespace WithBot
+
+/-- Strict monotonicity of `+` on `WithBot ℕ`: `a < b → c < d → a + c < b + d`. -/
+lemma add_lt_add {a b c d : WithBot ℕ} (h1 : a < b) (h2 : c < d) : a + c < b + d := by
+  cases a <;> cases b <;> cases c <;> cases d <;> simp_all [← WithBot.coe_add]; omega
+
+end WithBot

CompPoly/ToMathlib/Polynomial/Roots.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Conejero
+-/
+import Mathlib.Algebra.Polynomial.Roots
+
+/-!
+# Root sets of products of distinct linear factors
+
+- `∏ i ∈ s, (X - C (a i))` over injectively indexed points: it divides every polynomial
+vanishing on the points (`prod_X_sub_C_dvd`)
+- A nonzero polynomial vanishes at boundedly many of the points (`card_eval_zero_le_natDegree`)
+- The product divides `(∏ i ∈ E, (X - C (a i))) * (f - b)` whenever `f` and `b` agree off `E`
+(`prod_X_sub_C_dvd_prod_mul_sub`).
+-/
+
+namespace Polynomial
+
+variable {R : Type*}
+
+/-- `∏ i ∈ s, (X - aᵢ)` divides `p` when the distinct `aᵢ` are all roots of `p`. -/
+lemma prod_X_sub_C_dvd [Field R]
+    {ι : Type*} (s : Finset ι) (a : ι → R) (hinj : Set.InjOn a s)
+    (p : R[X]) (hr : ∀ i ∈ s, p.eval (a i) = 0) :
+    (∏ i ∈ s, (X - C (a i))) ∣ p :=
+  Finset.prod_dvd_of_coprime
+    (fun _ hi _ hj hij =>
+      isCoprime_X_sub_C_of_isUnit_sub (sub_ne_zero.mpr (hij <| hinj hi hj ·)).isUnit)
+    (fun i hi => dvd_iff_isRoot.mpr (hr i hi))
+
+/-- A nonzero `v` vanishes at at most `v.natDegree` of the distinct points. -/
+lemma card_eval_zero_le_natDegree [CommRing R] [IsDomain R]
+    {ι : Type*} [DecidableEq R] (s : Finset ι) (a : ι → R)
+    (hinj : Set.InjOn a s) (v : R[X]) (hv : v ≠ 0) :
+    {i ∈ s | v.eval (a i) = 0}.card ≤ v.natDegree := by
+  rw [← Finset.card_image_of_injOn (hinj.mono (Finset.filter_subset _ _))]
+  refine card_le_degree_of_subset_roots fun x hx => ?_
+  obtain ⟨i, hi, rfl⟩ := Finset.mem_image.mp hx
+  exact (mem_roots hv).mpr (Finset.mem_filter.mp hi).2
+
+/-- When `f, b` agree off `E ⊆ s`, the product `∏_{i∈s}(X−aᵢ)` divides
+`(∏_{i∈E}(X−aᵢ))·(f − b)`. -/
+lemma prod_X_sub_C_dvd_prod_mul_sub [Field R] {ι : Type*} [DecidableEq ι]
+    (s E : Finset ι) (hE : E ⊆ s) (a : ι → R) (hinj : Set.InjOn a s)
+    (f b : R[X]) (hagree : ∀ i ∈ s \ E, f.eval (a i) = b.eval (a i)) :
+    (∏ i ∈ s, (X - C (a i))) ∣ (∏ i ∈ E, (X - C (a i))) * (f - b) := by
+  rw [← Finset.prod_sdiff hE, mul_comm]
+  exact mul_dvd_mul_left _ (prod_X_sub_C_dvd _ _
+    (hinj.mono (Finset.coe_subset.mpr Finset.sdiff_subset)) _
+    fun i hi => by rw [eval_sub, hagree i hi, sub_self])
+
+end Polynomial

CompPoly/Univariate/DivisionCorrectness.lean

@@ -552,6 +552,20 @@ theorem mod_toPoly_eq_smul_mod (p q : CPolynomial R) :
     ←Polynomial.smul_modByMonic, ← Polynomial.smul_eq_C_mul,
     mod_toPoly_eq_modByMonic p q hq]
 
+/-- Exact-division bridge: `G.toPoly` factors as `f.toPoly * V.toPoly` iff the computable
+`mod` vanishes and the computable division recovers `f`. -/
+theorem exactDiv_toPoly_iff (G V f : CPolynomial R) (hV : V.toPoly ≠ 0) :
+    G.toPoly = f.toPoly * V.toPoly ↔ G.mod V = 0 ∧ (G / V).toPoly = f.toPoly := by
+  have hdivP : (G / V).toPoly = G.toPoly / V.toPoly := div_toPoly_eq_div _ _
+  have hmod : G.mod V = 0 ↔ G.toPoly % V.toPoly = 0 := by
+    rw [← toPoly_eq_zero_iff, mod_toPoly_eq_smul_mod, smul_eq_zero_iff_right
+      (inv_ne_zero (leadingCoeff_ne_zero ((toPoly_eq_zero_iff V).not.mp hV)))]
+  refine ⟨fun hGV => ?_, fun ⟨hmod0, hdiv⟩ => ?_⟩
+  · exact ⟨hmod.mpr (EuclideanDomain.mod_eq_zero.mpr (Dvd.intro_left _ hGV.symm)),
+      by rw [hdivP, hGV, mul_div_cancel_right₀ _ hV]⟩
+  · rw [← hdiv, hdivP, _root_.mul_comm,
+      EuclideanDomain.mul_div_cancel' hV (EuclideanDomain.mod_eq_zero.mp (hmod.mp hmod0))]
+
 private theorem reversal_remainder_toPoly_eq_modByMonic
     (M : Raw.MulLowContext R) (p q : CPolynomial R)
     (hmonic : (q.leadingCoeff == 1) = true)

CompPoly/Univariate/EuclideanAlgorithm.lean

@@ -5,13 +5,18 @@ Authors: Juan Conejero, Valerii Huhnin
 -/
 import CompPoly.Univariate.Basic
 import CompPoly.Univariate.DivisionCorrectness
+import CompPoly.ToMathlib.Order.WithBot
 
 /-!
 # Extended Euclidean Algorithm for `CPolynomial`
 
 `xgcd p q` returns a triple `(r, s, t)` with `r = s * p + t * q`.
 Early stop when `r.natDegree < threshold`.
 The default `threshold = 0` makes `r` the Greatest Common Divisor of `p` and `q`.
+
+For positive thresholds, `xgcd_stopSpec` characterizes the output: `BezoutStopSpec` packages
+the Bézout identity together with the residue/cofactor degree bounds at the stopping point,
+via the loop invariant `BezoutDegreeInvariant`.
 -/
 
 namespace CompPoly
@@ -362,4 +367,143 @@ theorem normXgcd_fst_comm
 
 end CPolynomial
 
+/-! ## Stop specification for positive thresholds
+
+`BezoutDegreeInvariant` is the invariant of the partial-EEA (`xgcd`) loop: each non-stop
+step preserves it (`BezoutDegreeInvariant.step`), and at the stopping threshold it yields
+the output specification `BezoutStopSpec` (`xgcd_stopSpec`).
+
+This is the classical degree theory of the extended Euclidean algorithm — the row identity
+`deg t + deg r' = deg g₀` and the complementary cofactor bound at the stop — i.e. the
+contract behind rational-function reconstruction and Reed-Solomon decoding. -/
+
+open Polynomial
+open CPolynomial hiding X C add_comm zero_add mul_comm mul_zero mul_one one_mul mul_assoc
+
+variable {F : Type*}
+
+/-- Loop invariant of one partial-EEA (`xgcd`) step. -/
+structure BezoutDegreeInvariant [Ring F] (g₀ g₁ : F[X]) (threshold : ℕ)
+    (r s t r' s' t' : F[X]) : Prop where
+  bez : r = s * g₀ + t * g₁
+  bez' : r' = s' * g₀ + t' * g₁
+  det : IsUnit (s' * t - s * t')
+  degt : t'.degree < t.degree
+  degr : r.degree < r'.degree
+  thr : threshold ≤ r'.degree
+
+/-- `BezoutDegreeInvariant` on the `toPoly` images of a `CPolynomial` reference pair `g₀, g₁` and
+the two state triples `(r, s, t)`, `(r', s', t')`. -/
+abbrev BezoutDegreeInvariantOf [Ring F] (g₀ g₁ : CPolynomial F) (threshold : ℕ)
+    (r s t r' s' t' : CPolynomial F) : Prop :=
+  BezoutDegreeInvariant
+    g₀.toPoly g₁.toPoly threshold r.toPoly s.toPoly t.toPoly r'.toPoly s'.toPoly t'.toPoly
+
+/-- `BezoutDegreeInvariant` implies `deg t + deg r' = deg g₀`. -/
+lemma BezoutDegreeInvariant.degree_complement [CommRing F] [NoZeroDivisors F] [Nontrivial F]
+    {g₀ g₁ : F[X]} {threshold : ℕ} {r s t r' s' t' : F[X]}
+    (h : BezoutDegreeInvariant g₀ g₁ threshold r s t r' s' t') :
+    t.degree + r'.degree = g₀.degree := by
+  have hid : t * r' - t' * r = (s' * t - s * t') * g₀ := by rw [h.bez, h.bez']; ring
+  have hdom : (t' * r).degree < (t * r').degree := by simpa using WithBot.add_lt_add h.degt h.degr
+  rw [← degree_mul, ← degree_sub_eq_left_of_degree_lt hdom, hid, degree_mul,
+    degree_eq_zero_of_isUnit h.det, zero_add]
+
+/-- One Euclidean step grows the cofactor degree: `deg t < deg (t' - (r'/r) t)`. -/
+private lemma cofactor_degree_grows [Field F]
+    (r r' t t' : F[X]) (hr : r ≠ 0)
+    (hrr : r.degree < r'.degree) (htt : t'.degree < t.degree) :
+    t.degree < (t' - r' / r * t).degree := by
+  have hgt : t.degree < (r' / r * t).degree := by
+    simpa using WithBot.add_lt_add_right (degree_ne_bot.mpr (ne_zero_of_degree_gt htt))
+      (pos_of_lt_add_right (degree_add_div hr hrr.le ▸ hrr))
+  rwa [degree_sub_eq_right_of_degree_lt (htt.trans hgt)]
+
+/-- A non-stop Euclidean step preserves the invariant. -/
+lemma BezoutDegreeInvariant.step [Field F]
+    {g₀ g₁ : F[X]} {threshold : ℕ} {r s t r' s' t' : F[X]}
+    (h : BezoutDegreeInvariant g₀ g₁ threshold r s t r' s' t') (hr : r ≠ 0)
+    (hstop : ¬ r.natDegree < threshold) :
+    BezoutDegreeInvariant
+      g₀ g₁ threshold (r' - r' / r * r) (s' - r' / r * s) (t' - r' / r * t) r s t := by
+  refine ⟨(by rw [h.bez, h.bez']; ring), h.bez, ?_, ?_, ?_, ?_⟩
+  · ring_nf; simpa [mul_comm] using h.det.neg
+  · exact cofactor_degree_grows _ _ _ _ hr h.degr h.degt
+  · rw [mul_comm, ← EuclideanDomain.mod_eq_sub_mul_div]; exact degree_mod_lt _ hr
+  · rw [degree_eq_natDegree hr]; exact_mod_cast not_lt.mp hstop
+
+/-- Stop spec of the partial EEA: `R = S g₀ + T g₁`, residue degree below `threshold`,
+and the cofactor `T` nonzero with complementary degree `deg T + threshold ≤ deg g₀`. -/
+structure BezoutStopSpec [Semiring F] (g₀ g₁ : F[X]) (threshold : ℕ) (R S T : F[X]) : Prop where
+  bez : R = S * g₀ + T * g₁
+  resDeg : R.natDegree < threshold
+  cofDeg : T.degree + threshold ≤ g₀.degree
+  cofNe : T ≠ 0
+
+/-- `BezoutStopSpec` on the `toPoly` images of a `CPolynomial` reference pair `g₀, g₁` and
+result triple. -/
+abbrev BezoutStopSpecOf [Semiring F] (g₀ g₁ : CPolynomial F) (threshold : ℕ)
+    (result : CPolynomial F × CPolynomial F × CPolynomial F) : Prop :=
+  BezoutStopSpec
+    g₀.toPoly g₁.toPoly threshold result.1.toPoly result.2.1.toPoly result.2.2.toPoly
+
+/-- `BezoutDegreeInvariant` implies `xgcdAux`'s output satisfies the stop spec. -/
+lemma xgcdAux_stopSpec_of_invariant
+    [Field F] [BEq F] [LawfulBEq F] (g₀ g₁ : CPolynomial F) (threshold : ℕ) (hthr : 1 ≤ threshold)
+    (hg₀ : g₀.toPoly ≠ 0) :
+    ∀ (n : ℕ) (r s t r' s' t' : CPolynomial F),
+      BezoutDegreeInvariantOf g₀ g₁ threshold r s t r' s' t' →
+      r.natDegree < n →
+      BezoutStopSpecOf g₀ g₁ threshold (xgcdAux threshold n r s t r' s' t') := by
+  intro n; induction n with
+  | zero => intros; contradiction
+  | succ k ih =>
+    intro r s t r' s' t' hinv hlt; simp only [xgcdAux]
+    by_cases hd : r.natDegree < threshold
+    · rw [if_pos hd]
+      exact ⟨hinv.bez, natDegree_toPoly r ▸ hd,
+        (add_le_add le_rfl hinv.thr).trans_eq hinv.degree_complement, fun htz =>
+        hg₀ (Polynomial.degree_eq_bot.mp (by simp [← hinv.degree_complement, htz]))⟩
+    · rw [if_neg hd]; have hrne : r ≠ 0 := fun h => hd (by rwa [h]); rw [if_neg (by simpa)]
+      have hd' : ¬ r.toPoly.natDegree < threshold := natDegree_toPoly r ▸ hd
+      have hstep := hinv.step ((toPoly_eq_zero_iff _).not.mpr hrne) hd'
+      simp only [← toPoly_sub_div_mul] at hstep
+      refine ih _ _ _ _ _ _ hstep ((Nat.lt_succ_iff.mp hlt).trans_lt' ?_)
+      rw [natDegree_toPoly, natDegree_toPoly, toPoly_sub_div_mul, _root_.mul_comm,
+        ← EuclideanDomain.mod_eq_sub_mul_div]
+      exact r'.toPoly.natDegree_mod_lt (by omega)
+
+/-- `xgcd`'s output satisfies the stop spec. -/
+lemma xgcd_stopSpec
+    [Field F] [BEq F] [LawfulBEq F] (g₀ g₁ : CPolynomial F) (threshold : ℕ)
+    (hdeg : g₁.degree < g₀.degree)
+    (hthr : 1 ≤ threshold) (hthr' : threshold ≤ g₀.degree) :
+    BezoutStopSpecOf g₀ g₁ threshold (xgcd g₀ g₁ threshold) := by
+  have hdeg' : g₁.toPoly.degree < g₀.toPoly.degree := by rwa [← degree_toPoly, ← degree_toPoly]
+  have hg₀poly : g₀.toPoly ≠ 0 := Polynomial.ne_zero_of_degree_gt hdeg'
+  have hthr'poly : threshold ≤ g₀.toPoly.degree := degree_toPoly g₀ ▸ hthr'
+  have hstop : ¬ g₀.natDegree < threshold :=
+    natDegree_toPoly g₀ ▸ (le_natDegree_of_coe_le_degree hthr'poly).not_gt
+  have hge1 : 1 ≤ g₀.toPoly.natDegree := natDegree_toPoly g₀ ▸ hthr.trans (not_lt.mp hstop)
+  have hM : g₀.toPoly.natDegree + 1 ≤ g₀.val.size :=
+    (Polynomial.natDegree_lt_iff_degree_lt hg₀poly).mpr
+      (degree_toPoly g₀ ▸ mem_degreeLT_iff_size_le.mpr le_rfl)
+  obtain ⟨N, hN⟩ : ∃ N, g₀.val.size = N + 1 := ⟨g₀.val.size - 1, by omega⟩
+  obtain ⟨hr1, hs1, ht1⟩ : (g₁ - g₁/g₀*g₀).toPoly = g₁.toPoly ∧ (0 - g₁/g₀*1).toPoly = 0 ∧
+      (1 - g₁/g₀*0).toPoly = 1 := by
+    refine ⟨?_, ?_, ?_⟩ <;>
+      rw [toPoly_sub_div_mul, (Polynomial.div_eq_zero_iff hg₀poly).mpr hdeg'] <;>
+      simp [toPoly_zero, toPoly_one]
+  simp only [xgcd, hN, xgcdAux]
+  rw [if_neg hstop, if_neg (by simpa using (toPoly_eq_zero_iff _).not.mp hg₀poly)]
+  have hinv : BezoutDegreeInvariantOf g₀ g₁ threshold
+      (g₁ - g₁/g₀*g₀) (0 - g₁/g₀*1) (1 - g₁/g₀*0) g₀ 1 0 := by
+    rw [BezoutDegreeInvariantOf, hr1, hs1, ht1, toPoly_one, toPoly_zero]
+    exact ⟨by ring, by ring, by simp, by simp, hdeg', hthr'poly⟩
+  have hfuel : (g₁ - g₁/g₀*g₀).natDegree < N := by
+    rw [natDegree_toPoly, hr1]
+    rcases eq_or_ne g₁.toPoly 0 with hz | hz; rw [hz, Polynomial.natDegree_zero]; omega
+    exact (Polynomial.natDegree_lt_natDegree hz hdeg').trans_le (by omega)
+  exact xgcdAux_stopSpec_of_invariant _ _ _ hthr hg₀poly _ _ _ _ _ _ _ hinv hfuel
+
 end CompPoly

CompPoly/Univariate/ReedSolomon.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Conejero
+-/
+import CompPoly.Univariate.ToPoly.Impl
+
+/-!
+# Reed-Solomon Codes
+
+The Reed-Solomon code over a finite field: evaluation domain, message polynomial, and
+encoder. Decoders live in their own files.
+
+A Reed-Solomon code is fixed by an evaluation domain `(a₀, ..., aₙ₋₁) ∈ Fⁿ` of distinct
+points and a message length `k`. The codeword for a message `(m₀, ..., mₖ₋₁) ∈ Fᵏ` is
+`cᵢ = f(aᵢ)` with `f(x) = m₀ + m₁ x + ... + mₖ₋₁ xᵏ⁻¹`. For `1 ≤ k < n ≤ #F` this is an
+`(n, k, d)` code of minimum distance `d = n − k + 1`.
+
+## Main definitions
+
+* `Domain`: evaluation domain, an array of distinct points of `F`.
+* `messagePoly`, `encode`: the message polynomial of a coefficient vector and the encoder
+  evaluating it on the domain.
+-/
+
+namespace CompPoly
+
+namespace ReedSolomon
+
+variable {F : Type*}
+
+/-- Evaluation domain: an array of distinct points in `F`. -/
+def Domain (F : Type*) := {a : Array F // a.toList.Nodup}
+
+namespace Domain
+
+/-- Block length. -/
+abbrev n (D : Domain F) : ℕ := D.val.size
+
+/-- Indexing into the (nodup) domain array is injective on `Fin D.n`. -/
+lemma node_injective (D : Domain F) :
+    Function.Injective (fun i : Fin D.n => D.val[i]) :=
+  fun _ _ hxy => Fin.ext ((List.getElem_inj D.property).mp hxy)
+
+end Domain
+
+/-- Message polynomial `m₀ + m₁ x + ... + mₖ₋₁ xᵏ⁻¹` from a length-`k`
+coefficient vector `msg`. -/
+def messagePoly [Zero F] [BEq F] [LawfulBEq F]
+    {k : ℕ} (msg : Vector F k) : CPolynomial F :=
+  ⟨(CPolynomial.Raw.mk msg.toArray).trim,
+   CPolynomial.Raw.Trim.isCanonical_trim _⟩
+
+/-- `(messagePoly msg).degree < k`. -/
+lemma messagePoly_degree_lt [Zero F] [BEq F] [LawfulBEq F] {k : ℕ} (msg : Vector F k) :
+    (messagePoly msg).degree < k :=
+  CPolynomial.mem_degreeLT_iff_size_le.mpr
+    ((CPolynomial.Raw.Trim.size_le_size msg.toArray).trans_eq msg.size_toArray)
+
+/-- `messagePoly` recovers a `CPolynomial` of degree `< k` from its bounded coefficient vector. -/
+lemma messagePoly_ofFn_coeff [Semiring F] [BEq F] [LawfulBEq F] (k : ℕ) (f : CPolynomial F)
+    (hf : f.degree < k) : messagePoly (Vector.ofFn fun i : Fin k => f.coeff i) = f := by
+  rw [CPolynomial.eq_iff_coeff]; intro j
+  rw [messagePoly, CPolynomial.coeff, CPolynomial.Raw.Trim.coeff_eq_coeff, CPolynomial.Raw.coeff,
+    CPolynomial.Raw.mk, Vector.toArray_ofFn, Array.getD_eq_getD_getElem?, Array.getElem?_ofFn]
+  split; rfl
+  rename_i hjk
+  rw [Option.getD_none, CPolynomial.coeff_toPoly, Polynomial.coeff_eq_zero_of_degree_lt
+    ((CPolynomial.degree_toPoly f ▸ hf).trans_le (Nat.cast_le.mpr (not_lt.mp hjk)))]
+
+/-- Encode: the message polynomial `messagePoly msg` evaluated at the domain `D`. -/
+def encode [Semiring F] [BEq F] [LawfulBEq F]
+    (D : Domain F) {k : ℕ} (msg : Vector F k) : Vector F D.n :=
+  ⟨D.val.map (messagePoly msg).eval, by simp only [Array.size_map, Domain.n]⟩
+
+/-- The codeword entry at node `i` is `messagePoly msg` evaluated at `D.val[i]`. -/
+lemma encode_get [Semiring F] [BEq F] [LawfulBEq F] (D : Domain F) {k : ℕ}
+    (msg : Vector F k) (i : Fin D.n) :
+    (encode D msg).get i = (messagePoly msg).eval (D.val[i]) := Array.getElem_map ..
+
+end ReedSolomon
+
+end CompPoly