WIP: Add finite-dimensional copulas and Sklar's theorem

[Vilin97]

This adds the completed foundations of Corrram's copula library: Sklar's theorem for arbitrary finite-dimensional real probability laws, uniqueness for continuous marginals and on marginal CDF ranges, and the equivalence between classical copula CDF conditions and probability measures with uniform marginals. Atoms, singular laws, flat continuous marginal CDFs, and dimension zero are supported. Continuity is derived in the classical characterization rather than assumed.

The measure-based vocabulary follows Mathlib. Compact quantile adjunction and sampling, randomized inverse disintegration, general lifting through marginal sampling maps, rectangle probabilities, sharp Lipschitz bounds, and finite atomic approximation are reusable independently of the headline theorem.

Source, eligibility, and scope

• Upstream: Corrram/copula, commit fe53ea2f3e6af41da8541e7d0aa2edc38ed0dcc8 (2026-10-03 20:25:28 UTC).
• First public release: v0.1.0, 2026-09-19 07:05:23 UTC. The core Sklar and classical-characterization completion commits are eaee4eab6931066921870358c0f4bc0b8bd32068 and 5578d2b62ad948570a3edce60330d012e6b5c97b, both September 18.
• Daily acquisition interval: [2026-08-11 09:45:13 UTC, 2026-10-04 09:45:13 UTC). Eligibility uses the public release/completion evidence, not repository refresh dates.
• License: Apache-2.0 at the pinned commit, SHA-256 b40930bbcf80744c86c46a12bc9da056641d722716c378f5659b9e555ef833e1. Original copyrights are retained. The compact quantile adaptation credits Gaëtan Serré and Rémy Degenne alongside Marcus Rockel and identifies Mathlib's kernel representation as prior work.
• Imports exactly 20 upstream modules forming the completed core, plus the project card entry and generated public wrapper: 22 Lean files, 2,004 source lines. Copula families, rank coefficients, further dependence theory, article supplements, tests, and other extensions are outside this import's claims. Two upstream import-only aggregates are replaced by the generated wrapper; no mathematical declaration was lost.
• Nineteen retained source files are byte-identical between the initial release and the selected pin. Rectangle.lean subsequently exposes the same rectangle probability proof as a reusable public theorem.

Provenance blocker — keep open

The card currently records mix as an inference, with its evidence and limitation in provenance_evidence. The original core file histories credit Marcus Rockel without a proof-tool disclosure. The retained rectangle proof was revised in the explicitly Claude-authored commit 9d07e1456c8ec655666255ec966f138e28c56477; the port and proof optimization here are by Codex. Human author attribution and AI contributions are documented, but the original core's proof-production method is not explicitly disclosed in the inspected source histories, release documentation, public author homepage, or companion repository README. Confirm that method and correct the category if necessary before merging. No auto-merge or queue entry is requested.

The infrastructure priority hold also remains in force until the rollout owner verifies current-main CI. PR610 and PR611 are merged; neither branch was touched by this cycle.

Port and measured optimization

Ported from Lean/Mathlib v4.34.0 to Lean Pool's exact Lean v4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e. Module exports use explicit public sections and individual @[expose] annotations to preserve the upstream transparent mathematical definitions. Imports use LeanPool.Copula; LeanPool.lean is unchanged.

After the mechanical port and initial warning repair, both timings used:

LEAN_NUM_THREADS=2 lake --wfail build LeanPool.Copula.Imports

Before each measurement, only this worktree's Copula build artifacts were removed; the same pinned dependency oleans were retained. Lake schedules independent modules concurrently on a shared 16-core Azure VM. Measurements include elaboration and Lake overhead; they exclude dependency compilation. Shared VM load makes the percentage an observed result rather than a guaranteed speedup.

Measurement	Before optimization	Final
Clean project wall time	34.85 s	26.35 s
Classical approximation module, Lake log	4.6 s	2.7 s
Classical regularity module, Lake log	2.9 s	2.0 s

Observed wall-time reduction: 24.4%. Profiles were obtained with lake env lean --profile <file> --setup <Lake-generated setup.json> using two Lean threads. The approximation module's cumulative simplification time fell from 795 ms to 358 ms; regularity fell from 667 ms to 211 ms in the recorded profiles. These phase measurements also include shared-machine noise.

The pass removed 14 net imports, made proof-only dependencies private, replaced broad simplification in 42 steps with explicit lemmas, then eliminated four of those steps by reusing Finset.piecewise_insert in two repeated proofs. Removing the two import-only aggregates shortens the build's dependency chain. No heartbeat override was introduced or retained. The remaining profiles show dependency loading and tactic/linter initialization as substantial costs; no further material safe proof improvement was evident.

