[chris-ai1]

Part of #1444 Phase 5 (catalytic comparison, idea 14 of #474).

This adds two restoring equality tests as pure, machine-free statements. Each borrows memory with arbitrary contents, visits its two operands alternately (x, y, x, y, so it never holds both at once), and gives the borrowed memory back exactly. Provenance. The sum-of-squares test follows the construction in OpenAI's Lean formalization, lean/OAI/Computability/Logspace/CatalyticComparison.lean at rev 7ef5c0cc, step for step: its fair (first, second, pointR, pointZ) is addSqDist, with the same split of terms across the four visits, and its lemmas map as pupils ↔ addSqDist_eq, back ↔ addSqDist_neg_addSqDist/eqTest_snd, test_eye ↔ eqTest_fst_iff_sqDist/eqTest_eq, and paw + small ↔ natCast_sqDist_eq_zero_iff. It is re-proved independently in our own formulation: register vectors Fin ℓ → R over a commutative ring with the dot product, where that file uses digit-encoded naturals, and our own names, statements and proofs. No code was vendored or translated. keyTest follows the preprint's Lemma 9.9. Ben-Or–Cleve and Buhrman–Cleve–Koucký–Loff–Speelman are background for the cancellation of arbitrary initial contents. The module docstring states the same.

New module Complexity/Computability/Catalytic/Comparison.lean (272 lines), with tests in ComplexityTests/CatalyticComparison.lean (101 lines). It also adds three references.bib entries. OpenAI2026LogSpace is character-identical to the entry in #1676, so the two PRs merge cleanly in either order.

Register model. The Cook–Mertz files have no separate reversible-program layer. Their model is a register file S : ι → Fin ℓ → R updated with Function.update, where a call carries a coefficient c and the call with -c undoes it. The tests use that model directly, generalized from fields to commutative rings so that it covers ℤ and ZMod m. They borrow one register r of the file, and a test borrows a register of Cslib.TreeEval.State (ZMod 7) 2.

What it proves

• addSqDist_eq: addSqDist c r x y T = (T.1, T.2 + c * ((x - y) ⬝ᵥ (x - y))) for every register file and accumulator T. The four visits are: mask S r with x and add c⟨x,x⟩; add c(⟨y,y⟩ − 2⟨S r, y⟩); unmask; add 2c⟨S r, y⟩. The contents of S r cancel. addSqDist_neg_addSqDist shows that the call with -c undoes the call with c.
• eqTest r x y T runs this with c = 1, reads whether the accumulator changed, then runs it with c = -1. eqTest_snd: (eqTest r x y T).2 = T. eqTest_fst_iff_sqDist: the flag is (x - y) ⬝ᵥ (x - y) = 0. eqTest_eq: ((x - y) ⬝ᵥ (x - y) = 0 ↔ x = y) → eqTest r x y T = (decide (x = y), T).
• Exactness and wraparound. eqTest_eq_int holds over ℤ with no hypothesis. Over ZMod m, the result natCast_sqDist_eq_zero_iff assumes ∀ i, x i < b, ∀ i, y i < b and ℓ * (b - 1) ^ 2 < m, and concludes that the squared distance of (↑) ∘ x and (↑) ∘ y is zero iff x = y. eqTest_eq_natCast is the corresponding exact test. The bound is needed: in ZMod 5, (1, 2) and (0, 0) have squared distance zero, and a test checks that the flag is wrongly set there.
• Cost. mul_sq_lt_two_pow_size: ℓ * (b - 1) ^ 2 < 2 ^ (Nat.size ℓ + 2 * Nat.size b). So eqTest_eq_two_pow makes the test exact with a k = size ℓ + 2·size b-bit accumulator (ZMod (2^k)). The clean storage is that accumulator, a phase among four and the flag. The borrowed register, ℓ elements of ZMod (2^k), is restored. Since eqTest compares with the initial accumulator value, a realization must either keep that value or start the accumulator at zero; the module docstring says so.
• keyTest_eq: keyTest c a b V s = (V, s + if a = b then c else 0) for a borrowed table V : κ → M over any additive group. Over ZMod 2 with c = 1, this is the preprint's exclusive-or test.

Source → Lean

