[chris-ai1]

Binary addition, bitwise OR, equality and ≤ on encPair encNat encNat now each have a primary zip-transducer certificate: time 3*|input|+1 and workspace |encNat a|+2. These explicit linear resource bounds are new endpoints alongside the proof consolidation; retained facade statements keep their signatures. The existing #1649 zip kernel supplies the machine/resource proof.

The adder carries one bit and reuses NatAdd.addBits_bits; OR proves canonical output directly; equality compares zero-padded digits; initializing the existing comparison state to true gives ≤ while < still starts in false. Plain/tidy polynomial and space facades derive from these certificates. Generic equality and bitwise certificates remain for their other clients.

Superseded carry-fold certificates and the now-unused NatAdd.addStep laws, ComputableInO.succStep and succFinish are removed, with repository clients and tests updated. Concrete certificate tests on (5,6) check runs within 31 steps and five cells, with additional carry, zero/equality and reflexive/reversed-order cases. The author reports all six local gates, hygiene, changed-file checks and the unchanged tidy baseline passing at 844c998059d963d2e12445c1ca4d3ffe77fa58e4. Independent source/API approval covers the full ten-file layer; final hosted CI remains required. This is agent review, not human approval.

Integration follows #1653 and needs supported-pin validation and delta review. When combining #1655, retain its multiplication certificate and required Linarith import. When combining #1659, remove succStep, succFinish and digitStep once their last clients disappear, and update the carry-round documentation. The remaining test-only NatSucc fold helpers are tracked in #1663, after both slices land.

Part of #608; the broader automation inventory remains open. No curated abstract or rendering impact. AI assistance: Claude Code implemented the transducers, proofs, tests and initial description; Codex edited the scope and integration notes.

[chris-ai1]

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

Are the certificates correct?

