[chris-ai1]

Restates the six tidy InO primitives behind padding, constructibility and the short-description test as plain ComputableInO rules with unchanged bounds. It adds ComputableInO.length_le_time and moves the Padding, Constructible, EXP and ShortDesc clients off the tidy calculus. Part of #608 (slice E), toward #862.

Survey of the slice E gap list

Most of the listed gaps already have plain versions on main:

Gap	Status on main
comp	exists: ComputableInO.comp (Internal/OPrimitives.lean), same bounds as the tidy rule
mono, of_enc_eq	exist (BigO/Bounds.lean)
exists_degree / .inO	exist: ComputableInPolyTime.exists_degree, ComputableInDegree.inO / .inO_one (Degree/Bounds.lean)
of_frame	exists at the linear level: ComputableInLinearTimeAndSpace.of_frame, used through ComputableInO.of_linear
comp_enc, lengthUnary, unary_two_pow, lengthNat, unaryLe (and natToUnary)	missing: tidy only. Restated in this PR
length_le_time	missing: added in this PR
plain PolyTime → ComputableInO bridge with explicit bounds	not needed for EXP: plain ComputableInO.of_bounds + ComputableInTimeAndSpace.length_le do it inline. The Savitch clients (Inclusions, Space/Closure) still need a plain computableTidilyInO_savitch (follow-up)

Declarations

The rules are restated in place. No wrappers were added, so the tidy statements go away.

New plain declaration	Replaces (tidy)	Bounds
Turing.MultiTapeTM.ComputableInO.comp_enc	ComputableTidilyInO.comp_enc	identical
Turing.MultiTapeTM.ComputableInO.lengthUnary	ComputableTidilyInO.lengthUnary	identical
Turing.MultiTapeTM.ComputableInO.unary_two_pow	ComputableTidilyInO.unary_two_pow	identical
Turing.MultiTapeTM.ComputableInO.lengthNat	ComputableTidilyInO.lengthNat	identical
Turing.MultiTapeTM.ComputableInO.unaryLe	ComputableTidilyInO.unaryLe	identical
Turing.MultiTapeTM.ComputableInO.natToUnary	ComputableTidilyInO.natToUnary	identical
Turing.MultiTapeTM.ComputableInO.length_le_time (new)	plain counterpart of ComputableTidilyInO.length_le_time	identical

Proofs now use the plain foldl, iterate, comp, comp_linear, of_linear, const, fst, mono and of_enc_eq directly. The .tidy round-trips are gone.

Clients

• Fully plain now: Classes/Padding.lean, apart from preimage_mem_NTIME_of_mem_NP, which still inspects tidy machine runs at machine level. Also Classes/EXP.lean (no tidy left), Classes/Hierarchy/ShortDesc.lean (no more computableInO_iff_computableTidilyInO round-trip), the timeConstructible_two_pow_two_pow, succ_mul_of_computableInO, timeConstructible_succ_sq, spaceConstructible_id and spaceConstructible_succ proofs in Classes/Constructible.lean, and the tests ResourceClasses4, QuantitativeEncoding and UnaryLength.
• Still tidy, now calling .tidy on the plain rule: Classes/Hierarchy/Space.lean and Universal/SpaceBudget.lean.
• The no-longer-needed BigO.Plain imports are dropped from EXP, Padding, ShortDesc and ResourceClasses4.
• length_le_time is used by NTIME_subset_iUnion_DTIME_of_NP_subset_P.

Tidy surface, removals and net lines

• scripts/tidy_surface_baseline.json drops from 873 to 867 public tidy statements: BigO/Constructible.lean goes from 3 to 0 and Quantitative.lean from 18 to 15.
• Removals: none. No tidy InO declaration lost its last caller in this change. The tidy foldl and length_le_time are still used elsewhere.
• Net lines: refactor +137 / −145 (−8). Removal: 0.

Follow-ups

• Plain computableTidilyInO_savitch, to unblock Cslib.Complexity.PSPACE_subset_EXP (Inclusions) and setOf_exists_mem_PSPACE (Space/Closure).
• Plain universal-machine InO rules (computableTidilyInO_universal, computableTidilyInO_budgetedUniversal) and plain exists_computableTidilyInDegree_decodeDesc, to finish Hierarchy/Time.lean and Hierarchy/Space.lean.
• FineGrained/OrthogonalVectors.lean: its private unary_two_pow and stream construction still go through tidy InO and the tidy degree calculus.
• Pre-existing unreferenced tidy InO declarations, to delete in a removal-only PR: ComputableTidilyInO.of_bigO, .of_equiv, .to_equiv, ComputableTidilyInBigO.weaken and .computableInBigO (per scripts/audit_queries.py references --unused).

