[chris-ai1]

Retires the superseded tidy InO findWith, filterWith, and mapWith rules after #1773’s plain migration, plus the unused tidy space mapWith wrapper. The existing plain space theorem now follows from the plain InO rule in four lines, replacing another fold proof while preserving its full charged-space expression. All in-repository clients use the retained plain interface; no aliases are added.

The tidy baseline drops by four declarations (BigO 32→29, InSpaceLib 45→44). The measured update used freshly compiled module metadata; the global checker needs the whole-library artifacts supplied by CI. A concrete captured-parameter mapping client checks linear space and empty/nonempty outputs. Strict affected-module/client builds, hygiene and aggregate checks passed locally. Full validation: hosted Lean CI.

Part of #862; the broader tidy-calculus deletion remains open. Selected formal abstracts and their semantics are unaffected. Source credit is preserved. AI assistance: Codex implementation and independent non-author review, recorded below against the committed revision.

[chris-ai1]

reviewer-codex-review_time_classes (independent non-author Codex session): APPROVE at ea97f8c. This is agent review, not human approval. The committed sources match the reviewed files.

The plain ComputableInSpace.mapWith signature and full charged-space bound are unchanged. Its proof now reuses the plain ComputableInO.mapWith rule through conversions preserving that space bound while leaving time existential. The four removed tidy declarations have no remaining clients; distinct degree and polynomial-time APIs remain intact. Public import availability and source credit are preserved, and the two baseline reductions match the removals exactly.

The new captured-parameter fill client covers both Boolean values and an empty list. The author's strict focused build passed for the affected modules, InSpacePlain tests and Universal.Complexity; full hosted validation is pending. No curated abstract statement changes. I inspected the source, resource conversions, references, imports and final deltas without editing or running builds.

[SamuelSchlesinger]

reviewer-claude-e6cf7b0d-10 (Claude Code, Opus; Claude fleet, outside this PR's fleet): reviewing at ea97f8c.

[SamuelSchlesinger]

reviewer-claude-e6cf7b0d-10 (Claude Code, Opus; Claude fleet, outside this PR's fleet). Verdict at ea97f8c: APPROVE. Agent review, not human approval.

• The PR removes four tidy declarations: ComputableTidilyInO.findWith, .filterWith and .mapWith, and ComputableTidilyInSpace.mapWith. None has a remaining reference on the branch. The step helpers they used (findStep, filterStep, mapStep, their foldl_* lemmas and length_encList_filter_le) are still used by the plain BigO/Lists.lean and by Lists.lean, so nothing is left dead.
• The statement of ComputableInSpace.mapWith is unchanged, including its full charged-space expression. Its proof is now exists_inO followed by of_inO (ComputableInO.mapWith …). That replaces a copy of the fold argument with the plain rule, which is the intended direction for #862.
• The baseline drops 32→29 for BigO.lean and 45→44 for InSpaceLib.lean, matching the four removals. The -- vendored: note records the local adaptation of the vendored file, and the credit to Christian Reitwiessner's construction is kept in BigO/Lists.lean.
• fill_inSpace is a real client: a captured parameter, linear space, and rfl checks on empty and nonempty lists. Hosted CI is green at this head.

Nit, optional: the module docstring of BigO.lean now reads ".foldl, .foldlWith: left folds with a parameter", but only foldlWith takes a parameter.

[SamuelSchlesinger]

auditor-claude-e6cf7b0d-22 (Claude Code, Opus; Claude fleet). Statement-level audit of ea97f8c: no public statement is lost. This is not a full review.

• The three removed ComputableTidilyInO.findWith/filterWith/mapWith have exactly the same hypotheses and time/space bounds as the retained plain ComputableInO.findWith/filterWith/mapWith in BigO/Lists.lean, with ComputableTidilyInO replaced by ComputableInO (checked by normalized text comparison).
• The removed ComputableTidilyInSpace.mapWith has the same bound as the retained ComputableInSpace.mapWith, whose header this PR leaves unchanged; only its proof is rerouted through ComputableInO.mapWith.
• No library, test or abstract file references the removed names. The baseline drops 3 (BigO) + 1 (InSpaceLib), matching the four removals.
• The new fill_inSpace test exercises a captured parameter and checks both empty and nonempty outputs.