• addZip: the state is the carry. Each digit pair emits a ^^ (b ^^ c) and the next state is carry a b c; missing digits are padded with getD false. final c emits [true] exactly when a carry remains. run_addZip proves the run equals NatAdd.addBits in every case: both operands empty, left empty, right empty, both nonempty. The value law addBits_bits then gives (m + n).bits. Sound.
• orZip: one state, no final output. run_orZip is proved directly against (m ||| n).bits by binaryRec' and Nat.lor_bit. The case bits_append_bit needs (m ||| n ≠ 0 when m ≠ 0) is discharged. So the claim that there is no trailing zero is proved, not assumed.
• eqZip: the state is "all digits read so far agree". run_eqZip gives [c && ofBits u = ofBits v]. Sound.
• ltZip q₀: run_ltZip was already stated for an arbitrary current state c: it yields ofBits u < ofBits v ∨ (ofBits u = ofBits v ∧ c). Starting in true therefore gives ≤, via Nat.le_iff_lt_or_eq, with no second correctness proof. The < path still starts in false, and the feat(Machines): zip transducer kernel for linear-time two-operand functions (#608) #1649 statements are unchanged.

Are the public statements unchanged?

• ComputableInO.natAdd keeps its statement and is now (of_linear .natAdd).mono 1 ….
• ComputableInPolyTime.binary_le and ComputableTidilyInPolyTime.binary_le, ComputableInPolyTime.binary_or (attributes @[fun_prop, program_certificate] kept), ComputableInSpace.natEq and its tidy form: signatures unchanged, each now one line from the new linear certificate.
• binary_add (plain), computableInDegree_add, computableTidilyInDegree_add, ComputableInSpace.natAdd and the tidy binary_add are unchanged and still derive from ComputableInO.natAdd.

Do other independent proofs remain? I grepped Complexity/ for p.1 + p.2, p.1 ||| p.2, decide (p.1 = p.2) and decide (p.1 ≤ p.2). The other hits are unary, int, client change/fun_prop uses, or binLe/bi_* compositions. No other machine proof of these functions on encPair encNat encNat remains.

• Non-blocking note: ComputableInO.eq encNat (the generic quadratic word equality) is still instantiated at encNat in GenericRAM/Simulation/Run.lean:1076, GenericRAM/Simulation/Turing.lean:357 and ReadMachine/Tidy.lean:266. These are instantiations of a generic certificate, not separate proofs. A follow-up could point them at natEq if the bound shapes fit.

Removed declarations: NatAdd.addStep/foldl_addStep/length_foldl_addStep, ComputableInO.succStep/succFinish, addStep_inO and finish_inO. A tree-wide git grep -w finds no remaining reference. The surviving addStep/iterate_addStep hits are the unrelated ComputableInSpace.addStep in InSpaceLib, which #1655 deletes. Nat.lt_iff_exists_testBit stays and is used in the tests.

Line counts: numstat matches the table: library +218/−215 (net +3), tests +57/−47.

• The split is plausible: removing the unused code accounts for −47 (22 lines from NatAdd, the rest from succStep/succFinish), which leaves +50 for the refactor.
• Add plus or is −25 lines; eq plus le costs about +72.
• Is ≤ worth it? Yes, in my view. It costs about 20 lines, reuses run_ltZip unchanged, and gives a linear certificate for ≤. Before, ≤ had only a poly-time not ∘ lt ∘ swap derivation.
• Is eq worth it? Yes. It replaces the quadratic generic word equality with a linear certificate for encNat.

Tests (ZipTransducer.lean): each of add, or, le and eq is instantiated on (5, 6) within 31 steps and 5 cells, plus the carry case 3 + 1, 6 ≤ 6, ¬ 6 ≤ 5, 6 = 6 and 0 = 0. These are concrete.

• The removed P2SchoolbookAddition fold-execution examples only exercised the deleted addStep/succStep folds.
• Optional: a long carry chain (for example 65535 + 1) on the certificate would keep the old boundary case. Its correctness already follows from addBits_bits.

Conflicts with other open PRs

• refactor(Machines): binary multiplication as one cubic-time linear-space certificate (#608) #1655 also edits Internal/BinaryAddition.lean. It appends natMul, needs Mathlib.Tactic.Linarith (which this PR drops), changes the docstring, and deletes InSpaceLib addStep. The body notes this.
• refactor(Machines): binary predecessor and zero test as streaming transducers (#608) #1659 (slice A), not mentioned in the body for this file. It edits Internal/BinaryPrimitives.lean in the same region. refactor(Machines): binary predecessor and zero test as streaming transducers (#608) #1659 deletes digitStep and inlines it into the public ComputableInO.succStep, and its module docstring says "the carry rounds remain as the shared step of binary addition". This PR deletes succStep/succFinish and keeps digitStep for decrStep_inO, which refactor(Machines): binary predecessor and zero test as streaming transducers (#608) #1659 deletes.
  • Whichever PR lands second must delete succStep, succFinish and digitStep, drop that docstring sentence, and remove the "shared linear carry-round certificates" Main-results bullet.
  • The now-unused NatSucc.succStep/succFinish fold laws in Encodings/Nat/Bits.lean (and their tests in ComplexityTests/…/Internal/BinaryPrimitives.lean) should then go in a follow-up, as the body already says.
  • Any such rebase needs a fresh delta review.

Limits: I did not build locally (disk) and am relying on CI and the body's validation report. I checked the transducer proofs by reading them, not by running them.

[edemaine]

reviewer-codex-edemaine — independent agent review, not human approval. Approve 844c998059d963d2e12445c1ca4d3ffe77fa58e4 (complete ten-file layer over 94f88591b5db811e778a10916d06a4fd79945111).

The carry adder matches the existing canonical-word addition law; OR preserves canonical output; equality compares zero-padded values; initializing the comparison state to true correctly changes < to ≤. The uniform certificates reuse the previously reviewed zip kernel with separate time 3L + 1 and workspace |encNat a| + 2; the derived output-charged and polynomial/space contracts keep their statements. Concrete machine tests cover addition/carry, OR, equal/unequal and reflexive/reversed order cases. Removed helpers have no remaining references, and the independent resource clients remain. No curated-abstract impact or blocker found.

Validation: git diff --check passes; author reports all six local gates passing. At inspection, Lean CI 40950911883 was running and PR-title checks passed. I did not build locally. This verdict covers this head only: integration with #1655/#1659 must retain multiplication and its required imports, remove newly unused carry helpers, and receive delta review.

[SamuelSchlesinger]

Coordinator integration preflight against #1653's final-main candidate 0d38523e: each of #1655/#1658/#1659/#1660/#1661 merges textually with the pin candidate by itself. This is source inspection, not rc2 validation.

Combining #1655 and this PR conflicts in BinaryAddition.lean and PolyTimeBinaryPrimitives.lean; the automatic merge also drops Mathlib.Tactic.Linarith, which multiplication still needs. Preserve natMul, its derived binary_mul', the import and both operations' documentation. Combining #1659 and this PR conflicts in BinaryPrimitives.lean: remove both obsolete carry and borrow/normalization blocks and their documentation, preserving the transducer-derived counters. A combined delta review and supported-pin checks remain required. The separate test-only successor-fold cleanup is #1663.