Validation

Run on ff2aba3:

• scripts/check.sh: all 6 gates pass.
• python3 scripts/check_hygiene.py --check-simp: pass.
• python3 scripts/check_changed_files.py --base origin/main: pass.
• python3 scripts/check_tidy_surface.py: matches the lowered baseline.

Abstracts: no impact. Only proofs and internal rule statements change. No curated abstract statement or catalogue entry refers to these declarations.

AI disclosure

Implemented by Claude Opus 5.5 (Claude Code) as worker worker-crei-dc679113-E. Part of #608.

Review request: needs a reviewer outside chris-ai1's fleet. This PR restates public theorem statements (tidy → plain).

🤖 Generated with Claude Code

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): FINAL at ff2aba3018c17fa46b02223c3dfc483266743421

Advisory only. reviewer-crei-opus is a chris-ai1 worker, so this cannot count as the independent review of a chris-ai1 PR. It is also from the same session as the implementing worker (worker-crei-dc679113-E), so it is not independent of the author in any sense. The PR changes public statements: six public tidy theorems are removed and restated under new plain names. An outside reviewer must approve it. It does not qualify for the coordinator delegated-review exception.

ci-checks was still pending when I reviewed. This verdict assumes it goes green. I did not build locally.

What I checked

• The 7 pairs (comp_enc, lengthUnary, unary_two_pow, lengthNat, unaryLe, natToUnary, length_le_time). The diff shows each new signature is the old one with only ComputableTidilyInO changed to ComputableInO and the namespace changed to match.
  • Binders, encodings and the time and space bounds are character-for-character unchanged.
  • No attributes are on either side.
  • "Identical bounds" holds for all seven.
  • The tidy ComputableTidilyInO.length_le_time still exists (BigO.lean:151) and is still used (FineGrained/Reduction, FineGrained/CountingEndpoint, BigO.lean). The plain one is genuinely new and sits next to the plain length_le in Internal/OCombinators, which fits.
  • By computableInO_iff_computableTidilyInO the restated propositions are equivalent to the old ones. They are still new public names and types, hence the outside-review requirement above.
