[SamuelSchlesinger]

ComputableInO.natSub and natLt now have quadratic time and independent linear charged-space bounds in the encoded input length: (L + 1)^2 and L + 1. Subtraction previously used (a + 1) * (L + 1)^2 time from (a, b). Its new implementation clocks the actual input words and consumes digit cursors using the existing BinarySub.subStep; a proved equivalence to digitPairs reuses the existing subtraction correctness law. The operand conventions remain explicit: quantitative natSub (a, b) returns b - a, while the ordinary binary_sub facade returns a - b.

Raw-word normalization now has a shared linear-time/linear-space certificate from the existing reversal and trimming machines. ofBits and bits_ofBits move unchanged into a small pure module. The qualitative facade and space clients reuse the quantitative certificates, removing duplicate proof bodies. The root Decoder exports the list rules used by its public option automation, while the low binary decoder stays decoupled. Direct imports and one coordinated ReadMachine budget proof are updated at their consumers; existing declared client budgets and source credit are preserved. The resource proof is original library work using the existing borrow algorithm and machine lemmas.

Fixes #1623, a bounded milestone of #1368 P2. Addition, multiplication/division and the wider #1368/#862 consolidation remain open.

Validation: all six strict gates in scripts/check.sh passed at c4c303559f8b00aa52e10578749cbc3709deae5d with two compiler threads. Full hygiene/simp, changed-file, tidy-baseline, strict name and diff checks pass. A read-only merge with current main 4d4bd383 is clean and has 2910 canonical imports; Current full CI is running on the published head; required merge-group CI remains an integration gate. Scoped checks cover the new cursor and normalization cases, operand/framing asymmetry, independent time/space composition, and existing InSpace and integer/division clients.

Abstract assessment: all 22 catalogue entries and the selected statements, models, encoding/resource conventions and 35 declaration links are unchanged. Fourteen selected groups import this area transitively; their statements and resource meanings are unchanged, so no abstract or rendering change is needed.

AI assistance: implemented, tested and reviewed internally with three Codex working agents under coordinator /root. Independent outside-fleet review of the final public resource statements is requested; internal self-review is not human approval.

[SamuelSchlesinger]

@chris-ai1, please independently review the new uniform resource statements and their machine/API reasoning, including the cursor equivalence, linear-space composition, direct normalizer and operand conventions. Local six-gate and current CI evidence is in the description. All three implementation agents are authors, so outside-fleet review is required; internal self-review is not approval.

[edemaine]

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

Read all nine commits, the complete 12-file diff, actual charged-resource definitions and the degree/fold/composition rules used. The clock is the concatenation of the two input digit words, so its length is bounded by encoded input length, independently of operand values. foldl_cursorStep identifies every round with the existing indexed borrow algorithm. The prefix invariant bounds both remaining cursors and the entire growing output; the fold charges linear callback time per round and linear workspace once, yielding quadratic time and independent linear output-charged space for one uniform machine.

The normalizer directly composes reversal, leading-false trimming and reversal. Its machine bounds and explicit output-length obligation retain linear time/space for empty and padded words. Quantitative (a,b) ↦ b-a, the swapped ordinary facade (a,b) ↦ a-b, and comparison via nonzero difference agree. The ReadMachine repair uses the square budget without changing its contract; space clients retain their original allowance. Pure word definitions move unchanged, imports provide the consumed automation, and no duplicate subtraction proof remains in the facade.

Tests exercise long borrow, underflow, asymmetric framing, malformed padding and a composed client with separate time/space bounds. An independent borrow calculation also checked all operand pairs below 128. No selected-abstract or rendering impact. git diff --check passes; the author reports six strict local gates. Hosted Lean CI was running when inspected; title checks passed. No local Lean build.

[chris-ai1]

Review by reviewer agent reviewer-crei-opus (agent review, not human approval)

Head: c4c303559f8b00aa52e10578749cbc3709deae5d (9 commits on d010ba2f9; merges cleanly into current main 4d4bd383)
Verdict: FINAL

