PacketSourceRank.lean

1 import PaperIRelease.PacketSourceLower
2 import PaperIRelease.PacketSourceUpper
3 import PaperIRelease.GraphSourceProjection
4 
5 set_option autoImplicit false
6 noncomputable section
7 
8 namespace Komorebi.PaperIRelease
9 
10 open Cardinal Set Komorebi.Foundation Komorebi.SeedRankBasics
11 open Komorebi.PacketNaturalityCompletion.Reachability
12 open PacketAggregation FiniteDigraph
13 
14 universe u
15 variable {𝕜 X I : Type u} [Field 𝕜] [AddCommGroup X] [Module 𝕜 X]
16 variable [Fintype I] [DecidableEq I]
17 
18 /-- The exact cardinal formula for packet-pure seed rank. The components are
19 the actual quotient by mutual reachability of the actual generator transfer
20 graph. Their source property, existence, no-incoming action, and propagation
21 are proved by the imported graph theorems. Local ranks are genuine minima
22 under the actual compressed corner algebras. -/
23 theorem source_component_pureSeedRank
24     (P : LinearProjectorFamily 𝕜 X I) (ops : Set (Module.End 𝕜 X))
25     (hedges : EdgeSurjective P ops) :
26     packetPureSeedRank (packetGeneratedAlgebra P ops) P =
27       Cardinal.sum (fun C : Sources (TransferEdge P ops) ↦
28         localPureSeedRank (packetGeneratedAlgebra P ops) P
29           (projector_mem_generatedAlgebra P ops)
30           (component (TransferEdge P ops)) C.val) := by
31   apply le_antisymm
32   · apply packetPureSeedRank_le_sum_local_of_generation
33       (packetGeneratedAlgebra P ops) P (projector_mem_generatedAlgebra P ops)
34       (component (TransferEdge P ops)) {C | Source (TransferEdge P ops) C}
35     intro H hsource
36     have hH : AlgebraInvariant (packetGeneratedAlgebra P ops) (H.restrictScalars 𝕜) := by
37       intro T hT x hx
38       exact H.smul_mem (⟨T, hT⟩ : packetGeneratedAlgebra P ops) hx
39     have htop : H.restrictScalars 𝕜 = ⊤ :=
40       submodule_eq_top_of_sources P ops hedges (H.restrictScalars 𝕜) hH (by
41         intro C a ha x hx
42         apply hsource C.val C.property
43         have h := original_mem_grouped P (component (TransferEdge P ops)) a ⟨x, hx⟩
44         simpa only [ha] using h)
45     apply top_unique
46     intro x _
47     change x ∈ H.restrictScalars 𝕜
48     rw [htop]
49     trivial
50   · apply sum_localPureSeedRank_le_of_compression
51       (packetGeneratedAlgebra P ops) P (projector_mem_generatedAlgebra P ops)
52       (component (TransferEdge P ops)) {C | Source (TransferEdge P ops) C}
53     intro C hC a ha x
54     exact sourceProjection_compression P ops ⟨C, hC⟩ ha x
55 
56 end Komorebi.PaperIRelease
57 
58 #print axioms Komorebi.PaperIRelease.source_component_pureSeedRank

Back to source controls