BrowserCoreLocal.lean

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

Back to source controls