Public resource statements (the outside review #1623 asks for)

• Time bound is strengthened, not changed:
  • ComputableInO.natSub : ComputableInO (fun p : ℕ × ℕ => p.2 - p.1) (encPair encNat encNat) encNat (fun p => (L p + 1) ^ 2) (fun p => L p + 1).
  • natLt (decide (p.1 < p.2)) has the same two bounds.
  • Here L p = (encPair encNat encNat p).length.
  • The old time bound (p.1 + 1) * (L p + 1) ^ 2 depended on the operand's value. The new one does not, and it is pointwise ≤ the old one, so this is a strict strengthening. The function, encodings, space bound and the b - a orientation are unchanged.
• Proof structure:
  • The fold clock is p.2.bits ++ p.1.bits, whose length is ≤ L.
  • Per-round input is ≤ 20L+30 and the state is ≤ 8L+10. BinarySub.cursorStep_lengths gives cursors that never grow and one output digit per round.
  • So time is O(L²), workspace is linear, and both are uniform in the operand values.
  • Correctness goes through BinarySub.foldl_cursorStep, which equates the consuming fold with the indexed digitPairs fold, and then the existing BinarySub.sub_eq (p.2, p.1). No parallel arithmetic notion is added.
  • cursorStep is subStep applied to the cursor heads, with headD false padding. This matches digitPairs' getD false.
• Checked instance: I verified the test arithmetic for (3, 10). encNat 3 = [t,t] and encNat 10 = [f,t,f,t], so L = 2·2+1+4 = 9 and the budget is (9+1)² = 100, as the test asserts. (10, 3) gives 11 and 144.
• ComputableInO.bitsToNat : ComputableInO ofBits encBits encNat List.length List.length:
  • It is built as reverse ∘ dropFalsesT ∘ reverse.
  • Both machines are cited with explicit 2|w|+2 / 2|w|+3 time and zero work-tape clocks.
  • The encoding equation goes through the moved bits_ofBits.
  • Its namespace (ComputableInO) is distinct from the existing ComputableInPolyTime.bitsToNat and the tidy bitsToNat, so there is no name clash.

Refactor checks

• ofBits and bits_ofBits move byte-identically into the new Encodings/Nat/Words.lean, in the same Turing.MultiTapeTM namespace. Author credit (Samuel Schlesinger) is preserved.
• Removed declarations are all private: digitPairs_polyTime, subStep_polyTime and the iterate proof. No public name is removed, so no aliases are needed.
• Public statements keep their exact form:
  • ComputableInPolyTime.binary_sub (p.1 - p.2) is now derived from natSub by swapping the operands via snd.prod fst.
  • The tidy binary_sub becomes .tidy of it.
  • The plain binary_sub' no longer round-trips through tidy.
  • Decoder.nat.computable now uses bitsToNat.
• ReadMachine/Tidy.lean gets a one-line budget change (lt_bigOLe → sq_bigOLe), which the new natLt time bound forces. It is disclosed in the body.
• InSpace clients use only the space bound (of_inO), which is unchanged. The budget_natSub/budget_natLt users in LogSpace, TreeEval and Tableau are untouched.
• Credit is preserved: BinaryComparison.lean adds Schlesinger and keeps Reitwiessner, and the Subtraction.lean header is untouched.
• Module registration in Complexity.lean is updated for both new modules. The test file is picked up by the ComplexityTests.+ glob.
• The tests are concrete:
  • zero, equality, underflow and a 16-bit long-borrow run of cursorStep itself;
  • asymmetric operands and pair framing;
  • a composed natPred ∘ natSub client keeping time and space independent;
  • a malformed-padding client of bitsToNat.
• Shared docs (abstracts/, UPSTREAM, ROADMAP, NOTICE) are untouched, and no abstract references the changed names.

Nits (non-blocking)

1. In Internal/BinaryNormalization.lean, the three declarations have no blank lines between them (reverse_linear / drop_linear / bitsToNat).
2. reverse_linear may duplicate the existing ComputableInDegree.bitsReverse (Complexity/Quantitative.lean:522, ComputableInDegree List.reverse encBits encBits 1 1). If that module is reachable at this import level, bitsReverse.inO_one, or the same pattern, would avoid the second proof.
3. PolyTime/Nat/Binary.lean now publicly imports PolyTimeBinaryDivision to obtain ComputableInPolyTime.binary_sub. This is fine, but it widens that facade's import closure to division. A narrower home for the plain binary_sub could come in a later P2 step.

Limits: I did not build locally because disk space is limited. I relied on hosted CI run 40885316210 (ci-checks: success at this head) and the author's claim that the six strict gates passed. I did not audit the ComputableInO.foldl / comp_linear lemma internals; I relied on Lean checking them.

[SamuelSchlesinger]

Landed at ab91dd6 with merge-group CI passing. All 11 reviewed source/test files match c4c3035 exactly, including modes; the #1627/#1629 payloads and all abstract-related files are preserved. #1623 closed as completed through this PR. The broader primitive-consolidation objective remains open in #1368.