PositivePacketExamples.lean

1 import MachineTheory.CoordinatePackets
2 import MachineTheory.PacketTransport
3 import Mathlib.Tactic.NormNum
4 import Mathlib.Tactic.Ring
5 
6 /-!
7 # Exact packet examples and hypothesis boundaries
8 
9 The examples are actual linear maps over the reals. They distinguish a signed
10 Haar detail from a valid state in a transported cone, strict from non-strict mass,
11 complete positive maps from idempotent ones, and empty coordinate edge cases.
12 -/
13 namespace Komorebi.MachineTheory.PositivePackets.Examples
14 
15 noncomputable section
16 
17 open scoped BigOperators
18 
19 abbrev V2 := ℝ × ℝ
20 
21 def first : V2 →ₗ[ℝ] ℝ := LinearMap.fst ℝ ℝ ℝ
22 def second : V2 →ₗ[ℝ] ℝ := LinearMap.snd ℝ ℝ ℝ
23 def mass2 : V2 →ₗ[ℝ] ℝ := first + second
24 
25 def quadrant : ConvexCone ℝ V2 where
26   carrier := {v | 0 ≤ v.1 ∧ 0 ≤ v.2}
27   smul_mem' := by
28     intro c hc v hv
29     exact ⟨mul_nonneg (le_of_lt hc) hv.1, mul_nonneg (le_of_lt hc) hv.2⟩
30   add_mem' := by
31     intro v hv w hw
32     exact ⟨add_nonneg hv.1 hw.1, add_nonneg hv.2 hw.2⟩
33 
34 def leftPacket : V2 →ₗ[ℝ] V2 := first.prod 0
35 def rightPacket : V2 →ₗ[ℝ] V2 := (0 : V2 →ₗ[ℝ] ℝ).prod second
36 
37 def coordinateFamily (b : Bool) : V2 →ₗ[ℝ] V2 := if b then rightPacket else leftPacket
38 
39 theorem strict_mass2 : StrictMass quadrant mass2 := by
40   intro v hv hn
41   change 0 < v.1 + v.2
42   have h0 : v.1 ≠ 0 ∨ v.2 ≠ 0 := by
43     by_contra h
44     push Not at h
45     apply hn
46     exact Prod.ext h.1 h.2
47   change 0 ≤ v.1 ∧ 0 ≤ v.2 at hv
48   rcases h0 with h | h
49   · have hp : 0 < v.1 := lt_of_le_of_ne hv.1 (Ne.symm h)
50     linarith
51   · have hp : 0 < v.2 := lt_of_le_of_ne hv.2 (Ne.symm h)
52     linarith
53 
54 theorem coordinate_family_preserves (b : Bool) : Preserves quadrant (coordinateFamily b) := by
55   intro v hv
56   cases b with
57   | false => simpa [coordinateFamily, leftPacket, first, quadrant] using hv.1
58   | true => simpa [coordinateFamily, rightPacket, second, quadrant] using hv.2
59 
60 theorem coordinate_family_complete : Complete coordinateFamily := by
61   apply LinearMap.ext
62   intro v
63   ext <;> simp [coordinateFamily, leftPacket, rightPacket, first, second]
64 
65 theorem coordinate_family_idempotent (b : Bool) :
66     (coordinateFamily b).comp (coordinateFamily b) = coordinateFamily b := by
67   apply LinearMap.ext
68   intro v
69   cases b <;> ext <;> simp [coordinateFamily, leftPacket, rightPacket, first, second]
70 
71 theorem zero_weight_is_present :
72     IsState quadrant mass2 (1, 0) ∧ weight mass2 coordinateFamily (1, 0) true = 0 ∧
73     coordinateFamily true (1, 0) = 0 := by
74   norm_num [IsState, quadrant, weight, mass2, coordinateFamily, leftPacket, rightPacket, first, second]
75 
76 /-- The actual nonzero-index construction applies to a zero-weight boundary input. -/
77 theorem boundary_mixture :
78     (∑ i : PositiveIndex mass2 coordinateFamily (1, 0),
79       weight mass2 coordinateFamily (1, 0) i.val • normalized mass2 coordinateFamily (1, 0) i) =
80       ((1, 0) : V2) :=
81   mixture_reconstruction quadrant mass2 strict_mass2 coordinateFamily coordinate_family_preserves
82     coordinate_family_complete (by norm_num [quadrant])
83 
84 def average : V2 →ₗ[ℝ] V2 := ((1 / 2 : ℝ) • mass2).prod ((1 / 2 : ℝ) • mass2)
85 def detail : V2 →ₗ[ℝ] V2 := LinearMap.id - average
86 def haarFamily (b : Bool) : V2 →ₗ[ℝ] V2 := if b then detail else average
87 
88 theorem haar_complete : Complete haarFamily := by
89   apply LinearMap.ext
90   intro v
91   ext <;> simp [haarFamily, detail]
92 
93 theorem haar_idempotent (b : Bool) : (haarFamily b).comp (haarFamily b) = haarFamily b := by
94   apply LinearMap.ext
95   intro v
96   cases b <;> ext <;>
97     simp [haarFamily, detail, average, mass2, first, second] <;> ring
98 
99 /-- The two ranges are orthogonal for the ordinary real coordinate inner product. -/
100 theorem haar_orthogonal (v w : V2) :
101     (average v).1 * (detail w).1 + (average v).2 * (detail w).2 = 0 := by
102   simp [average, detail, mass2, first, second]
103   ring
104 
105 theorem haar_detail_packet : detail (3 / 4, 1 / 4) = ((1 / 4, -(1 / 4)) : V2) := by
106   ext <;> norm_num [detail, average, mass2, first, second]
107 
108 theorem haar_detail_zero_mass_nonzero :
109     mass2 (detail (3 / 4, 1 / 4)) = 0 ∧ detail (3 / 4, 1 / 4) ≠ 0 := by
110   rw [haar_detail_packet]
111   norm_num [mass2, first, second]
112 
113 theorem haar_detail_not_preserving : ¬ Preserves quadrant detail := by
114   intro h
115   have hv := h (1, 0) (by norm_num [quadrant])
116   norm_num [quadrant, detail, average, mass2, first, second] at hv
117 
118 /-- A nonnegative but non-strict functional misses a nonzero cone member. -/
119 theorem nonstrict_mass_counterexample :
120     (∀ v ∈ quadrant, 0 ≤ first v) ∧ ((0, 1) : V2) ∈ quadrant ∧
121     first (0, 1) = 0 ∧ ((0, 1) : V2) ≠ 0 ∧ ¬ StrictMass quadrant first := by
122   refine ⟨fun _ hv => hv.1, by norm_num [quadrant], rfl, by norm_num, ?_⟩
123   intro h
124   have hp := h (0, 1) (by norm_num [quadrant]) (by norm_num)
125   norm_num [first] at hp
126 
127 def halfIdentity : V2 →ₗ[ℝ] V2 := (1 / 2 : ℝ) • LinearMap.id
128 
129 theorem half_identity_preserves : Preserves quadrant halfIdentity := by
130   intro v hv
131   change 0 ≤ (1 / 2 : ℝ) * v.1 ∧ 0 ≤ (1 / 2 : ℝ) * v.2
132   exact ⟨mul_nonneg (by norm_num) hv.1, mul_nonneg (by norm_num) hv.2⟩
133 
134 theorem two_halves_complete : Complete (fun _ : Bool => halfIdentity) := by
135   apply LinearMap.ext
136   intro v
137   ext <;> simp [halfIdentity]
138 
139 theorem half_identity_not_idempotent : halfIdentity.comp halfIdentity ≠ halfIdentity := by
140   intro h
141   have hh := congrArg Prod.fst (LinearMap.congr_fun h (1, 0))
142   norm_num [halfIdentity] at hh
143 
144 theorem incomplete_weight_counterexample :
145     weight mass2 (fun _ : Unit => halfIdentity) (1, 0) () = (1 / 2 : ℝ) := by
146   norm_num [weight, mass2, halfIdentity, first, second]
147 
148 def signedFamily (b : Bool) : V2 →ₗ[ℝ] V2 :=
149   if b then (2 : ℝ) • LinearMap.id else -(LinearMap.id : V2 →ₗ[ℝ] V2)
150 
151 theorem signed_family_complete : Complete signedFamily := by
152   apply LinearMap.ext
153   intro v
154   ext <;> simp [signedFamily] <;> ring
155 
156 theorem signed_weight_negative : weight mass2 signedFamily (1, 0) false = -1 := by
157   norm_num [weight, signedFamily, mass2, first, second]
158 
159 /-- A genuinely invertible coordinate map that creates signed coordinates. -/
160 def shear : V2 ≃ₗ[ℝ] V2 where
161   toFun v := (v.1 - v.2, v.2)
162   invFun w := (w.1 + w.2, w.2)
163   left_inv := by intro v; ext <;> simp
164   right_inv := by intro v; ext <;> simp
165   map_add' := by
166     intro v w
167     apply Prod.ext
168     · change (v.1 + w.1) - (v.2 + w.2) = (v.1 - v.2) + (w.1 - w.2)
169       ring
170     · rfl
171   map_smul' := by
172     intro c v
173     apply Prod.ext
174     · change c * v.1 - c * v.2 = c * (v.1 - v.2)
175       ring
176     · rfl
177 
178 theorem transported_signed_state :
179     IsState (Transport.cone shear quadrant) (Transport.mass shear mass2) (-1, 1) := by
180   have h := (Transport.state_iff shear quadrant mass2 (0, 1)).mpr
181     (by norm_num [IsState, quadrant, mass2, first, second])
182   have hs : shear ((0, 1) : V2) = ((-1, 1) : V2) := by ext <;> norm_num [shear]
183   rw [hs] at h
184   exact h
185 
186 theorem transported_mass_strict :
187     StrictMass (Transport.cone shear quadrant) (Transport.mass shear mass2) :=
188   Transport.strictMass shear quadrant mass2 strict_mass2
189 
190 theorem signed_state_not_in_original_cone : ((-1, 1) : V2) ∉ quadrant := by
191   norm_num [quadrant]
192 
193 theorem transported_family_preserves (b : Bool) :
194     Preserves (Transport.cone shear quadrant) (Transport.operator shear (coordinateFamily b)) :=
195   Transport.preserves shear quadrant (coordinateFamily b) (coordinate_family_preserves b)
196 
197 /-- The transported second projector has a negative coordinate, with positive valid mass. -/
198 theorem transported_packet_explicit :
199     Transport.operator shear rightPacket (0, 1 / 2) = ((-(1 / 2), 1 / 2) : V2) ∧
200     Transport.mass shear mass2 (-(1 / 2), 1 / 2) = (1 / 2 : ℝ) := by
201   norm_num [Transport.operator, Transport.mass, shear, rightPacket, second, mass2, first]
202 
203 /-- Empty coordinate and index sets are allowed by the selector construction. -/
204 theorem empty_coordinate_family :
205     Complete (Coordinate.selector (fun x : Fin 0 => x)) := Coordinate.selector_complete _
206 
207 /-- Completeness on an empty index family cannot support a unit-mass input. -/
208 theorem no_state_for_empty_family {V : Type*} [AddCommGroup V] [Module ℝ V]
209     (C : ConvexCone ℝ V) (m : V →ₗ[ℝ] ℝ) (P : Fin 0 → V →ₗ[ℝ] V)
210     (hc : Complete P) (v : V) : ¬ IsState C m v := by
211   intro hv
212   have h := sum_weights_one C m P hc hv
213   simp at h
214 
215 end
216 end Komorebi.MachineTheory.PositivePackets.Examples

Back to source controls