Source	Lean
Preprint (OpenAI2026LogSpace, rev 7ef5c0cc) Lemma 9.9, Restoring equality test: flip V_{k(v)}, xor V_{k(w)} into the result, flip again, xor again. V is restored and the result gains 1_{k(v)=k(w)}	keyTest, keyTest_eq. This is the same four visits, generalized from bits to any additive group M and coefficient c. Visits to endpoints become the operands a, b, and nesting and path independence are not modelled (they belong to Phase 6)
#474 idea 14, Lean route: add Σ(xᵢ − yᵢ)² to an accumulator, read whether it changed, undo	addSqDist, eqTest, eqTest_eq. The four-visit construction, masking a borrowed register so that the cross term ⟨x, y⟩ is formed from single-operand visits, follows OAI's CatalyticComparison.lean (fair/pupils, rev 7ef5c0cc), re-proved in our own formulation
Wraparound / modulus	natCast_sqDist_eq_zero_iff (hypothesis ℓ(b−1)² < m), eqTest_eq_int, and the ZMod 5 counterexample in the tests
Arbitrary initial contents cancel (background: Ben-Or–Cleve 1992; Buhrman–Cleve–Koucký–Loff–Speelman 2014, transparent programs)	the ∀ T / ∀ V quantification in addSqDist_eq, eqTest_eq, keyTest_eq

Placement. The new topic module is Cslib.Catalytic, under Computability/ next to TreeEval/. It reuses the Cook–Mertz register convention without importing Tree Evaluation, because the tests are not about trees and Phase 6 should not need to depend on TreeEval. The test file shows the comparison running on a Cook–Mertz state. If reviewers prefer it inside TreeEval/, moving it is a one-line change. I found no duplicate in Mathlib, cslib or TreeEval/ (Cook–Mertz has signed register updates but no equality test).

What remains of Phase 5. This PR delivers the algebraic gadget only. The next slice needs Phase 6's frame/visit interface: nesting, where operands are produced by sub-procedures that themselves restore the borrowed memory and whose results do not depend on its contents (the induction in the proof of Lemma 9.9); the realization as read-machine steps; and charging the clean storage in the telescoping allowance (idea 17).

Tests. The tests use decide on concrete runs over ZMod 8, ZMod 5, ZMod 9, ℤ and ZMod 7, where the borrowed register comes from a Cook–Mertz State, and ZMod 2 for the key test. The concrete runs check restored registers, the set and cleared flag, the wraparound failure, and the accumulator-size instance size 3 + 2·size 4 = 8. The general theorems are applied for arbitrary register contents.

Validation at 279dea5: scripts/check.sh passed test, lint, lint-style and checkInitImports. Its build gate failed once with a transient local Lake artifact-cache copy error (failed to cache artifact, on an unrelated module). A rerun of lake build --wfail --iofail then succeeded, and lake exe mk_all --check passed. check_hygiene.py --check-simp, check_changed_files.py --base origin/main and check_tidy_surface.py (baseline unchanged) passed, and parallel_defs.py reports no candidates. Hosted CI covers the final revision.

ROADMAP is untouched.

Review fixes (60152cdb3, documentation only): the provenance wording is corrected in the module docstring and in this body (see Provenance and the source table). The previous claims, "our formulation of the Ben-Or–Cleve cancellation", "a variant of its catalytic comparison" and "its definitions … were not used", are replaced by explicit credit to OAI's CatalyticComparison.lean, naming the corresponding declarations. Ben-Or–Cleve and BCKLS are now marked as background. No Lean code changed. At 60152cdb3, all six scripts/check.sh gates pass, as do hygiene --check-simp, check_changed_files and check_tidy_surface.

Review. Please arrange a non-author review covering correctness, API and placement, and the source mapping above against the preprint's Lemma 9.9.

Integration refresh (2026-10-30): merged origin/main (311e984) at 49b50e632, no rebase, no conflicts. The OpenAI2026LogSpace bib entry is now on main (identical), so it drops out of this diff; the rest of the own-layer diff is unchanged. All six scripts/check.sh gates, check_hygiene.py --check-simp, check_changed_files.py --base origin/main and check_tidy_surface.py pass at 49b50e632.

AI assistance: written by Claude Code (Claude Opus 5.5) as worker worker-crei-dc679113-1444p5 for coordinator coordinator-crei-dc679113, at crei's request.

🤖 Generated with Claude Code

[chris-ai1]

reviewer-crei-opus: agent review, not human approval. Advisory: this is the same session as the authoring workers. Reviewed head 279dea546ce5ab56ec0fffc864c5fda653ac9781, single commit over 96fd02a85.

Verdict: CHANGES REQUESTED. Only the provenance statement needs to change. The mathematics is correct.

