RequiredPacketBoundary.lean

1 import PaperX.OccupancyExamples
2 
3 /-! The required-packet quantifier cannot be replaced by occupancy of one
4 packet or by a fixed finite sample. These are actual one-dimensional packets
5 over ℚ, with a split identity operator and its polynomial spectral projector.
6 For each omitted index N a different family is constructed. This does not
7 claim that one family can satisfy every finite prefix and fail globally. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperX.RequiredPacketBoundary
11 
12 open PaperX.SpectralProjectors PaperX.JointOccupancy PaperX.OccupancyExamples
13 
14 /-- Every packet has the same actual one-dimensional carrier and operator. -/
15 def operator (_ : Unit) : Module.End ℚ (Fin 1 → ℚ) :=
16   diagOp (fun _ => 1)
17 
18 /-- Exactly the N-th packet asks for the absent zero eigenvalue. -/
19 def target (N n : ℕ) (_ : Unit) : ℚ := if n = N then 0 else 1
20 
21 theorem operator_split (i : Unit) : Split (operator i) :=
22   diag_split _
23 
24 theorem operators_commute (i j : Unit) : Commute (operator i) (operator j) :=
25   diag_commute _ _
26 
27 /-- The projector is computed from the spectral polynomial, not assigned. -/
28 theorem projector (N n : ℕ) :
29     joint operator (target N n) [()] =
30       diagOp (fun _ : Fin 1 => if n = N then (0 : ℚ) else 1) := by
31   simp only [joint_cons, joint_nil, mul_one, operator, spectral_diag]
32   congr 1
33   funext j
34   by_cases h : n = N <;> simp [target, h]
35 
36 theorem projector_trace (N n : ℕ) :
37     LinearMap.trace ℚ (Fin 1 → ℚ) (joint operator (target N n) [()]) =
38       if n = N then 0 else 1 := by
39   rw [projector, trace_diag]
40   simp
41 
42 theorem occupied_iff (N n : ℕ) :
43     Occupied operator (target N n) [()] ↔ n ≠ N := by
44   rw [occupied_iff_trace_ne_zero operator (target N n) operator_split
45     operators_commute, projector_trace]
46   by_cases h : n = N <;> simp [h]
47 
48 theorem omitted_packet_empty (N : ℕ) :
49     ¬ Occupied operator (target N N) [()] := by
50   simp [occupied_iff]
51 
52 theorem prefix_occupied (N n : ℕ) (hn : n < N) :
53     Occupied operator (target N n) [()] :=
54   (occupied_iff N n).mpr (Nat.ne_of_lt hn)
55 
56 theorem no_family_fully_occupied (N : ℕ) :
57     ¬ ∀ n, Occupied operator (target N n) [()] := by
58   intro h
59   exact omitted_packet_empty N (h N)
60 
61 /-- One occupied required packet does not imply occupancy of every packet. -/
62 theorem some_but_not_all :
63     (∃ n, Occupied operator (target 1 n) [()]) ∧
64       ¬ ∀ n, Occupied operator (target 1 n) [()] := by
65   exact ⟨⟨0, prefix_occupied 1 0 (by decide)⟩, no_family_fully_occupied 1⟩
66 
67 /-- For every prefix length there is a family passing it and failing next. -/
68 theorem finite_prefix_misses_failure (N : ℕ) :
69     (∀ n < N, Occupied operator (target N n) [()]) ∧
70       ¬ Occupied operator (target N N) [()] :=
71   ⟨prefix_occupied N, omitted_packet_empty N⟩
72 
73 /-- An arbitrary predetermined finite sample can miss an empty packet. -/
74 theorem finite_sample_misses_failure (s : Finset ℕ) :
75     ∃ N, (∀ n ∈ s, Occupied operator (target N n) [()]) ∧
76       ¬ Occupied operator (target N N) [()] := by
77   refine ⟨s.sup id + 1, ?_, omitted_packet_empty _⟩
78   intro n hn
79   apply prefix_occupied
80   exact Nat.lt_succ_of_le (Finset.le_sup (f := id) hn)
81 
82 end PaperX.RequiredPacketBoundary

Back to source controls