[chris-ai1]

Two-operand functions on binary naturals (encPair encNat encNat, i.e. frame a.bits ++ b.bits on the single read-only input tape) are only quadratic today: no combinator moves a work-tape head in lockstep with the input head, so every round of a fold re-reads its operands. Following the one-primary-certificate plan of #608 (and the Transducer.toTM pattern of #1645 for the successor), this PR adds the missing kernel: a finite-state zip transducer that reads both operands simultaneously, with an explicit linear-time machine, plus one client (natLt) whose quadratic proof it replaces.

API

Internal/KernelZipTransducer.lean

• ZipTransducer Q: q₀, step : Q → Option Bool × Option Bool → Q × List Bool (pair = (digit of the first word, digit of the second), none pads the shorter word), final : Q → List Bool, both emitting at most two symbols.
• ZipTransducer.run q u v with simp equations run_nil_nil, run_cons_nil, run_nil_cons, run_cons_cons and run_of_ne.
• ZipTransducer.State Q (finite when Q is) and ZipTransducer.toTM : MultiTapeTM 1 Bool (State Q): unframes u onto work tape 1 (two steps per digit), rewinds it, then scans v on the input and u on the work tape in lockstep, applying step, then final.
• ZipTransducer.computesInTimeAndSpace_toTM u v: τ.toTM.ComputesInTimeAndSpace (frame u ++ v) (τ.run τ.q₀ u v) (3 * (frame u ++ v).length + 1) (u.length + 2).

Combinators/ZipTransducer.lean (upstream ComputableInTimeAndSpace, Q : Type with [Finite Q])

• ZipTransducer.computableInTimeAndSpace (hf : ∀ p, encOut (f p) = τ.run τ.q₀ (enc₁ p.1) (enc₂ p.2)): f is computable on encPair enc₁ enc₂ within time 3 * (encPair enc₁ enc₂ p).length + 1 and work space (enc₁ p.1).length + 2.
• ZipTransducer.computableInTimeAndSpace_run: the same on raw words (encPair encBits encBits → encBits).
• ZipTransducer.computableInLinearTimeAndSpace (constant 3) and ZipTransducer.computableInDegree … 1 1.

Internals (configurations, the transition function, phase lemmas) are private. Transducer.toList_head?_append in KernelTransducer.lean is made public so the kernel reuses it instead of re-proving it.

Client: binary comparison, now with one primary certificate

Internal/BinaryComparison.lean now proves comparison with a two-state zip transducer (state = "the low-order digits read so far compare as less than"):

• computableInTimeAndSpace_natLt: decide (a < b) on encPair encNat encNat → encBool within 3 * (encPair encNat encNat p).length + 1 steps and (encNat p.1).length + 2 cells. This is the primary certificate.
• ComputableInLinearTimeAndSpace.natLt.

The three previously independent comparison proofs keep their statements and are now one-line derivations from it; their old proofs are deleted:

• ComputableInO.natLt (quadratic/linear bounds used by InSpaceLib): via of_linear … |>.mono (old proof via natSub/natIsZero).
• ComputableInPolyTime.binary_lt in Internal/PolyTimeBinaryPrimitives.lean: via ComputableInO.of_linear … |>.computableInPolyTime (old bit-position scan with allWithInput, hbit).
• ComputableTidilyInPolyTime.binary_lt in PolyTime/Nat/Binary.lean: ComputableInPolyTime.binary_lt.tidy (old tidy bit-position scan).
  No helper became unused (the scans used only public combinators; Nat.lt_iff_exists_testBit stays as tested public API). Two imports that only served the scan (Mathlib.Data.List.GetD, Mathlib.Data.Nat.Bitwise in PolyTimeBinaryPrimitives) are dropped. Nothing was deferred.

Tests (ComplexityTests/Machines/Turing/MultiTape/ZipTransducer.lean): run on concrete words in both padding directions (bitwise OR and a state-changing transducer), the kernel bound instantiated on frame [true, false] ++ [false, false, true] (25 steps, 4 cells), the natLt certificate on (5, 6) (31 steps, 5 cells), and correct outputs for (6, 5), (6, 6), (0, 1).

What follows

Slice H ports the remaining two-operand functions. A streaming zip transducer emits output while it reads, so it fits functions whose output digits are determined by the digits read so far: add, or, eq, lt can be ported directly. sub, min, max depend on the comparison result, which is known only after the last digit, and sub, xor, and can end in zeros that encNat strips; buffering an unbounded run of pending zeros is not finite-state. These need a different scheme (e.g. a second pass over a work tape, or comparison first and then a transducer selected by its result). Nothing in ROADMAP.md changes.

Size and validation

+851 / −90 over 8 files (rebased on main d6ccb24).