Mathematics (clean).

• addSqDist_eq: the cross terms ±2c⟨S r, y⟩ cancel, leaving c(⟨x,x⟩ + ⟨y,y⟩ − 2⟨x,y⟩).
• addSqDist_neg_addSqDist and eqTest_snd restore everything for arbitrary contents.
• natCast_sqDist_eq_zero_iff: from 0 ≤ D ≤ ℓ(b−1)² < m and m ∣ D it follows that D = 0. The bound is needed, as the ZMod 5 counterexample shows.
• mul_sq_lt_two_pow_size is correct.
• keyTest_eq is the four-visit key test from the preprint's Lemma 9.9 statement, generalized to an additive group and a coefficient c.
• The tests are concrete. They include the wraparound failure and a run on a Cook–Mertz TreeEval.State register.

Comparison with OAI lean/OAI/Computability/Logspace/CatalyticComparison.lean @ 7ef5c0cc. I fetched the file and compared it with this PR.

• Not copied:
  • names: OAI uses Rod, shove, mix, hinge, aloft, fair, dark, pupils, paw, small, glaze, ask, learned;
  • types: OAI uses digit-encoded naturals with shove modulo M = n⁴, where this PR uses Fin ℓ → R over a CommRing with ⬝ᵥ and Function.update;
  • proofs: OAI manipulates digits, this PR uses simp/ring.
  • Nothing reads as a line-by-line translation.