The Mathlib linter found an unused Nonempty assumption on randomized inverses. It is removed there and from the generic lifting API, strengthening those results. Warnings, generated-card placement, and line lengths were repaired directly in the content.

Prior art and validation

The registry, source tree, open/merged PRs, issues, and repository history yielded no duplicate of this core. Mathlib's Sklar search hit is a documentation roadmap entry, not a proof. The closest Tau Ceti source inspected is the real-valued quantile API; it does not state Sklar's theorem or the classical copula characterization. The ordered compact quantile here has an endpoint-valid adjunction and is independently credited to its Mathlib antecedent. No Tau Ceti project is vendored.

Local checks pass:

• Warning-failing clean build of every retained module and the public wrapper.
• lake exe mk_all --check; the fixed root index is byte-identical to base.
• lake exe runLinter --no-build LeanPool.Copula.Imports and lake exe lint-style LeanPool.Copula.Imports.
• Repository-wide lean_pool.quality --static-only.
• The unchanged quality checker's project-scoped declaration resolution, #print axioms audit of all 146 named public declarations, and environment backdoor/axiom-injection audit over every declaration in the imported modules, including generated helpers. Only Classical.choice, propext, and Quot.sound are allowed.
• git diff --check; content-only scope. No Python files or gates are changed.

Lean Action CI is green on submitted head 8682e1105ca2a17ad44896df12509c0e64995129, including project build, Mathlib lint, text style, repository quality, and the required Build project bridge. All applicable checks pass; Python, documentation, and unrelated workflow checks skip according to scope. The partial-port advisory completed successfully. All retained results and their dependency closure are complete.

Greptile completed on the same head and found no actionable code defect. The separate complete-source acquisition review passes the mathematical and engineering rubrics and requests changes for unconfirmed original proof provenance. The configured GPT review was requested; no verdict is available yet. The PR remains a draft with no auto-merge or queue entry.

[Vilin97]