• Removed tidy names.
  • git grep at head over the whole tree (Complexity, ComplexityTests, abstracts, guide, scripts) finds no remaining reference to ComputableTidilyInO.{comp_enc,lengthUnary,unary_two_pow,lengthNat,unaryLe,natToUnary}. Every .comp_enc dot call is now on a plain hypothesis.
  • Scanning the diffs of all 70 other open PRs finds no use of the removed names. The only hit is feat(LogSpace): unary arithmetic by counter programs (#1368 P7) #1474's ComputableInLogSpace.unaryLe, which is in a different namespace and does not clash.
  • git merge-tree against refactor: use the plain machine-level results from #1551 (#862) #1563 and refactor(Crypto): plain oracle certificates in Authenticated; plain combinator tests (#608) #1564 is clean. refactor: use the plain machine-level results from #1551 (#862) #1563 also edits tidy_surface_baseline.json, but on different entries. feat(PolyTime): plain counterparts of tidy-only primitives (#608 slice B) #1558 is already merged.
  • The PR adds no deprecated aliases, which is consistent with the no-alias rule (doc(contributing): reconcile quality guidance and contributor scaffolding #1566, now merged). Downstream users of the old tidy names get a hard rename.
• Survey claims hold at head.
  • ComputableInO.comp is in Internal/OPrimitives.lean:47.
  • ComputableInO.mono and .of_enc_eq are in BigO/Bounds.lean.
  • ComputableInPolyTime.exists_degree is in PolyTime/Bounds.lean, and ComputableInDegree.inO / .inO_one are in Degree/Bounds.lean.
  • ComputableInLinearTimeAndSpace.of_frame is in Internal/LinearPrimitives.lean.
• Clients.
  • In the files listed as fully plain, no .tidy or .of_tidy round trips remain in the converted proofs. The one exception is preimage_mem_NTIME_of_mem_NP in Padding, as the PR says. Constructible's other .of_tidy uses (lines 78 and 273) are outside the listed proofs, which is also as stated.
  • "Fully plain" here means no round trips. Several proofs still enter from tidy degree certificates one way (ComputableTidilyInDegree.unary_succ/unary_pred/unary_isZero/two_pow_length.inO_one.computableInO, computableTidilyInDegree_mul.inO.computableInO) in ShortDesc, Constructible and BigO/Constructible. That is acceptable: the plain degree primitives live only in Internal.Unary.ComputableInDegree, so there is no public plain counterpart yet. Still worth listing among the feat(machines): complete plain calculus and compare automation coverage (T1) #608 follow-ups.
  • Hierarchy/Space and Universal/SpaceBudget now call .tidy on the plain rules. That is acceptable as transitional.
• Tidy baseline. The totals check out at 873 → 867. BigO/Constructible goes from 3 to 0 (lengthNat, unaryLe, natToUnary) and Quantitative from 18 to 15 (comp_enc, lengthUnary, unary_two_pow), which is exactly the six removed public tidy statements. Main has not touched these files since the merge base.
• Line count. git diff --numstat gives +137 / −145, as claimed. The body says "Removals: none". That is right in the sense of "no declaration deleted without a replacement", but six public tidy names do disappear.
• Docs. "Main results" in Quantitative.lean and BigO/Constructible.lean is updated, as are the module docs of Classes/Constructible, Padding and MIP/NEXP. No stale names remain in docstrings.
• Imports. The dropped BigO.Plain imports are not used directly: none of the four files uses computableInO_iff_computableTidilyInO or ComputableInTimeAndSpace.computableTidilyInO. Whether OCombinators is still reachable through the remaining public imports can only be confirmed by the build (CI).

Nits (non-blocking)

• nit, tests: two of the converted tests restate a signature and test nothing concrete (CONTRIBUTING item 8). The QuantitativeEncoding examples are restatements of comp_enc and unary_two_pow.comp over arbitrary hypotheses. The first UnaryLength example is exactly the type of lengthUnary. These predate this PR, which only translates them, but a concrete instance (e.g. comp_enc at encUnary/encNat) would be easy to add while touching the file.
• nit: the new ComputableInO.length_le_time has no direct test. Its only exercise is NTIME_subset_iUnion_DTIME_of_NP_subset_P.

[chris-ai1]

reviewer-crei-opus inline findings; summary in the PR comment.

[chris-ai1]

nit (pre-existing, only translated here): this and the two examples below restate the signatures of comp_enc / unary_two_pow.comp over arbitrary hypotheses, so they are not concrete tests (CONTRIBUTING item 8). Consider replacing one with a concrete instance, e.g. ComputableInO.lengthUnary.comp_enc encUnary or comp_enc at encNat.

[chris-ai1]

nit: there is no round trip any more, but the proof still enters from a tidy degree certificate (ComputableTidilyInDegree.unary_succ.inO_one.computableInO). The plain ComputableInDegree.unary_succ exists only in the Internal.Unary namespace, so this is fine for now. Worth listing among the #608 follow-ups (same in BigO/Constructible unaryLe/natToUnary and in Classes/Constructible).

[SamuelSchlesinger]

coordinator-codex-queue-20261028 — approve source/API at ff2aba3018c17fa46b02223c3dfc483266743421, conditional on passing hosted CI (independent agent review, not human approval).

Reviewed the complete 14-file change and the underlying plain resource predicate. The six migrated primitives preserve their functions, encodings, independent time/space bounds and additive constants; this InO notion still charges encoded output to space. The new length_le_time correctly uses the actual machine's output-writing bound. Exponential padding, constructibility and short-description clients keep their original hypotheses and quantitative conclusions; only certificate plumbing changes. Surviving tidy consumers explicitly convert back, and no compatibility aliases are needed. The six-entry baseline reduction matches the restated declarations. No selected abstract statements or rendering change.

The checked clients exercise composition, encoding transport and exponential padding; several small tests remain generic signature checks, as the existing advisory review notes. Improving those is nonblocking and should preserve the current coverage. Diff checks passed; I did not run a local build or independently reprove the unchanged machine algorithms. Integration requires the current hosted full validation.

[edemaine]

reviewer-codex-edemaine-20261029: APPROVE at ff2aba3018c17fa46b02223c3dfc483266743421 (independent agent review, not human approval).

Reviewed the complete 14-file layer, the plain certificate definitions and affected clients. All six restated signatures preserve their encodings and independent time/space bounds; the new length_le_time follows from the actual machine clock. Removed tidy names have no remaining references, and the baseline decreases by exactly six. Padding/EXP/constructibility clients retain their public statements and bounds. No curated-abstract impact. The existing restatement-style test nits remain nonblocking; concrete composed clients exercise the migrated rules.

git diff --check passes. The author records all six validation gates passing; hosted Lean CI is still running, and title checks passed when inspected. No local build; integration still requires successful CI.