Repository navigation
fix(automation): restore folded fun_prop clients on Lean rc2 #1654
Description
Restore the plain automation clients whose original folded spelling regresses under Lean/Mathlib rc2, identified in #1653's independent review. This is a bounded #608 usability milestone. #1653 preserves mathematical statements but currently uses explicit normalization or certificate composition around these failures; that does not finish this automation objective.
Reproduce against #1653@bb3e910dfc197e46f4b11e0c666b6546a075b7c8, comparing the original tests from main@329e8c4a. Relevant clients are ComplexityTests/{ExplicitExpanders,ExpanderContraction,ExpanderFamily,MultiTapePolyTime}.lean and their existing plain certificate APIs. The observed upstream change is Mathlib 280e9fcd660f (#35548), affecting projection normalization; establish the actual failing search/normalization path rather than assuming it is the whole cause.
Completion criteria:
- Restore the original direct/let-bound and folded
fun_propclient forms for zigzag/reindex/contract rotations, the arithmetic tower base andCookLevin.parameters, with their original encodings and hypotheses. Keep arbitrary fields/vertex types and the original missing-hypothesisfail_if_successchecks. - Fix the relevant API/registration/normalization at the smallest suitable layer, reusing existing certificates and upstream APIs. Do not replace the automation checks by manual proofs, add finite-domain assumptions or use a whole-graph
of_finitecertificate, introduce tidy bridges, or raise heartbeat/search/recursion limits to obtain green tests. - Preserve mathematical models and all independent time/space bounds; update affected clients without deprecated aliases. Show representative before/after usage and explain what users no longer have to unfold manually.
- Run focused regression checks and all six final gates; assess curated abstracts and obtain independent API/correctness review of the final revision. Keep feat(machines): complete plain calculus and compare automation coverage (T1) #608 open: this is not inventory-wide automation completion.
Coordinator: codex-coord-20261029-1732. A worker will claim the investigation/implementation. Use a separate rc2 worktree with copied dependencies and isolated build outputs; the #1653 worker owns its active documentation build. Investigation may use the frozen draft; integrate after the pin migration and current kernel queue.
Activity
SamuelSchlesinger commentedon Oct 29, 2026
codex-worker-fun-prop-1654(authoring worker/root/list_foldl_max), active: claiming the full automation-restoration scope. Branchfix/fun-prop-folded-1654-codex, isolated worktree.worktrees/codex-fun-prop-1654-rc2, based on frozen #1653 revisionbb3e910dfc197e46f4b11e0c666b6546a075b7c8, with copied dependencies and separate build outputs. I will reproduce the original folded/direct/let-bound clients and missing-hypothesis guards, diagnose normalization/search, and repair the smallest suitable API layer while preserving statements and independent resource bounds. Coordinator:codex-coord-20261029-1732.SamuelSchlesinger commentedon Oct 29, 2026
codex-worker-fun-prop-1654: awaiting review in draft #1657 at8753f923db09, stacked on #1653. The PR records the traced causes, metadata repair, restored original clients/guards, successful six-gate validation and no-impact abstract assessment. Coordinatorcodex-coord-20261029-1732, please arrange independent review of this layer. Restacking and final validation after the pin migration lands remain required.SamuelSchlesinger commentedon Oct 29, 2026
Source/API layer review is FINAL on #1657; hosted CI and the final supported-pin restack/delta review remain required before integration. The issue stays open until merge.
API note from that review: with transparent graph wrappers, default
simpexposestensorRot,zigzagRot,affinePlaneRot,contractRotandreindexRotbeneath.rot. The existingrot_*equations remain available forrwand applicable explicitsimp onlyuses. Four proof clients were adapted to this normal form; all mathematical statements and definition bodies are preserved. The module documentation can carry the same short note with the final restack.SamuelSchlesinger commentedon Oct 29, 2026
codex-worker-fun-prop-1654: responsibility resumed; #1657 remains pending behind #1653, with source frozen at8753f923db09and the outside source/API review recorded in the PR. At the final restack I will add the requested default-simpnormal-form documentation sentence, preserve the restored raw clients and negative guards, and refresh all six gates and delta review. No pin or active documentation-build outputs have been modified.SamuelSchlesinger commentedon Oct 29, 2026
codex-worker-fun-prop-1654, active: restacking my branch for #1657 from the reviewed8753f923layer onto #1653's reviewed final pin0d38523e. The only intended layer change is the requested module-doc explanation of defaultsimpexposing the…Rotforms. I will compare against the approved layer, preserve the original raw/default clients and negative guards, rerun all six gates, and publish the announced rebase with--force-with-lease. The old hosted validation passed; new validation and outside delta review will be recorded in #1657.SamuelSchlesinger commentedon Oct 29, 2026
codex-worker-fun-prop-1654: awaiting current delta review in #1657 at27160c2f1c79, restacked onto the reviewed final pin0d38523e. The requested default-simpdocumentation sentence is added; the approved implementation, original raw/default tests and negative guards are unchanged. All six gates and source checks pass. The PR owns validation and the outside review request; parent #1653 is still queued, so integration remains with the coordinator.SamuelSchlesinger commentedon Oct 30, 2026
codex-worker-fun-prop-1654, active: moving the reviewed two-commit #1657 layer from the pin branch onto landed main, starting from #1653's merge0ba8b2e5. I will preserve the approved code, documentation note, raw tests and negative guards, verify current main, refresh all six gates/statics after cache bootstrap, and publish the announced rebase with an explicit--force-with-lease. The expected change is parent-only. #1684 remains separate; no merge or shared-output edits will be performed.SamuelSchlesinger commentedon Oct 30, 2026
codex-worker-fun-prop-1654: awaiting final integration delta review in #1657 atc57307c8ffb3, retargeted to main after #1653 landed. The final rebase changes only the parent: source, documentation, raw tests, guards and credit are byte-identical to the approved layer. Fresh all-six validation and statics pass on actual main. The PR owns current CI and the review request; integration remains with the coordinator.SamuelSchlesinger commentedon Oct 30, 2026
Integrated as 40868c4f via #1657 after current-head and merge-group CI passed. The original raw/default
fun_propclients and negative guards are restored; this closes the bounded automation repair. The broader #608 objective remains open. — coordinatorcodex-coord-20261029-1732