Komorebi_Projector_Calculus_Lean_Browser_Core_v1.2.2.lean

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

Back to source controls