• New kernel and API: Internal/KernelZipTransducer.lean +598 (about 120 lines of public API, the rest private phase lemmas), Combinators/ZipTransducer.lean +83, KernelTransducer.lean ±1 (lemma made public), Complexity.lean +2.
• Client (new natLt certificate): BinaryComparison.lean +74 / −14, of which the transducer, its correctness proof and the two new theorems are the additions and the deleted quadratic ComputableInO.natLt proof is the removal.
• Removal of the independent binary_lt proofs: PolyTimeBinaryPrimitives.lean +9 / −49, PolyTime/Nat/Binary.lean +5 / −26.
• Tests: +79.

Local scripts/check.sh on 1724ef1: all six gates ok (build, mk_all, test, lint, lint-style, checkInitImports). check_hygiene.py --check-simp, check_changed_files.py --base origin/main and check_tidy_surface.py (708 statements, baseline unchanged) pass. Abstracts: no impact (no catalogued statement changes; every re-derived theorem keeps its statement).

Part of #608 by worker worker-crei-dc679113-zip.

Independent agent review: approved at the current revision. Full hosted CI passed on the same revision. The small List-helper placement follow-up is tracked separately.

AI disclosure: implemented with Claude Code (Claude Opus 5.5), which wrote the machine, proofs, tests and this description.

🤖 Generated with Claude Code

[chris-ai1]

reviewer-crei-opus: review at head 9ccece476521d635dcdff6ba939572fb504c1eaf. This is an independent agent review, not human approval.

Verdict: CHANGES REQUESTED (advisory: written in the same session as the authoring workers). The kernel and the natLt client are sound. The requested change is small: this PR leaves two other independent proofs of the same comparison in place.

Checked and fine

• Kernel semantics. run pads the shorter word with none. tr reads the digit of v from the input tape and the digit of u from the work tape, then calls τ.step q (y, x), so the pair passed to step is (digit of u, digit of v) as documented.
  • Copy phase: per frame marker true, the machine moves to copyBit, which writes the digit and moves right. The end marker steps the head back by one, and rewind then walks to cell −1 and steps back to cell 0.
  • Zip phase: the second symbol of each emission is held in the pending state and output on the next step. final is emitted through flush.
• Bounds are meaningful. The time bound is checked against the phases. Copy takes 2|u|+1 steps, the end marker 1, rewind about |u|+1, and zip at most 2·max(|u|,|v|)+2. That is well inside 3·(2|u|+1+|v|)+1, and the slack is what makes the proof work for every step. The space bound u.length + 2 is exactly the cells Icc (-1) |u| (Int.card_Icc). It is the honest work-tape footprint; it is not charged for output.
• Public statements. computesInTimeAndSpace_toTM, ZipTransducer.computableInTimeAndSpace, _run, computableInLinearTimeAndSpace (constant 3, using length_le_encPair_left for space) and computableInDegree … 1 1 say what the PR body says. There is no sorry, set_option or @[fun_prop]. The machine internals are private, and only ZipTransducer, run with its simp equations, State (with its Finite instance) and toTM are public.
• ltZip is correct. Its state means "the low-order digits read so far compare as less than". When the two digits differ, the new state is the digit of v; otherwise the state is kept. run_ltZip proves this by induction for all three padding shapes, and encBool_natLt closes it with Nat.foldr_bit_bits.
• ComputableInO.natLt keeps its statement (same function, encodings and bounds). It is now (of_linear …natLt).mono 1 …. The old hnot ∘ natIsZero ∘ natSub proof is fully deleted. InSpaceLib's ComputableInSpace.natLt, ComputableTidilyInSpace.natLt and all budget_natLt clients still go through it.
• Transducer.toList_head?_append made public. This is justified: without it, the kernel would need a copy. Nit: it is a general List fact sitting in the Turing.MultiTapeTM.Transducer namespace. That is acceptable as is, but Foundations/Data/List would be the natural home if more users appear.
• Tests are concrete and registered (the ComplexityTests.+ glob picks the file up).
  • run is tested in both padding directions and with a state change on one-sided input.
  • The kernel bound is instantiated at 25 steps / 4 cells for input length 8.
  • natLt is tested on (5,6) at 31 steps / 5 cells, with |encPair| = 10, and on outputs for (6,5), (6,6) and (0,1).
• Tidy baseline is untouched and sums to 708. Complexity.lean gains exactly the two new modules.

Requested: two other independent natLt proofs remain

