[chris-ai1]

Binary predecessor and the zero test on encNat now each have a streaming-transducer certificate with explicit linear-time and zero-work-space bounds, following #1645's successor pattern. These sharper primary resource certificates replace the quadratic predecessor fold and expose zero work-tape use. Retained predecessor and zero-test facades derive from them with their original statements. The superseded fold proof and its helpers are deleted.

Predecessor transducer (private, Encodings/Nat.lean). States are Option Bool:

• none is the borrow state: 0 ↦ 1.
• The first 1 moves to some false and emits nothing. This is the pending 0, held back because it would be a leading zero if it were the last digit (4 = [0,0,1] ↦ 3 = [1,1]).
• From some false, the next digit b emits [0, b] and moves to some true, which copies the remaining digits.
• final _ = [].

The existing Transducer structure (at most two symbols per step) is enough, so one digit of lookahead suffices. run_predTransducer : predTransducer.run none n.bits = (n - 1).bits is proved by strong induction on n, using the even/odd split.

Zero-test transducer: the state is "no digit read yet", step _ _ = (false, []) and final b = [b].

Certificates (public, plain, explicit upper bounds from Transducer.computesInTimeAndSpace_toTM):

theorem computableInTimeAndSpace_pred :
    ComputableInTimeAndSpace (· - 1) encNat encNat (fun n => 2 * (encNat n).length + 3) (fun _ => 0)
theorem computableInTimeAndSpace_isZero :
    ComputableInTimeAndSpace (fun n => decide (n = 0)) encNat encBool
      (fun n => 2 * (encNat n).length + 3) (fun _ => 0)

New, one line each: ComputableInLinearTimeAndSpace.natPred and .natIsZero, via a private ComputableInTimeAndSpace.linear. That helper now also gives .natSucc (previously a four-line proof).

Every remaining pred / isZero statement (from grep -rnE "\(· - 1\) encNat|decide \(n = 0\)\) encNat|computableInTimeAndSpace_(pred|isZero)|\.(natPred|natIsZero)\b" Complexity ComplexityTests guide abstracts, paths under Complexity/Computability/Machines/Turing/MultiTape/):

Location	Statement	Derivation
Encodings/Nat.lean:158	computableInTimeAndSpace_pred	the proof (transducer)
Encodings/Nat.lean:166	ComputableInLinearTimeAndSpace.natPred	computableInTimeAndSpace_pred.linear
Encodings/Nat.lean:173	computableInTimeAndSpace_isZero	the proof (transducer)
Encodings/Nat.lean:184	ComputableInLinearTimeAndSpace.natIsZero	computableInTimeAndSpace_isZero.linear
Internal/BinaryPrimitives.lean:77	ComputableInO.natPred (unchanged statement)	(of_linear .natPred).mono_le …
Internal/BinaryPrimitives.lean:84	ComputableInO.natIsZero (unchanged statement)	of_linear .natIsZero
Complexity/InSpaceLib.lean:144/147	ComputableInSpace.natPred / .natIsZero	of_inO ComputableInO.… (unchanged)
Complexity/InSpaceLib.lean:634/639	budget_natPred / budget_natIsZero	budget_comp_lin … (unchanged)
Complexity/InSpaceLib.lean:776/779	ComputableTidilyInSpace.natPred / .natIsZero	ComputableInSpace.….tidy (unchanged)
Complexity/InSpaceLib.lean:966/970	tidy budget_natPred / budget_natIsZero	budget_comp_lin … (unchanged)
ComplexityTests/Encodings.lean	tests	exact certificates and concrete values
ComplexityTests/…/Internal/BinaryPrimitives.lean	test	clients of ComputableInO.natPred/natIsZero

All other hits are compositions (ComputableInO.natPred.comp …, natIsZero.comp_linear …, .tidy) in client proofs. PolyTime/Nat/PowMod.lean gets modulus - 1 from binary_sub, and Internal/PolyTimeBinaryDivision.lean gets decide (b = 0) from binary_le. Both are compositions of other primitives, not separate predecessor or zero-test proofs; I left them alone (divMod is slice F).

