CommonRefinementConsumers.lean

1 import KomorebiVerification.PaperII.FiniteCommonRefinement
2 
3 /-! Exact manuscript consumers and closed mathematical controls. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace Komorebi.PaperII.CommonRefinement
7 open Komorebi.Foundation Komorebi.PaperII.NestedRefinement
8 universe u v w x y z
9 variable {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M]
10 variable {ι : Type w} {κ : Type x} {τ : Type y}
11 variable [Fintype ι] [Fintype κ] [Fintype τ]
12 
13 /-- The exact binary supported-product conclusion, with onto parent maps. -/
14 theorem manuscript_common_refinement
15     (P : LinearProjectorFamily R M ι) (Q : LinearProjectorFamily R M κ)
16     (h : CrossCommutes P Q) (hp : Nonzero P) (hq : Nonzero Q) :
17     Nonzero (common P Q h) ∧
18     Refines P (common P Q h) (fun k => k.val.1) ∧
19     Refines Q (common P Q h) (fun k => k.val.2) :=
20   ⟨supported_nonzero _, common_refines_left P Q h hp, common_refines_right P Q h hq⟩
21 
22 /-- The coarsest theorem supplies an actual, unique parent map. -/
23 theorem manuscript_coarsest_unique
24     (P : LinearProjectorFamily R M ι) (Q : LinearProjectorFamily R M κ)
25     (h : CrossCommutes P Q) (S : LinearProjectorFamily R M τ) (hs : Nonzero S)
26     (p : τ → ι) (q : τ → κ) (hp : Refines P S p) (hq : Refines Q S q) :
27     ∃! parent : τ → Support (product P Q h), Refines (common P Q h) S parent := by
28   refine ⟨jointParent P Q h S hs p q hp hq, common_coarsest P Q h S hs p q hp hq, ?_⟩
29   intro parent hparent
30   exact parent_unique _ S hs _ _ hparent (common_coarsest P Q h S hs p q hp hq)
31 
32 /-- A finite collection, including an empty collection, under only pairwise commutation. -/
33 theorem manuscript_finite_common {T : Type z} [Fintype T]
34     (F : T → Packet.{u,v,w} R M)
35     (hc : ∀ s t, s ≠ t → CrossCommutes (F s).family (F t).family) :
36     ∃ S : Packet.{u,v,w} R M,
37       (∀ t, HasRefinement (F t) S) ∧
38       (∀ U : Packet.{u,v,w} R M,
39         (∀ t, HasRefinement (F t) U) → HasRefinement S U) :=
40   finite_common_coarsest F hc
41 
42 /-- The zero-module edge case does not introduce an illegal zero member. -/
43 theorem supported_index_empty_on_zero_module [Subsingleton M]
44     (P : LinearProjectorFamily R M ι) : IsEmpty (Support P) := by
45   refine ⟨?_⟩
46   intro i
47   exact i.property (by ext a; exact Subsingleton.elim _ _)
48 
49 section ConcreteControl
50 
51 def p0 : Matrix (Fin 2) (Fin 2) Int := !![1,0;0,0]
52 def p1 : Matrix (Fin 2) (Fin 2) Int := !![0,0;0,1]
53 def q0 : Matrix (Fin 2) (Fin 2) Int := !![1,1;0,0]
54 def q1 : Matrix (Fin 2) (Fin 2) Int := !![0,-1;0,1]
55 
56 theorem first_matrix_packet :
57     p0 * p0 = p0 ∧ p1 * p1 = p1 ∧ p0 * p1 = 0 ∧ p1 * p0 = 0 ∧ p0 + p1 = 1 := by
58   decide
59 
60 theorem second_matrix_packet :
61     q0 * q0 = q0 ∧ q1 * q1 = q1 ∧ q0 * q1 = 0 ∧ q1 * q0 = 0 ∧ q0 + q1 = 1 := by
62   decide
63 
64 theorem noncommuting_product_nonzero : p0 * q1 ≠ 0 := by decide
65 
66 theorem noncommuting_product_square_zero : (p0 * q1) * (p0 * q1) = 0 := by decide
67 
68 theorem noncommuting_product_not_idempotent : (p0 * q1) * (p0 * q1) ≠ p0 * q1 := by decide
69 
70 end ConcreteControl
71 end Komorebi.PaperII.CommonRefinement

Back to source controls