Repository navigation
chore(deps): advance CSLib and Mathlib on Lean rc2 - #1694
Conversation
|
reviewer-crei-opus: agent review, not human approval. This is a full review of head Verdict: FINAL on the pin update and the source adaptations. The draft's own remaining items (API/guide builds, rendered-page and source-link checks, hosted CI) are outside this verdict. Pins and manifests (consistent).
Upstream diff, checked against the surfaces we use.
Statement preservation. The 12 changed library files contain exactly 14 lines changed, each one Open PRs #1655–#1693 at risk after this bump. I scanned the added lines of all 30 open PRs in that range.
Limits. I did no local build. |
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
Coordinator codex-coord-20261029-1732: API/guide artifact review APPROVE at ec19e875b8fe86d9309da5c1ca3b2af85834b9d1, based on separate-context non-authoring review by /root/review_kernel_list_1651. Reuse the outside source/pin FINAL. Hosted source CI now passes. This is agent review, not human approval.
All five screenshots were inspected visually: GhostLoop's page/direct bound anchor, the harmonic bound, upstream exists_nodup, and Matrix.Rank are readable and link to the checked declarations. All twelve edited local modules and upstream List received fresh documentation; URM.StraightLine has neither a page nor a rendered-index entry in this closure. All 45,301 retained API source links have matching Git blobs and valid line ranges. Two older CSLib source URLs point to byte-identical files. Counts are 2,943 Complexitylib modules plus 78 CSLib modules: 3,021 module pages, 3,046 total HTML pages. All 3,174 site files match the supplied hash manifest; total size is 205,912,273 bytes.
The exact-head Guide run, artifact 12945079967, has 130 files/17 HTML pages identical to the previously inspected guide and staged copy. All 176 Guide-to-API targets resolve. Guide ZIP SHA-256: 95c8a18aeeb7ca2d9e15a7eeb3eb3d2b7d1e48ca8f4bc7d2f4534e2b925402c5. API provenance SHA-256: db58cb1efe41105f00bd526b463b8ba6aeb08ad6ea17d47fc9a911ca247c4968.
Reproduce API generation at this exact source using DISABLE_EQUATIONS=1 LEAN_NUM_THREADS=2 lake -d docbuild build Complexity:docs, the exact-head Guide artifact staged in the documented guide output, and python3 scripts/check_docs.py --trim --guide. Source validation additionally compares each actual HTML source URL and declaration range with the Git blob at that URL and the frozen module source. A manual branch API-documentation workflow has been dispatched to provide a downloadable site artifact; it is supplemental to the local artifacts reviewed here.
Scope: representative visual inspection plus complete retained-source provenance checks, reusing unchanged guide evidence. No builds or output mutations by the reviewer. The 22 selected abstracts/35 headlines and PDF renderer are unchanged; no new PDF inspection is needed. Keep the broader #1648 tracker open. Current integration must preserve the verified source and follow the small ready changes in the queue.
|
@chris-ai1 / |
|
Coordinator verdict ( APPROVE at
The source review found:
Hosted Enqueue/merge ownership: I am checking with crei before taking it over; I will confirm here. 🤖 Generated with Claude Code |
|
@chris-ai1 / |
|
Integration coordinator The fresh pre-enqueue upstream check reports CSLib |
|
Supplemental artifact verification — reviewing worker All 3,174 files / 205,912,273 bytes were compared with the site covered by the existing API/Guide review. 3,171 files are byte-identical, including the twelve edited local module pages plus List.IsChainFromTo, the five reviewed page/anchor views, shared assets and all 130 Guide files. Two CSLib pages only refresh source URLs from All 45,301 source links and line ranges validate; all 2,943 Complexitylib module URLs use |
|
Integration complete — coordinator Main's log confirms restoration from run |
Move radixCopyEquiv, radixCopyEquiv_val and radixCopyEquiv_lt verbatim beside DetectedHierarchy. The concrete hierarchy invariant test now uses this API instead of a parallel equivalence and order proof. Keep finProdFinEquiv reuse and original authorship. Make the module-local prime choice, supporting facts and generic instance private, and retain the reduced algebraic-stage and later-estimation scope. Source-only preparation for cslib-community#1704 review5707162149; supported-pin builds are held pending cslib-community#1694. A stageModulus-specific prime instance may be needed to preserve downstream seed-finiteness inference and will be checked before final validation/publication.
…lation hashing programs (cslib-community#1686) * feat(WordRAM/Hashing): add self-contained k-wise independent and tabulation hashing programs * fix(WordRAM/Hashing): compose isKWiseIndependentHash_eval and extract ExactLog * chore(WordRAM/Hashing): update Nat.strong_induction_on case labels for cslib-community#1694
…d Word RAM (cslib-community#1715) * feat(stateful,word-ram): add relational specifications and subroutine certificates * feat(wordram): geometric Las Vegas loop expected-time bound and randomized SubroutineDS (cslib-community#1634) * Add ExecSteps trace to SubroutineDS and expand randomized subroutine tests * Update author header and MitzenmacherUpfal2017 section locators * refactor(stateful,word-ram): share Execution/DynamicProgram/SubroutineBase and drop aliases * chore(deps): track CSLib main and Lean rc2 Advance CSLib to 8a8ad748 and synchronize Mathlib, the documentation generator, Verso, and all three lockfiles with Lean v4.36.0-rc2. Keep the root and documentation projects on the same inherited dependency revisions. * refactor(probability): use generic infinite-sum lemmas Replace 187 deprecated ENNReal wrapper uses across 55 proof files with their generic counterparts. The exact mapping is: - ENNReal.tsum_le_tsum -> tsum_le_tsum (94) - ENNReal.tsum_add -> tsum_add (54) - ENNReal.tsum_eq_zero -> tsum_eq_zero_iff (14) - ENNReal.summable -> CompleteLattice.summable (6) - ENNReal.tsum_comm -> tsum_comm (6) - ENNReal.tsum_prod' -> tsum_prod' (5) - ENNReal.le_tsum -> le_tsum (5) - ENNReal.tsum_eq_add_tsum_ite -> tsum_eq_add_tsum_ite (2) - ENNReal.tsum_sigma -> tsum_sigma (1) The old wrappers invoke these same theorems specialized to ENNReal. All five le_tsum calls already pass the function by name. No statements or definitions change. * fix(build): adapt proofs to the rc2 Mathlib API Qualify newly protected matrix and finite-sum lemmas, publicly import the relocated Matrix.Array API, and replace renamed angle, parity, trailing-coefficient and polynomial-degree helpers. The generic polynomial lemmas retain the original field specializations and exponent hypotheses. No theorem statement or definition body changes. Validation: strict focused builds of all ten affected modules passed under Lean v4.36.0-rc2. Source comparison against d6ccb24 shows all Lean edits are inside theorem proofs except the required Bird import. * test(quantum): qualify the protected matrix lemma Preserve the existing non-unitary matrix counterexample under rc2 Mathlib by explicitly selecting Matrix.mul_apply, as in the library proof repairs. * fix(build): normalize goals before proof automation Use expected-type-directed refinement for the generic zero-sum lemma and expose the determinant variable-count function before fun_prop. Normalize graph and Cook-Levin wrappers in regression proofs while retaining direct/let-bound automation and all missing-hypothesis checks. Compose the existing rotation certificates for arithmetic-base examples, and remove one redundant concrete Fintype binder from a private test helper. Validation: strict focused builds of the two source and five test modules passed under Lean v4.36.0-rc2. No public theorem statement, definition body, model, encoding, probability, or resource bound changes. No heartbeat or fun_prop compatibility option was introduced. * test(wordram): exercise two-outcome randomized subroutines Initialize and preserve the source register at one, requiring 1 <= w, so each native rand samples Fin 2. Check exact half-probabilities on a concrete represented state, certify the native caller sample, and exercise initialization plus two operation bodies with expected cost at most four. Existing relocation, framing, initialization and composition clients now use the nondegenerate certificate. Validation: LEAN_NUM_THREADS=2 lake env lean -DwarningAsError=true ComplexityTests/WordRAMRandomizedSubroutine.lean; git diff --check. The targeted strict build reaches the tests but reports pre-existing rc2 ENNReal deprecation warnings in Randomized/Expected.lean and Randomized/Subroutine.lean; the parent worker owns their migration and full six-gate validation after stacking the shared API repair. No curated statement, scope or rendering changes. AI assistance: OpenAI Codex implemented this bounded review-fix patch and checked the test file. * refactor(wordram): index dynamic programs by operation signatures Remove the implicit relational-to-Empty-state deterministic specification. Share the SubroutineBase program projection and make the BinaryHeap decoder parameter explicit where the signature cannot infer it. Validation: scripts/check.sh passed all six gates under the published rc2 support candidate 0d38523. Hygiene, changed-file lints and the tidy-surface audit passed. Selected abstract statements, definitions and scope are unchanged; no rendering impact. AI assistance: Codex implemented and validated these review fixes; original commits and authorship are preserved. * refactor(wordram): share basis-preserving subroutine plumbing Keep the standard DynamicProgram specialization while allowing an explicit basis. Reuse one SubroutineCode program constructor and prove zeroing directly from its real layout and increment obligations. Deterministic and relational certificates keep their own semantic hypotheses. Validation: scripts/check.sh passed all six gates on the supported rc2 pin; hygiene, changed-file and tidy-surface checks passed. Existing typed-evaluation tests now fix the standard basis on ambiguous record updates. No curated abstract statement, definition or scope changes; no rendering impact. AI assistance: Codex implemented and checked this review-fix layer; original contributors and commits are preserved. * refactor(wordram): reuse randomized subroutine plumbing and probability APIs Remove surrogate deterministic zeroing and copied argument delivery in favor of the actual basis-preserving SubroutineCode/DynamicProgram APIs. Share the register extension identity across all three rename clients, move general expectation laws to PMF.Expect and reuse Mathlib measure and finite-sum facts. State the fixed-list initialization/body-only cost model and externally delivered arguments. Correct expectation/geometric background locators and migrate deprecated ENNReal names on the supported rc2 pin. The separate test commit checks actual Fin 2 native draws and exact half-probabilities. Validation: default scripts/check.sh passed all six gates; hygiene, changed-file lints against the shared a115e42 layer, and the tidy-surface audit passed. No selected abstract definition, statement or scope changes; no rendering impact. Original geometric/native mathematics is unchanged. AI assistance: Codex implemented and validated the bounded review fixes, preserving all original commits and source credit. * feat(WordRAM/Hashing): add self-contained k-wise independent and tabulation hashing programs * fix(WordRAM/Hashing): compose isKWiseIndependentHash_eval and extract ExactLog * chore(WordRAM/Hashing): update Nat.strong_induction_on case labels for cslib-community#1694 * feat(Algorithms/WordRAM): Pagh-Rodler cuckoo hashing on the randomized Word RAM * Refine Pagh-Rodler and Dietzfelbinger-Woelfel source mapping in docstrings * Extract UniformSubset and UniformLoopExit modules and add references.bib entries --------- Co-authored-by: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
…crete stage bound (cslib-community#1704) * feat(Foundations): correction factorization and reward transport for transition matrices Pure linear algebra for the correction-and-copy hierarchy (cslib-community#1444 Phase 2, ideas 2 and 4 of cslib-community#474), following the OpenAI preprint (2026-09-23), Section 4: the factorization 1 - (C - E + EC) = (1 + E)(1 - C), the corrected inverse, copy splitting intertwined with its projection, and the reward transport identity with the stage error bound. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * fix(Foundations): expose IsStrictUpperTriangular so importers can apply it Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * fix(Foundations): separate row-sum control from nonnegativity; add reward lower bound Review of cslib-community#1676: correction_mulVec_one_le only shows that row sums do not grow, so its docstring, the module summary and the test comment no longer call it substochasticity. Add rewardTransport_mulVec_nonneg, the lower half of (4.30), under nonnegative projections, corrections and reward. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * feat(Foundations): factorial truncation of cutoff corrections Second slice of cslib-community#1444 Phase 2 (idea 3 of cslib-community#474), following the OpenAI preprint (2026-09-23), Lemma 4.1 and Lemma 4.4: the cutoff correction recursion E = phi((C + EC)) on a strictly upper triangular C has a unique fixed point, its iterates increase towards it, and after k iterations the error is at most f e^(1/theta) (L/theta)^k / k!, independently of the size of the matrix. The corrected matrix of a finite iterate is nonnegative and small in fully corrected columns. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * refactor(Foundations): use Nat.sum_Icc_choose for the hockey-stick step Review nit on cslib-community#1677: drop the private hockey-stick lemma. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * doc(Foundations): count chains with the integer support size Review of cslib-community#1677: the module docstring now bounds the chain count by m.choose k for the actual support size m, as the proof does. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * feat(Probability): retention by pairwise independent hashing (cslib-community#1444) A point is retained when its hash lies in a target set B. Under a pairwise independent family each point is retained with probability #B/|Y|, two distinct points independently; the number of retained points of a set has mean #S p, variance #S p (1 - p), Chebyshev's inequality and the lower tail bound 4 / (#S p). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * feat(Foundations): one stage of the correction-and-copy hierarchy Third slice of cslib-community#1679 (Phase 2 of cslib-community#1444, ideas 3 and 4 of cslib-community#474), following the OpenAI preprint (2026-09-23), Lemma 4.2, Lemma 4.4 and Proposition 4.5: row-sum, entry, domination and support bounds for cutoff corrections; the copy step with explicit split fractions, its density and active-copy bounds; incidence counting; and the one-stage rates that feed the stage bound, given an abstract detector interface. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * feat(Probability): affine retention channels over a prime field (cslib-community#1682) Identifiers y : ZMod P are retained when A y + b lies in the box {v | all coordinates < L} of ZMod P ^ H. Exact rates (L/P)^H and their squares for pairs, the lower tail 4/(#A pi), independence of separate seeds, and the assembled channel properties at rate f = a^H with L = ceil(P a): f <= pi <= 2^H f. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * feat(Foundations): copy stages preserve strict upper triangularity Add cutoffCorrectionIter_isStrictUpperTriangular, cutoffCorrection_residual_isStrictUpperTriangular and copyStage_isStrictUpperTriangular (for the lexicographic order on Lex (V × Fin (m + 1))), so a stage's output can feed the next stage. Correct two descriptions: the pilot inputs have bounded row sums, not necessarily at most one, and copyStage_mulVec_one_le preserves the row-sum bound, with nonnegativity from copyStage_nonneg. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * refactor(Foundations): general copySplit_isStrictUpperTriangular beside copySplit State the preservation lemma for arbitrary weights and proportions in CorrectionHierarchy.lean, for the lexicographic order on Lex (V × ι), and derive copyStage_isStrictUpperTriangular from it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * feat(Foundations): pilot with step-dependent multipliers and probabilistic column detectors Phase 2 slice 4 of cslib-community#1444 (tracked in cslib-community#1679): the pilot of Lemma 4.2 with step-dependent multipliers, the column detector of Lemma 4.3 over an abstract retention-channel interface, and one stage of the hierarchy whose multipliers, copy weights and overloaded set come from the detector, discharging the detector interface of copyStage_rates. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * refactor(Foundations): derive fixed-multiplier iterate bounds from IsCorrectionSeq The row-sum, entry and input bounds of cutoffCorrectionIter in CopyStage are the fixed-multiplier case of the correction-sequence bounds; reuse them instead of re-proving. Statements are unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * feat(Probability): affine retention channels satisfy the detector interface Instantiate RetentionChannels (cslib-community#1696) with the affine channels of cslib-community#1688 at rate a^H, with c_pi = 1, C_pi = C_pair = 2^H and C_var = 4. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * feat(Foundations): constants of the correction-and-copy hierarchy Bundle the constants and cutoffs of one hierarchy stage with all conditions used by the stage lemmas, prove that they exist for every density divisor q > 0, and restate one detector-driven stage with the bundled constants. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * feat(Foundations): the iterated correction-and-copy hierarchy and its stage bound Iterate the detector-driven stages on V (l+1) ≃ Lex (V l × Fin D₀) at rates q⁻¹ ^ l and prove 0 ≤ p x - W_l(x̄_l) ≤ |V 0| (2^c)⁻¹^l from the construction. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * doc(Foundations): document every HierarchyParams field Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * feat(Probability): affine channels at every stage of the hierarchy Stage l hashes identifiers into a prime field P_l >= max(2^l, M l) at rate (2^H)^-l with uniform constants, discharging the channel hypotheses of sub_hierarchyReward_le; radix identifiers give a fully concrete instance. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * doc(Foundations): clarify reduced hierarchy parameter scope Address cslib-community#1702 review5707105708: parameter existence is the reduced algebraic-stage package. Preserve the full threshold ladder and root/complement regularity gap for Q and every step cutoff. Correct m=ceilNat(q)*(k+1) and D0=m+1. No Lean declaration or proof body changes. Codex worker codex-hierarchy-fixes-1702-1704-20261030. Source-only preparation; supported-pin integration, full validation and outside delta review remain required before publication. * refactor(Probability): share hierarchy radix identification Move radixCopyEquiv, radixCopyEquiv_val and radixCopyEquiv_lt verbatim beside DetectedHierarchy. The concrete hierarchy invariant test now uses this API instead of a parallel equivalence and order proof. Keep finProdFinEquiv reuse and original authorship. Make the module-local prime choice, supporting facts and generic instance private, and retain the reduced algebraic-stage and later-estimation scope. Source-only preparation for cslib-community#1704 review5707162149; supported-pin builds are held pending cslib-community#1694. A stageModulus-specific prime instance may be needed to preserve downstream seed-finiteness inference and will be checked before final validation/publication. * fix(Foundations): qualify Matrix apply lemmas for the rc2 Mathlib API Under rc2 the root-namespace add_apply/neg_apply/sub_apply/mul_apply/one_apply no longer apply to matrices; use the Matrix.* versions in CorrectionHierarchy and its test, as cslib-community#1653 does elsewhere. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit ea663ce) * fix(Foundations): qualify Matrix apply lemmas in FactorialTruncation for rc2 Under rc2 the root-namespace add_apply/sub_apply/mul_apply no longer apply to matrices; use the Matrix.* versions in FactorialTruncation and its test, rewrapping lines that crossed 100 columns. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit 19cf8a8) * fix(Foundations): qualify Matrix apply lemmas in CopyStage and PilotCorrection for rc2 Under rc2 the root-namespace add_apply/sub_apply/mul_apply no longer apply to matrices; use the Matrix.* versions, as rc2-refresh/1676 and /1677 do for the lower modules of this stack. Proof-only; no statement changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit 34406a0) * fix(Probability): retain prime stage-modulus inference Keep the generic prime-choice implementation and supporting facts private. Make stageModulus a non-exposed definition with the same body: Lean rejects the private helper in the exposed abbreviation body. Export only Fact (stageModulus M l).Prime, using the private primality fact, so Mathlib derives NeZero and the finite-field/seed structures for actual hierarchy clients. Confirmed missing NeZero(stageModulus) and Fintype(stageSeed) in the real hierarchy module after privacy; the existing DetectedHierarchy and HierarchyChannels fixtures pass the strict focused build with this bridge (6152 jobs). No new prime-size, encoding, channel or resource guarantee. Full final validation and outside exact-head API delta review follow. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Co-authored-by: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Closes #1684; follows the landed rc2 migration #1653. Advance CSLib
8a8ad748→254e30e6and inherited Mathlib9d581dff→69552756, keeping root, API-doc and guide manifests aligned. Lean, doc-gen4 and Verso stay on their existing rc2 pins. Separate commits update pins and repair fourteen strong-induction case labels in twelve local proof files. Local public statements, definition bodies, models, encodings, independent resource bounds and source credit are unchanged.The outside source/pin review covers CSLib's one-commit diff and a targeted audit of the 96-file Mathlib diff, with its limits stated there. It checks the relevant Turing/computability, PMF, bit/list, matrix and automation surfaces, Nat recursor/proof-parameter changes and actual clients; it is not a complete semantic audit of Mathlib. The final upstream audit reports pin CURRENT and the same fourteen documented unpublished-machine-rewrite MOVED markers; those adaptations are preserved.
At
ec19e875b8fe86d9309da5c1ca3b2af85834b9d1, all six local gates, statics and hosted source CI pass. API and Guide builds, coverage, links, complete retained-source provenance and representative browser inspection pass. The independent artifact review records artifact IDs, digests, reproduction commands and scope in one place. Affected output covers the twelve edited local modules plus upstream List.IsChainFromTo; URM.StraightLine is outside this documentation closure and was source-reviewed only. The reviewed site is below the hosting size limit. The exact-head hosted API/Guide build also passes; its downloadable site artifact received bounded provenance and delta review, reusing the unchanged local render review.The 22 selected abstracts and 35 headline statements, definitions and scopes are unchanged; bridges/audits pass, the PDF renderer is unchanged, and PDF generation passes. Existing PDF content review carries forward. Original rc2 evidence remains in #1653. Keep the broader #1648 tracker open; this is a pin/proof-compatibility update, with no new mathematics or headline promotion.
The integration record tracks final combined-tree validation, landing and cache publication.
AI assistance: Codex implemented the pin/proof update, inspected targeted dependency diffs, validated the result and arranged separate-context source/artifact reviews. Agent review is not human approval.