OccupancyBinary.lean

1 import MachineTheory.PartitionOccupancy
2 import Mathlib.Data.Fintype.BigOperators
3 
4 /-!
5 # Exact fixed-width binary occupancy memory
6 
7 The state is a Boolean vector indexed by exactly the attained cell-target pairs.
8 Readout projects occupied pairs to targets. Evidence update masks cell coordinates.
9 The lower bound is for exact deterministic memory on all candidate subsets, with
10 fixed-width binary states. No variable-length, average-bit or runtime bound is claimed.
11 -/
12 
13 namespace Komorebi.MachineTheory.PartitionCorrection
14 
15 variable {Ω I Y : Type*} [Fintype Ω]
16 
17 /-- Characteristic vectors of occupancy subsets, using one bit per attained pair. -/
18 noncomputable def bitsEquiv (c : Ω → I) (t : Ω → Y) :
19     Set (Pair c t) ≃ (Fin (Fintype.card (Pair c t)) → Bool) := by
20   classical
21   let e := Fintype.equivFin (Pair c t)
22   refine
23     { toFun := fun S i => decide (e.symm i ∈ S)
24       invFun := fun b => {d | b (e d) = true}
25       left_inv := ?_
26       right_inv := ?_ }
27   · intro S
28     ext d
29     simp only [Set.mem_ofPred_eq, Equiv.symm_apply_apply, decide_eq_true_eq]
30   · intro b
31     funext i
32     simp only [Set.mem_ofPred_eq, Equiv.apply_symm_apply]
33     cases b i <;> rfl
34 
35 /-- The attained signature state is equivalent to the complete r-bit state space. -/
36 noncomputable def binaryMemoryEquiv (c : Ω → I) (t : Ω → Y) :
37     (algebra c).Memory t ≃ (Fin (Fintype.card (Pair c t)) → Bool) :=
38   (memoryEquiv c t).trans (bitsEquiv c t)
39 
40 noncomputable def encode (c : Ω → I) (t : Ω → Y) (V : Set Ω) :
41     Fin (Fintype.card (Pair c t)) → Bool := bitsEquiv c t (occupancy c t V)
42 
43 noncomputable def readBits (c : Ω → I) (t : Ω → Y)
44     (b : Fin (Fintype.card (Pair c t)) → Bool) : Set Y :=
45   readOccupancy c t ((bitsEquiv c t).symm b)
46 
47 noncomputable def updateBits (c : Ω → I) (t : Ω → Y)
48     (e : (algebra c).Event) (b : Fin (Fintype.card (Pair c t)) → Bool) :
49     Fin (Fintype.card (Pair c t)) → Bool :=
50   bitsEquiv c t (restrictOccupancy c t (eventCells c e) ((bitsEquiv c t).symm b))
51 
52 @[simp] theorem encode_read (c : Ω → I) (t : Ω → Y) (V : Set Ω) :
53     readBits c t (encode c t V) = t '' V := by
54   unfold readBits encode
55   rw [Equiv.symm_apply_apply, readOccupancy_occupancy]
56 
57 @[simp] theorem encode_update (c : Ω → I) (t : Ω → Y)
58     (e : (algebra c).Event) (V : Set Ω) :
59     updateBits c t e (encode c t V) = encode c t ((algebra c).filter e V) := by
60   unfold updateBits encode
61   rw [Equiv.symm_apply_apply, occupancy_filter]
62 
63 theorem encode_surjective (c : Ω → I) (t : Ω → Y) :
64     Function.Surjective (encode c t) := by
65   intro b
66   refine ⟨realize c t ((bitsEquiv c t).symm b), ?_⟩
67   unfold encode
68   rw [occupancy_realize, Equiv.apply_symm_apply]
69 
70 theorem bits_finite_continuation (c : Ω → I) (t : Ω → Y)
71     (events : List (algebra c).Event) (V : Set Ω) :
72     run (updateBits c t) events (encode c t V) =
73       encode c t (run (algebra c).filter events V) := by
74   induction events generalizing V with
75   | nil => rfl
76   | cons e es ih =>
77     simp only [run_cons, encode_update]
78     exact ih _
79 
80 theorem bits_readout_continuation (c : Ω → I) (t : Ω → Y)
81     (events : List (algebra c).Event) (V : Set Ω) :
82     readBits c t (run (updateBits c t) events (encode c t V)) =
83       t '' (run (algebra c).filter events V) := by
84   rw [bits_finite_continuation, encode_read]
85 
86 omit [Fintype Ω] in
87 /-- An exact b-bit memory cannot merge distinct occupancy subsets. -/
88 theorem exact_bits_occupancy_injective (c : Ω → I) (t : Ω → Y) (b : ℕ)
89     (r : Set Ω → (Fin b → Bool)) (readout : (Fin b → Bool) → Set Y)
90     (step : (algebra c).Event → (Fin b → Bool) → (Fin b → Bool))
91     (hq : ∀ V, readout (r V) = t '' V)
92     (hs : ∀ e V, step e (r V) = r ((algebra c).filter e V)) :
93     Function.Injective (fun S : Set (Pair c t) => r (realize c t S)) := by
94   intro S T h
95   have hsig := (algebra c).any_exact_memory_separates t r readout step hq hs _ _ h
96   have hocc := (signature_eq_iff_occupancy_eq c t _ _).mp hsig
97   simpa only [occupancy_realize] using hocc
98 
99 /-- Counting all initialized occupancies gives the exact fixed-width bit bound. -/
100 theorem fixed_bits_necessary (c : Ω → I) (t : Ω → Y) (b : ℕ)
101     (r : Set Ω → (Fin b → Bool)) (readout : (Fin b → Bool) → Set Y)
102     (step : (algebra c).Event → (Fin b → Bool) → (Fin b → Bool))
103     (hq : ∀ V, readout (r V) = t '' V)
104     (hs : ∀ e V, step e (r V) = r ((algebra c).filter e V)) :
105     Fintype.card (Pair c t) ≤ b := by
106   classical
107   have hcard := Fintype.card_le_of_injective _
108     (exact_bits_occupancy_injective c t b r readout step hq hs)
109   have hpow : 2 ^ Fintype.card (Pair c t) ≤ 2 ^ b := by
110     simpa only [Fintype.card_set, Fintype.card_fun, Fintype.card_bool,
111       Fintype.card_fin] using hcard
112   by_contra h
113   have hb : b < Fintype.card (Pair c t) := Nat.lt_of_not_ge h
114   exact (not_lt_of_ge hpow) (Nat.pow_lt_pow_right (by decide : 1 < 2) hb)
115 
116 /-- The raw source partition contract: nonempty cells, exact union evidence,
117 arbitrary target, all candidate subsets, exact count and an optimal binary memory. -/
118 theorem partition_correction_memory (c : Ω → I) (t : Ω → Y)
119     (_hc : Function.Surjective c) :
120     (Fintype.card ((algebra c).Memory t) = 2 ^ Fintype.card (Pair c t)) ∧
121     (∀ V W, (algebra c).signature t V = (algebra c).signature t W ↔
122       occupancy c t V = occupancy c t W) ∧
123     (∀ V, readBits c t (encode c t V) = t '' V) ∧
124     (∀ e V, updateBits c t e (encode c t V) = encode c t ((algebra c).filter e V)) ∧
125     (∀ b (r : Set Ω → (Fin b → Bool)) (readout : (Fin b → Bool) → Set Y)
126       (step : (algebra c).Event → (Fin b → Bool) → (Fin b → Bool)),
127       (∀ V, readout (r V) = t '' V) →
128       (∀ e V, step e (r V) = r ((algebra c).filter e V)) →
129       Fintype.card (Pair c t) ≤ b) := by
130   exact ⟨card_memory c t, signature_eq_iff_occupancy_eq c t,
131     encode_read c t, encode_update c t, fixed_bits_necessary c t⟩
132 
133 end Komorebi.MachineTheory.PartitionCorrection

Back to source controls