UnarySelectors.lean

1 import RealizationBoundaries.SubgroupSpectrum
2 import Mathlib.Data.Fintype.Pigeonhole
3 
4 /-! # Genuine finite unary state machines and their selector groups -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace RealizationBoundaries
8 
9 /-- A unary deterministic finite automaton: one transition for each input symbol. -/
10 structure UnaryMachine where
11   State : Type
12   finite_state : Finite State
13   start : State
14   step : State → State
15   accepting : Set State
16 
17 attribute [instance] UnaryMachine.finite_state
18 
19 /-- Acceptance after the unary word of length `n`. -/
20 def UnaryMachine.accepts (M : UnaryMachine) (n : ℕ) : Prop :=
21   M.step^[n] M.start ∈ M.accepting
22 
23 /-- A finite prefix followed by a repeated nonempty period. -/
24 def UltimatelyPeriodic (B : Set ℕ) : Prop :=
25   ∃ N d : ℕ, 0 < d ∧ ∀ n, N ≤ n → (n + d ∈ B ↔ n ∈ B)
26 
27 /-- A selector is realized by a finite unary automaton with its actual iterated transition. -/
28 def UnaryRecognizable (B : Set ℕ) : Prop :=
29   ∃ M : UnaryMachine, ∀ n, M.accepts n ↔ n ∈ B
30 
31 /-- Two equal orbit states force equality of all subsequent states. -/
32 theorem unary_iterate_propagates (M : UnaryMachine) {i j : ℕ}
33     (h : M.step^[i] M.start = M.step^[j] M.start) (k : ℕ) :
34     M.step^[i + k] M.start = M.step^[j + k] M.start := by
35   rw [Nat.add_comm i k, Nat.add_comm j k, Function.iterate_add_apply, Function.iterate_add_apply]
36   exact congrArg M.step^[k] h
37 
38 /-- The pigeonhole principle gives eventual periodicity of the actual finite-state orbit. -/
39 theorem unaryMachine_ultimatelyPeriodic (M : UnaryMachine) :
40     UltimatelyPeriodic {n | M.accepts n} := by
41   classical
42   have hnot : ¬ Function.Injective (fun n : ℕ => M.step^[n] M.start) := by
43     intro hi
44     let := Finite.of_injective _ hi
45     exact not_finite ℕ
46   obtain ⟨i, j, hij, hne⟩ := Function.not_injective_iff.mp hnot
47   wlog hlt : i < j generalizing i j
48   · exact this j i hij.symm hne.symm (by omega)
49   refine ⟨i, j-i, by omega, ?_⟩
50   intro n hn
51   have he := unary_iterate_propagates M hij (n-i)
52   have hi : i + (n-i) = n := Nat.add_sub_of_le hn
53   have hj : j + (n-i) = n + (j-i) := by omega
54   rw [hi, hj] at he
55   exact Iff.of_eq (congrArg (fun q => q ∈ M.accepting) he.symm)
56 
57 /-- The tail seen after a prefix is the future Boolean acceptance sequence. -/
58 def unaryTail (B : Set ℕ) (n : ℕ) : Set ℕ := {k | n+k ∈ B}
59 
60 theorem unaryTail_periodic {B : Set ℕ} {N d : ℕ}
61     (h : ∀ n, N ≤ n → (n+d ∈ B ↔ n ∈ B)) {n : ℕ} (hn : N ≤ n) :
62     unaryTail B (n+d) = unaryTail B n := by
63   ext k
64   exact (show n+d+k ∈ B ↔ n+k ∈ B by
65     simpa only [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using h (n+k) (by omega))
66 
67 /-- Every eventual-period tail is represented among the first `N+d` tails. -/
68 theorem unaryTail_bounded {B : Set ℕ} {N d : ℕ} (hd : 0 < d)
69     (h : ∀ n, N ≤ n → (n+d ∈ B ↔ n ∈ B)) (n : ℕ) :
70     ∃ m, m < N+d ∧ unaryTail B n = unaryTail B m := by
71   induction n using Nat.strong_induction_on with
72   | h n ih =>
73     by_cases hn : n < N+d
74     · exact ⟨n, hn, rfl⟩
75     · have hlt : n-d < n := by omega
76       obtain ⟨m, hm, he⟩ := ih (n-d) hlt
77       refine ⟨m, hm, ?_⟩
78       have hnd : N ≤ n-d := by omega
79       have heq := unaryTail_periodic h hnd
80       have hadd : n-d+d = n := by omega
81       rw [hadd] at heq
82       exact heq.trans he
83 
84 theorem unaryTail_range_finite {B : Set ℕ} (hB : UltimatelyPeriodic B) :
85     (Set.range (unaryTail B)).Finite := by
86   obtain ⟨N, d, hd, h⟩ := hB
87   apply ((Finset.range (N+d)).finite_toSet.image (unaryTail B)).subset
88   rintro t ⟨n, rfl⟩
89   obtain ⟨m, hm, he⟩ := unaryTail_bounded hd h n
90   exact ⟨m, Finset.mem_range.mpr hm, he.symm⟩
91 
92 /-- The finite set of tails is a DFA state space, with transition given by deleting one symbol. -/
93 def unaryTailMachine {B : Set ℕ} (hB : UltimatelyPeriodic B) : UnaryMachine where
94   State := Set.range (unaryTail B)
95   finite_state := (unaryTail_range_finite hB).to_subtype
96   start := ⟨unaryTail B 0, ⟨0, rfl⟩⟩
97   step t := ⟨{k | k+1 ∈ t.val}, by
98     obtain ⟨n, hn⟩ := t.property
99     refine ⟨n+1, ?_⟩
100     ext k
101     change n+1+k ∈ B ↔ k+1 ∈ t.val
102     rw [← hn]
103     change n+1+k ∈ B ↔ n+(k+1) ∈ B
104     have he : n+1+k = n+(k+1) := by omega
105     rw [he]⟩
106   accepting := {t | 0 ∈ t.val}
107 
108 theorem unaryTailMachine_orbit {B : Set ℕ} (hB : UltimatelyPeriodic B) (n : ℕ) :
109     ((unaryTailMachine hB).step^[n] (unaryTailMachine hB).start).val = unaryTail B n := by
110   induction n with
111   | zero => rfl
112   | succ n ih =>
113     rw [Function.iterate_succ_apply']
114     ext k
115     change k+1 ∈ ((unaryTailMachine hB).step^[n] (unaryTailMachine hB).start).val ↔ n+1+k ∈ B
116     rw [ih]
117     change n+(k+1) ∈ B ↔ n+1+k ∈ B
118     have he : n+(k+1) = n+1+k := by omega
119     rw [he]
120 
121 theorem unaryTailMachine_accepts {B : Set ℕ} (hB : UltimatelyPeriodic B) (n : ℕ) :
122     (unaryTailMachine hB).accepts n ↔ n ∈ B := by
123   change 0 ∈ ((unaryTailMachine hB).step^[n] (unaryTailMachine hB).start).val ↔ n ∈ B
124   rw [unaryTailMachine_orbit]
125   simp [unaryTail]
126 
127 /-- Unary finite-state recognition is exactly ultimate periodicity. -/
128 theorem unaryRecognizable_iff_ultimatelyPeriodic (B : Set ℕ) :
129     UnaryRecognizable B ↔ UltimatelyPeriodic B := by
130   constructor
131   · rintro ⟨M, hM⟩
132     have hB : {n | M.accepts n} = B := Set.ext hM
133     exact hB ▸ unaryMachine_ultimatelyPeriodic M
134   · intro hB
135     exact ⟨unaryTailMachine hB, unaryTailMachine_accepts hB⟩
136 
137 /-- Prime-index selectors interpreted in the actual subgroup D_B. -/
138 def indexedSpectrum (B : Set ℕ) : Set Prime := primeAt '' B
139 
140 theorem indexedSpectrum_injective : Function.Injective indexedSpectrum :=
141   Set.image_injective.mpr primeAt_injective
142 
143 /-- A unary-selector grammar may output a group isomorphic to its selected prime subgroup. -/
144 def UnaryGroupRealizable (B : Set ℕ) : Prop :=
145   ∃ C : Set ℕ, UnaryRecognizable C ∧
146     Nonempty (spectrumSubgroup (indexedSpectrum C) ≃+
147       spectrumSubgroup (indexedSpectrum B))
148 
149 /-- Monograph 3.5: abstract group isomorphism cannot hide a different unary selector. -/
150 theorem unary_selector_classification (B : Set ℕ) :
151     UnaryGroupRealizable B ↔ UltimatelyPeriodic B := by
152   constructor
153   · rintro ⟨C, hC, he⟩
154     have hCB : C = B := indexedSpectrum_injective
155       ((spectrumSubgroup_isomorphic_iff _ _).mp he)
156     exact hCB ▸ (unaryRecognizable_iff_ultimatelyPeriodic C).mp hC
157   · intro hB
158     exact ⟨B, (unaryRecognizable_iff_ultimatelyPeriodic B).mpr hB, ⟨AddEquiv.refl _⟩⟩
159 
160 end RealizationBoundaries

Back to source controls