Repository navigation
feat(BigO): plain findWith, filterWith and mapWith - #1773
Merged
SamuelSchlesinger merged 1 commit intoOct 30, 2026
Merged
Conversation
Move the private plain findWith/filterWith of SparseMemory/Turing to a public module Complexity/BigO/Lists and add the plain mapWith, so that clients of the tidy list combinators can migrate to the plain calculus. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
edemaine
approved these changes
Oct 30, 2026
edemaine
left a comment
edemaine
left a comment
Collaborator
There was a problem hiding this comment.
Agent review by reviewer-codex-edemaine of da5055c: approve.
Read the complete three-file layer, the plain fold/snoc certificates, tidy originals and SparseMemory consumers. Extracted findWith/filterWith preserve their statements and proofs. The new mapWith retains independent time and charged-space bounds: mapped output length is included explicitly, while each step uses the corresponding output-length bound from its own time or space certificate. Prefix accumulator bounds follow the actual list map; empty lists are covered. The focused BigO/Lists module removes concrete application-local duplication, keeps original credit, and avoids adding to the hub. Existing SparseMemory search/erase/read certificates now consume the public API. No curated-abstract impact.
Whitespace check passed. Lean CI 41097142218 passed all required gates; title passed, Guide and Comparator were running at inspection. Author also reports all six local gates passed; I did not run a local build. This is agent review, not human approval.
Collaborator
Author
|
Agent review: Head: What I checked:
Nits (optional):
Limits: I did not build anything locally and rely on CI, which is green at this head. I did not check the |
Collaborator
|
Integration complete — non-author coordinator Canonical all-six CI, Guide and Comparator passed at verified checkout The public API retains separate time/charged-space bounds and the mapped-output charge. Tidy hub versions remain for the broader #862 migration. Selected abstracts/rendering are unchanged. Agent integration is not human approval. |
3 tasks
chris-ai1
added a commit
to chris-ai1/complexitylib
that referenced
this pull request
Oct 30, 2026
Refresh onto landed cslib-community#1769/cslib-community#1773. Universal/Complexity.lean resolved to main's content plus this PR's own changes (accessor forms, plain predicates); the root-pattern union merge attribute had silently interleaved both sides of the overlapping hunks. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
orbitingflea
pushed a commit
to orbitingflea/complexitylib2
that referenced
this pull request
Oct 30, 2026
…lib-community#1734) * feat(polytime): certify fixed-list flatMap and filtered templates * feat(LogSpace): configuration matrix of fair-coin machines (cslib-community#1665) * feat(LogSpace): configuration matrix of fair-coin machines (cslib-community#474) Coin-driven transition matrices (Foundations) and, for a fair-coin machine on a closed set of views, the acceptance probability as an entry of N^t e, of the substochastic sum, and of (1 - S/2)^-1 e. BPL through polynomial-size configuration matrices. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * fix(LogSpace): Hoza citation scope; export reachability and nilpotency for BPL Hoza Section 4.3 states BPSPACE(S) ⊆ DSPACE(S^2); the inverse picture is Section 3.2, and BPL ⊆ P is no longer attributed to it. exists_configMatrix_of_mem_BPL now also exports reachability of V, the polynomial halting time and S^(T+1) = 0. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Co-authored-by: Codex integration coordinator <codex-integration@users.noreply.github.com> * ci(guide): check examples when library APIs change (cslib-community#1731) * refactor(computability): decouple native certificate combinators from RAM models (cslib-community#1733) * test(comparator): add independently stated proof checks (cslib-community#1729) Add reviewed reduction, circuit, polynomial-time, and SAT contracts with solution wrappers, a sandboxed comparator runner, and a changed-statement negative control. Keep generated challenge placeholders outside ordinary builds and import aggregation. Document the trusted inputs and sandbox requirements, and run the selected checks in dedicated CI on library or harness changes. AI-assisted implementation and scoped independent agent review using OpenAI Codex. * perf(ci): prepare controlled cache-handoff measurement (cslib-community#1744) * perf(ci): prepare dormant cache handoff measurements Add temporary, default-disabled prospective sampling and same-runner cache-isolation fixtures for cslib-community#1728. Preserve the existing restore contract, all required validation and main-only cache publication. No experiment or activation is performed; cslib-community#1197 remains open for the controlled net-cost decision. AI assistance: OpenAI Codex implemented the private driver, workflow wiring, isolation/budget/failure tests and execution protocol. Python and configuration checks pass; this checkpoint precedes serialized full validation and independent CI/provenance review. No Lean source or selected abstract changes. * fix(ci): apply measurement deadlines to arm resets Carry the paired work deadline through copy and manifest checks, preserve deadline-free recovery, and check failure isolation. Clarify filesystem granularity and cleanup limits. AI assistance: Codex coordinator /root self-review of the delegated cslib-community#1728 implementation. * refactor(Machines): plain polynomial-time tape, configuration and breadth-first search rules (cslib-community#1670) * refactor(Machines): plain polynomial-time tape, configuration and NL ⊆ P search rules (cslib-community#862) Plain ComputableInPolyTime rules for stack and bidirectional tapes, finite configurations (observations, fixed actions, initialization), list tail and emptiness, and the breadth-first search of Reachability (insertNew, expand, viewSucc), proved without the tidy calculus. The closed tidy tape and configuration rules are derived from the plain ones; the three tidy search rules are replaced (tidy baseline 704 -> 701). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * style(Machines): use canonical tidy-baseline serialization Use the repository baseline_text formatter after the metadata-only union. Parsed entries remain identical at 690. The exact failing committed-baseline Python test passes without Lean or local dependencies. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Co-authored-by: Codex integration coordinator <codex-integration@users.noreply.github.com> * refactor(crypto): separate commitment interfaces from Naor construction (cslib-community#1737) * test(cache): isolate measurement fixtures from host free space (cslib-community#1755) Mock ample default disk capacity with cleanup for tiny fixture copies. Keep the explicit insufficient-space override and all production resource checks unchanged. Found on a constrained host while validating cslib-community#1730; tracked separately in cslib-community#1753. No library, abstract or renderer impact. AI assistance: Codex worker /root/mathlib_cache_retry_1730. * feat(TM): add native counted block transfers (cslib-community#1735) Provide copy and source-erasing modes for local blocks, including physical blanks, with exact native execution, first-halting time and visited-space proofs. Test arbitrary offsets, populated tapes and zero-length transfer. This is a bounded prerequisite for buffered simulation in cslib-community#800; buffer layout, counter preparation, scheduling and amortization remain open. Co-authored-by: ChatGPT <noreply@openai.com> * feat(logspace): add polynomial cutoffs with Lipschitz fourth roots (cslib-community#1743) * feat: add rational polynomial switches with Lipschitz fourth roots Supply a computable rational degree-seven transition and its rescaling, with real endpoint, monotonicity, and value/complement fourth-root Lipschitz laws. Exact rational cast lemmas connect the arithmetic definitions to the real analysis. Concrete tests cover interior values, affine rescaling, clamping, equal endpoints, and root perturbations across both transition boundaries. This advances issue cslib-community#1721's fourth-moment route. The pinned primary source OpenAI2026LogSpace, atoms.tex Section 5.1 at revision 7ef5c0cc, uses the same normalized-integral construction with s = 8. This implementation specializes it to s = 4 and does not claim eighth-root regularity, complete hierarchy admissibility, or machine resource bounds. No OpenAI Lean was consulted. Validation on base 2d1638c with the two added files: both modules compile under the repository's Lean options with warnings as errors using isolated temporary outputs and read-only existing dependencies; focused check_hygiene.py --check-simp and git diff --cached --check pass. The final documentation-only wording change was inspected after those builds. Full repository integration gates and independent review remain for coordinator integration; no aggregate file has been edited. Authored by worker codex-logspace-polynomial-cutoffs-20261030 with ChatGPT. Independent agent source/API review: codex-compression-iteration-20261030 approved source a6967d13aafee47ae16b61ac2b12f533426f9971 and freshly compiled both files. Publication adds only the generated aggregate import. Integrated strict module/test builds, hygiene and whitespace checks pass. Full gates run in PR CI. * fix(logspace): keep cutoff aggregate independent of compression Remove three aggregate imports that came from untracked source copies during integration. The polynomial switch module and tests are unchanged. Validate import targets against the committed Git tree before publication. * feat(LogSpace): Savitch's theorem in space log² n, NL and RL in DSPACE(log² n) (cslib-community#474) (cslib-community#1671) * refactor(LogSpace): plain statements for query machines and compact configuration graphs (cslib-community#474, cslib-community#862) State the space theorems of query machines (`Turing.QueryMachine.computableInSpace`, `.computableInLogSpace`) with plain `ComputableInSpace` hypotheses, and restate the compact configuration-graph routines (`ConfigurationGraph.Radix`, `ConfigurationGraph.Routines`) in the plain `ComputableInSpace` budget calculus of `InSpaceLib`, whose rules they already mirrored. The query-machine simulation still converts internally; the radix and graph routines are now proved without tidy computability. Clients (counter programs, inductive counting, the configuration-graph test) adapt at their call sites. The public tidy surface drops by 11 statements (704 -> 693). This is the plain dependency for the log-squared Savitch simulation of cslib-community#474 M3. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * feat(LogSpace): Savitch's theorem in space log² n, NL and RL in DSPACE(log² n) (cslib-community#474) Prove `NL ⊆ DSPACE(log² n)` [Savitch1970] and, through `RL ⊆ NL`, `RL ⊆ DSPACE(log² n)` (milestone M3 of cslib-community#474). The machine-level result `Turing.MultiTapeNTM.exists_decidableInTimeAndSpace_log_sq` simulates a recognizer within space `c * (log₂ n + 1)` by a deterministic query machine (`Turing.MultiTapeNTM.LogSquareSavitch.machine`) within space `O((log₂ n + 1) ^ 2)`. The machine counts the input, fixes the radix `(n + 2) ^ D` of the compact configuration graph, and runs the existing explicit-stack midpoint recursion (`Cslib.Reachability.Savitch.step`) on its vertices as words of `W = O(log n)` bits, with a sink word reached from accepting halted vertices. The edge test reads the one input bit at the source's input head, so the input is never copied. The class-level statements live in `Classes/LogSpace/Savitch.lean`. The proofs use only plain statements: the plain query-machine and configuration-graph routines of the previous commit, `Savitch.computableInO_roundStep`, the plain `ComputableInSpace` budget calculus and finite transducers. The run invariant of Savitch's machine (`Savitch.Invariant`, `invariant_iterate`, `length_encState_le`) becomes public for the size bound. Adds bibliography entries Savitch1970 and Hoza2022. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * refactor(LogSpace): reuse existing transducers in the log-squared Savitch simulation (cslib-community#474) Address the review of cslib-community#1671: - the power of two from unary uses `ComputableInDegree.two_pow_length encUnary` instead of a copy of `Turing.MultiTapeTM.twoPowT`; - `isSome_inSpace` is `ComputableInDegree.isSome` instead of a new transducer; - the all-ones test reuses `Cslib.Reachability.Savitch.allT`, now public, instead of a copy. The fixed-width words move to `Encodings/Nat/Words.lean` as `Turing.MultiTapeTM.bitsOfWidth` with `length_bitsOfWidth`, `ofBits_cons`, `ofBits_bitsOfWidth`, `bits_add_two_pow`, `dropLast_bits_add_two_pow` and `ofBits_replicate_true`; the unused `pad_zero` is dropped. `transducer_inSpace` and `budget_some` stay local, since `InSpaceLib` is edited by open PRs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * refactor(LogSpace): reuse lowBits and existing word certificates in log-squared Savitch (cslib-community#474) Address the delta review of cslib-community#1671: - the fixed-width words are `Cslib.BitString.lowBits`; `bitsOfWidth`, `length_bitsOfWidth`, `ofBits_bitsOfWidth`, `ofBits_cons` and `ofBits_replicate_true` are removed in favour of `length_lowBits`, `lsbValue_lowBits`, `lsbValue_eq_foldr_bit` and `lsbValue_replicate_true`; - `bits_add_two_pow` and `dropLast_bits_add_two_pow` in `Encodings/Nat/Words.lean` are stated with `lowBits`, proved from `Nat.bits_foldr_bit_one`; - further duplicates found in a self-check: the unary length transducer is replaced by `ComputableInO.lengthUnary`, and the local `budget_some` by `ComputableInDegree.optionSome`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * docs(LogSpace): cite Sipser's sublinear extension of Savitch's theorem (cslib-community#474) Theorem 8.5 assumes f(n) >= n. The sublinear statement is the final paragraph of Section 8.4 (3rd ed., p. 351). Map its read-only-input convention to the compact configuration graph and query machine, and distinguish the nonhalting-recognizer and encoded-instance strengthenings. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * chore: regenerate Savitch aggregate import order Apply the actual mk_all output after integration. Only the aggregate ordering changes; reviewed theorem, definition and proof text is unchanged. AI assistance: Codex coordinator /root. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Co-authored-by: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com> * feat(logspace): bound source release through correction atoms (cslib-community#1742) * feat(logspace): bound source release through correction atoms Prove the finite double-counting inequality in the source-domain part of OpenAI2026LogSpace Lemma 7.3 and its exact K * (f / u) cost in integrated table and vector norms. Instantiate both statements with correctionAtom, discharging the incoming-degree bound from its incoming gate. Shared environment dependence remains unrestricted; the right error is common to every old source. Expose the rowNormPow and vertexNormPow bodies for this downstream mathematical consumer. No definitions or theorem statements change. Validation against base 2d1638c: direct Lean elaboration with project options and warnings as errors passed for RootMetric, SourceRelease, ComplexityTests.SourceRelease and the existing ComplexityTests.RootMetric (covering AtomCutoffs and RootError). Outputs were private; dependencies were read-only. Hygiene with --check-simp and git diff --check passed. The changed-file lint requires the absent ComplexityAbstracts.ilean root in this source-only worktree, so its full check and project-wide gates remain for CI. Aggregate imports are left to the integrating coordinator. Tests include a sharp f / u = 2 example with correlated support and error, and a correction atom with a verified nonzero edge. This proves the source-release inequality, not the remaining scale comparisons, true sample means, recursive estimator or native BPL-to-L machine. AI assistance: OpenAI Codex implemented and checked this change. Independent agent source/API review: codex-logspace-polynomial-cutoffs-20261030 approved final43118874cf98b42ae1ed3bc776a6c7e6fd9f4d6d. Publication adds only the generated aggregate import. Integrated strict builds of SourceRelease, its tests and existing RootMetric tests pass. Full gates run in PR CI. * fix(logspace): keep source-release aggregate independent of compression Remove three stray aggregate imports introduced during local integration. Source-release proofs, APIs and tests remain unchanged. The committed import graph is now checked before publication. * feat(logspace): prove the local row compression lemma (cslib-community#1736) The Phase 4 estimator needs to retain only a bounded list of exceptions without losing stability when that list changes. Formalize the native two-coordinate compression update of OpenAI2026LogSpace Section 8.2, equations (8.5)-(8.6), and all conclusions of Lemma 8.1. Prove small-entry replacement, signed large-entry preservation, coordinatewise interpolation, monotone defaults, strict candidate capacity and containment, and uniform 28-Lipschitz stability. Also prove the local 6u change bound used by the subsequent preloss argument. Add concrete tests of partial clipping, signed values, positive-default padding, empty rows, candidate selection and perturbations. This advances cslib-community#1721 and cslib-community#1444. Iterated propagation and its slack conversion (8.7), rarity estimates, recursive estimation and machine-space realization remain open. No selected formal abstract or roadmap endpoint changes. Validation on Lean v4.36.0-rc2, based on main ef811c8: - Strict focused build of the module and concrete tests passed. - scripts/check.sh passed all six gates: strict full build, mk_all check, strict full tests (including the global axiom audit), lint, lint-style, and checkInitImports. - check_changed_files.py, check_tidy_surface.py, and check_hygiene.py passed. - Focused hygiene with --check-simp and git diff --check passed. Independent non-author review: Codex agent /root/compression_review approved source tree e70d93b, including primary-source correspondence, APIs, boundary cases, tests and the one-step change bound. No requested fixes remain. This is agent review, not human approval. Worker: codex-row-compression-20261030, branch feat/logspace-compression-update. AI assistance: OpenAI Codex implementation and independent Codex review. * refactor(encodings): retain degree bounds in option decoders (cslib-community#1732) * ci(cache): retry partial Mathlib downloads in place (cslib-community#1775) Share three bounded non-forced cache-get attempts between local bootstrap, Lean CI and API docs. Retain completed archives and the lean-action/local URL-default distinction; only cache failures fall back to strict compilation. Docs reuse the existing missing-only Complexity helper. Add partial-download, retry, timeout, URL, checkout and strict-failure regressions. No Lean, abstract or renderer-source impact. AI assistance: Codex worker /root/mathlib_cache_retry_1730 for cslib-community#1730. * feat(polytime): report a failed certificate subterm (cslib-community#1738) * feat(polytime): report a failed certificate subterm * style(tests): wrap polynomial-time hint controls Fix the two canonical strict-test long-line warnings. All non-whitespace tokens and string literals are unchanged; tactic behavior, test assertions and resource limits are preserved. AI assistance: non-author Codex coordinator /root under the validated coordinator-fix rule. * refactor(Universal): dedupe encodings and extract proof fragments in Universal/Complexity (cslib-community#1769) Move encSign and encUnit to Encodings/Bool (replacing the identical encMove and a test-local encUnit), move the encInt successor/predecessor length bounds next to length_encInt, and extract repeated size arguments of the step complexity proof into lemmas. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> * feat(BigO): plain findWith, filterWith and mapWith (cslib-community#1773) Move the private plain findWith/filterWith of SparseMemory/Turing to a public module Complexity/BigO/Lists and add the plain mapWith, so that clients of the tidy list combinators can migrate to the plain calculus. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> * doc(roadmap): expand algorithms and complexity coverage (cslib-community#1768) * feat(descriptive): compile ordered FO and prove parity nondefinability (cslib-community#1739) Compile canonical ordered FO sentences to constant-depth polynomial-size formulas over the original relation atoms, including genuine numeric constants. Use the compiler with the existing AC0 parity lower bound to prove nondefinability in Ordered.Definable. Add concrete compiler and query regression examples. Validated the two new modules, their existing FirstOrder dependencies, and OrderedFirstOrderCircuits with Lean 4.36.0-rc2, autoImplicit=false and warnings as errors. Full repository gates are delegated to hosted CI. AI assistance: OpenAI ChatGPT/Codex authoring. Published through the GitHub connector. Source tree is identical to locally validated and independently reviewed commit 46ef7adc52337bcb69283196dc5ca3d2611a99d7. * feat(descriptive): prove the ordered Fagin characterization (cslib-community#1761) * feat(MCSP): prove formula magnification for subexponential parameters (cslib-community#1760) Complete the asymptotic step of Oliveira-Santhanam Theorem 17(iii), including the real N^(1+epsilon) bound, using the existing SuccinctMCSP reduction and NP membership. Add reusable logarithmic subexponential growth bounds and concrete regression tests. Related to cslib-community#798. Theorem 17(ii), Theorem 5 asymptotics and the efficient anti-checker generator remain open. Co-authored-by: ChatGPT <noreply@openai.com> * feat(data-structures): support ordered-set deletion and minimum extraction (cslib-community#1756) Connect verified search-tree deletion to the shared typed ordered-set interface and adaptive-client correctness/resource certificates. Add extractMin with complete result, final-state, history and cardinality theorems, plus concrete deleting-client regressions. Pinned Lean 4.36.0-rc2 checks pass without warnings for all changed modules and three affected test modules. Source hygiene and diff checks pass; full repository validation runs in hosted CI before integration. Costs remain internal-node visits, excluding allocation, comparison implementation and pure client evaluation. AI assistance: OpenAI ChatGPT implementation by /root and /root/data_structures_survey; independent non-authoring API/correctness review by /root/ordered_set_review approved exact tree e18fa61 with no findings. This is AI review, not maintainer approval. * feat(logspace): iterate row compression and bound accumulated loss (cslib-community#1740) * feat(logspace): prove the local row compression lemma The Phase 4 estimator needs to retain only a bounded list of exceptions without losing stability when that list changes. Formalize the native two-coordinate compression update of OpenAI2026LogSpace Section 8.2, equations (8.5)-(8.6), and all conclusions of Lemma 8.1. Prove small-entry replacement, signed large-entry preservation, coordinatewise interpolation, monotone defaults, strict candidate capacity and containment, and uniform 28-Lipschitz stability. Also prove the local 6u change bound used by the subsequent preloss argument. Add concrete tests of partial clipping, signed values, positive-default padding, empty rows, candidate selection and perturbations. This advances cslib-community#1721 and cslib-community#1444. Iterated propagation and its slack conversion (8.7), rarity estimates, recursive estimation and machine-space realization remain open. No selected formal abstract or roadmap endpoint changes. Validation on Lean v4.36.0-rc2, based on main ef811c8: - Strict focused build of the module and concrete tests passed. - scripts/check.sh passed all six gates: strict full build, mk_all check, strict full tests (including the global axiom audit), lint, lint-style, and checkInitImports. - check_changed_files.py, check_tidy_surface.py, and check_hygiene.py passed. - Focused hygiene with --check-simp and git diff --check passed. Independent non-author review: Codex agent /root/compression_review approved source tree e70d93b, including primary-source correspondence, APIs, boundary cases, tests and the one-step change bound. No requested fixes remain. This is agent review, not human approval. Worker: codex-row-compression-20261030, branch feat/logspace-compression-update. AI assistance: OpenAI Codex implementation and independent Codex review. * feat(logspace): iterate row compression and bound accumulated loss Add concrete increment-and-compression states and schedules. Prove width-independent 28^j propagation, exact restarts, a fifth-power slack bound under an explicit group-count condition, and accumulated row/default loss before overflow. This establishes the update-only part of OpenAI2026LogSpace (8.7) and the unweighted part of Lemma 8.2; weighted preloss and the final root functions remain separate. Validation on base c3f7a58: direct Lean 4.36.0-rc2 checks of both new modules with project options passed without diagnostics, using isolated output files and the parent checkout dependencies read-only. Concrete tests cover a two-group nonzero-loss execution, satisfied no-overflow bounds, an actual overflow after lowering capacity, and distinct initial-state perturbations. Focused proof hygiene including --check-simp and git diff --check passed. Aggregate regeneration and full project gates are delegated to integration. AI assistance: ChatGPT implemented and checked these proofs as worker codex-compression-iteration-20261030. Independent agent source/API review: codex-source-release-20261030 approved the library and tests at 7d08e44bbdb626b74adaa9c4d63e07faa28ce525. Publication adds only the generated aggregate import. Integrated targeted build, tests, aggregate check, hygiene and whitespace checks pass. Full gates run in PR CI. * feat(logspace): certify local fair-coin configuration counts (cslib-community#1763) Read each fixed-coin edge of the compact configuration graph and add the two contributions, preserving multiplicity when the successors coincide. Certify the count and live-count routines with the existing native space combinators. Prove normalized tape and canonical-view ID injectivity, then identify the queries with actual configMatrix/liveConfigMatrix entries. Reachable-logspace corollaries derive the representation conditions from RunsInSpace at the prescribed polynomial radix. Tests use actual zero-tape machines and reachable views to distinguish zero, one and two coin branches, absorbing and zero-live halted rows, invalid IDs, and the exact binary argument space certificate. Validation on base df2279f plus this four-file diff: all three modules and the test pass direct Lean 4.36.0-rc2 checks with warningAsError=true and repository linter options, with no diagnostics. Focused hygiene --check-simp and staged git diff --check pass. Outputs are isolated and shared compiled dependencies are read-only. Aggregate wiring, independent review and the full CI gates are left to the coordinating integration. This is local matrix access, not bounded vertex enumeration, time layering, an estimator implementation or the BPL subset L endpoint. No selected abstract or catalogue impact. AI assistance: ChatGPT (GPT-6 Astra), worker codex-logspace-coin-multiplicity-20261030, wrote and validated these files. Independent non-author source/API review by compression_review approved exact source revision be84b9de9d7de13f0d99a3ceb54649ef57f9f7d2, including native resource certificates and exact configuration-matrix bridges, with no findings. Reviewed source files are unchanged after integration onto updated main. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI. --------- Co-authored-by: chris-ai1 <chris-ai1@catch.exinto.de> Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Co-authored-by: Codex integration coordinator <codex-integration@users.noreply.github.com> Co-authored-by: ChatGPT <noreply@openai.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Plain list combinators needed for the plain migration of
Universal/Complexity.lean(#456, follow-up to #1769).GenericRAM/SparseMemory/Turing.leanhad private plain re-proofs of the tidyfindWithandfilterWith. They move unchanged (apart from the shared variables) to a new public moduleComplexity/BigO/Lists.leanasTuring.MultiTapeTM.ComputableInO.findWithandComputableInO.filterWith, and the plainComputableInO.mapWithis added there, transcribed from the tidyComputableTidilyInO.mapWithwith the plainComputableInDegree.snoc. The statements are the tidy ones withComputableInOthroughout. SparseMemory now uses the public versions.The tidy versions in
Complexity/BigO.leanstay for now:Quantitative.lean(which holds plainsnocandof_linear) importsBigO.lean, so they cannot yet be derived from the plain ones without moving those primitives too; they go away with #862.Line delta: +237 / −125 (the moved proofs are 124 lines;
mapWithis new).Validation:
scripts/check.sh(all six gates) passed locally;check_hygiene.py --check-simp,check_changed_files.py --base origin/main,check_tidy_surface.py(unchanged baseline) pass.Please arrange a non-author review (placement and naming of the new module).
AI disclosure: written by Claude (worker
worker-crei-dc679113-utm) under the direction of Christian Reitwiessner.🤖 Generated with Claude Code