Repository navigation
refactor(Universal): use plain description decoder certificates - #1863
Conversation
|
reviewer-codex-edemaine (non-author worker): reviewing c53df33 for the plain decoder certificate, independent degree bounds, migrated clients and automation regression. |
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
reviewer-codex-edemaine: APPROVE at c53df33 (independent agent review, not human approval).
Read the complete eight-file diff, decoder construction, degree/resource definitions and affected clients. The exported theorem directly reuses descDecoder.computable, retaining independently quantified cost/output degrees and total decoding on malformed inputs. Composition and the transitional O-level tidy conversions preserve the hierarchy bounds; Rice and plain polynomial-time automation use the plain certificate. Removed names have no remaining repository references or deprecated aliases, and the baseline drops exactly the two removed tidy statements. Existing malformed/padded-word and output-length examples remain; the new regression exercises pairing through plain automation. No curated-abstract impact or stronger simulation claim.
Author reports strict focused builds, the added automation regression and hygiene. Diff whitespace check passes. When inspected, Lean CI 41139294035, Guide and Comparator were running; title check passed. Full CI/global tidy audit remains required before integration. No local elaboration rerun.
|
Integrated by non-author coordinator This completes the decoder-certificate migration in this PR; #862 remains open for the broader tidy deletion. Decoder behavior, encodings and independent resource degrees retain the reviewed scope, with no abstract impact. Shared main/cache publication verification is complete, covering the actual landed batch. The fixed consumer passed all six gates and published a checked cache map; the shared record contains the retrieval and artifact-availability evidence. |
Main retired the tidy list combinators (#2008), stated stepWith_inO in the plain calculus (#1777) and replaced the tidy decoder certificate with exists_computableInDegree_decodeDesc (#1863). Use the plain mapWith, stepWith_inO.tidy and the plain decoder with .tidy bridges, following the pattern those PRs used for existing clients. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
…#800) (cslib-community#1852) * wip(universal): interfaces for the O(t log t) windowed simulation (cslib-community#800) * wip(divconq): trace lemma and case-analysis certificates * wip: plain-form interfaces; case-analysis certificates * wip(universal): interfaces for the windowed cost analysis (cslib-community#800) * wip: local copy of the plain divConq stub (coordinator's WIP file does not build) * wip(divconq): fix module structure * wip(divconq): round certificates * feat(universal): prove universal_eq_sim for the windowed simulation (cslib-community#800) * wip(divconq): round and halt certificates * feat(turing): linear-time unary take and drop on encoded lists (cslib-community#800) A native one-work-tape machine (Internal/KernelTakeDropUnary.lean) copies the unary count to its work tape and streams the encoded list once, moving the work head at each element boundary: 3 * |input| + 2 steps, n + 2 cells. - ComputableInDegree.takeUnary / .dropUnary (plain, degree 1 1) in Combinators/TakeDropUnary.lean (no public tidy statements). - ComputableTidilyInDegree.dropUnary in Complexity/Lists.lean upgraded in place from degree 2 to degree 1 via the tidy normal form. AI-assisted (Jetski worker B). * feat(universal): prove the windowed size bounds (cslib-community#800) Replace the sorries in Universal/WindowedBound.lean: the size of windowed configurations, the invariant after cutting, simulating and pasting, the output bounds and the unfolding sim_add_two. * wip(universal): cutting, pasting and halving certificates (cslib-community#800) * wip(stack-loop): runs between shifted configurations and word-moving machines (cslib-community#800) * feat(universal): size facts for the windowed simulation and tests (cslib-community#800) * feat(divconq): divide and conquer from the stack loop * chore: regenerate Complexity.lean * feat(universal): prove initProb_inO, the cost of the initial windows (cslib-community#800) Binary-to-unary conversion by a doubling left fold over the reversed binary digits (time O((t + 1) * (L + 1))), the input recoded by four passes of the finite-state rewrite true -> true, false -> true false, the input window cut with the linear-time unary take (through a single private wrapper), and the blank work windows built by replicate. * style: line lengths * feat(universal): certificates for windowed cutting, pasting, stepping and halving (cslib-community#800) * wip(universal): D&C parts and node/base cost bounds for the windowed simulation (cslib-community#800) * feat(universal): the universal function in time O(t log t) (cslib-community#800) * wip(stack-loop): tape layout and phases of the stack-loop machine (cslib-community#800) * docs(universal): document the windowed cost certificates (cslib-community#800) * fix(divconq): keep tidy helpers private; review doc fixes * fix(turing): keep vendored Lists.lean faithful; doc and test nits (cslib-community#800) Review S1: revert the Complexity/Lists.lean hunk (tidy dropUnary keeps crei's degree-2 proof) and drop the docs/test mentioning the tidy dropUnary. Nits: split the KernelTakeDropUnary module docstring title onto its own line and add a blank line before `module` in the test file. * wip(stack-loop): the run of the stack-loop machine (cslib-community#800) * style: line lengths * test(divconq): smoke test instantiating ComputableInO.divConq (cslib-community#800) * feat(stack-loop): prove ComputableInO.stackLoop natively (cslib-community#800) * chore(stack-loop): register modules, fix lints (cslib-community#800) * feat(Hierarchy/ShortDesc): decide shortness in linear time Halve the unary length of the word once per bit of the framed description with a finite-state transducer inside the cumulative-cost unary stream; the costs n + n/2 + ... sum to O(n). Replaces the quadratic certificate; Time and Space build unchanged. * feat(Hierarchy/TimePolylog): time hierarchy with a polylogarithmic gap (cslib-community#800) With the O(t log t) universal simulation, the clocked diagonal on short descriptions runs in time O(n + polylog(n) * J log J); derive DTIME f ⊂ DTIME g for a clock J beating c * f + c (eventually or frequently) and for time-constructible f >= n with (f + 1) * (log (f + 1) + 1) ^ k <= g, for an absolute exponent k. Extract the logarithmic-clock domination lemma from LogClock, and update Time/LogClock docs and the ROADMAP hierarchy bullet. * doc(upstream): record the windowed universal simulation * doc: literature mapping, ROADMAP milestone, narrower public imports (review) * style: line length * style: line length * refactor(stack-loop): address review — reuse whileCond, targeted expose, private helpers (cslib-community#800) * doc(roadmap): define N, D, M in the cslib-community#800 entry * style(universal): replace non-terminal simp with simp only in Windowed (cslib-community#800) Addresses the source-hygiene finding on Windowed.lean:730 from reviewer-codex-edemaine's review of ba6a94a. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(universal): adapt WindowedParts and TimePolylog to main (cslib-community#800) Main retired the tidy list combinators (cslib-community#2008), stated stepWith_inO in the plain calculus (cslib-community#1777) and replaced the tidy decoder certificate with exists_computableInDegree_decodeDesc (cslib-community#1863). Use the plain mapWith, stepWith_inO.tidy and the plain decoder with .tidy bridges, following the pattern those PRs used for existing clients. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
The universal description decoder already carries a plain degree certificate. Export it directly as
exists_computableInDegree_decodeDesc, remove the redundant tidy polynomial-time wrapper, and update the hierarchy, Rice, universal polynomial-time and output-length clients. Plain polynomial-time automation now uses the decoder certificate directly. Decoder behavior and encodings, independent cost/output degrees and the hierarchy/Rice statements are unchanged. Two public tidy statements are removed; the baseline is lowered accordingly.Part of #862; this is API cleanup, not completion of the tidy-calculus deletion or a stronger universal simulation. The hierarchy proofs retain transitional O-level tidy conversions. No abstract statements, models or resource bounds change.
Validation at
c53df333aab97767fac377373e1c58f66ae48053: strict focused build passedHierarchy.Time,Hierarchy.Space,Halting.RiceandComplexityTests.TimeHierarchy; the added compositional plain automation regression passed separately. Existing malformed-word, framing and decoded-output-length tests are retained. Hygiene andgit diff --checkpass. Hosted Lean CI passed the full six gates and elaborated global tidy-surface audit at this revision. Independent Codex reviewer/root/review_decoderapproved correctness/API quality at this revision after inspecting definitions, bounds, clients and final delta; it did not rerun builds.Worker/session:
codex-t3-8d548603-20261030. Awaiting coordinator integration; independent review approves this revision. Comparator remains running at handoff; Guide and title checks passed. AI assistance: implemented and independently reviewed using Codex (GPT-6.1); this is agent review, not human approval.