The aim (#608) is one primary certificate per function. Two independent proofs of the same decide (p.1 < p.2) on encPair encNat encNat → encBool survive. Both use the quadratic bit-position scan (any/all over List.range).

• Internal/PolyTimeBinaryPrimitives.lean:44, binary_lt : ComputableInPolyTime …. This can become ComputableInO.natLt.computableInPolyTime (PolyBounded…) (PolyBounded…), exactly like binary_add directly above it.
• Complexity/PolyTime/Nat/Binary.lean:245, binary_lt : ComputableTidilyInPolyTime …. This can become computableInTimeAndSpace_natLt.exists_computableTidilyInTimeAndSpace plus polynomial bounds, as refactor(Machines): binary successor as one linear-time streaming transducer (#608) #1645 did for computableTidilyInPolyTime_succ.

Both keep their statements and do not change the baseline. Alternatively, defer them explicitly in the PR body to a tracked slice-H item.

PR body: the slice-H note is not accurate

• min/max are listed as zip-transducer ports, but they cannot be one. The output is one of the operands, and which one depends on the comparison. In least-significant-digit-first order, the comparison is decided by the last differing digit, so a finite-state transducer cannot know which digits to emit while streaming.
• Truncated sub has the same problem: whether the result is 0 depends on a < b. Trailing zeros are a second, separate problem.
• "A delayed-zeros state" cannot be finite. A run of zeros that might turn out to be trailing has unbounded length. Normalising needs a counter or a second pass, for example on the work tape.
• add, eq, lt and bitwise or stream fine.

Please reword the note so slice H plans for this.

Limits

• I did not run a local build. Hosted ci-checks was still in progress. The author reports check.sh passing locally.
• I reviewed the private phase lemmas (seg_copy/seg_rewind/seg_zip/seg_run) at the level of their statements and step accounting, not line by line; Lean checks them.

[chris-ai1]

reviewer-crei-opus: delta review at head 1724ef1e2f8a83778d1704c7a1526de7af97e75c, following up my CHANGES REQUESTED at 9ccece476521d635dcdff6ba939572fb504c1eaf. This is an independent agent review, not human approval.

Verdict: FINAL (advisory: written in the same session as the authoring workers), provided hosted ci-checks passes. It was still in progress when I reviewed.

Delta

• The branch is rebased onto current main d6ccb24fd. git range-diff reports the kernel commit as 9ccece476 = ce0a964d2, so the layer I reviewed before is unchanged. The only new commit is 1724ef1e2, touching 2 files (+14/−75).
• Internal/PolyTimeBinaryPrimitives.lean binary_lt. The statement is unchanged (ComputableInPolyTime … (encPair encNat encNat) encBool, @[fun_prop]). It is now (ComputableInO.of_linear ComputableInLinearTimeAndSpace.natLt).computableInPolyTime with linear PolyBounded bounds, the same pattern as binary_add. The scan and all its local helpers (hbits/hlen/hwords/hsum/hscan/hbit) are deleted.
  • The imports drop Mathlib.Data.Nat.Bitwise and Mathlib.Data.List.GetD and add Internal.BinaryComparison. No testBit or getD use remains in the file; binaryMulPair only uses Nat.bits.
• PolyTime/Nat/Binary.lean binary_lt. The statement is unchanged (ComputableTidilyInPolyTime, @[fun_prop]). It is now ComputableInPolyTime.binary_lt.tidy, and its own scan is deleted. The module docstring now points to computableInTimeAndSpace_natLt.
• One certificate for natLt. git grep 'decide (p.1 < p.2)' now finds only:
  • computableInTimeAndSpace_natLt, the primary certificate;
  • its derivations ComputableInLinearTimeAndSpace.natLt, ComputableInO.natLt, the two binary_lt, and InSpaceLib's ComputableInSpace.natLt / ComputableTidilyInSpace.natLt;
  • unary_lt and intBin_lt, which are different functions on other encodings.
• Tidy baseline is unchanged versus main.
• PR body. The slice-H note is corrected. It now says that add/or/eq/lt stream directly; that sub/min/max need the comparison, which is only known after the last digit; that sub/xor/and can end in zeros encNat strips; and that buffering an unbounded run of pending zeros is not finite-state. It suggests a second pass or comparing first. This is accurate. The body was last updated at 18:54Z, matching the new commit.

Nits (not blocking)

• Nat.lt_iff_exists_testBit (Encodings/Nat/Arithmetic.lean:144) no longer has any library user; only two tests use it. PolyTime/Nat/Binary.lean:56 still lists it under "Main results", although it is declared elsewhere (this predates the PR). It is a general Nat fact outside Foundations. Moving it or dropping the stale bullet can be a follow-up.

Limits

• I did not run a local build. Hosted CI is still running, and it will show whether the dropped Mathlib imports were relied on transitively.

[edemaine]

reviewer-codex-edemaine — APPROVE at 1724ef1 (independent agent review, not human approval).

Reviewed the complete eight-file layer over d6ccb24, including the private copy/rewind/zip/flushing proofs. No findings. The framed encoding and transition argument order match run; exhausted operands stay at their blank boundaries, and pending second output symbols preserve the two-symbol emission semantics. The segment invariant accounts for visited cells, including -1 and the first blank after u, giving workspace |u|+2 independently of output length and time at most 3|frame u ++ v|+1. The public computability certificates retain one finite machine uniformly over inputs.

The comparison invariant handles equality, padding and the last differing digit correctly. All three former comparison proofs now derive from the linear certificate with their original statements and output-charge conventions preserved. The earlier advisory findings are resolved. Tests exercise both padding directions, changing state, two-symbol final output, concrete machine bounds and true/false/equal comparisons. Existing curated abstracts and the tidy baseline are unaffected.

Validation: git diff --check passed. The author reports all six local gates passed. At inspection PR title passed and Lean Action CI run 40935166868 was still running. No local elaboration/build.