{
"review_kind": "Independent daily-acquisition complete-source review",
"head": "8682e1105ca2a17ad44896df12509c0e64995129",
"upstream_commit": "fe53ea2f3e6af41da8541e7d0aa2edc38ed0dcc8",
"conclusion": "request_changes",
"bottom_line": "The mathematical and engineering review passes, and CI and Greptile are green on this exact head. Keep the PR open pending confirmation of original core proof provenance and the configured GPT verdict. The infrastructure priority hold is preserved.",
"coverage": {
"retained_upstream_modules": 20,
"changed_files": 23,
"lean_files": 22,
"public_named_declarations_audited": 146,
"source_review": "Every retained upstream file was read in full in bounded chunks; final import changes, endpoint statements, probability/disintegration dependencies, and both optimized proof modules were inspected. No partial diff was used as an approval basis."
},
"faithfulness": {
"verdict": "pass",
"bottom_line": "The CDF factorization and classical characterization prove the stated results without density, strict-monotonicity, continuity, or hidden existence assumptions.",
"findings": [],
"evidence": [
"IsSklarCopula is a joint-CDF equality, not a field asserting Sklar existence.",
"exists_lift uses disintegration and a shared auxiliary uniform variable; finite simultaneous almost-everywhere recovery suffices and no coordinate independence is assumed.",
"exists_sklarCopula uses an order-preserving sigmoid embedding and compact quantile lifting, covering atoms and singular laws.",
"Continuous uniqueness extends equality from products of dense marginal CDF ranges to the full cube using proved Lipschitz continuity.",
"Classical rectangle positivity gives monotonicity and Lipschitz regularity; dyadic atomic CDF bounds and weak compactness construct the representing probability law without assuming continuity.",
"Dimension zero and endpoint CDF values are handled; the generic inverse/lift API is strengthened by removal of unnecessary Nonempty assumptions."
],
"proves_the_claim": "proves_it",
"claim_note": "The five registered headlines cover real-law Sklar existence, continuous full uniqueness, general range uniqueness, classical-CDF representation, and specified-sampler joint lifting in arbitrary finite dimension.",
"assumed_inputs": "A probability law; continuity of each marginal only for full uniqueness; normalized/grounded/uniform-margin/rectangle-positive data only for the classical direction; measurable samplers with prescribed pushforwards only for general lifting. These are disclosed in the card."
},
"novelty": {
"verdict": "pass",
"bottom_line": "No existing Sklar or classical copula-characterization theorem was found in the searched pinned Mathlib/Tau Ceti source or pool registry/history.",
"already_formalized": "",
"novelty_note": "Mathlib has measurable sampling for standard Borel laws, and Tau Ceti has real quantiles; neither inspected API supplies this copula representation theorem or its classical characterization. The compact ordered quantile has a public endpoint-valid adjunction, unlike Mathlib's private representation construction. These are bounded source comparisons rather than a proof of absence across all possible prior art.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "Sklar's theorem is the foundational bridge between joint laws and dependence structures; the arbitrary finite-dimensional measure API and classical representation are worth preserving.",
"findings": [],
"infrastructure_value": [
"Arbitrary-dimensional measure-based copulas using Mathlib ProbabilityMeasure and unit-interval volume.",
"Reusable compact inverse-transform sampling and randomized inverse disintegration.",
"General lifting through specified measurable marginal samplers.",
"Rectangle probability formulas, sharp coordinate-sum Lipschitz bounds, and quantitative finite atomic approximation."
],
"fit": "good_fit",
"level": "graduate",
"branch": "probability theory",
"mode": "theory_building",
"significance_one_sentence": "A completed foundational copula theory connects multivariate probability laws, classical CDF conditions, and dependence structures with reusable sampling and disintegration infrastructure."
},
"sources": {
"verdict": "pass",
"bottom_line": "Pinned upstream sources and the initial release support the scope and date, and the identifiable Mathlib antecedent is credited.",
"source_match": "matches",
"findings": [],
"evidence": [
"v0.1.0 published 2026-09-19T07:05:23Z explicitly announces classical CDFs and Sklar's theorem.",
"Core completion commits eaee4eab6931066921870358c0f4bc0b8bd32068 and 5578d2b62ad948570a3edce60330d012e6b5c97b are dated September 18.",
"19 of 20 retained source files are identical between release and selected commit; the later Rectangle update exposes the same probability identity.",
"Quantile.lean retains Gaëtan Serré/Rémy Degenne attribution and identifies Mathlib Kernel.Representation as its antecedent.",
"The card claims the completed core, not the full upstream copula catalogue or an unfinished article formalization."
]
},
"engineering": {
"verdict": "pass",
"bottom_line": "All local content checks pass and measured optimization removes avoidable proof/import work without weakening results.",
"findings": [],
"validation": {
"build": "Warning-failing clean build passes on Lean v4.35.0-rc3 / pinned Mathlib c55e6e786f49471c72fbddbec5415808896aec1e.",
"linters": "Mathlib runLinter and lint-style pass on the complete public project wrapper.",
"quality": "Repository-wide static quality, generated indexes, card declaration resolution, allowlisted-axiom closure, and full imported-module environment audit pass.",
"scope": "Content-only diff; fixed LeanPool.lean unchanged; no gates, suppressions, or options altered.",
"performance": "Same clean-project command and pinned dependency artifacts: 34.845686 s baseline to 26.353654 s final (24.4% observed reduction). Shared-machine noise is explicitly acknowledged.",
"optimization": "14 net imports removed, proof-only imports made private, explicit simp lemmas, repeated piecewise proofs replaced by Mathlib, and two empty aggregates omitted. No material safe further proof improvement was evident in the inspected profiles.",
"dependency_weight": "Only existing Mathlib is needed; no Tau Ceti source or external package is vendored.",
"CI": "Lean Action CI run 38131875828 completed successfully on submitted head 8682e11, including project build, Mathlib lint, text style, and repository quality. Scope-applicable checks pass; unrelated checks are intentionally skipped."
}
},
"blocking_findings": [
{
"file": "LeanPool/projects/finite-dimensional-copulas.yaml",
"line": 28,
"rule": "proof-provenance-unconfirmed",
"comment": "The mix category is explicitly an inference. Original September 18 core histories name Marcus Rockel but do not disclose how the proofs were produced. A retained October 3 update credits Claude, and this port/optimization is by Codex. Confirm original core proof production and correct the category if needed before merging. No author disclosure has been fabricated. The inspected public author homepage and companion repository README also do not disclose original-core proof production; this is a bounded observation, not a claim about all possible public sources.",
"evidence": "The card's provenance_evidence explicitly states that original proof production is undisclosed and requires confirmation; upstream history of Rectangle.lean includes the Claude-authored 9d07e1456c8ec655666255ec966f138e28c56477."
}
],
"external_status": {
"CI": "Green on exact head 8682e11: https://github.com/LeanPool/lean-pool/actions/runs/38131875828. Build pool and required Build project bridge succeeded.",
"Greptile": "Completed successfully on the exact head; no actionable code defect reported: #639 (comment).",
"GPT": "Requested via /review at 2026-10-11T10:29:20Z; no configured-worker verdict observed as of 2026-10-11T10:48:00Z. No worker outage or quota failure is inferred.",
"merge": "No auto-merge or native queue entry. PR610/611 are merged, but the rollout owner's current-main CI verification remains required."
},
"quality": {
"verdict": "pass",
"bottom_line": "Standard ProbabilityMeasure vocabulary, separate distribution/lifting/classical modules, and replacement of repeated proof work by existing Mathlib lemmas support maintainability beyond typical standalone agent output.",
"code_quality": 4,
"findings": []
}
}