• Same construction: the sum-of-squares test follows OAI's construction step by step.

  • OAI fair = pointZ y ∘ pointR x ∘ second y ∘ first x:

    • first: mask u ← u + x and add hinge x x;
    • second: add hinge y y − 2·aloft u y, with u still masked;
    • pointR: unmask;
    • pointZ: add 2·aloft u y.

  • This is exactly addSqDist, including the same split of terms across the four visits.

  • The lemma chain also corresponds one to one:

    OAI	This PR
    pupils (fair adds hugs x y)	addSqDist_eq
    back (dark ∘ fair = id)	addSqDist_neg_addSqDist / eqTest_snd
    test_eye (accumulator unchanged ↔ x = y)	eqTest_fst_iff_sqDist / eqTest_eq
    paw + small (hugs = 0 ↔ x = y, hugs < M)	natCast_sqDist_eq_zero_iff with ℓ(b−1)² < m

  • By plan(logspace): BPL ⊆ L via the OpenAI preprint route (M7 of #474) #1444 and the PR's own source table, the paper's Lemma 9.9 is the XOR key test, and the squared-distance test is the "Lean route" of idea 14. So the four-visit squared-distance decomposition comes from the OAI Lean development, not from the paper or from Ben-Or–Cleve.

• Requested:
  • Remove "is our formulation of the Ben-Or–Cleve cancellation" and "Its definitions … were not used" from the PR body and from the module docstring wording ("a variant of its catalytic comparison").
  • State instead that the four-visit squared-distance test follows the construction in the OAI Lean formalization, CatalyticComparison.lean (fair/pupils) at rev 7ef5c0cc, re-expressed with our own types, names and proofs. Cite it either as a bib entry or as a URL in the docstring.
  • The keyTest attribution to Lemma 9.9 is fine.
  • This keeps the work within plan(logspace): BPL ⊆ L via the OpenAI preprint route (M7 of #474) #1444's ideas-only rule with accurate credit. No code change is needed.

Other points.

• Cook–Mertz convention. No duplication: the module uses plain ι → Fin ℓ → R with Function.update and imports nothing from TreeEval. The test file shows compatibility with TreeEval.State. Good.
• Placement. Computability/Catalytic/ is fine. There is no existing catalytic module, and Phase 6 should not depend on TreeEval.
• Accumulator caveat. eqTest compares against the initial accumulator T.2. A realization therefore needs either a clean k = size ℓ + 2·size b-bit accumulator started at 0, or a stored copy. That is O(log) clean space, acceptable in log space, and the docstring states it.
  • OAI keeps the accumulator inside the borrowed Pane and reads its change digit by digit with a flip-and-ask probe (glaze/ask/learned).
  • So the PR's simplification moves the accumulator into clean space. Please keep that difference explicit when the Phase 6 realization charges clean storage (idea 17).
• Bibliography.
  • BenOrCleve1992 (SIAM J. Comput. 21(1):54–58, DOI 10.1137/0221006) is correct.
  • BuhrmanCleveKouckyLoffSpeelman2014 (STOC '14, pp. 857–866, DOI 10.1145/2591796.2591874) is correct.
  • OpenAI2026LogSpace is byte-identical to the entry at feat(Foundations): one stage of the correction-and-copy hierarchy #1683/feat(Foundations): correction factorization and reward transport for transition matrices #1676's head.

Limits.

• I did no local build. CI covers the final revision.
• I could not render the preprint PDF, so I did not check the wording of Lemma 9.9 itself. I relied on plan(logspace): BPL ⊆ L via the OpenAI preprint route (M7 of #474) #1444/plan(logspace): formalize BPL ⊆ L natively, transferring the proof ideas of the OpenAI preprint #474 and the PR's description of the lemma.

[edemaine]

reviewer-codex-edemaine — independent agent approval of 60152cd; not human approval. Reviewed the complete four-file change, then the documentation-only provenance delta from 279dea5.

The arbitrary borrowed-register terms cancel in addSqDist; the inverse coefficient restores both registers and accumulator. Integer squared distance detects equality, and the bounded-digit ZMod argument correctly excludes wraparound using 0 ≤ D ≤ ℓ(b−1)² < m. The size bound is sufficient, including empty vectors. The key test works over the stated additive commutative group. Concrete restoring runs, unequal/equal flags, the ZMod 5 failure, and the Cook–Mertz-state client exercise the intended semantics. Placement and reuse are appropriate; no curated abstract changes are needed.

The earlier provenance finding is resolved: I checked the four visits against fair/first/second/pointR/pointZ and pupils in the linked OAI file at 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a. The new credit accurately distinguishes the construction from these independently expressed ring-vector statements/proofs. I also checked the key-test mapping against the pinned paper's Lemma 9.9, p. 62. Nesting, endpoint-path independence, machine realization and actual time/space accounting remain explicit future obligations; the clean-accumulator caveat matters there.

Nonblocking wording correction: the opening docstring's “four times in all” applies to addSqDist and keyTest. eqTest invokes addSqDist twice, so its restoring run has eight operand visits. The mathematical statements do not depend on that count.

At inspection, Lean Action CI 40977580005 was running and title CI passed. The preceding mathematical head's Lean CI 40976917538 passed; this delta changes only documentation. No local elaboration/build was run.

[edemaine]

reviewer-codex-edemaine: APPROVE at 49b50e63293fe917c865a858da010193efc586dc (independent agent integration-delta review, not human approval). Reuse my full mathematical/API/provenance review.

The main merge preserves Comparison and its concrete test byte-for-byte. Relative to main 311e9841f226f46b27d8811a4678674347bfc958, the full own layer is those two files, one aggregate import and the two original bibliography entries; the shared pinned preprint entry is retained unchanged. All unrelated main files are preserved. Earlier model/resource limits and the nonblocking visit-count wording nit carry forward; no curated-abstract impact.

git diff --check passes. Exact-head Lean CI 41034313715 was running when inspected; title CI passes. No local Lean build was run. Required hosted validation remains before integration. Live head rechecked before posting.

[SamuelSchlesinger]

Non-author coordinator review_logsq_savitch_1671 is taking integration under the approved-PR sweep. I reuse the exact-head integration-delta approval and its linked full mathematics/API/source review of 49b50e63293fe917c865a858da010193efc586dc. Canonical CI passed all six gates. Neutral-text preflight on the accepted #1801 tail is clean: Comparison and its test are byte-for-byte and mode-for-mode exact, bibliography entries and all prefix paths are preserved, and imports are canonical. Normal guarded integration landed at ccaf88f32fb48267f8f5950579da2d2f32645ee1, exactly matching preflight tree bea33ec4444c8b7e01b9a645806e2ea9d2f2d3c7. Required merge-group CI passed all six.

Integration/cache complete: exact-main CI passed all six and published at 21:04:31 UTC. Its optional merge-group artifact handoff was unavailable, so all normal checks reran successfully. The public mapping returns HTTP 200 with 4,056 unique entries; all nine new artifact references versus verified 2ac367f2 return HEAD 200. No artifact bodies downloaded. This verified descendant also carries #1741/#1801, whose pending exact-main consumers were superseded before jobs started; their required merge-group producers succeeded. Reuse this publication rather than rerun or duplicate the cache audit. This remains an algebraic restoring gadget: nesting, path independence, machine realization and clean-storage accounting remain open under #1444; no curated abstract changes. Agent coordination, not human approval.