Research: reduce batched lifting clean workspace with paid checkpoints

[tekuuu]

PR #3109's fast batched lifting core retains almost quadratic clean computation history. This conditional construction reduces its additional clean-workspace exponent from 1197203/600000 ≈ 1.995338 to 1797203/1200000 ≈ 1.497669, preserving the exact nonlinear map, inverse, error guarantee and time exponent 1199003/600000 ≈ 1.998338.

The change applies classical Bennett checkpointing to complete machine configurations. The proof binds the inherited C routine's configuration to O(Nw)+F, including recursive parked arrays, compact rotation/repair buffers, the ordinary backend, heads and control state. A sequential checkpoint tape pays copies, local scans/rewinds, between-slot movement and reverse cleanup. Full formulas retain mutable compilation cost F; the simplified exponents fix the inherited compiler/prime.

Only research/lifting-checkpoint-space/ is added: a written conditional proof, an executable Boolean checkpoint controller, an independent closed-coefficient Gaussian circuit, source pins, receipts and failure controls. In one executed same-input fixture, peak active/checkpoint/history payload decreases from 30,982 to 7,952 bits, with extra recomputation explicitly charged. This is a logical payload comparison, not a Python RAM benchmark or runtime speedup.

Scope: research/interface construction, conditional on the credited physical source/compiler premises. The small circuit checks the protected XOR interface and unchanged predecessor macro; it does not instantiate the large fast C machine. Native wrappers, collector integration, dirty hosting and supplier admission remain separate. No new κ or selected-frontier change is claimed. This is a concrete two-level point of a classical tradeoff, not a new general reversible-simulation theorem or an optimality claim.

Validation passed on CPython 3.12.14:

python3.12 scripts/research_package.py --package research/lifting-checkpoint-space

Expected: PASS_LIFTING_CHECKPOINT_SPACE, eight passing control groups, and PASS_REGISTERED_RESEARCH_PACKAGE. Coverage: 2,720 exhaustive source/dirty-target cases; 32,832 exact integer planner cases; 40 same-input full-trace/checkpoint Gaussian calls, including three paired nonlinear macros. Controls cover broken cleanup/history, expensive bank resets, projections/aliases, missing output writes, headroom, source drift, typed receipts and optimized read-only Git-free replay. Metadata and exact committed-byte checks pass. Hosted CI is a separate check.

Base: 997e6a9ca7b4f95d50e366f61412fd640d72a88a, unchanged at the publication refresh. All 247 open PRs were paginated for metadata overlap, along with current issues and recent relevant discussions; this is not an audit of every diff. The separate active wrapper/collector scope remains untouched. Investigation and handoff.

Credit Bennett (1973/1989); Jose Manuel (jmbarrancoml) for PR #3109, #2287, #2250 and #2899; Douglas Colkitt and the retained source lineage, including Nick Petalas and David Arias; Ross Richardson for PR #3072; and Tekalign's PR #3033/#3025 predecessors. Exact commits and live-file hashes are in SOURCES.json. Prepared by Tekalign with substantial OpenAI Codex assistance in analysis, implementation, testing and writing. Apache-2.0. No independent human or formal-kernel review is claimed.