The core module lean/FrcCore/Theme/Poly.lean — the substrate from first principles, no Mathlib, no axioms; one of the core's 137 modules (the index); it rests on 17 modules: Nat, Pigeonhole, Shell, Series, Cycle, Ring, FrameCore, Frame, Parity, Transform, Orbit, Sum, Theme/Quadratic, Theme/Extension, Instances, Theme/Dirac, Theme/Hermitian: 25 theorems (10 definitions): 25 with no axioms, 0 at tier 1 (propext, Quot.sound), 0 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (green, the core; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import FrcCore.Theme.Hermitian2/-!3# FrcCore.Theme.Poly — polynomials over `K` (the operator theme)45A polynomial over `K = 𝔽_p[w]/(w² − ν)` is its list of coefficients, the constant term first; trailing zeros are allowed, so6two lists may name one polynomial, and the statements below are about the evaluation map and the coefficients, never about7the lists as such. The operations: sum, negative, scalar multiple, product (the convolution, by recursion on the first8factor), the constants, `X`. The evaluation `eval f x` by Horner's scheme is a ring homomorphism (`eval_padd`, `eval_pneg`,9`eval_psmul`, `eval_pmul`, `eval_C`, `eval_X`), the facts the characteristic polynomial of `Theme/CharPoly` rests on. The10coefficients: `coeff f k` is the `k`-th entry (`0` beyond the list), `DegLE f d` says every coefficient above `d` is zero,11and the coefficient lemmas of the sum and the product (`coeff_padd`, `coeff_pmul_top`) give the leading term of a product.12No axioms.13-/1415namespace FRC.Dirac.Poly1617open FRC FRC.Extension FRC.Dirac FRC.Dirac.Hermitian18open FRC.Dirac.Mat (nth)1920variable {p : Nat} [Pos p] {ν : Shell p}2122/-- A polynomial over `K`: its coefficients, the constant term first. -/23
abbrev Poly (p : Nat) [Pos p] (ν : Shell p) := List (Ext p ν)2425/-! ## The operations -/2627def padd : Poly p ν → Poly p ν → Poly p ν28 | [], g => g29 | f, [] => f30 | a :: f, b :: g => (a + b) :: padd f g3132def pneg (f : Poly p ν) : Poly p ν := f.map (- ·)3334def psmul (c : Ext p ν) (f : Poly p ν) : Poly p ν := f.map (c * ·)3536/-- The product by recursion on the first factor: `(a + X f) g = a g + X (f g)`. -/37def pmul : Poly p ν → Poly p ν → Poly p ν38 | [], _ => []39 | a :: f, g => padd (psmul a g) (0 :: pmul f g)4041/-- The constant polynomial. -/42def C (a : Ext p ν) : Poly p ν := [a]4344/-- The indeterminate. -/45def X : Poly p ν := [0, 1]4647/-- Horner's scheme: `eval (a :: f) x = a + x · eval f x`. -/48def eval : Poly p ν → Ext p ν → Ext p ν49 | [], _ => 050 | a :: f, x => a + x * eval f x5152/-- The `k`-th coefficient (`0` beyond the list). -/53def coeff (f : Poly p ν) (k : Nat) : Ext p ν := nth 0 f k5455/-- Every coefficient above `d` vanishes. -/56def DegLE (f : Poly p ν) (d : Nat) : Prop := ∀ k, d < k → coeff f k = 05758/-! ## Evaluation is a ring homomorphism -/5960
theorem eval_nil (x : Ext p ν) : eval ([] : Poly p ν) x = 0 := rfl6162theorem eval_cons (a : Ext p ν) (f : Poly p ν) (x : Ext p ν) : eval (a :: f) x = a + x * eval f x := rfl6364theorem eval_padd : ∀ (f g : Poly p ν) (x : Ext p ν), eval (padd f g) x = eval f x + eval g x65 | [], g, x => (zero_add _).symm66 | _ :: _, [], x => (add_zero _).symm67 | a :: f, b :: g, x => by68 show a + b + x * eval (padd f g) x = (a + x * eval f x) + (b + x * eval g x)69 rw [eval_padd f g x, mul_add, add_assoc, add_assoc, ← add_assoc b, add_comm b, add_assoc]7071theorem eval_pneg : ∀ (f : Poly p ν) (x : Ext p ν), eval (pneg f) x = -(eval f x)72 | [], _ => (neg_zero_ext).symm73 | a :: f, x => by74 show -a + x * eval (pneg f) x = -(a + x * eval f x)75 rw [eval_pneg f x, ← mul_neg, neg_add_eq]76where77 neg_zero_ext : (-0 : Ext p ν) = 0 := Ext.ext Shell.neg_zero Shell.neg_zero78 neg_add_eq (a b : Ext p ν) : -a + -b = -(a + b) := by79 have h : (a + b) + (-a + -b) = 0 := by80 rw [add_assoc, ← add_assoc b, add_comm b, add_assoc, add_neg, add_zero, add_neg]81 have h2 := congrArg (fun z => -(a + b) + z) h82 show -a + -b = -(a + b)83 have : -(a + b) + ((a + b) + (-a + -b)) = -a + -b := by rw [← add_assoc, neg_add, zero_add]84 rw [← this, h, add_zero]8586theorem eval_psmul (c : Ext p ν) : ∀ (f : Poly p ν) (x : Ext p ν), eval (psmul c f) x = c * eval f x87 | [], _ => (mul_zero c).symm88 | a :: f, x => by89 show c * a + x * eval (psmul c f) x = c * (a + x * eval f x)90 rw [eval_psmul c f x, mul_add, ← Ext.mul_assoc, Ext.mul_comm x c, Ext.mul_assoc]9192theorem eval_pmul : ∀ (f g : Poly p ν) (x : Ext p ν), eval (pmul f g) x = eval f x * eval g x93 | [], g, x => (zero_mul _).symm94 | a :: f, g, x => by95 show eval (padd (psmul a g) (0 :: pmul f g)) x = (a + x * eval f x) * eval g x96 rw [eval_padd, eval_psmul, eval_cons, zero_add, eval_pmul f g x, add_mul, Ext.mul_assoc]9798theorem eval_C (a x : Ext p ν) : eval (C a) x = a := by show a + x * 0 = a; rw [mul_zero, add_zero]99100theorem eval_X (x : Ext p ν) : eval (X : Poly p ν) x = x := by101 show 0 + x * (1 + x * 0) = x; rw [mul_zero, add_zero, Ext.mul_one, zero_add]102103/-! ## Coefficients -/104105theorem coeff_nil (k : Nat) : coeff ([] : Poly p ν) k = 0 := rfl106107theorem coeff_cons_zero (a : Ext p ν) (f : Poly p ν) : coeff (a :: f) 0 = a := rfl108109theorem coeff_cons_succ (a : Ext p ν) (f : Poly p ν) (k : Nat) : coeff (a :: f) (k + 1) = coeff f k := rfl110111theorem coeff_padd : ∀ (f g : Poly p ν) (k : Nat), coeff (padd f g) k = coeff f k + coeff g k112 | [], g, k => by show coeff g k = coeff [] k + coeff g k; rw [coeff_nil, zero_add]113 | a :: f, [], k => by show coeff (a :: f) k = coeff (a :: f) k + coeff [] k; rw [coeff_nil, add_zero]114 | _ :: _, _ :: _, 0 => rfl115 | _ :: f, _ :: g, k + 1 => coeff_padd f g k116117theorem coeff_psmul (c : Ext p ν) : ∀ (f : Poly p ν) (k : Nat), coeff (psmul c f) k = c * coeff f k118 | [], k => by show coeff [] k = c * coeff [] k; rw [coeff_nil, mul_zero]119 | _ :: _, 0 => rfl120 | _ :: f, k + 1 => coeff_psmul c f k121122theorem coeff_pneg : ∀ (f : Poly p ν) (k : Nat), coeff (pneg f) k = -(coeff f k)123 | [], k => by show coeff [] k = -(coeff [] k); rw [coeff_nil]; exact (Ext.ext Shell.neg_zero Shell.neg_zero).symm124 | _ :: _, 0 => rfl125 | _ :: f, k + 1 => coeff_pneg f k126127theorem coeff_pmul_zero : ∀ (f g : Poly p ν), coeff (pmul f g) 0 = coeff f 0 * coeff g 0128 | [], g => by show coeff [] 0 = coeff [] 0 * coeff g 0; rw [coeff_nil, zero_mul]129 | a :: f, g => by130 show coeff (padd (psmul a g) (0 :: pmul f g)) 0 = a * coeff g 0131 rw [coeff_padd, coeff_psmul, coeff_cons_zero, add_zero]132133theorem coeff_pmul_succ : ∀ (f g : Poly p ν) (k : Nat), coeff (pmul f g) (k + 1) = coeff f 0 * coeff g (k + 1) + coeff (pmul f.tail g) k134 | [], g, k => by show coeff [] (k + 1) = coeff [] 0 * coeff g (k + 1) + coeff (pmul [] g) k; rw [coeff_nil, coeff_nil, zero_mul, zero_add]; rfl135 | a :: f, g, k => by136 show coeff (padd (psmul a g) (0 :: pmul f g)) (k + 1) = a * coeff g (k + 1) + coeff (pmul f g) k137 rw [coeff_padd, coeff_psmul, coeff_cons_succ]138139theorem degLE_of_length (f : Poly p ν) (d : Nat) (h : f.length ≤ d + 1) : DegLE f d := fun k hk => by140 show nth 0 f k = 0141 exact nth_beyond' f k (Nat.le_trans h hk)142where143 nth_beyond' : ∀ (l : Poly p ν) (i : Nat), l.length ≤ i → nth 0 l i = 0144 | [], _, _ => rfl145 | _ :: _, 0, h => absurd h (Nat.not_succ_le_zero _)146 | _ :: l, i + 1, h => nth_beyond' l i (Nat.le_of_succ_le_succ h)147148theorem degLE_padd (f g : Poly p ν) (d : Nat) (hf : DegLE f d) (hg : DegLE g d) : DegLE (padd f g) d := fun k hk => by149 rw [coeff_padd, hf k hk, hg k hk, add_zero]150151theorem degLE_psmul (c : Ext p ν) (f : Poly p ν) (d : Nat) (hf : DegLE f d) : DegLE (psmul c f) d := fun k hk => by152 rw [coeff_psmul, hf k hk, mul_zero]153154theorem degLE_pneg (f : Poly p ν) (d : Nat) (hf : DegLE f d) : DegLE (pneg f) d := fun k hk => by155 rw [coeff_pneg, hf k hk]; exact Ext.ext Shell.neg_zero Shell.neg_zero156157theorem degLE_mono (f : Poly p ν) {d e : Nat} (hde : d ≤ e) (hf : DegLE f d) : DegLE f e := fun k hk => hf k (Nat.lt_of_le_of_lt hde hk)158159theorem degLE_cons (a : Ext p ν) (f : Poly p ν) (d : Nat) (hf : DegLE f d) : DegLE (a :: f) (d + 1) := fun k hk =>160 match k, hk with161 | k + 1, hk => hf k (Nat.lt_of_succ_lt_succ hk)162163theorem degLE_tail : ∀ (f : Poly p ν) (d : Nat), DegLE f (d + 1) → DegLE f.tail d164 | [], _, _ => fun _ _ => rfl165 | _ :: _, _, hf => fun k hk => hf (k + 1) (Nat.succ_lt_succ hk)166167/-- The degree of a product: `DegLE f d`, `DegLE g e` give `DegLE (f g) (d + e)`. -/168theorem degLE_pmul : ∀ (f g : Poly p ν) (d e : Nat), DegLE f d → DegLE g e → DegLE (pmul f g) (d + e)169 | [], _, _, _, _, _ => fun k _ => rfl170 | a :: f, g, d, e, hf, hg => by171 show DegLE (padd (psmul a g) (0 :: pmul f g)) (d + e)172 match d with173 | 0 =>174 -- `f` is zero beyond its constant term: every coefficient of `f` vanishes, and so does `f · g`175 have hf0 : ∀ k, coeff f k = 0 := fun k => hf (k + 1) (Nat.succ_pos k)176 intro k hk177 rw [coeff_padd, coeff_psmul, hg k (Nat.zero_add e ▸ hk), mul_zero, zero_add]178 match k with179 | 0 => rfl180 | k + 1 => exact coeff_pmul_zero_poly f g hf0 k181 | d + 1 =>182 refine degLE_padd _ _ _ (degLE_mono _ (Nat.le_add_left e (d + 1)) (degLE_psmul a g e hg)) ?_183 have := degLE_pmul f g d e (degLE_tail (a :: f) d hf) hg184 rw [Nat.succ_add]; exact degLE_cons 0 _ _ this185where186 coeff_pmul_zero_poly : ∀ (f g : Poly p ν), (∀ k, coeff f k = 0) → ∀ k, coeff (pmul f g) k = 0187 | [], _, _, _ => rfl188 | a :: f, g, h, k => by189 show coeff (padd (psmul a g) (0 :: pmul f g)) k = 0190 rw [coeff_padd, coeff_psmul, show a = 0 from h 0, zero_mul, zero_add]191 match k with192 | 0 => rfl193 | k + 1 => exact coeff_pmul_zero_poly f g (fun k => h (k + 1)) k194195/-- The top coefficient of a product: with `DegLE f d`, `DegLE g e`, `coeff (f g) (d + e) = coeff f d · coeff g e`. -/196theorem coeff_pmul_top : ∀ (f g : Poly p ν) (d e : Nat), DegLE f d → DegLE g e → coeff (pmul f g) (d + e) = coeff f d * coeff g e197 | [], g, d, e, _, _ => by show coeff [] (d + e) = coeff [] d * coeff g e; rw [coeff_nil, coeff_nil, zero_mul]198 | a :: f, g, d, e, hf, hg => by199 show coeff (padd (psmul a g) (0 :: pmul f g)) (d + e) = coeff (a :: f) d * coeff g e200 rw [coeff_padd, coeff_psmul]201 match d with202 | 0 =>203 rw [Nat.zero_add]204 have hf0 : ∀ k, coeff f k = 0 := fun k => hf (k + 1) (Nat.succ_pos k)205 match e with206 | 0 => show a * coeff g 0 + 0 = a * coeff g 0; rw [add_zero]207 | e + 1 =>208 rw [coeff_cons_succ, degLE_pmul.coeff_pmul_zero_poly f g hf0 e, add_zero]; rfl209 | d + 1 =>210 rw [Nat.succ_add, coeff_cons_succ, hg (d + e + 1) (Nat.succ_le_succ (Nat.le_add_left e d)), mul_zero, zero_add,211 coeff_pmul_top f g d e (degLE_tail (a :: f) d hf) hg]212 rfl213214end FRC.Dirac.Poly215