Deleted (all used only by the old natPred proof or by its tests):

• Internal/BinaryPrimitives.lean: private linear_tail, digitStep (inlined into its one remaining client succStep), decrStep_inO, normStep_inO, normFinish_inO; the old 30-line natPred and 12-line natIsZero proofs.
• Public, now unused: ComputableInO.foldl_bits; the NatPred namespace in Encodings/Nat/Bits.lean: decr, norm, norm_cons, bits_ne_nil, decr_ne_nil, norm_bits, bits_pred, decrStep, length_decr, foldl_decrStep, normStep, normFinish, length_foldl_normStep, normFinish_foldl. The only other users were the word-level boundary tests in ComplexityTests/…/Internal/BinaryPrimitives.lean. Those are replaced by tests of the certificates themselves.

The tidy surface is unchanged (704, matching the baseline), since only plain statements were touched.

Line counts (against main): +168 / −259 in total, net −91.

File	+	−
Encodings/Nat.lean (two transducers, certificates)	123	10
Encodings/Nat/Bits.lean (NatPred word functions)	2	100
Internal/BinaryPrimitives.lean (fold proof and certificates, foldl_bits)	19	130
tests	24	19

• Quantitative certificates and refactor: the new primary bounds are above; retained facade proofs are derived from them. Every deleted helper became unused through this change.
• Removal of pre-existing unused code: none.

Tests (ComplexityTests/Encodings.lean): the exact pred and isZero certificates on the raw output word (encBits), plus concrete values:

• encNat (4 - 1) = [true, true]
• encNat (0 - 1) = []
• encNat (6 - 1) = [true, false, true]
• the certified time bound evaluates to 9 at 4
• encBool (decide (0 = 0)) = [true] and encBool (decide (4 = 0)) = [false]

Validation at the head commit:

• scripts/check.sh: all six gates pass (build, mk_all, test, lint, lint-style, checkInitImports).
• scripts/check_hygiene.py --check-simp passes.
• scripts/check_changed_files.py --base origin/main passes.
• scripts/check_tidy_surface.py matches the baseline.

Curated abstracts are unaffected.

Independent source/API review is recorded in this PR. Final validation and a delta check after refreshing onto the supported rc2 pins remain required; integration follows #1653. Part of #608, slice A, by worker worker-crei-dc679113-sliceA. AI disclosure: written with Claude Code (Claude Opus 5.5), including the proofs, the refactor and this description.

🤖 Generated with Claude Code

[chris-ai1]

reviewer-crei-opus (agent review, not human approval). Verdict: FINAL, advisory (same session as the authoring workers). Head 229189df83cda2f3ca31a874cb197d257ce2665a, one commit on 94f88591b (current main).

Correctness of the transducers

• predTransducer: for odd n = 2m+1, the input true :: m.bits goes to some false with no output. If m = 0 the output is [] = (2m).bits. Otherwise it is false :: m.bits = (2m).bits by run_predTransducer_pending and bit0_bits. For even n = 2m, m > 0, the input false :: m.bits gives true :: run none m.bits = true :: (m-1).bits = (2(m-1)+1).bits by IH. n = 0 gives []. Each step emits at most 2 symbols, within Transducer's bound. final _ = [] is right: a pending 0 at the end is a leading zero and is dropped, as 4 ↦ [1,1] shows. Sound.
• isZeroTransducer: run q l = [q && l.isEmpty], with true && n.bits.isEmpty ↔ n = 0 via Nat.bits_eq_nil_iff (Foundations). Sound.
• Both certificates come straight from computesInTimeAndSpace_toTM, with the same exact bound 2 * |encNat n| + 3 and zero work space as _succ.

One certificate per function

