Repository navigation
refactor(circuit): simplify kernel-step synthesis bookkeeping #523
Description
Synthesis.full_kernelStep currently maintains six intermediate wire-set unions, six availability helpers and a nested composition chain for seven arithmetic stages. The newly available Synthesis.Builder and synthesis_available can express the same computation while keeping its arithmetic stages visible.
Scope is only the proof of Cslib.Circuits.Synthesis.full_kernelStep in Complexity/Computability/Circuit/KernelVector.lean, plus a proof-only tactic import. Preserve its public statement, quantifiers and 8 * (n + 1)^2 bound, the unchanged kernelStep_budget, named arithmetic stages/comments and final semantic rewrite. No new API, second client or mathematical endpoint.
Worker worker-codex-kernel-synthesis-20261023 owns preparation on refactor/circuit-kernel-synthesis-20261023 in an independent repository and cache after explicit donor coordination. Completion requires existing-client validation, all six project gates, Python/tooling checks, no-impact assessment for selected abstracts and independent review of the exact published revision. AI-assisted work; no human review is implied.
Activity
SamuelSchlesinger commentedon Oct 23, 2026
active —
worker-codex-kernel-synthesis-20261023claims the single-proof refactor onrefactor/circuit-kernel-synthesis-20261023, following coordinator approval. Planned independent repository/private/tmp/complexitylib-kernel-synthesis-20261023; waiting for the cache owner's explicit copy permission before creating the isolated build environment. Then implement the seven-stage Builder proof, validate existing clients and all required gates, and request exact-revision coordinator review.SamuelSchlesinger commentedon Oct 23, 2026
active —
worker-codex-kernel-synthesis-20261023: the one-proof Builder refactor passes whole-file Lean MCP diagnostics; the theorem statement, budget lemma and all other declarations are unchanged. Full validation and PR publication are pending the coordinated upstream pin update in #525. Source/cache are idle while the coordinator reviews the bounded diff; all six gates will run on the combined final source.SamuelSchlesinger commentedon Oct 23, 2026
active —
worker-codex-kernel-synthesis-20261023: all six project gates, 89 Python tests and hygiene/documentation/catalogue checks pass on the corrected #525 source plus this one-file proof change. Whole-file MCP diagnostics are clean with CSLib6ff325e8. Publication waits for #525’s actual merged-tree parity so the PR contains only the KernelVector refactor; statements, numerical bounds and selected abstracts remain unchanged.refactor(circuit): simplify kernel-step synthesis bookkeeping
SamuelSchlesinger commentedon Oct 23, 2026
awaiting review —
worker-codex-kernel-synthesis-20261023submitted #535, stacked on #533 so hosted CI can run while that dependency finishes. The published tree exactly matches the validated combined source; the PR contains only the reviewed one-file proof refactor. Validation, dependency and abstract-impact details are in the PR. Coordinator review/integration requested.refactor(circuit): simplify kernel-step synthesis bookkeeping