ProjectorCore.lean

1 import Mathlib.Analysis.SpecificLimits.Normed
2 import Mathlib.Algebra.Order.Floor.Div
3 import Mathlib.Data.Fintype.BigOperators
4 import Mathlib.Data.List.OfFn
5 import Mathlib.Algebra.Polynomial.Basic
6 import Mathlib.Algebra.Polynomial.Coeff
7 import Mathlib.Data.Finset.NatAntidiagonal
8 import Mathlib.Data.Fintype.Card
9 import Mathlib.Data.Matrix.Basic
10 import Mathlib.LinearAlgebra.Matrix.Adjugate
11 import Mathlib.RingTheory.PowerSeries.Basic
12 import Mathlib.RingTheory.PowerSeries.Inverse
13 import Mathlib.Analysis.Normed.Ring.Basic
14 import Mathlib.Tactic.NoncommRing
15 import Mathlib.Algebra.BigOperators.Intervals
16 import Mathlib.Algebra.Module.Submodule.LinearMap
17 import Mathlib.Algebra.Polynomial.Eval.Defs
18 import Mathlib.Analysis.Normed.Operator.Basic
19 import Mathlib.Tactic.Abel
20 import Mathlib.Util.AssertNoSorry
21 import Mathlib.Analysis.Complex.Exponential
22 import Mathlib.LinearAlgebra.Matrix.Notation
23 import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
24 import Mathlib.Data.Nat.ChineseRemainder
25 import Mathlib.GroupTheory.SpecificGroups.Cyclic
26 import Mathlib.NumberTheory.Padics.PadicVal.Basic
27 import Mathlib.RingTheory.Polynomial.Resultant.Basic
28 import Mathlib.Tactic.NormNum
29 import Mathlib.Tactic.Ring
30 import Mathlib.Tactic.FinCases
31 import Mathlib.Tactic.FieldSimp
32 import Mathlib.Tactic.Push
33 import Mathlib.Tactic.ByContra
34 import Mathlib.Tactic.SplitIfs
35 import Mathlib.Tactic.FunProp
36 
37 /-!
38 # Komorebi Projector Calculus — browser-safe formal core
39 
40 This file is intentionally conservative.  It contains the foundational theorem
41 tranche only.  The larger source-claim ledger is included in the companion
42 `..._Full_Fixed.lean` file as data, not as theorem assumptions.
43 -/
44 
45 set_option maxRecDepth 100000
46 set_option maxHeartbeats 4000000
47 set_option autoImplicit false
48 
49 namespace Komorebi
50 
51 /-! ## Proof-status vocabulary -/
52 
53 inductive ClaimKind where
54   | definitionClaim
55   | theoremClaim
56   | propositionClaim
57   | lemmaClaim
58   | corollaryClaim
59   | exampleClaim
60   | remarkClaim
61   | algorithmClaim
62   | numericalCertificate
63   | classicalInput
64   | conjecture
65   | boundary
66   deriving Repr, DecidableEq, BEq, Inhabited
67 
68 inductive FormalizationStatus where
69   | kernelChecked
70   | proofTermPresent
71   | partialFormalization
72   | encodedDefinition
73   | queued
74   | blockedByLibrary
75   | numericalOnly
76   | conjectural
77   | externalInput
78   | contextOnly
79   | boundaryOnly
80   deriving Repr, DecidableEq, BEq, Inhabited
81 
82 structure ClaimRecord where
83   id : String
84   corpus : String
85   volume : String
86   source : String
87   ordinal : Nat
88   title : String
89   heading : String
90   statement : String
91   kind : ClaimKind
92   status : FormalizationStatus
93   sourceStatus : String := ""
94   phase : String := ""
95   targetNamespace : String := ""
96   difficulty : String := ""
97   notes : String := ""
98   deriving Repr, Inhabited
99 
100 def ClaimRecord.dependencySafe (claim : ClaimRecord) : Bool :=
101   claim.status == .kernelChecked
102 
103 def ClaimRecord.isOpenOrBoundary (claim : ClaimRecord) : Bool :=
104   claim.kind == .conjecture || claim.kind == .boundary
105 
106 /-! ## A browser-safe operator grammar -/
107 
108 namespace Seed
109 
110 universe u v
111 
112 inductive OperatorExpr (Atom : Type u) where
113   | id
114   | atom (f : Atom)
115   | comp (f g : OperatorExpr Atom)
116   deriving Repr
117 
118 namespace OperatorExpr
119 
120 variable {Atom : Type u} {X : Type v}
121 
122 def eval (interpret : Atom → X → X) : OperatorExpr Atom → X → X
123   | .id => fun x => x
124   | .atom f => interpret f
125   | .comp f g => fun x => eval interpret g (eval interpret f x)
126 
127 @[simp] theorem eval_id (interpret : Atom → X → X) (x : X) :
128     eval interpret .id x = x := rfl
129 
130 @[simp] theorem eval_atom (interpret : Atom → X → X) (f : Atom) (x : X) :
131     eval interpret (.atom f) x = interpret f x := rfl
132 
133 @[simp] theorem eval_comp
134     (interpret : Atom → X → X) (f g : OperatorExpr Atom) (x : X) :
135     eval interpret (.comp f g) x = eval interpret g (eval interpret f x) := rfl
136 
137 end OperatorExpr
138 
139 structure OperatorRelation (Atom : Type u) where
140   lhs : OperatorExpr Atom
141   rhs : OperatorExpr Atom
142 
143 namespace OperatorRelation
144 
145 variable {Atom : Type u} {X : Type v}
146 
147 def Satisfied (interpret : Atom → X → X) (r : OperatorRelation Atom) : Prop :=
148   ∀ x, OperatorExpr.eval interpret r.lhs x = OperatorExpr.eval interpret r.rhs x
149 
150 @[simp] theorem satisfied_refl
151     (interpret : Atom → X → X) (f : OperatorExpr Atom) :
152     Satisfied interpret ⟨f, f⟩ := by
153   intro x
154   rfl
155 
156 theorem satisfied_symm
157     (interpret : Atom → X → X) {r : OperatorRelation Atom}
158     (h : Satisfied interpret r) :
159     Satisfied interpret ⟨r.rhs, r.lhs⟩ := by
160   intro x
161   exact (h x).symm
162 
163 theorem satisfied_trans
164     (interpret : Atom → X → X) {f g h : OperatorExpr Atom}
165     (hfg : Satisfied interpret ⟨f, g⟩)
166     (hgh : Satisfied interpret ⟨g, h⟩) :
167     Satisfied interpret ⟨f, h⟩ := by
168   intro x
169   exact (hfg x).trans (hgh x)
170 
171 theorem satisfied_postcomp
172     (interpret : Atom → X → X) {r : OperatorRelation Atom}
173     (h : Satisfied interpret r) (g : OperatorExpr Atom) :
174     Satisfied interpret ⟨.comp r.lhs g, .comp r.rhs g⟩ := by
175   intro x
176   simp only [OperatorExpr.eval_comp]
177   rw [h x]
178 
179 end OperatorRelation
180 
181 universe w
182 
183 variable {R : Type u} {M : Type v}
184 variable [Semiring R] [AddCommMonoid M] [Module R M]
185 
186 def algebraicHull (S : Set M) : Submodule R M :=
187   Submodule.span R S
188 
189 @[simp] theorem seed_subset_hull (S : Set M) :
190     S ⊆ algebraicHull (R := R) S :=
191   Submodule.subset_span
192 
193 theorem hull_le {S : Set M} {P : Submodule R M} (h : S ⊆ P) :
194     algebraicHull (R := R) S ≤ P :=
195   Submodule.span_le.2 h
196 
197 @[simp] theorem hull_empty :
198     algebraicHull (R := R) (∅ : Set M) = ⊥ := by
199   simp [algebraicHull]
200 
201 @[simp] theorem hull_univ :
202     algebraicHull (R := R) (Set.univ : Set M) = ⊤ := by
203   apply le_antisymm le_top
204   intro x hx
205   exact Submodule.subset_span (Set.mem_univ x)
206 
207 end Seed
208 
209 /-! ## Complete finite projector families -/
210 
211 namespace Foundation
212 
213 universe u v w x y
214 
215 structure LinearProjectorFamily
216     (R : Type u) (M : Type v) (ι : Type w)
217     [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] where
218   proj : ι → Module.End R M
219   idempotent : ∀ i x, proj i (proj i x) = proj i x
220   orthogonal : ∀ {i j}, i ≠ j → ∀ x, proj i (proj j x) = 0
221   complete : ∀ x, (∑ i, proj i x) = x
222 
223 namespace LinearProjectorFamily
224 
225 variable {R : Type u} {M : Type v} {ι : Type w}
226 variable [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι]
227 
228 
229 def analyze (P : LinearProjectorFamily R M ι) (x : M) : ι → M :=
230   fun i => P.proj i x
231 
232 
233 def synthesize (_P : LinearProjectorFamily R M ι) (packets : ι → M) : M :=
234   ∑ i, packets i
235 
236 @[simp] theorem synthesize_analyze
237     (P : LinearProjectorFamily R M ι) (x : M) :
238     P.synthesize (P.analyze x) = x := by
239   simpa [synthesize, analyze] using P.complete x
240 
241 theorem eq_of_projectors_eq
242     (P : LinearProjectorFamily R M ι) {x y : M}
243     (h : ∀ i, P.proj i x = P.proj i y) : x = y := by
244   calc
245     x = ∑ i, P.proj i x := (P.complete x).symm
246     _ = ∑ i, P.proj i y := by
247       apply Finset.sum_congr rfl
248       intro i hi
249       exact h i
250     _ = y := P.complete y
251 
252 end LinearProjectorFamily
253 
254 variable {R : Type u} {M : Type v} {N : Type w} {L : Type x}
255 variable {ι : Type y} {κ : Type*} {τ : Type*}
256 variable [Semiring R]
257 variable [AddCommMonoid M] [Module R M]
258 variable [AddCommMonoid N] [Module R N]
259 variable [AddCommMonoid L] [Module R L]
260 variable [Fintype ι] [Fintype κ] [Fintype τ]
261 
262 
263 def transferBlock
264     (P : LinearProjectorFamily R M ι)
265     (Q : LinearProjectorFamily R N κ)
266     (T : M →ₗ[R] N) (j : κ) (i : ι) : M →ₗ[R] N :=
267   (Q.proj j).comp (T.comp (P.proj i))
268 
269 
270 theorem transferBlock_reconstruction
271     (P : LinearProjectorFamily R M ι)
272     (Q : LinearProjectorFamily R N κ)
273     (T : M →ₗ[R] N) (x : M) :
274     (∑ j, ∑ i, Q.proj j (T (P.proj i x))) = T x := by
275   calc
276     (∑ j, ∑ i, Q.proj j (T (P.proj i x))) =
277         ∑ j, Q.proj j (T (∑ i, P.proj i x)) := by
278           apply Finset.sum_congr rfl
279           intro j hj
280           simp only [map_sum]
281     _ = ∑ j, Q.proj j (T x) := by rw [P.complete x]
282     _ = T x := Q.complete (T x)
283 
284 
285 theorem transferBlock_comp
286     (P : LinearProjectorFamily R M ι)
287     (Q : LinearProjectorFamily R N κ)
288     (S : LinearProjectorFamily R L τ)
289     (T : M →ₗ[R] N) (U : N →ₗ[R] L)
290     (k : τ) (i : ι) (x : M) :
291     S.proj k (U (T (P.proj i x))) =
292       ∑ j, S.proj k (U (Q.proj j (T (P.proj i x)))) := by
293   have h := (Q.complete (T (P.proj i x))).symm
294   calc
295     S.proj k (U (T (P.proj i x))) =
296         S.proj k (U (∑ j, Q.proj j (T (P.proj i x)))) :=
297           congrArg (fun y => S.proj k (U y)) h
298     _ = ∑ j, S.proj k (U (Q.proj j (T (P.proj i x)))) := by
299           simp only [map_sum]
300 
301 end Foundation
302 
303 /-! ## Fibre and coordinate packets -/
304 
305 namespace Packet
306 
307 universe u v w
308 
309 variable {α : Type u} {β : Type v} {M : Type w}
310 
311 
312 def fibreProj [DecidableEq β] [Zero M]
313     (address : α → β) (b : β) (x : α → M) : α → M :=
314   fun a => if address a = b then x a else 0
315 
316 @[simp] theorem fibreProj_apply_same
317     [DecidableEq β] [Zero M]
318     (address : α → β) (b : β) (x : α → M) (a : α)
319     (h : address a = b) :
320     fibreProj address b x a = x a := by
321   simp [fibreProj, h]
322 
323 @[simp] theorem fibreProj_apply_ne
324     [DecidableEq β] [Zero M]
325     (address : α → β) (b : β) (x : α → M) (a : α)
326     (h : address a ≠ b) :
327     fibreProj address b x a = 0 := by
328   simp [fibreProj, h]
329 
330 
331 theorem fibreProj_idempotent
332     [DecidableEq β] [Zero M]
333     (address : α → β) (b : β) (x : α → M) :
334     fibreProj address b (fibreProj address b x) = fibreProj address b x := by
335   funext a
336   by_cases h : address a = b <;> simp [fibreProj, h]
337 
338 
339 theorem fibreProj_orthogonal
340     [DecidableEq β] [Zero M]
341     (address : α → β) {b c : β} (hbc : b ≠ c) (x : α → M) :
342     fibreProj address b (fibreProj address c x) = 0 := by
343   funext a
344   by_cases h : address a = b <;> simp [fibreProj, h, hbc]
345 
346 
347 theorem fibreProj_reconstruction
348     [DecidableEq β] [Fintype β] [AddCommMonoid M]
349     (address : α → β) (x : α → M) :
350     (∑ b, fibreProj address b x) = x := by
351   funext a
352   simp [fibreProj]
353 
354 
355 def coordinateProj {ι : Type u} [DecidableEq ι] [Zero M]
356     (i : ι) (x : ι → M) : ι → M :=
357   fun j => if j = i then x j else 0
358 
359 
360 theorem coordinateProj_reconstruction
361     {ι : Type u} [DecidableEq ι] [Fintype ι] [AddCommMonoid M]
362     (x : ι → M) :
363     (∑ i, coordinateProj i x) = x := by
364   funext j
365   simp [coordinateProj]
366 
367 end Packet
368 
369 /-! ## Block and factor-first operators -/
370 
371 namespace Operator
372 
373 universe u v w
374 
375 variable {ι : Type u} {κ : Type v} {M : Type w}
376 
377 
378 def blockApply
379     [Fintype κ] [AddCommMonoid M]
380     (T : ι → κ → M →+ M) (x : κ → M) : ι → M :=
381   fun i => ∑ j, T i j (x j)
382 
383 @[simp] theorem blockApply_zero
384     [Fintype κ] [AddCommMonoid M]
385     (T : ι → κ → M →+ M) :
386     blockApply T (0 : κ → M) = 0 := by
387   funext i
388   simp [blockApply]
389 
390 variable {ρ : Type*} {R : Type*}
391 
392 
393 def lowRankApply
394     [Fintype κ] [Fintype ρ] [CommSemiring R]
395     (U : ι → ρ → R) (V : κ → ρ → R) (x : κ → R) : ι → R :=
396   fun i => ∑ r, U i r * (∑ j, V j r * x j)
397 
398 @[simp] theorem lowRankApply_zero_vector
399     [Fintype κ] [Fintype ρ] [CommSemiring R]
400     (U : ι → ρ → R) (V : κ → ρ → R) :
401     lowRankApply U V (0 : κ → R) = 0 := by
402   funext i
403   simp [lowRankApply]
404 
405 end Operator
406 
407 /-! ## Relation-supported matrix algebra -/
408 
409 namespace Algebra
410 
411 universe u v
412 
413 
414 def MatrixSupported {ι : Type u} {A : Type v} [Zero A]
415     (rel : ι → ι → Prop) (M : Matrix ι ι A) : Prop :=
416   ∀ i j, ¬ rel i j → M i j = 0
417 
418 
419 theorem matrixSupported_zero
420     {ι : Type u} {A : Type v} [Zero A]
421     (rel : ι → ι → Prop) :
422     MatrixSupported rel (0 : Matrix ι ι A) := by
423   intro i j h
424   rfl
425 
426 
427 theorem MatrixSupported.add
428     {ι : Type u} {A : Type v} [AddMonoid A]
429     {rel : ι → ι → Prop} {M N : Matrix ι ι A}
430     (hM : MatrixSupported rel M) (hN : MatrixSupported rel N) :
431     MatrixSupported rel (M + N) := by
432   intro i j h
433   simp [hM i j h, hN i j h]
434 
435 
436 theorem MatrixSupported.neg
437     {ι : Type u} {A : Type v} [AddGroup A]
438     {rel : ι → ι → Prop} {M : Matrix ι ι A}
439     (hM : MatrixSupported rel M) :
440     MatrixSupported rel (-M) := by
441   intro i j h
442   simp [hM i j h]
443 
444 
445 theorem MatrixSupported.mul
446     {ι : Type u} {A : Type v}
447     [Fintype ι] [DecidableEq ι] [Semiring A]
448     {rel : ι → ι → Prop}
449     (htrans : ∀ i j k, rel i j → rel j k → rel i k)
450     {M N : Matrix ι ι A}
451     (hM : MatrixSupported rel M) (hN : MatrixSupported rel N) :
452     MatrixSupported rel (M * N) := by
453   intro i j hij
454   rw [Matrix.mul_apply]
455   apply Finset.sum_eq_zero
456   intro k hk
457   by_cases hik : rel i k
458   · by_cases hkj : rel k j
459     · exact (hij (htrans i k j hik hkj)).elim
460     · simp [hN k j hkj]
461   · simp [hM i k hik]
462 
463 
464 def IsLowerTriangular {ι : Type u} {A : Type v}
465     [Preorder ι] [Zero A] (M : Matrix ι ι A) : Prop :=
466   ∀ i j, i < j → M i j = 0
467 
468 
469 def IsUpperTriangular {ι : Type u} {A : Type v}
470     [Preorder ι] [Zero A] (M : Matrix ι ι A) : Prop :=
471   ∀ i j, j < i → M i j = 0
472 
473 
474 theorem IsLowerTriangular.add
475     {ι : Type u} {A : Type v} [Preorder ι] [AddMonoid A]
476     {M N : Matrix ι ι A}
477     (hM : IsLowerTriangular M) (hN : IsLowerTriangular N) :
478     IsLowerTriangular (M + N) := by
479   intro i j hij
480   simp [hM i j hij, hN i j hij]
481 
482 
483 theorem IsUpperTriangular.add
484     {ι : Type u} {A : Type v} [Preorder ι] [AddMonoid A]
485     {M N : Matrix ι ι A}
486     (hM : IsUpperTriangular M) (hN : IsUpperTriangular N) :
487     IsUpperTriangular (M + N) := by
488   intro i j hij
489   simp [hM i j hij, hN i j hij]
490 
491 end Algebra
492 
493 /-! ## Finite-difference and weighted-shift calculus -/
494 
495 namespace FiniteDifference
496 
497 universe u
498 
499 variable {R : Type u}
500 
501 
502 def forwardDiff [Ring R] (f : ℕ → R) (n : ℕ) : R :=
503   f (n + 1) - f n
504 
505 
506 def iteratedDiff [Ring R] : ℕ → (ℕ → R) → (ℕ → R)
507   | 0, f => f
508   | k + 1, f => forwardDiff (iteratedDiff k f)
509 
510 
511 theorem forwardDiff_add [CommRing R]
512     (f g : ℕ → R) (n : ℕ) :
513     forwardDiff (fun j => f j + g j) n = forwardDiff f n + forwardDiff g n := by
514   simp [forwardDiff]
515   ring
516 
517 
518 theorem forwardDiff_neg [CommRing R]
519     (f : ℕ → R) (n : ℕ) :
520     forwardDiff (fun j => -f j) n = -forwardDiff f n := by
521   simp [forwardDiff]
522   ring
523 
524 
525 theorem iteratedDiff_two [CommRing R]
526     (f : ℕ → R) (n : ℕ) :
527     iteratedDiff 2 f n = f (n + 2) - 2 * f (n + 1) + f n := by
528   simp [iteratedDiff, forwardDiff]
529   ring
530 
531 
532 theorem iteratedDiff_three [CommRing R]
533     (f : ℕ → R) (n : ℕ) :
534     iteratedDiff 3 f n =
535       f (n + 3) - 3 * f (n + 2) + 3 * f (n + 1) - f n := by
536   simp [iteratedDiff, forwardDiff]
537   ring
538 
539 
540 def weightedDiff [Ring R] (q : R) (f : ℕ → R) (n : ℕ) : R :=
541   f n - q * f (n + 1)
542 
543 
544 def iteratedWeightedDiff [Ring R] (q : R) : ℕ → (ℕ → R) → (ℕ → R)
545   | 0, f => f
546   | k + 1, f => weightedDiff q (iteratedWeightedDiff q k f)
547 
548 
549 theorem iteratedWeightedDiff_geometric [CommRing R]
550     (q r : R) (k n : ℕ) :
551     iteratedWeightedDiff q k (fun j => r ^ j) n =
552       (1 - q * r) ^ k * r ^ n := by
553   induction k generalizing n with
554   | zero => simp [iteratedWeightedDiff]
555   | succ k ih =>
556       simp [iteratedWeightedDiff, weightedDiff, ih, pow_succ]
557       ring
558 
559 end FiniteDifference
560 
561 /-! ## Polyphase coefficient sections -/
562 
563 namespace Polyphase
564 
565 universe u
566 
567 variable {A : Type u}
568 
569 
570 def coeffSection (m r : ℕ) (f : ℕ → A) (n : ℕ) : A :=
571   f (m * n + r)
572 
573 @[simp] theorem coeffSection_one_zero (f : ℕ → A) :
574     coeffSection 1 0 f = f := by
575   funext n
576   simp [coeffSection]
577 
578 
579 theorem coeffSection_comp
580     (l s m r : ℕ) (f : ℕ → A) (n : ℕ) :
581     coeffSection m r (coeffSection l s f) n =
582       coeffSection (l * m) (l * r + s) f n := by
583   simp [coeffSection, Nat.mul_add, Nat.mul_assoc, Nat.add_assoc]
584 
585 end Polyphase
586 
587 /-! ## Finite diagonal quantum coordinates -/
588 
589 namespace Quantum
590 
591 universe u
592 
593 
594 def diagonalApply {ι : Type u} {R : Type*} [Mul R]
595     (diagonal : ι → R) (x : ι → R) : ι → R :=
596   fun i => diagonal i * x i
597 
598 @[simp] theorem diagonalApply_one
599     {ι : Type u} {R : Type*} [Monoid R] (x : ι → R) :
600     diagonalApply (fun _ => 1) x = x := by
601   funext i
602   simp [diagonalApply]
603 
604 noncomputable def logPhase {ι : Type u}
605     (energy : ι → ℝ) (t : ℝ) : ι → ℂ :=
606   fun i => Complex.exp (-Complex.I * ((energy i * t : ℝ) : ℂ))
607 
608 @[simp] theorem logPhase_zero {ι : Type u} (energy : ι → ℝ) :
609     logPhase energy 0 = fun _ => 1 := by
610   funext i
611   simp [logPhase]
612 
613 noncomputable def finiteAmplitude {ι : Type u} [Fintype ι]
614     (weight sign : ι → ℂ) (energy : ι → ℝ) (t : ℝ) : ℂ :=
615   ∑ i, weight i * sign i * logPhase energy t i
616 
617 @[simp] theorem finiteAmplitude_zero {ι : Type u} [Fintype ι]
618     (weight sign : ι → ℂ) (energy : ι → ℝ) :
619     finiteAmplitude weight sign energy 0 = ∑ i, weight i * sign i := by
620   simp [finiteAmplitude, logPhase]
621 
622 end Quantum
623 
624 end Komorebi
625 
626 /-! ## Browser smoke checks -/
627 
628 #check Komorebi.Foundation.LinearProjectorFamily.synthesize_analyze
629 #check Komorebi.Foundation.transferBlock_reconstruction
630 #check Komorebi.Foundation.transferBlock_comp
631 #check Komorebi.Packet.fibreProj_reconstruction
632 #check Komorebi.Algebra.MatrixSupported.mul
633 #check Komorebi.FiniteDifference.iteratedWeightedDiff_geometric
634 #check Komorebi.Polyphase.coeffSection_comp
635 #check Komorebi.Quantum.finiteAmplitude_zero
636 
637 #eval "Komorebi Projector Calculus browser-safe core loaded"

Back to source controls