Series.lean — FrcCore

1import FrcCore.Shell2import FrcCore.Pigeonhole34/-!5# FrcCore.Series — bounded search, finite sums and products on the shell (the base theme, task LM22)67What every theme above needs and no frame provides: bounded quantifiers decided by search, without `propext`8(`decExistsLT`, `decForallLT`); sums `Σ_{l<n} f l` by structural recursion (`sumRange`), with congruence,9linearity, the single-term and the geometric sum; sums and products over lists of indices, and their invariance10under a permutation of `[0, n)` (`sum_perm`, `prod_perm`). No `Finset`, no quotient, no function extensionality.1112Moved here by task LM22 from `Frame.lean` (the two deciders) and `Sum.lean` (the sums and the lists), so that the13prime shell's toolkit (`Theme/Field.lean`) stands without the frame; every name is unchanged. The products are14LM22's. Task LM23 moved the pigeonhole on maps, `FRC.Logic.no_mirror` (5:C2), here from `Theme/Logic.lean`, under its15old name. No axioms.16-/1718namespace FRC19namespace Shell2021variable {p : Nat} [Pos p]2223/-- Bounded existence `∃ m < n, P m`, decided by search — Lean's own `Nat.decidableExistsLT` carries24`propext` and `Quot.sound`; this one carries nothing. -/25def decExistsLT (P : Nat → Prop) [DecidablePred P] : (n : Nat) → Decidable (∃ m, m < n ∧ P m)26  | 0 => isFalse (fun ⟨m, hm, _⟩ => Nat.not_lt_zero m hm)27  | n + 1 =>28    match decExistsLT P n with29    | isTrue h => isTrue (match h with | ⟨m, hm, hp⟩ => ⟨m, Nat.lt_succ_of_lt hm, hp⟩)30    | isFalse hno =>31      if h : P n then isTrue ⟨n, Nat.lt_succ_self n, h⟩32      else isFalse (fun ⟨m, hm, hp⟩ =>33        match Nat.lt_or_ge m n with34        | .inl hlt => hno ⟨m, hlt, hp⟩35        | .inr hge => h ((Nat.le_antisymm (Nat.le_of_lt_succ hm) hge) ▸ hp))3637/-- `∀ m < n, P m`, decided by recursion on `n` — Lean's own instance carries `propext`; this one nothing. -/38def decForallLT (P : Nat → Prop) [DecidablePred P] : (n : Nat) → Decidable (∀ m, m < n → P m)39  | 0 => isTrue (fun m hm => absurd hm (Nat.not_lt_zero m))40  | n + 1 =>41    match decForallLT P n with42    | isFalse h => isFalse (fun hall => h (fun m hm => hall m (Nat.lt_succ_of_lt hm)))43    | isTrue h =>44      if hn : P n then45        isTrue (fun m hm =>46          match Nat.lt_or_ge m n with47          | .inl hlt => h m hlt48          | .inr hge => (Nat.le_antisymm (Nat.le_of_lt_succ hm) hge) ▸ hn)49      else isFalse (fun hall => hn (hall n (Nat.lt_succ_self n)))5051/-! ## Finite sums -/5253/-- `sumRange f n = f 0 + f 1 + ⋯ + f (n−1)`. -/54def sumRange (f : Nat → Shell p) : Nat → Shell p55  | 0 => 056  | n + 1 => sumRange f n + f n5758theorem sumRange_zero (f : Nat → Shell p) : sumRange f 0 = 0 := rfl59theorem sumRange_succ (f : Nat → Shell p) (n : Nat) : sumRange f (n + 1) = sumRange f n + f n := rfl6061theorem sum_congr {f h : Nat → Shell p} (n : Nat) (e : ∀ l, l < n → f l = h l) :62    sumRange f n = sumRange h n := by63  induction n with64  | zero => rfl65  | succ n ih =>66    rw [sumRange_succ, sumRange_succ, ih (fun l hl => e l (Nat.lt_succ_of_lt hl)),67      e n (Nat.lt_succ_self n)]6869theorem sum_add (f h : Nat → Shell p) (n : Nat) :70    sumRange (fun l => f l + h l) n = sumRange f n + sumRange h n := by71  induction n with72  | zero => rw [sumRange_zero, sumRange_zero, sumRange_zero, add_zero]73  | succ n ih =>74    rw [sumRange_succ, sumRange_succ, sumRange_succ, ih, add_add_add_comm]7576theorem sum_mul_right (f : Nat → Shell p) (c : Shell p) (n : Nat) :77    sumRange (fun l => f l * c) n = sumRange f n * c := by78  induction n with79  | zero => rw [sumRange_zero, sumRange_zero, zero_mul]80  | succ n ih => rw [sumRange_succ, sumRange_succ, ih, right_distrib]8182theorem sum_mul_left (f : Nat → Shell p) (c : Shell p) (n : Nat) :83    sumRange (fun l => c * f l) n = c * sumRange f n := by84  induction n with85  | zero => rw [sumRange_zero, sumRange_zero, mul_zero]86  | succ n ih => rw [sumRange_succ, sumRange_succ, ih, left_distrib]8788theorem sum_neg (f : Nat → Shell p) (n : Nat) : sumRange (fun l => -(f l)) n = -(sumRange f n) := by89  induction n with90  | zero => rw [sumRange_zero, sumRange_zero, neg_zero]91  | succ n ih => rw [sumRange_succ, sumRange_succ, ih, neg_add_rev]9293theorem sum_const (c : Shell p) (n : Nat) : sumRange (fun _ => c) n = ofNat n * c := by94  induction n with95  | zero => rw [sumRange_zero]; exact (zero_mul c).symm96  | succ n ih =>97    rw [sumRange_succ, ih]98    have : (ofNat (n + 1) : Shell p) = ofNat n + 1 := ext (by99      rw [val_ofNat, val_add, val_ofNat, val_one, FRC.Nat.mod_add_mod _ _ _ hp, FRC.Nat.add_mod_mod _ _ _ hp])100    rw [this, right_distrib, one_mul]101102theorem sum_zero {f : Nat → Shell p} (n : Nat) (h : ∀ l, l < n → f l = 0) : sumRange f n = 0 := by103  induction n with104  | zero => rfl105  | succ n ih => rw [sumRange_succ, ih (fun l hl => h l (Nat.lt_succ_of_lt hl)), h n (Nat.lt_succ_self n), add_zero]106107/-- A sum with a single nonzero term. -/108theorem sum_eq_single {f : Nat → Shell p} {l₀ : Nat} : ∀ {n : Nat}, l₀ < n → (∀ l, l < n → l ≠ l₀ → f l = 0) →109    sumRange f n = f l₀110  | 0, h, _ => absurd h (Nat.not_lt_zero _)111  | n + 1, hl₀, h => by112    rw [sumRange_succ]113    exact match Nat.decEq l₀ n with114      | isTrue e => by115          rw [sum_zero n (fun l hl => h l (Nat.lt_succ_of_lt hl) (fun e' => absurd hl (by rw [e', e]; exact Nat.lt_irrefl n))),116            zero_add, e]117      | isFalse e => by118          rw [sum_eq_single (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hl₀) (fun e' => e e')) (fun l hl hne => h l (Nat.lt_succ_of_lt hl) hne),119            h n (Nat.lt_succ_self n) (fun e' => e e'.symm), add_zero]120121/-- The telescoping geometric sum: `(Σ_{l<n} x^l)·(x − 1) = x^n − 1`. -/122theorem geom_sum_mul (x : Shell p) (n : Nat) :123    sumRange (fun l => x ^ l) n * (x + -1) = x ^ n + -1 := by124  induction n with125  | zero => rw [sumRange_zero, zero_mul, pow_zero, add_neg]126  | succ n ih =>127    rw [sumRange_succ, right_distrib, ih, left_distrib, ← mul_neg, mul_one, ← pow_succ]128    rw [add_add_add_comm, add_comm (x ^ n) (x ^ (n + 1)), add_comm (-1) (-(x ^ n)), add_assoc,129      ← add_assoc (x ^ n), add_neg, zero_add]130131/-- `Σ_{l<n+1} f l = f 0 + Σ_{l<n} f (l + 1)`. -/132theorem sumRange_succ' (f : Nat → Shell p) : ∀ n, sumRange f (n + 1) = f 0 + sumRange (fun l => f (l + 1)) n133  | 0 => by rw [sumRange_succ, sumRange_zero, sumRange_zero, zero_add, add_zero]134  | n + 1 => by rw [sumRange_succ, sumRange_succ' f n, sumRange_succ, add_assoc]135136/-! ## Sums over lists, permutation invariance (the reindexing `j ↦ u·j` of 2:F5) -/137138/-- The sum of `F` over a list of indices. -/139def sumList (F : Nat → Shell p) : List Nat → Shell p140  | [] => 0141  | a :: l => F a + sumList F l142143/-- `[n−1, …, 0]`. -/144def listRange : Nat → List Nat145  | 0 => []146  | n + 1 => n :: listRange n147148/-- `[σ (n−1), …, σ 0]`. -/149def imageList (σ : Nat → Nat) : Nat → List Nat150  | 0 => []151  | n + 1 => σ n :: imageList σ n152153theorem sumList_imageList (F : Nat → Shell p) (σ : Nat → Nat) (n : Nat) :154    sumList F (imageList σ n) = sumRange (fun j => F (σ j)) n := by155  induction n with156  | zero => rfl157  | succ n ih => show F (σ n) + sumList F (imageList σ n) = sumRange (fun j => F (σ j)) n + F (σ n); rw [ih, add_comm]158159theorem sumList_erase (F : Nat → Shell p) {v : Nat} : ∀ {l : List Nat}, Pigeonhole.mem v l →160    sumList F l = F v + sumList F (Pigeonhole.erase v l)161  | [], h => absurd h id162  | a :: l, h => by163    exact match Nat.decEq a v with164      | isTrue e => by rw [show Pigeonhole.erase v (a :: l) = l from ite_eq_left e, e]; rfl165      | isFalse e => by166          rw [show Pigeonhole.erase v (a :: l) = a :: Pigeonhole.erase v l from ite_eq_right e]167          have hm : Pigeonhole.mem v l := match h with168            | Or.inl h' => absurd h'.symm e169            | Or.inr h' => h'170          show F a + sumList F l = F v + (F a + sumList F (Pigeonhole.erase v l))171          rw [sumList_erase F hm, add_left_comm]172173theorem imageList_length (σ : Nat → Nat) (n : Nat) : (imageList σ n).length = n := by174  induction n with175  | zero => rfl176  | succ n ih => show (imageList σ n).length + 1 = n + 1; rw [ih]177178theorem mem_imageList {σ : Nat → Nat} {v : Nat} : ∀ {n : Nat}, Pigeonhole.mem v (imageList σ n) → ∃ j, j < n ∧ σ j = v179  | 0, h => absurd h id180  | n + 1, h => match h with181    | Or.inl e => ⟨n, Nat.lt_succ_self n, e.symm⟩182    | Or.inr h' => match mem_imageList h' with183      | ⟨j, hj, e⟩ => ⟨j, Nat.lt_succ_of_lt hj, e⟩184185theorem imageList_nodup {σ : Nat → Nat} {n : Nat} (hinj : ∀ i j, i < n → j < n → σ i = σ j → i = j) :186    ∀ {m : Nat}, m ≤ n → Pigeonhole.NoDup (imageList σ m)187  | 0, _ => trivial188  | m + 1, hm => ⟨fun h => match mem_imageList h with189      | ⟨j, hj, e⟩ => Nat.lt_irrefl j (hinj j m (Nat.lt_of_lt_of_le hj (Nat.le_of_lt hm)) hm e ▸ hj),190    imageList_nodup hinj (Nat.le_of_lt hm)⟩191192/-- A sum over any list of `n` distinct indices below `n` is the sum over `0, …, n−1`. -/193theorem sumList_eq_sumRange (F : Nat → Shell p) : ∀ (n : Nat) (l : List Nat), Pigeonhole.NoDup l →194    (∀ e, Pigeonhole.mem e l → e < n) → l.length = n → sumList F l = sumRange F n195  | 0, [], _, _, _ => rfl196  | 0, a :: l, _, hb, _ => absurd (hb a (Or.inl rfl)) (Nat.not_lt_zero a)197  | n + 1, l, hnd, hb, hlen => by198    have hm : Pigeonhole.mem n l := Pigeonhole.mem_of_nodup_of_length_lt (n + 1) l hnd hb hlen n (Nat.lt_succ_self n)199    rw [sumList_erase F hm, sumRange_succ, add_comm]200    have hb' : ∀ e, Pigeonhole.mem e (Pigeonhole.erase n l) → e < n := fun e he =>201      match Nat.lt_or_ge e n with202      | Or.inl hlt => hlt203      | Or.inr hge =>204        have : e = n := Nat.le_antisymm (Nat.le_of_lt_succ (hb e (Pigeonhole.mem_of_mem_erase he))) hge205        absurd (this ▸ he) (Pigeonhole.not_mem_erase_self n hnd)206    have hlen' : (Pigeonhole.erase n l).length = n := by207      have := Pigeonhole.length_erase_of_mem hm; rw [hlen] at this; exact Nat.succ.inj this208    rw [sumList_eq_sumRange F n (Pigeonhole.erase n l) (Pigeonhole.nodup_erase n hnd) hb' hlen']209210/-- Permutation invariance: for `σ` injective on `[0, n)` with values below `n`,211`Σ_{j<n} F (σ j) = Σ_{l<n} F l`. -/212theorem sum_perm (F : Nat → Shell p) (σ : Nat → Nat) (n : Nat) (hlt : ∀ j, j < n → σ j < n)213    (hinj : ∀ i j, i < n → j < n → σ i = σ j → i = j) :214    sumRange (fun j => F (σ j)) n = sumRange F n := by215  rw [← sumList_imageList]216  exact sumList_eq_sumRange F n (imageList σ n) (imageList_nodup hinj (Nat.le_refl n))217    (fun e he => match mem_imageList he with | ⟨j, hj, e'⟩ => e' ▸ hlt j hj) (imageList_length σ n)218219/-! ## Products over `[0, n)`, invariant under a permutation (the products of `Sum.lean`'s sums) -/220221/-- `Π_{j<n} f j`. -/222def prodRange (f : Nat → Shell p) : Nat → Shell p223  | 0 => 1224  | n + 1 => prodRange f n * f n225226theorem prodRange_zero (f : Nat → Shell p) : prodRange f 0 = 1 := rfl227theorem prodRange_succ (f : Nat → Shell p) (n : Nat) : prodRange f (n + 1) = prodRange f n * f n := rfl228229theorem prodRange_congr {f h : Nat → Shell p} : ∀ n, (∀ j, j < n → f j = h j) → prodRange f n = prodRange h n230  | 0, _ => rfl231  | n + 1, e => by232    rw [prodRange_succ, prodRange_succ, prodRange_congr n (fun j hj => e j (Nat.lt_succ_of_lt hj)),233      e n (Nat.lt_succ_self n)]234235/-- A common factor leaves the product as its power: `Π_{j<n} a·G j = aⁿ · Π_{j<n} G j`. -/236theorem prodRange_mul_left (a : Shell p) (G : Nat → Shell p) :237    ∀ n, prodRange (fun j => a * G j) n = a ^ n * prodRange G n238  | 0 => (one_mul 1).symm239  | n + 1 => by rw [prodRange_succ, prodRange_succ, prodRange_mul_left a G n, pow_succ, mul_mul_mul_comm]240241/-- The product of `F` over a list of indices. -/242def prodList (F : Nat → Shell p) : List Nat → Shell p243  | [] => 1244  | a :: l => F a * prodList F l245246theorem prodList_imageList (F : Nat → Shell p) (σ : Nat → Nat) (n : Nat) :247    prodList F (imageList σ n) = prodRange (fun j => F (σ j)) n := by248  induction n with249  | zero => rfl250  | succ n ih =>251    show F (σ n) * prodList F (imageList σ n) = prodRange (fun j => F (σ j)) n * F (σ n); rw [ih, mul_comm]252253theorem prodList_erase (F : Nat → Shell p) {v : Nat} : ∀ {l : List Nat}, Pigeonhole.mem v l →254    prodList F l = F v * prodList F (Pigeonhole.erase v l)255  | [], h => absurd h id256  | a :: l, h => by257    exact match Nat.decEq a v with258      | isTrue e => by rw [show Pigeonhole.erase v (a :: l) = l from ite_eq_left e, e]; rfl259      | isFalse e => by260          rw [show Pigeonhole.erase v (a :: l) = a :: Pigeonhole.erase v l from ite_eq_right e]261          have hm : Pigeonhole.mem v l := match h with262            | Or.inl h' => absurd h'.symm e263            | Or.inr h' => h'264          show F a * prodList F l = F v * (F a * prodList F (Pigeonhole.erase v l))265          rw [prodList_erase F hm, mul_left_comm]266267/-- A product over any list of `n` distinct indices below `n` is the product over `0, …, n−1`. -/268theorem prodList_eq_prodRange (F : Nat → Shell p) : ∀ (n : Nat) (l : List Nat), Pigeonhole.NoDup l →269    (∀ e, Pigeonhole.mem e l → e < n) → l.length = n → prodList F l = prodRange F n270  | 0, [], _, _, _ => rfl271  | 0, a :: l, _, hb, _ => absurd (hb a (Or.inl rfl)) (Nat.not_lt_zero a)272  | n + 1, l, hnd, hb, hlen => by273    have hm : Pigeonhole.mem n l := Pigeonhole.mem_of_nodup_of_length_lt (n + 1) l hnd hb hlen n (Nat.lt_succ_self n)274    rw [prodList_erase F hm, prodRange_succ, mul_comm]275    have hb' : ∀ e, Pigeonhole.mem e (Pigeonhole.erase n l) → e < n := fun e he =>276      match Nat.lt_or_ge e n with277      | Or.inl hlt => hlt278      | Or.inr hge =>279        have : e = n := Nat.le_antisymm (Nat.le_of_lt_succ (hb e (Pigeonhole.mem_of_mem_erase he))) hge280        absurd (this ▸ he) (Pigeonhole.not_mem_erase_self n hnd)281    have hlen' : (Pigeonhole.erase n l).length = n := by282      have := Pigeonhole.length_erase_of_mem hm; rw [hlen] at this; exact Nat.succ.inj this283    rw [prodList_eq_prodRange F n (Pigeonhole.erase n l) (Pigeonhole.nodup_erase n hnd) hb' hlen']284285/-- Permutation invariance: for `σ` injective on `[0, n)` with values below `n`,286`Π_{j<n} F (σ j) = Π_{l<n} F l`. -/287theorem prod_perm (F : Nat → Shell p) (σ : Nat → Nat) (n : Nat) (hlt : ∀ j, j < n → σ j < n)288    (hinj : ∀ i j, i < n → j < n → σ i = σ j → i = j) :289    prodRange (fun j => F (σ j)) n = prodRange F n := by290  rw [← prodList_imageList]291  exact prodList_eq_prodRange F n (imageList σ n) (imageList_nodup hinj (Nat.le_refl n))292    (fun e he => match mem_imageList he with | ⟨j, hj, e'⟩ => e' ▸ hlt j hj) (imageList_length σ n)293294end Shell295296namespace Logic297298/-- 5:C2, 29:C10 (Proposition mirror) — a part with fewer records than the frame has elements holds no injective299representation of the frame's domain: no `f : [0, N) → [0, R)` is injective when `R < N`. In the base since task LM23300(from `Theme/Logic.lean`, under its old name), so that the foundation's A4 (Observation; the bounded observer, A5 at task LM23) stands on it. -/301theorem no_mirror {N R : Nat} (hR : R < N) (f : Nat → Nat) (hf : ∀ i, i < N → f i < R)302    (hinj : ∀ i j, i < N → j < N → f i = f j → i = j) : False :=303  have hnd := FRC.Shell.imageList_nodup hinj (Nat.le_refl N)304  have hlen := FRC.Shell.imageList_length f N305  have hb : ∀ e, Pigeonhole.mem e (FRC.Shell.imageList f N) → e < R := fun _ he =>306    match FRC.Shell.mem_imageList he with307    | ⟨j, hj, ej⟩ => ej ▸ hf j hj308  have := Pigeonhole.length_le_of_nodup_lt R _ hnd hb309  Nat.lt_irrefl N (Nat.lt_of_le_of_lt (hlen ▸ this) hR)310311end Logic312end FRC313