• ComputableInLinearTimeAndSpace.natPred/.natIsZero/.natSucc are each ….linear (one line). ComputableInO.natPred/.natIsZero keep their statements unchanged and are now of_linear … weakenings. The InSpaceLib plain and tidy natPred/natIsZero/budget_* already derive from ComputableInO.* and are unchanged.
• I grepped Complexity/ComplexityTests for (· - 1) encNat, decide (_ = 0)) encNat, natPred|natIsZero|*_pred|*_isZero declarations and ListEncoding.isEmpty uses. The remaining *_pred/*_isZero hits are unary/int/intBin or bit-list (encBits) primitives, not encNat. I found no other independent binary predecessor or zero-test proof.

Deletions

• ComputableInO.foldl_bits, every NatPred.* word function and lemma (decr, norm, norm_cons, bits_ne_nil, decr_ne_nil, norm_bits, bits_pred, decrStep, length_decr, foldl_decrStep, normStep, normFinish, length_foldl_normStep, normFinish_foldl), and the private linear_tail/digitStep/decrStep_inO/normStep_inO/normFinish_inO are removed.
• A whole-tree word grep (all files except .lake/.git, including guide/, abstracts/, docbuild, scripts) finds no remaining reference. The foldl_bits_* hits are distinct declarations (Streaming.lean, Tactic/PolyTime.lean). The new NatPred namespace in Encodings/Nat.lean holds only private declarations.
• Inlining digitStep into succStep keeps its statement unchanged. Dropping import Mathlib.Tactic.Ring from BinaryPrimitives matches the removed ring-heavy fold proof. CI will confirm.

Tests

• The removed borrowChain 128, norm (decr …) boundary values and encNat (n-1) = norm (decr (encNat n)) only exercised the deleted word functions. They lose no coverage of anything that still exists.
• The new tests restate the exact certificates on encBits output. The existing test still uses .natPred, .natIsZero and ComputableInO.natPred.
• The concrete-value examples (encNat (4-1) = [true,true], etc.) check the specification, not the private transducer, which is unavoidable here. That is fine.

Line counts: numstat is 123/10, 2/100, 19/130, 20/0, 4/19, for +168/−259 (net −91). This matches the body.

Nit (non-blocking): the diff removes the blank line between the module docstring and namespace Turing.MultiTapeTM in Encodings/Nat.lean.

Limits: I did not build locally (disk). ci-checks was still pending at review time. This verdict assumes it goes green.

[edemaine]

reviewer-codex-edemaine — APPROVE source at 229189d (independent agent review, not human approval).

Reviewed the complete five-file diff over 94f8859 and the reused Transducer machine certificate. No findings. On canonical encNat inputs, the borrow state emits ones until the first one; retaining that resulting zero until another digit arrives correctly handles the only possible one-digit shortening, including 0 and 1. The zero test uses the proved empty-bits characterization. Both constructions give one uniform finite-state machine, time 2L+3 and zero work space; the existing O/space facades preserve their output charges and statements.

The shared linear conversion preserves successor's certificate. Deleted borrow/normalization/fold APIs have no remaining clients; the surviving carry-round proof is the former specialization inlined. Checked the raw-output certificate tests, zero/power-of-two/value cases and existing resource clients. No abstract or tidy-baseline impact.

Validation: git diff --check passed; author reports all six local gates passed. PR title passed and Lean Action CI run 40950655547 was running when inspected. No local elaboration/build. Resolve and check any integration delta with #1660 on the supported pins before merging.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732 — APPROVE source at 229189df83cda2f3ca31a874cb197d257ce2665a (independent agent review, not human approval). I reviewed the five-file API/client delta; non-author reviewer /root/review_list_foldl_max checked the induction, transducer semantics and resource conversions.

The fixed finite machines are chosen before all natural inputs. The predecessor proof covers zero, one, powers of two and mixed digits, using canonical Nat.bits; it makes no claim for padded arbitrary words. Both machines have zero work tapes and explicit time upper bound 2L+3. The linear helper keeps the same machine. Retained O/space/tidy facades preserve their statements and output charge, and addition's carry API remains. Deleted helper names have no remaining repository uses; certificate and concrete zero/4/6 tests cover the replacement. Curated abstracts are unaffected.

Validation limits: source-only review, no local elaboration/build. The author reports all six local gates passed; final supported-pin refresh, delta review and CI remain before integration, following #1653.

[SamuelSchlesinger]

Nit: say the certified time bound evaluates to 9 here. ComputesInTimeAndSpace gives an upper bound; this example does not show the machine takes exactly 9 steps.