[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 accepted

The card retains the disclosed project-level mix classification: the original core is attributed to Marcus Rockel, the retained rectangle proof has an explicitly Claude-authored revision 9d07e1456c8ec655666255ec966f138e28c56477, and the port and proof optimization include Codex contributions. The original core's proof-production method remains unspecified; this does not certify that it was exclusively human-written. The independent reviewer accepts this evidence and classification under the repository's provenance rules.

The completed mathematical core is preserved byte-for-byte. The current integration commit incorporates main 9a853f89bd0e191a181ca32017aaddb47a9ea4fa and replaces only the card's obsolete confirmation imperative with that factual limitation. Its fresh required checks must pass before protected queue admission. PR610 and PR611 are merged, and that main's applicable own-push validation is qualified.

Historical author port and measurement notes

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 original-head 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 original provenance condition is resolved above; current integration validation remains required.

[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 8682e1105ca2a17ad44896df12509c0e64995129, 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 8682e1105ca2a17ad44896df12509c0e64995129: 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: https://github.com/LeanPool/lean-pool/pull/639#issuecomment-6108091423.",
    "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 actionable code defect was established, but the unverified source and dependency comparisons prevent an unconditional merge recommendation.

Summary

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

• Every finite real joint law now has a copula factorization.
• Classical copula conditions now determine one probability law.
• Continuous marginal CDFs give a unique copula on the whole cube.
• Copulas now have measure, CDF, and rectangle-probability tools.

_{Reviews (2) · Last reviewed commit: "Integrate the completed Copula core and ..." · 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.

[github-actions]

This PR has been inactive for 30 days and is marked stale.

[Vilin97]

Approve — completed source and disclosed mixed provenance accepted at d56c8f3e7f168df4b8b4283f371103a1555e3181.

The existing favorable mathematical review and configured review 2077 stand. The original core is attributed to Marcus Rockel; a retained rectangle proof has an explicitly Claude-authored revision, and the port includes Codex proof work. This supports the card's disclosed project-level mix classification. I do not require an additional certificate of every original proof's production method, and do not claim that the original core was exclusively human-written.

I replaced the obsolete confirmation imperative with that factual limitation, reconciled the PR description, and marked the completed contribution ready for review. The integration commit preserves the entire Copula proof subtree and facade byte-for-byte while incorporating qualified main 9a853f89. Fresh checks on this head must pass before normal protected queue admission; the old head's green checks are historical.

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 38.75 s (= 0.65 min) — user 49.30 s, sys 19.40 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 167,533 maxHeartbeats units across 22 valid files (2,004 added LOC).

Sum of lean --profile: 44315.0 ms (= 44.31 s) across 22 valid files. Import-excluded time: 14905.0 ms (= 14.90 s).

Count-heartbeats wall-clock total: 93.28 s. Repeated import cost inside lean --profile: 29410.0 ms (= 29.41 s).

Heartbeat values sum disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted from raw allocations to maxHeartbeats units by dividing by 1000. They include command elaboration and kernel checking, exclude imports, and include profiler overhead; they are not comparable to the deprecated linter's totals. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Commands	Errors
LeanPool/Copula/Classical/Regularity.lean	195	25,913	6.04	2.65	1.40	1.25	67	0
LeanPool/Copula/Classical/Characterization.lean	127	23,570	5.51	2.20	0.94	1.26	27	0
LeanPool/Copula/Classical/Approximation.lean	285	22,745	7.08	3.55	2.29	1.26	38	0
LeanPool/Copula/Rectangle.lean	156	17,804	5.99	2.63	1.38	1.25	20	0
LeanPool/Copula/CDF/Bounds.lean	58	10,138	5.31	1.95	0.72	1.23	11	0
LeanPool/Copula/Classical/Basic.lean	102	9,821	4.25	1.84	0.58	1.26	31	0
LeanPool/Copula/CDF/Continuity.lean	76	6,628	4.59	1.93	0.69	1.24	13	0
LeanPool/Copula/CDF.lean	91	6,308	3.46	1.97	0.73	1.24	18	0
LeanPool/Copula/Sklar/Lift.lean	65	6,073	4.44	1.78	0.53	1.25	8	0
LeanPool/Copula/Comonotonic.lean	47	6,012	3.88	1.76	0.51	1.25	10	0
LeanPool/Copula/Distribution/RandomizedInverse.lean	59	5,935	4.17	1.85	0.53	1.32	8	0
LeanPool/Copula/Sklar/Continuous.lean	139	5,315	4.27	1.91	0.64	1.27	28	0
LeanPool/Copula/Distribution/Quantile.lean	86	5,200	4.29	1.79	0.57	1.22	12	0
LeanPool/Copula/Independence.lean	47	4,377	4.17	1.70	0.47	1.23	11	0
LeanPool/Copula/Distribution/ProbabilityIntegralTransform.lean	104	4,114	3.92	1.84	0.58	1.26	14	0
LeanPool/Copula/Basic.lean	98	2,204	3.88	1.71	0.48	1.23	22	0
LeanPool/Copula/CDF/Extensionality.lean	60	1,894	2.88	1.64	0.38	1.26	11	0
LeanPool/Copula/Sklar/UnitInterval.lean	45	1,562	3.46	1.62	0.35	1.27	10	0
LeanPool/Copula/Sklar/General.lean	63	1,320	3.17	1.70	0.35	1.35	9	0
LeanPool/Copula/Unique.lean	41	597	2.67	1.56	0.32	1.24	11	0
LeanPool/Copula.lean	31	0	3.31	3.25	0.23	3.02	3	0
LeanPool/Copula/Imports.lean	29	0	2.54	1.47	0.22	1.25	1	0
Total	2,004	167,533	93.28	44.31	14.90	29.41	383	0

Aggregate phase totals

Phase	Time
import	29410.0 ms (= 29.41 s)
interpretation	6158.0 ms (= 6.16 s)
typeclass inference	3194.3 ms (= 3.19 s)
tactic execution	1377.2 ms (= 1.38 s)
simp	1167.4 ms (= 1.17 s)
initialization	809.3 ms (= 0.81 s)
elaboration	575.5 ms (= 0.58 s)
type checking	386.0 ms (= 0.39 s)
linting	199.8 ms (= 0.20 s)
aesop	178.9 ms (= 0.18 s)
blocked (unaccounted)	156.6 ms (= 0.16 s)
parsing	133.3 ms (= 0.13 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.Copula.Distribution.ProbabilityIntegralTransform	5.70 s
LeanPool.Copula.Distribution.Quantile	5.60 s
LeanPool.Copula.Basic	5.50 s
LeanPool.Copula.Distribution.RandomizedInverse	4.90 s
LeanPool.Copula.Rectangle	3.60 s
LeanPool.Copula.CDF.Bounds	3.20 s
LeanPool.Copula.Independence	2.90 s
LeanPool.Copula.Comonotonic	2.80 s
LeanPool.Copula.CDF.Extensionality	2.80 s
LeanPool.Copula.Classical.Approximation	2.80 s
LeanPool.Copula.Sklar.UnitInterval	2.60 s
LeanPool.Copula.Unique	2.60 s

Per-file `lean --profile` output

LeanPool/Copula.lean

import took 3.02s
cumulative profiling times:
	declTypeLinter 0.789ms
	elaboration 0.373ms
	import 3.02s
	initialization 32.3ms
	interpretation 200ms
	linting 0.917ms
	module linting 0.011ms
	parsing 0.053ms
	tacticAnalysis 0.441ms
real 3.98
user 1.35
sys 1.27

LeanPool/Copula/Basic.lean

import took 1.23s
cumulative profiling times:
	attribute application 2.4ms
	blocked (unaccounted) 6.61ms
	compilation (IR) 0.041ms
	compilation (LCNF base) 0.403ms
	compilation (LCNF impure) 0.19ms
	compilation (LCNF mono) 0.152ms
	congr simp thm 1.48ms
	declTypeLinter 6.06ms
	elaboration 41.7ms
	fix level params 0.222ms
	import 1.23s
	initialization 32.1ms
	instantiate metavars 0.255ms
	interpretation 260ms
	let-to-have transformation 0.115ms
	linting 9.37ms
	module linting 0.0135ms
	parsing 6.13ms
	process pre-definitions 2.32ms
	share common exprs 1.01ms
	simp 15.9ms
	tactic execution 22.2ms
	tacticAnalysis 2.98ms
	type checking 14.4ms
	typeclass inference 49.6ms
real 2.30
user 1.45
sys 1.03

LeanPool/Copula/CDF.lean

import took 1.24s
cumulative profiling times:
	aesop 46.6ms
	attribute application 0.815ms
	compilation (IR) 0.156ms
	compilation (LCNF base) 1.13ms
	compilation (LCNF impure) 0.559ms
	compilation (LCNF mono) 0.942ms
	congr simp thm 2.77ms
	declTypeLinter 5.6ms
	elaboration 23.3ms
	fix level params 0.186ms
	import 1.24s
	initialization 39.3ms
	instantiate metavars 0.271ms
	interpretation 282ms
	let-to-have transformation 0.0891ms
	linting 8.36ms
	module linting 0.0174ms
	parsing 6.37ms
	process pre-definitions 2.31ms
	share common exprs 0.984ms
	simp 133ms
	tactic execution 21.2ms
	tacticAnalysis 3.24ms
	type checking 6.98ms
	typeclass inference 139ms
real 2.44
user 1.73
sys 1.01

LeanPool/Copula/CDF/Bounds.lean

import took 1.23s
cumulative profiling times:
	attribute application 0.0343ms
	congr simp thm 1.97ms
	declTypeLinter 2.64ms
	elaboration 14.7ms
	fix level params 0.178ms
	import 1.23s
	initialization 32.4ms
	instantiate metavars 0.261ms
	interpretation 264ms
	let-to-have transformation 0.0415ms
	linting 5.18ms
	module linting 0.0116ms
	norm_num 0.448ms
	parsing 3.83ms
	process pre-definitions 1.72ms
	ring 3.78ms
	share common exprs 1.27ms
	simp 98.8ms
	tactic execution 34.5ms
	tacticAnalysis 3.51ms
	type checking 11.4ms
	typeclass inference 238ms
real 2.60
user 1.71
sys 1.01

LeanPool/Copula/CDF/Continuity.lean

import took 1.24s
cumulative profiling times:
	aesop 65.3ms
	attribute application 0.0664ms
	blocked (unaccounted) 8.85ms
	compilation (IR) 0.0871ms
	compilation (LCNF base) 0.799ms
	compilation (LCNF impure) 0.364ms
	compilation (LCNF mono) 0.632ms
	congr simp thm 1.78ms
	declTypeLinter 2.9ms
	elaboration 19.4ms
	fix level params 0.199ms
	import 1.24s
	initialization 43ms
	instantiate metavars 0.251ms
	interpretation 296ms
	let-to-have transformation 0.0586ms
	linting 6.22ms
	module linting 0.0132ms
	norm_num 0.241ms
	parsing 5.21ms
	process pre-definitions 2.35ms
	ring 4.08ms
	share common exprs 1.19ms
	simp 27.6ms
	tactic execution 54.6ms
	tacticAnalysis 2.68ms
	type checking 16.1ms
	typeclass inference 134ms
real 2.39
user 1.66
sys 1.03

LeanPool/Copula/CDF/Extensionality.lean

import took 1.26s
cumulative profiling times:
	attribute application 0.0313ms
	blocked (unaccounted) 0.951ms
	congr simp thm 0.731ms
	declTypeLinter 4.08ms
	elaboration 9.01ms
	fix level params 0.0948ms
	import 1.26s
	initialization 37.9ms
	instantiate metavars 0.209ms
	interpretation 233ms
	let-to-have transformation 0.0222ms
	linting 4.62ms
	module linting 0.0118ms
	parsing 3.24ms
	process pre-definitions 1.1ms
	share common exprs 0.732ms
	simp 14.3ms
	tactic execution 21.3ms
	tacticAnalysis 1.56ms
	type checking 4.29ms
	typeclass inference 45.5ms
real 2.33
user 1.38
sys 1.03

LeanPool/Copula/Classical/Approximation.lean

import took 1.26s
cumulative profiling times:
	attribute application 0.185ms
	blocked (unaccounted) 135ms
	compilation (IR) 0.388ms
	compilation (LCNF base) 2.82ms
	compilation (LCNF impure) 2ms
	compilation (LCNF mono) 2.64ms
	congr simp thm 11.6ms
	declTypeLinter 7.85ms
	dsimp 14ms
	elaboration 145ms
	fix level params 1.16ms
	import 1.26s
	initialization 33.1ms
	instantiate metavars 2.23ms
	interpretation 511ms
	let-to-have transformation 9.79ms
	linting 36ms
	module linting 0.00986ms
	norm_num 29.1ms
	parsing 21ms
	process pre-definitions 25.5ms
	ring 44.6ms
	share common exprs 10.7ms
	simp 216ms
	tactic execution 436ms
	tacticAnalysis 7.5ms
	type checking 131ms
	typeclass inference 457ms
real 3.06
user 3.18
sys 1.09

LeanPool/Copula/Classical/Basic.lean

import took 1.26s
cumulative profiling times:
	attribute application 0.0666ms
	congr simp thm 1.74ms
	declTypeLinter 3.67ms
	elaboration 29.4ms
	fix level params 0.127ms
	import 1.26s
	initialization 37.9ms
	instantiate metavars 0.372ms
	interpretation 268ms
	let-to-have transformation 0.0622ms
	linting 8.17ms
	module linting 0.0129ms
	parsing 6.84ms
	process pre-definitions 1.56ms
	share common exprs 0.653ms
	simp 77.9ms
	tactic execution 28ms
	tacticAnalysis 4.18ms
	type checking 11.9ms
	typeclass inference 95.3ms
real 2.48
user 1.56
sys 1.05

LeanPool/Copula/Classical/Characterization.lean

import took 1.26s
cumulative profiling times:
	attribute application 0.401ms
	congr simp thm 1.17ms
	declTypeLinter 3.88ms
	dsimp 5.31ms
	elaboration 29.9ms
	fix level params 0.481ms
	import 1.26s
	initialization 40.8ms
	instantiate metavars 1.2ms
	interpretation 408ms
	let-to-have transformation 0.077ms
	linting 17.3ms
	module linting 0.011ms
	norm_num 2.98ms
	parsing 9.28ms
	process pre-definitions 6.01ms
	ring 21.2ms
	share common exprs 5.62ms
	simp 12.3ms
	tactic execution 108ms
	tacticAnalysis 4.96ms
	type checking 22.7ms
	typeclass inference 238ms
real 2.81
user 1.94
sys 1.05

LeanPool/Copula/Classical/Regularity.lean

import took 1.25s
cumulative profiling times:
	attribute application 0.166ms
	congr simp thm 4.61ms
	declTypeLinter 6.92ms
	elaboration 67.7ms
	fix level params 1.07ms
	import 1.25s
	initialization 32.6ms
	instantiate metavars 2.17ms
	interpretation 406ms
	let-to-have transformation 0.204ms
	linting 28.8ms
	module linting 0.0103ms
	norm_num 1.36ms
	parsing 14.9ms
	process pre-definitions 12.1ms
	ring 27.3ms
	share common exprs 8.48ms
	simp 102ms
	tactic execution 161ms
	tacticAnalysis 6.76ms
	type checking 53.4ms
	typeclass inference 466ms
real 2.55
user 2.39
sys 1.04

LeanPool/Copula/Comonotonic.lean

import took 1.25s
cumulative profiling times:
	attribute application 0.635ms
	congr simp thm 1.13ms
	declTypeLinter 1.99ms
	elaboration 11.4ms
	fix level params 0.0937ms
	import 1.25s
	initialization 42.7ms
	instantiate metavars 0.101ms
	interpretation 225ms
	let-to-have transformation 0.0319ms
	linting 3.4ms
	module linting 0.0111ms
	parsing 2.32ms
	process pre-definitions 1.38ms
	share common exprs 0.446ms
	simp 48.8ms
	tactic execution 10.9ms
	tacticAnalysis 1.53ms
	type checking 5.74ms
	typeclass inference 155ms
real 2.46
user 1.54
sys 1.00

LeanPool/Copula/Distribution/ProbabilityIntegralTransform.lean

import took 1.26s
cumulative profiling times:
	aesop 29.6ms
	attribute application 0.597ms
	blocked (unaccounted) 5.19ms
	compilation (IR) 0.0951ms
	compilation (LCNF base) 0.875ms
	compilation (LCNF impure) 0.392ms
	compilation (LCNF mono) 0.605ms
	congr simp thm 1.32ms
	declTypeLinter 5.54ms
	elaboration 23.5ms
	fix level params 0.257ms
	import 1.26s
	initialization 33ms
	instantiate metavars 0.684ms
	interpretation 286ms
	let-to-have transformation 0.0613ms
	linting 8.71ms
	module linting 0.0121ms
	norm_num 0.309ms
	parsing 6.93ms
	process pre-definitions 3.49ms
	ring 6.83ms
	share common exprs 2.54ms
	simp 7.68ms
	tactic execution 59ms
	tacticAnalysis 3.41ms
	type checking 16.7ms
	typeclass inference 78.4ms
real 2.47
user 1.60
sys 1.02

LeanPool/Copula/Distribution/Quantile.lean

import took 1.22s
cumulative profiling times:
	aesop 17.9ms
	attribute application 0.0511ms
	compilation (IR) 0.0491ms
	compilation (LCNF base) 0.443ms
	compilation (LCNF impure) 0.204ms
	compilation (LCNF mono) 0.333ms
	congr simp thm 1.53ms
	declTypeLinter 6.14ms
	elaboration 14.8ms
	fix level params 0.152ms
	import 1.22s
	initialization 41.1ms
	instantiate metavars 0.291ms
	interpretation 246ms
	let-to-have transformation 0.0486ms
	linting 7.74ms
	module linting 0.0134ms
	parsing 3.86ms
	process pre-definitions 2.33ms
	share common exprs 1.01ms
	simp 32.5ms
	tactic execution 60.1ms
	tacticAnalysis 2.97ms
	type checking 12.2ms
	typeclass inference 122ms
real 2.43
user 1.55
sys 1.03

LeanPool/Copula/Distribution/RandomizedInverse.lean

import took 1.32s
cumulative profiling times:
	attribute application 0.0136ms
	congr simp thm 0.603ms
	declTypeLinter 2.28ms
	elaboration 10.6ms
	fix level params 0.296ms
	import 1.32s
	initialization 33.8ms
	instantiate metavars 0.318ms
	interpretation 230ms
	let-to-have transformation 0.0223ms
	linting 4.71ms
	module linting 0.00915ms
	parsing 3.68ms
	process pre-definitions 1.54ms
	share common exprs 0.803ms
	simp 4.07ms
	tactic execution 60.6ms
	tacticAnalysis 1.5ms
	type checking 5.73ms
	typeclass inference 168ms
real 2.57
user 1.57
sys 1.03

LeanPool/Copula/Imports.lean

import took 1.25s
cumulative profiling times:
	declTypeLinter 0.133ms
	elaboration 0.095ms
	import 1.25s
	initialization 31.6ms
	interpretation 191ms
	linting 0.217ms
	module linting 0.0102ms
	parsing 0.00167ms
	tacticAnalysis 0.142ms
real 2.20
user 1.23
sys 1.01

LeanPool/Copula/Independence.lean

import took 1.23s
cumulative profiling times:
	attribute application 0.684ms
	congr simp thm 1.25ms
	declTypeLinter 2.65ms
	elaboration 15ms
	fix level params 0.0692ms
	import 1.23s
	initialization 34.2ms
	instantiate metavars 0.0801ms
	interpretation 229ms
	let-to-have transformation 0.0354ms
	linting 3.66ms
	module linting 0.0114ms
	parsing 2.74ms
	process pre-definitions 1.71ms
	share common exprs 0.399ms
	simp 27ms
	tactic execution 6.1ms
	tacticAnalysis 1.65ms
	type checking 5.38ms
	typeclass inference 137ms
real 2.41
user 1.49
sys 1.00

LeanPool/Copula/Rectangle.lean

import took 1.25s
cumulative profiling times:
	aesop 19.5ms
	attribute application 0.724ms
	compilation (IR) 0.344ms
	compilation (LCNF base) 6.03ms
	compilation (LCNF impure) 1.63ms
	compilation (LCNF mono) 2.96ms
	congr simp thm 6.85ms
	declTypeLinter 5.84ms
	elaboration 48.9ms
	fix level params 0.865ms
	import 1.25s
	initialization 36.9ms
	instantiate metavars 2.95ms
	interpretation 380ms
	let-to-have transformation 0.206ms
	linting 17.3ms
	module linting 0.0112ms
	norm_num 0.628ms
	parsing 13.7ms
	process pre-definitions 7.71ms
	ring 15ms
	share common exprs 6.2ms
	simp 312ms
	tactic execution 126ms
	tacticAnalysis 4.57ms
	type checking 38.5ms
	typeclass inference 322ms
real 2.94
user 2.41
sys 1.02

LeanPool/Copula/Sklar/Continuous.lean

import took 1.27s
cumulative profiling times:
	attribute application 0.381ms
	congr simp thm 0.703ms
	declTypeLinter 5.72ms
	dsimp 2.63ms
	elaboration 36.5ms
	fix level params 0.305ms
	import 1.27s
	initialization 37.9ms
	instantiate metavars 0.568ms
	interpretation 300ms
	let-to-have transformation 0.135ms
	linting 13.1ms
	module linting 0.0118ms
	parsing 10.7ms
	process pre-definitions 3.95ms
	share common exprs 1.82ms
	simp 25ms
	tactic execution 64.5ms
	tacticAnalysis 4.59ms
	type checking 13.5ms
	typeclass inference 119ms
real 2.42
user 1.66
sys 1.04

LeanPool/Copula/Sklar/General.lean

import took 1.35s
cumulative profiling times:
	attribute application 0.0122ms
	declTypeLinter 1.91ms
	elaboration 4.87ms
	fix level params 0.0723ms
	import 1.35s
	initialization 40.7ms
	instantiate metavars 0.182ms
	interpretation 233ms
	let-to-have transformation 0.0107ms
	linting 3.31ms
	module linting 0.0105ms
	parsing 3.34ms
	process pre-definitions 0.938ms
	share common exprs 0.426ms
	tactic execution 33ms
	tacticAnalysis 2.44ms
	type checking 3.57ms
	typeclass inference 19.9ms
real 2.44
user 1.42
sys 1.04

LeanPool/Copula/Sklar/Lift.lean

import took 1.25s
cumulative profiling times:
	attribute application 0.0135ms
	congr simp thm 0.67ms
	declTypeLinter 2.12ms
	dsimp 1.77ms
	elaboration 8.49ms
	fix level params 0.374ms
	import 1.25s
	initialization 38.5ms
	instantiate metavars 0.42ms
	interpretation 247ms
	let-to-have transformation 0.0238ms
	linting 5.42ms
	module linting 0.0151ms
	parsing 5.03ms
	process pre-definitions 1.56ms
	share common exprs 0.84ms
	simp 7.7ms
	tactic execution 47.3ms
	tacticAnalysis 2.43ms
	type checking 5.9ms
	typeclass inference 159ms
real 2.50
user 1.54
sys 1.02

LeanPool/Copula/Sklar/UnitInterval.lean

import took 1.27s
cumulative profiling times:
	attribute application 0.0247ms
	declTypeLinter 2.29ms
	elaboration 10.4ms
	fix level params 0.0884ms
	import 1.27s
	initialization 39.4ms
	instantiate metavars 0.154ms
	interpretation 225ms
	let-to-have transformation 0.0255ms
	linting 3.55ms
	module linting 0.0108ms
	parsing 2.39ms
	process pre-definitions 1.48ms
	share common exprs 0.408ms
	tactic execution 19.5ms
	tacticAnalysis 2.37ms
	type checking 3.74ms
	typeclass inference 39.3ms
real 2.33
user 1.36
sys 1.04

LeanPool/Copula/Unique.lean

import took 1.24s
cumulative profiling times:
	attribute application 0.4ms
	congr simp thm 0.394ms
	declTypeLinter 3.01ms
	elaboration 10.5ms
	fix level params 0.0754ms
	import 1.24s
	initialization 38.1ms
	instantiate metavars 0.299ms
	interpretation 238ms
	let-to-have transformation 0.0287ms
	linting 3.74ms
	module linting 0.0116ms
	parsing 1.71ms
	process pre-definitions 0.93ms
	share common exprs 0.355ms
	simp 4.87ms
	tactic execution 3.43ms
	tacticAnalysis 1.52ms
	type checking 2.87ms
	typeclass inference 12.3ms
real 2.26
user 1.33
sys 1.01

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.