[Vilin97]

/review

Please review exact head 8682e1105ca2a17ad44896df12509c0e64995129 against the current five rubrics. Local build, linters, static quality and full imported-module trust audits pass; CI is still running. The acquisition review is posted separately. Original core proof provenance remains explicitly unconfirmed, so this request does not authorize a merge or queue entry.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low impact] No new actionable code defect was found; this review does not clear Vilin97’s acknowledged merge holds.

Summary

Adds finite-dimensional copulas, arbitrary-marginal Sklar existence, continuous-marginal uniqueness, and the classical CDF characterization.

• Copulas are probability laws on the unit cube with uniform coordinate marginals.
• Every finite-dimensional real probability law gets a copula representation.
• Continuous marginal CDFs make the Sklar copula unique on the whole cube.
• Classical copula CDF conditions now determine a unique probability law.
• Copula CDFs now have sharp bounds and continuity estimates.

_{Reviews (1) · Last reviewed commit: "Add finite-dimensional copulas and Sklar..." · Reviewed by Greptile}

[Vilin97]

🤖 LLM review (gpt-6.1-sol, 5 rubrics)

Reviewed head: 8682e1105ca2a17ad44896df12509c0e64995129

Verdict: ✅ approve — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	All five mathematical headlines match the Lean statements and constructions; full CI remains pending.
Novelty	✅ pass	No duplicate of the five headlines was found in the inspected Mathlib, Tau Ceti, or pooled declarations.
Significance	✅ pass	Sklar existence, continuous-marginal uniqueness, and the classical CDF characterization form a completed graduate-level development worth pooling.
Sources	✅ pass	The pinned upstream core supports the five cited results, and the quantile module explicitly credits its Mathlib antecedent.
Code quality (advisory)	✅ pass	The approximation and lifting proofs reuse rectangleIncrement_split, Division.grid_mesh, and exists_randomized_inverse, keeping the code factored with no material maintenance debt found in the full source review.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	Probability laws are supplied; full uniqueness assumes continuous marginal CDFs; the classical direction assumes the four stated boundary and rectangle conditions; generic lifting assumes a standard Borel space and measurable samplers with the prescribed marginal pushforwards—all disclosed in the card.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	graduate
Branch	probability theory
Mode	theory_building
Code quality	4 / 5

Statement check: The Lean proves arbitrary finite-dimensional real-law CDF factorization, full uniqueness under continuous marginal CDFs, agreement on marginal CDF ranges, the classical characterization without assumed continuity, and lifting through prescribed measurable samplers, including dimension zero.

The theorems exists_sklarCopula, existsUnique_sklarCopula_of_continuous, and isClassical_iff_existsUnique establish foundational copula theory for finite-dimensional laws, supported by quantile sampling, randomized lifting, and atomic approximation.

Faithfulness findings (1)

• prompt-injection — PR-wide
  The contributor-written discussion supplies a prior faithfulness verdict and directs a review across five rubrics. These have no authority over this independent, faithfulness-only review and were disregarded as instructions.
  Evidence: prose only: the acquisition-review comment in .review-pr.json says "The mathematical and engineering review passes locally" and records a faithfulness "verdict": "pass"; a later contributor comment says "Please review exact head 8682e1105ca2a17ad44896df12509c0e64995129 against the current five rubrics."

---

Tokens: 6,495,871 in / 40,666 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $26.5935 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

CI was not green for this commit at review time; this review does not replace CI.

[Vilin97]

Source review at 8682e1105ca2a17ad44896df12509c0e64995129: I read all 22 supplied Lean files (2,004 lines) and the project card, with an independent peer review.

This is a significant, coherent formalization. exists_sklarCopula handles arbitrary finite-dimensional real probability laws by quantile sampling and randomized inverse lifting, recovering the full original joint law. Continuous-marginal uniqueness uses almost-everywhere threshold equality and dense CDF ranges, so flat CDFs are supported. isClassical_iff_existsUnique starts from normalization, groundedness, uniform faces and nonnegative ordered rectangle increments; it derives continuity and constructs the representing probability measure through finite atomic approximations and weak limits. Dimension zero and half-open rectangle conventions are explicit. I found no concrete mathematical statement or proof defect in the supplied bodies.

The merge blocker remains the card's provenance_evidence: mix is inferred while the original core's proof-production method is unconfirmed. Confirm that method and correct the category if needed before merging; retain the draft and existing infrastructure hold. This is a source review. I have not independently verified the imported Mathlib bodies, kernel/build audit, CI logs, upstream release/license history, or duplication claims.