ProjectorCore.lean

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

Back to source controls