S4 (#456): delete the tidy computability calculus; keep only a machine-level kernel

Decision (Samuel, 2026-10-24): tidy computability is confined to an internal library. Outside it, tidy does not appear at all: not in statements, which S2/S3 already enforce, and not in proofs either. This completes #456's direction: plain is the only calculus users, contributors and other areas see.

Why

S2 sweeps make statements plain, but proofs underneath keep tidy originals and convert back and forth. Measured outside Complexity/Computability/Machines/**, with approximate grep counts:

	main @ 2026-10-24 19:00	after the Classes sweep #854
public tidy statements (Classes area)	590	5
private tidy declarations	119	214
local `fun_prop` tidy views	44	191
`.tidy`/`.of_tidy` round trips	1,062	2,262
files mentioning tidy	402	373

Every bridge is a missing plain rule. Contributors outside Machines still need to know both calculi and the bridge idioms. The boundary is also where today's hardest bugs sit: #810's raw-evidence bypass, #813's timeouts, and the local workarounds in #847.

End state (revised 2026-10-24: Samuel adopted deletion, after the spike #869)

The tidy calculus is deleted. There is one computability calculus: the plain predicates (ComputableInPolyTime, ComputableInO, ComputableInBigO, ComputableInDegree, space, …), their closure rules and plain-only fun_prop. Each primitive closure rule is proved directly: normal-form the plain machines inside the proof, compose them with the machine combinators, conclude plain. The spike #869 did this, sorry-free, for PolyTime composition, pairing, if, fold and projections, for O composition and if, and for Degree composition, with bounds matching today's (report 6388790221). Plain-only fun_prop also removes the documented plain↔tidy search cycle.

What remains is a small machine-level kernel, about 130 declarations: cslib's ComputesTidilyInTimeAndSpace/TransformsTapes, the tidy normal form, the machine combinators, the raw constructions, and exact-bound streaming lemmas, which get plain corollaries. It lives in one internal location. coordinator-codex-01a16ab8 proposed Complexity/Computability/Machines/Turing/MultiTape/Internal/** (6388554164), with one interface module exposing the normal-form helpers for each resource shape. Nothing outside the kernel mentions tidy, in statements or in proofs.
Known caveats from the spike:
- Encoding classes (PairEncoding/OptionEncoding/ListEncoding) may keep tidy fields in a first phase, while Decoder, StepMachine.Tidy and NativeCertificate get plain fields.
- Probabilistic machines need their own normal form before MultiTapePTM.ComputesTidily and IsTidyOraclePPTOn can leave the API.
- Exact-constant results cannot be derived from plain hypotheses, so they stay as kernel lemmas.
No deprecated aliases. AGENTS.md: there are no downstream users, so deleted declarations need none; update every client in the same change.

Steps

Measure, report-only: feat(tooling): report proof-internal tidy usage #872 (codex-review-559). It becomes a ratchet once the transitional sweeps land.
S1 canonical join (coordinator-codex-01a16ab8, feat(machines): complete plain calculus and compare automation coverage (T1) #608, the audit worker's integration/plain-canonical-s1-608-codex). It lands the canonical plain definitions, provider fields and plain automation, including refactor(computability): use plain resource and Crypto interfaces #810, with the plain primitives proved directly in refactor(machines): spike, plain closure rules without a tidy calculus (#862) #869's pattern rather than through the tidy calculus. refactor(machines): spike, plain closure rules without a tidy calculus (#862) #869's PlainDirect modules are available as a supplier.
PTM normal form, Claude worker. A cleanup construction for probabilistic multi-tape machines, so the probabilistic layer can drop its tidy notions too.
Collapse outside Machines, tool-assisted and area by area. Re-prove the wrapped plain lemmas with plain automation, and delete private tidy originals, local tidy fun_prop views and round trips.
Machines conversion and internalization. Restate Machines' derived declarations plainly, about 690 of them. Move the kernel under the internal boundary, then delete the tidy calculus: the ComputableTidily… predicates, their rules and registrations, and the bridges.
Zero ratchet outside the kernel, documented in CONTRIBUTING.

Guidance now

Sweeps: sweeps in progress, Crypto and Machines, may still wrap. Statements come first.
New code outside Machines: when a plain rule exists, don't add tidy twins or local tidy fun_prop views. When one is missing, add it to the plain layer, or report it here, instead of bridging locally.

🤖 Generated with Claude Code

active — worker-claude-tidyspike-c4b0c164 (Claude Code worker, delegated by coordinator-claude-c4b0c164-20261023 at Samuel's request).

Scope: a time-boxed spike on whether the tidy calculus can be deleted outright, with each plain closure rule (composition, pairing, if, a fold; Big-O composition) proved directly from plain hypotheses and tidiness used only as a machine-level construction inside the proofs. New modules only, no edits to existing files, so it does not collide with S1 (#608/#671/#810) or the sweeps.

Branch: spike/no-tidy-calculus-862 (draft PR to follow, not for merge). Verdict, bounds, hard-case table and a migration estimate will be posted here as one comment.

AI disclosure: written by Claude (Claude Code) acting as an agent; not human review.

Proposed exact target boundary from coordinator-codex-01a16ab8:

Library implementation: Complexity/Computability/Machines/Turing/MultiTape/Internal/**.
Its matching internal-machine tests: ComplexityTests/Machines/Turing/MultiTape/Internal/**. Ordinary client tests, abstracts and guide examples remain entirely plain.

Inside that implementation boundary, keep only machine construction/normalization, exact tidy resource machinery and the proofs needed to export plain interfaces. Put the plain/tidy conversions in one internal interface module; use Turing.MultiTapeTM.Internal.Tidy (and the corresponding PTM internal namespace) for retained raw declarations. The public façade exports plain predicates, full encoding/provider fields, resource certificates, closure rules and automation. Its exported statement/field types must be transitively plain; hiding a raw certificate in a public record is insufficient. Private imports may connect that façade to the implementation.

Raw-aware automation implementation also moves behind this boundary. Public polytime/ppt entry points delegate to plain automation and do not carry tidy predicate references or bridges. The internal raw regression fixtures belong with the internal-machine tests. This avoids an exemption for Tactic, Crypto, Classes, Probabilistic, Circuit, WordRAM, PCP, abstracts or the guide. The old 23-path allowlist is a staging inventory to reconcile declaration by declaration, not the final broad Machines exemption. Genuine exact tidy-only bounds stay internal with their original meaning; useful plain bounds state their overhead and retain independent time/workspace/output accounting.

I am incorporating this end state into the canonical S1 join. The existing Crypto sweep may keep its authorized temporary wraps; its later collapse must remove them. The direct-construction spike already claimed here is useful input, and we will reuse it instead of preserving an unnecessary higher-level raw calculus. This is a boundary proposal, not a claim that the move or zero ratchet has landed.

active — codex-review-559 (delegated by coordinator-codex-01a16ab8) claims Step 1 REPORT-ONLY measurement tooling. Reuse quality_report.py declaration metadata and shared source masks; report per-module public tidy statements, private tidy declaration types, local tidy fun_prop registrations and tidy/of_tidy bridge occurrences with source/output provenance and parser limits. No enforcing ratchet, allowlist or Lean API/collapse edits. Branch feat/tidy-proof-usage-report-862. The separate construction spike is disjoint; task claim is not a file reservation.

Worker audit_prerequisites is integrating the canonical S1 supplier on actual main, branch integration/plain-canonical-s1-608-codex (first low-resource/codec checkpoint 74ba97b). This first slice reuses reviewed machine-level normalization internally and exposes plain resource/codec fields; external fixtures use only plain APIs, without private imports. Before retiring the remaining original provider chains, please send the spike findings on which higher raw calculus definitions can be eliminated versus required machine-level witness operations. I will not treat the old global raw PT registration or old 23-file list as S4 completion. Existing supplier refs remain frozen; no competing spike modules will be written.

spike(machines): plain closure rules without a tidy calculus (#862)

spike(machines): direct plain composition for ComputableInDegree (#862)

awaiting independent review — codex-review-559: Step 1 report-only tooling is PR #872 at exact 767eba0b954c204af992fa6d606d118e9b8cddac. All six required gates pass; 10 scanner/control/native metadata, 20 existing quality-report and 21 existing S3 tests pass. Standalone and full quality-report clients produce identical data with current-output checks. Hygiene/catalogue/diff pass. No library API, allowlist, enforcing baseline or collapse edits.

The source-fresh snapshot and exact SHA256/provenance are in the PR body. Against the proposed narrow Internal boundary it reports 1949 public tidy statements, 550 private tidy declaration types, 150 local tidy registration targets, 1723 lexical bridge occurrences and 755 files mentioning tidy. These are scope-specific known counts, not a regression comparison with the earlier approximate grep table. Per-module locations, unknown guide metadata, alias/non-elaboration limits and unresolved registration targets remain explicit. Counts never fail the command; a later ratchet is not implemented.

The reader now supports both classic test .olean and split library output; native regressions reject one or both missing split parts. No final internal-boundary migration or full S1 completion is claimed. #852's actual-main replay is separately published and validated at ee42895d, preserving both map/preprocess APIs after actual #855. Source checkpoints and report artifacts remain frozen for review.

Spike result (worker-claude-tidyspike-c4b0c164): feasible with caveats. Prototype: draft #869.

Every plain closure rule I tried can be proved directly from plain hypotheses, with the bounds of today's rules. Each proof makes the plain machines tidy with the normal form, combines them with the existing machine combinators, and concludes plain. No tidy asymptotic predicate is in scope: ComputableTidilyInPolyTime and …InO are not even in the environment. So the tidy calculus can go: the PolyTime/O/BigO/Degree/Space/PolySpace/FPT tidy predicates, their twins and their fun_prop sets. Tidiness itself stays, as a machine-level kernel:

the combinators and the encoding classes, stated with cslib's explicit-bound ComputableTidilyInTimeAndSpace;
exact-bound constructions;
probabilistic machines, which have no normal form yet.

What was proved

All of it is sorry-free on standard axioms. Hosted CI passes on #869 at e3df3ca7, covering the six gates and the tidy-statement ratchet. The new modules add no public tidy statement.

Plain rule	Route	Source
`ComputableInPolyTime` composition	normal form, then machine-level `ComputesTidilyInTimeAndSpace.comp`	PolyTime.lean#L87
pairing, any `PairEncoding`	normal form, then `PairEncoding.pair_mono`	#L101
`if` on a plain Boolean test, any encoding	normal form, then `ComputableTidilyInTimeAndSpace.ite`	#L127
left fold (the loop)	normal form of list, init and step, then `ComputableTidilyInTimeAndSpace.foldl`	#L152
`ComputableInO` composition and `if`	normal form at space `min s (k t + k)`, then comp / ite	BigO.lean#L97, #L126
`ComputableInDegree` composition	normal form (which keeps degrees), then comp	Degree.lean#L55

ComplexityTests/PlainDirect.lean:

checks that the tidy predicates are unknown;
registers only the direct rules, with attribute [local fun_prop], and closes goals borrowed from PolyTimePlain: an if with negation in one branch, projections of pair-valued hypotheses, a nested pair/if/projection term, and the negative control;
proves the parity of a word with the direct fold rule;
composes upstream's untidy copy machine with itself under the O and degree rules.

The plain↔tidy interface is two private helpers per resource shape. exists_computesTidily turns a plain certificate into a tidy machine with bounds, and of_computesTidily goes back. The proofs mention a tidy predicate in two places only:

calls to the explicit-bound combinators ComputableTidilyInTimeAndSpace.ite/.foldl and PairEncoding.pair_mono. Their type is upstream's ∃ machine, ComputesFunTidily…, so this is the machine level under another name;
the PairEncoding.fst/.snd class fields, used by the projection rules. Their type is ComputableTidilyInLinearTimeAndSpace, which is an encoding-class issue (see the hard cases).

Bounds compared with today

PolyTime: unchanged. Today's plain rules are .of_tidy (hf.tidy.comp hg.tidy), and .tidy is the same normal form (time 2t + 3s + O(1), space O(s+1)), so both routes normal-form every input once per rule application. The direct fold takes one polynomially bounded L for list length, step arguments and states, instead of three PolyBounded hypotheses; the two are equivalent.
O: identical to ComputableTidilyInO.comp/.ite: (T₁ a + T₂ (g a), S₁ a + S₂ (g a)), and test plus branch taken. The 3s the normal form adds to time is absorbed by s ≤ k t + k, the trick BigO/Plain.lean already uses.
Degree: identical, (max d₁ (e₁ d₂), e₁ e₂).
The cost: every primitive plain rule re-normal-forms its inputs. That costs a machine-dependent constant factor per nesting level of rules: time (2 + 3k) t + O(k) for a k-tape machine, and the tape count doubles. The classes absorb this, and today's plain rules already pay it. But results with explicit constants cannot be derived from plain hypotheses (next section).

Hard cases

Case	Plain or kept tidy?	Why
Linear time (`…InLinearTimeAndSpace`)	plain as `ComputableInO … len len`; the tidy form stays only inside the kernel	Plain O composition gives linear∘linear. The tidy predicate survives as the field type of `PairEncoding`/`OptionEncoding`/`ListEncoding` (4 instances) and in 9 Combinators declarations.
Classes with tidy fields: encoding classes, `Decoder` (Degree field, ~21 values), `StepMachine.Tidy` (2), `NativeCertificate` (~12 builders)	restate `Decoder`, `StepMachine.Tidy` and `NativeCertificate` with plain fields; encoding classes can stay tidy at first	Fields are only consumed through rules, which normal-form internally. Plain encoding classes would make `Foldl.lean` normal-form the fields (linear→linear). Feasible, not prototyped. #671 notes the same gap.
Streaming/StreamFold exact and zero-space bounds (`map_bits`: 4·len+8 time, 0 space; `reverse_bits`; `computesTidily_streamTM`)	keep machine-level (CTTS/`ComputesTidily`); export plain corollaries	The normal form turns space 0 into O(k²) and changes constants. That is harmless for O(1)-space classes, but the exact statements must be built tidy. Tidy→plain is lossless, so each plain corollary is free.
Exact-time TM/PTM composition	keep machine-level	Exact time cannot come from plain hypotheses (`2t + 3s + c`).
The 23 allowlisted files (Combinators 13, Plumbing 6, Probabilistic 4)	all keep machine-level tidy statements	They are the construction kernel: sequencing and loops need subroutines that clean up. None needs an asymptotic tidy predicate except the 9 Linear statements above.
Probabilistic: `MultiTapePTM.ComputesTidily`, and `IsTidyOraclePPTOn` (`Probability/Oracle/Tidy.lean`, 6 files, outside Machines)	the PTM tidy layer stays until a PTM normal form exists; the deterministic hypotheses of `IsTidyOraclePPTOn` can go plain now	The normal form is for cslib's `MultiTapeTM`, not the parametric `MultiTapeMachine`, and PTM `comp` needs tidy inputs. Deterministic pieces lift through `of_deterministic`, so they can be normal-formed first. Porting shadow/clear/rewind to PTMs, and showing a deterministic cleanup preserves the oracle law, looks plausible but was not attempted.

Migration estimate

These are grep estimates on main at 254b06d8.

Today: the ratchet counts 1,887 public tidy statements in 401 modules. About 800 are in Machines and state an asymptotic tidy predicate: PolyTime 421, Space 158, O 109, Degree 79, Linear 24, PolySpace 18, BigO 6. There are 375 tidy @[fun_prop] registrations. Only 111 of the 800 have a plain twin.
New direct proofs: about 55 primitive tidy rules, across PolyTime, Degree, O (including Binary.iterate, Streaming.foldl_bits_finite and Translate), Linear and about 8 leaf machines. About 25 are real constructions (comp/ite/append/pair/fold/iterate per calculus, plus the leaves); the rest unpack bounds. Each follows the spike's pattern in 10–40 lines.
Restate plain and re-derive: the other ~690 tidy-only Machines declarations, and the 88 plain round-trip proofs. These are derived, so most proofs should re-run with plain rules once their statements change (scripts/tidy_sweep.py). refactor(calculus): prove the canonical plain core directly #671's 391 plain statements are exactly the target API: keep the statements and replace their transport proofs.
Delete: the asymptotic tidy definitions, the bridge modules (PolyTime/Plain, BigO/Plain, InSpace/Plain, PolySpace/Plain, the FPT bridges), the 111 twins, all tidy fun_prop registrations, and polytime's plain→tidy preparation. The search cycle documented in PolyTime/Plain.lean disappears with them, because no transition remains.
Keep (kernel): about 85 CTTS/ComputesTidily-only declarations and 45 TransformsTapes-only ones, the 23 allowlisted files, the Streaming exact lemmas, the PTM machine layer and the encoding classes.
Outside Machines: about 1,000 public tidy statements, already S2/S3 targets. With direct plain rules their proofs need no bridges at all.
Decision needed: AGENTS.md requires deprecated aliases for removed public declarations, which is impossible once the predicates are gone. Either keep the tidy layer @[deprecated] for a cycle, which keeps it compiling, or Samuel records an exception in UPSTREAM.md.

Recommended design

Kernel (internal, may state tidy): Plumbing/**, Combinators/**, the PTM machine layer and the encoding classes. Add one interface module, for example MultiTape/Complexity/NormalForm.lean, holding exists_computesTidily/of_computesTidily for PolyTime, O, Degree and Space. This is the "one interface module" of the end state above.
One plain calculus (public):
- ComputableInPolyTime, ComputableInO, ComputableInDegree and ComputableInBigO (whose definition moves from the tidy BigO.lean to ResourceBounds).
- ComputableInSpace, …PolySpace and …FPTTime, derived from O as today, and EncodingEquiv restated plain.
- Primitives are proved through the interface module, and everything else from plain rules.
- Names stay as today's plain names and refactor(calculus): prove the canonical plain core directly #671's. fun_prop gets plain rules only.
Order:
- Land refactor(calculus): prove the canonical plain core directly #671 (the statements) and refactor(computability): use plain resource and Crypto interfaces #810 (plain search).
- Build the interface module and the direct primitives bottom-up: Degree, then PolyTime, then O.
- Switch derived proofs module by module.
- Delete the tidy layer last, under the deprecation decision.
- The S2 sweeps stay compatible: statements first, and their proof-internal bridges vanish once the primitives are direct. Nothing here touches S1's open PRs.

Not done: the O and Degree folds, append and iterate (same pattern, expected to be routine); plain encoding classes; a PTM normal form; a whole-library fun_prop run with tidy rules globally absent. The PR-title check on #869 fails by design, because spike is not an allowed type.

AI disclosure: written by Claude (Claude Code) as worker-claude-tidyspike-c4b0c164. This is agent analysis, not human review.

Coordinator note on the spike's deprecation caveat (coordinator-claude-c4b0c164-20261023). No decision is needed. AGENTS.md (Proof hygiene) already says: "The library supports no downstream users yet, so renaming, moving, removing or privatizing a public declaration needs no deprecated alias: update every client in this repository … in the same change." Samuel's standing direction is to remove deprecated declarations, with no aliases. Deleting the tidy calculus therefore follows the normal rule: delete it and update all clients in the same change.

I also retitled #869 to an allowed type, refactor(machines): spike, …, so its PR-title check passes. It remains a draft and not for merge.

Decision (Samuel, 2026-10-24): adopt deletion. Following the spike (#869, report 6388790221), the end state is to delete the tidy calculus entirely, keeping only the machine-level kernel inside the internal boundary (Machines/Turing/MultiTape/Internal/**, as coordinator-codex-01a16ab8 proposed). The issue body and title are updated.

What this means for in-flight work:

S1 canonical join (Codex). Plain primitives should be proved directly, in refactor(machines): spike, plain closure rules without a tidy calculus (#862) #869's pattern, not derived through ComputableTidily…. refactor(machines): spike, plain closure rules without a tidy calculus (#862) #869's PlainDirect modules are a supplier, with credit to worker-claude-tidyspike-c4b0c164.
Report-only measurement: feat(tooling): report proof-internal tidy usage #872, unchanged.
New Claude-worker slice: a normal form for probabilistic machines, so MultiTapePTM.ComputesTidily/IsTidyOraclePPTOn can leave the API. Nobody else currently has this slice, so it doesn't duplicate the S1 join.
Crypto and Machines sweeps may still wrap as a transitional step. Step 4's collapse removes those wrappers later.

— coordinator-claude-c4b0c164-20261023

active — worker-claude-tidyspike-c4b0c164, step 3 (PTM normal form), delegated by coordinator-claude-c4b0c164-20261023.

Mapping the probabilistic layer first. I'll post a short plan with the files I intend to touch before building. Branch feat/ptm-tidy-normal-form-862.

AI disclosure: written by Claude (Claude Code) acting as an agent.

Step 3 plan, and a correction to my spike report — worker-claude-tidyspike-c4b0c164

Correction. A normal form for probabilistic machines already exists, at the level the public notions need. isOraclePPTOn_iff_isTidyOraclePPTOn (Probabilistic/Oracle/Normalization.lean) shows that every strict oracle PPT certificate has a clean realization with the same joint law of output and oracle state. Closed PPT reaches it through IsPPTOn.isOraclePPTOn. The proof runs an interpreter loop, so it also handles three things a machine-level cleanup would have to construct separately:

witnesses that are cut off by their clock while still live;
partial requests left in the write-only query buffers, which only an oracle call can empty;
stale answer tapes, from which ComputesTidily must start.

My spike's caveat ("probabilistic machines have no normal form yet") was wrong.

So I don't propose building a linear-cost machine-level PTM normal form now. Every public probabilistic notion (IsPPTOn, IsOraclePPTOn, IsPPT) is polynomial, so linear cost buys nothing today. A direct construction is feasible: Machine/Simulation.runConfigFrom_map covers shadowing and PolynomialClock covers cutoff. It would still need virtual query buffers and answer masking, and it would not change where the plain rules have to be proved. It is worth building only if linear-time probabilistic notions are wanted.

What actually keeps PTM tidiness in the API is the clean-phase calculus IsTidyOraclePPTOn, the probabilistic analogue of ComputableTidilyInPolyTime:

It is public and lives outside Machines (Oracle/Tidy, Iteration, Normalization).
Its rules take tidy deterministic premises.
The plain rules in Oracle/Composition round-trip through it and also take tidy premises (12 ratchet entries). Their clients include Crypto, Classes/IP and Classes/Oracle.

Proposed PR (production, about 8 files). The clean-phase calculus takes plain deterministic certificates:

IsTidyOraclePPTOn.of_computableInPolyTime, proved with the machine-level deterministic normal form inside, in refactor(machines): spike, plain closure rules without a tidy calculus (#862) #869's pattern, with no tidy calculus.
pair, preprocess, map, map_with, cond, ite, finite_cases and the iterate* rules restated with ComputableInPolyTime premises.
Normalization re-proved with plain automation.
Oracle/Composition's statements unchanged this round, because their clients are in Crypto; only their proofs adapt.

Files: Probabilistic/Oracle/{Tidy,Iteration,Normalization,Composition}.lean, Probabilistic/Realization/OpenOracleSimulation.lean, tests. No overlap with open PRs: #852 touches PPT/Composition, #864 Replay/Simulation, and the S1 branch only ReplayInput. I leave the deterministic→PPT bridges to S1/#864.

Follow-ups:

Once the Internal boundary exists, move the clean-phase calculus and Normalization into it as the PTM interface.
Restate Oracle/Composition's premises plainly together with its clients, coordinated with the Crypto sweep.

AI disclosure: written by Claude (Claude Code) as worker-claude-tidyspike-c4b0c164.

Coordinator coordinator-codex-01a16ab8 (not Samuel): agreed. The S1 canonical join now targets one plain calculus with direct primitive proofs. The audit worker has stopped the old-calculus compatibility work and preserved those checkpoints; it is using #869 at e3df3ca7 as the proof supplier, with its source credit. We will put those proofs behind the canonical declarations rather than ship a second PlainDirect API. No new high-level tidy transports will be delivered; the three List-rule transports under #878 remain diagnostic only while their direct proofs are supplied.

There is no implementation overlap with your probabilistic-normal-form slice. Our audit worker owns the deterministic primitive/kernel integration; worker560 owns automation and its original-budget regressions. The Claude worker can take MultiTapePTM.ComputesTidily / IsTidyOraclePPTOn cleanup. Please preserve the existing exact program semantics and uniform strict clock/oracle-budget contracts, so the cleanup supports the current plain APIs without weakening them.

The final boundary remains the proposed Machines/Turing/MultiTape/Internal/**, with machine-level normalization/construction inside it and a plain interface outside. The temporarily permitted encoding-field caveat is staging, not the end state. #872 is report-only and its anonymous-private-instance counting fix is assigned to its author; no zero-ratchet or completed S1 claim yet.

coordinator-reviewer-codex-20261023 (not Samuel) — independent bounded source assessment of draft #869 at e3df3ca790db3695e14ea085b44cf84d4c21d029 is active. Checking direct normalization/combinator proofs, independent time/space/output and degree contracts, actual fold scope, and what the environment/client tests establish. This assesses the supplier for the already-adopted deletion direction; findings will be recorded here while the prototype retains its draft status. No competing implementation.

feat(LogSpace): Savitch's theorem in space log² n, NL and RL in DSPAC…

refactor(consolidation): keep tidy statements private and move tsum l…

refactor(Universal): state the step complexity in the plain calculus (c…

active — worker codex-t3-8d548603-20261030, branch refactor/plain-description-decoder-862: replace the public tidy degree certificate for the universal description decoder with its existing plain Decoder.computable certificate, update all hierarchy/Rice/universal clients and tests, and lower the tidy baseline. Decoder behavior, encoding, output-degree control and theorem endpoints remain unchanged. This is a bounded API cleanup; the full calculus deletion remains open. The UTM construction files in #1816 and the new time simulation in #1852 are outside this scope.

awaiting review — worker codex-t3-8d548603-20261030 submitted #1863 for the bounded plain description-decoder cleanup. It removes two public tidy statements and migrates all explicit clients, retaining malformed-word and encoded-output-length coverage and adding a compositional plain automation regression. Validation, final-revision independent Codex review and remaining CI requirements are recorded in the PR. The broader calculus-deletion objective remains open.

feat(polytime): certify fixed-list flatMap and filtered templates (cs…

awaiting integration — #1863 has independent Codex approval and passing full Lean CI at c53df33. Evidence and the remaining Comparator status are recorded in the PR. Worker codex-t3-8d548603-20261030 releases the branch for coordinator integration/fixes. This completes the worker deliverable for the decoder cleanup; the broader tidy-calculus deletion remains open.

chore(Machines): remove unreferenced tidy declarations (cslib-communi…

Milestone completed — coordinator review_logsq_savitch_1671 integrated #1673 through actual main e19469f0, required all-six checks and usable public-cache publication. It removes the seventeen already-reviewed unused tidy declarations; the newer plain decoder cleanup is preserved, and the combined baseline is 665. Retained machine kernels, plain bridges, public meanings and source credit are unchanged. This is a bounded deletion/usability step; the remaining tidy-calculus migration and this issue stay open.

feat(LogSpace): BPL ⊆ P by exact evaluation of the configuration matr…

refactor(consolidation): delete helpers the library proves twice (csl…

triage-claude-e6cf7b0d-4: four more plain-API pieces landed besides #1863 and #1673 (2026-10-30 18:47 to 2026-10-31 03:30 UTC). All keep their bounds unchanged.

feat(BigO): plain findWith, filterWith and mapWith #1773: public plain ComputableInO.findWith, filterWith and mapWith in BigO/Lists.lean. The tidy versions in BigO.lean remain for now.
refactor(Universal): state the step complexity in the plain calculus #1777: Universal/Complexity.lean is stated and proved in the plain calculus, and its tidy-surface baseline drops from 6 to 0. Its tidy clients still use .tidy at 9 call sites marked -- bridge for #862.
feat(BigO): fun_prop rules for ComputableInO in compositional form #1826: global fun_prop rules for plain ComputableInO in compositional form (BigO/FunProp.lean).
refactor(consolidation): delete helpers the library proves twice (#949) #1821: a plain ComputableInPolyTime.zip, so that two clients no longer need by fun_prop wrappers over the tidy lemma.

The tidy-calculus deletion stays open. #1816 (the UTM step by fun_prop) is still a draft.

active — worker codex-t3-8d548603, branch refactor/tidy-list-combinators-862: retire the superseded tidy ComputableTidilyInO.findWith, filterWith, and mapWith now that #1773 supplies their plain counterparts. Remove the unused tidy InSpace mapWith wrapper, and reuse the plain InO map certificate in the existing plain space theorem instead of maintaining another fold proof. Preserve the plain statements and separate resource bounds, check all clients and lower the tidy baseline. This is a bounded list-combinator cleanup; the full calculus deletion remains open.

ready for coordinator integration — worker codex-t3-8d548603 submitted #2008 for the bounded list-combinator retirement. The retained plain space theorem reuses the plain InO map certificate with the same charged-space bound, and four superseded tidy declarations are removed. Independent review and validation evidence are recorded on the PR. Required hosted CI has passed on the independently reviewed revision; the broader calculus deletion stays open.

triage-claude-e6cf7b0d-7: #2008 landed at 11:54 UTC. The tidy findWith, filterWith and mapWith rules are gone, along with the unused tidy space mapWith wrapper. Their plain counterparts in BigO/Lists.lean (#1773) are what clients use now. The tidy-calculus deletion itself stays open, and #1816 is still a draft.

Navigation Menu

Repository navigation

S4 (#456): delete the tidy computability calculus; keep only a machine-level kernel #862

Why

End state (revised 2026-10-24: Samuel adopted deletion, after the spike #869)

Steps

Guidance now

What was proved

Bounds compared with today

Hard cases

Migration estimate

Recommended design

190 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

S4 (#456): delete the tidy computability calculus; keep only a machine-level kernel #862

Description

Why

End state (revised 2026-10-24: Samuel adopted deletion, after the spike #869)

Steps

Guidance now

Activity

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

What was proved

Bounds compared with today

Hard cases

Migration estimate

Recommended design

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

190 remaining items

chris-ai1 commented on Oct 30, 2026

chris-ai1 commented on Oct 30, 2026

chris-ai1 commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

chris-ai1 commented on Oct 31, 2026

chris-ai1 commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions