[Vilin97]

This preserves a completed theory of real Michal–Bastiani calculus on Hausdorff locally convex spaces: the chain rule, symmetric continuous higher differentials, weak Taylor formulas, weak integration under sequential/Mackey completeness, and comparison with Fréchet smoothness. These spaces include important infinite-dimensional models outside Mathlib's normed-space calculus. The definitions and compositional API provide infrastructure for later geometry and Lie theory.

The import contains the nine mathematical modules of Gabriel Larotonda's LCAnalysis, its aggregate, a generated public Imports.lean, and one YAML card. Audit scripts, blueprint/doc tooling, and the developing LCManifolds companion are excluded. LeanPool.lean, dependencies, and all gates are unchanged.

Source, eligibility, and provenance

• Upstream: c7c5a228221bba0313e7caee62ca0f9b1e2e5c0f, Apache-2.0; original copyright and attribution retained.
• This run's window is 2026-10-28 10:15:14 ≤ t < 2026-11-04 10:15:14 UTC. Eligibility uses substantive completion commits: the initial calculus/integration development on November 2, the second-order chain rule on November 4 at 02:48:24 UTC, and bounded-below derivatives reflecting smoothness at 03:22:22 UTC. It does not rely on repository refresh times.
• Provenance is AI: the upstream README states that Claude wrote the proofs under Larotonda's mathematical direction. No independent human audit is claimed.
• The principal reference is Glöckner–Neeb, Infinite-Dimensional Lie Groups, especially Definitions 1.1.17/Remark 1.1.18, the higher-calculus results, and Proposition 2.3.17. The card restricts claims to the formalized real/open-domain setting. The bounded-below result is supplied by this upstream development; it is not attributed to a numbered result in the book.
• Deduplication found no matching pool card, source, history, or all-state issue/PR. Mathlib/TauCeti calculus and locally convex sources were compared, including TauCeti's local-injectivity, antilipschitz, and derivative-norm-comparison results. Those concern normed-space calculus and do not supply this locally convex calculus/integration theory. No TauCeti or Mathlib project is vendored.

Port and measured optimization

Ported from Lean/Mathlib 4.36.0-rc2 to the pool's exact Lean 4.35.0 / Mathlib 56a005855ea17e0b0958f73ec801ae140b0a1679. Changes add module/public/expose boundaries, adapt one set-membership proof, replace the broad Mathlib import with specific imports, move the normed comparison into MBFrechet, reuse the all-orders comparison for the former independent C²-to-C¹ proof, and remove unused assumptions from 14 helpers. All 202 public declaration names are retained; no theorem was weakened.

Measured command: lake build LeanPool.LCAnalysis.Imports, after deleting only this project's outputs under .lake/build/lib/lean/LeanPool/ and .lake/build/ir/LeanPool/. Mathlib oleans were present, the filesystem cache was warm, and default Lake parallelism was used on the same shared 16-core VM. Dependency download and tool builds are excluded.

Controlled clean project build	Wall time
Minimally ported upstream baseline, before optimization	62.75 s
Final optimized import	37.38 s

This is a 40.4% wall-time reduction. The build dependency closure shrank from 9,057 to 2,846 jobs; the core module fell from 16 s to 8.0 s. Profiling identified expensive import/typeclass inference rather than a single pathological tactic. Times are observations on shared hardware, not isolated benchmark guarantees. No heartbeat or recursion escape hatch was introduced.

Validation

Passed locally:

• Controlled clean build of the complete imported project, with no warnings.
• lake exe mk_all --check; the fixed pool root is byte-identical to the base.
• lake exe runLinter LeanPool.LCAnalysis.Imports and lake exe lint-style LeanPool.LCAnalysis.Imports.
• Full-repository static quality checks; source size/proof size/card/header/scope checks.
• Existing quality-checker axiom audit of all 202 public declarations, card declaration resolution, and the compiled-environment option/axiom-backdoor audit covering private/generated declarations too. Only Classical.choice, propext, and Quot.sound are allowed; no sorry, custom axiom, unsafe, partial, native decision procedure, or suppression is imported.

No Python code changed. Whole-pool build/quality and protected validation remain CI's responsibility. Greptile, GPT review, and a separate detailed acquisition review must finish before protected queue entry. Daily asynchronous documentation publishing is not a merge gate.

[Vilin97]

Acquisition review of exact head a13503aaaae23ab5c50c08ff334757694d192f9d.

Content verdict: APPROVE. No unresolved mathematical, source, licensing, or engineering findings. This is the acquisition agent's separate source assessment, not the configured GPT or Greptile verdict. Required CI and automated review are still pending and this comment does not authorize queue entry by itself.

I inspected the upstream revision and the complete imported file set in bounded source sections: all nine mathematical modules, their definitions and endpoint statements, the dependency closure, representative hard proofs, the optimized changes, aggregate/wrapper, and YAML card. The review includes the chain-rule limit argument, higher-derivative symmetry and multilinearity, Riemann-sum existence, the tent-curve argument for Mackey completeness, operator-norm bootstrapping, and bounded-below reflection of regularity.

• Faithfulness: HasDirDerivAt (MichalBastiani.lean:56) is the actual punctured difference-quotient limit; ContDiffMBOn (:65) recursively requires derivative existence and joint regularity. It does not bundle the chain rule or higher-derivative theorem as assumptions. The card's six endpoints match the formal quantifiers, real scalar field, open-domain hypotheses, Hausdorff/local-convex assumptions, and explicit completeness hypotheses. HasWeakIntegral (Integral.lean:44) tests every continuous real linear functional; its uniqueness is proved using separation. SeqComplete and MackeyComplete (IntegralExistence.lean:43,49) are disclosed mathematical completeness hypotheses, and the latter is characterized by Lipschitz-curve weak integrability. The bounded-below result (BoundedBelow.lean:291) explicitly has a Banach source, normed target, fixed positive lower bound on every derivative/vector, continuous inner map, and open locally convex test domain. The card states these limitations. The zero-order cases, arbitrary endpoint orientation of integration, and junk values outside derivative/integral existence do not overclaim anything.
• Novelty and reuse: pool cards/source/history and all-state PR/issues yielded no duplicate. I checked current TauCeti/Mathlib calculus/locally-convex module paths and nearest source declarations, including TauCeti's finite-dimensional local-injectivity theorem, compact-set antilipschitz theorem, and derivative-norm comparison. Those do not establish this general locally convex calculus/integration theory. Existing normed Fréchet calculus is reused as a comparison target, not vendored. The new core definitions have consumers throughout the chain, higher, integration, and bounded-below results.
• Significance: this is graduate/research-level theory building with a coherent reusable API for infinite-dimensional geometry and Lie theory. It is a completed calculus/integration development, not an isolated utility lemma or the unfinished geometric companion. There are no generated certificate tables or large opaque proof blobs.
• Sources and licensing: the exact Apache-2.0 upstream revision is recorded; copyright and authorship are retained. The AI provenance agrees with the upstream README. Glöckner–Neeb's definitions of Lipschitz curves/Mackey completeness, their sequence characterization, and Proposition 2.3.17 support the corresponding formal statements; the formal card honestly uses real spaces and open domains. The bounded-below extension comes from LCAnalysis and is not presented as a numbered theorem of that book. Substantive completion commits on November 2–4 establish eligibility in this acquisition window.
• Engineering and trust: specific imports replace the umbrella import; normed comparison is separated from the general core; the special C²-to-C¹ theorem reuses the all-orders comparison. The linter's unused assumptions were removed from thirteen named helpers and one instance, increasing generality. All 202 enumerated public names remain. A Lean elaborated-type comparison finds 189 definitionally identical types; the other thirteen are exactly the helpers with removed hypotheses. Thus the three raw-expression differences caused by different inferred instance proofs are definitionally equal. The named main results' types are preserved. Local clean build, 15 Mathlib linters, style, indexes, complete-repository static quality, card resolution, public-axiom closure, and the private/generated declaration backdoor audit pass. The source introduces no prohibited trust mechanism, option override, or waiver.
• Measured cost: under the documented identical clean-project/warm-dependency conditions on the shared 16-core VM, build wall time fell 62.75 s → 37.38 s (40.4%), and the dependency closure fell 9,057 → 2,846 jobs. The core fell 16 s → 8.0 s. The remaining proof structure is coherent; I found no further material safe simplification justified by the profile. Shared-host measurements are not guarantees of isolated performance.

At posting time, GitHub's metadata advisory has passed. The PR's synthetic merge revision has not been produced (mergeable: null, mergeable_state: unknown), so applicable pull-request validation workflows have not yet started. The local merge-tree check against main 01e7db404c7902d0ac652dc1a726a63208b67374 is conflict-free. Preserve this exact head; wait for actual protected checks and configured reviews. Daily asynchronous documentation publication is not a merge gate.

[greptile-apps]

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

[Medium impact] No blocking defect was found in the reviewed code, but external source and prior-art checks remain unverified.

Summary

Adds nine modules covering real Michal–Bastiani calculus, higher differentials, weak integrals, and comparison with Fréchet smoothness.

• Locally convex maps can now be differentiated and composed.
• Higher derivatives are continuous symmetric multilinear maps.
• Products, Taylor formulas, and second derivatives get calculus rules.
• Locally convex curves can now have weak integrals under completeness conditions.
• Mackey completeness is characterized by weak integrals of Lipschitz curves.
• Locally convex smoothness connects to Fréchet smoothness on normed spaces.
• A uniformly bounded-below derivative can reflect smoothness through composition.
• The new calculus project is available through the pool imports and catalog.

_{Reviews (2) · Last reviewed commit: "Import Michal–Bastiani calculus on local..." · Reviewed by Greptile}

[Vilin97]

/review

[Vilin97]

Exact-head checkpoint: a13503aaaae23ab5c50c08ff334757694d192f9d.

Local complete-project clean build, zero-warning scan, 15 Mathlib linters, style, generated indexes, complete-repository static quality, card declaration resolution, and public/private/generated trust audits pass. Controlled build time is 62.75 s → 37.38 s (40.4% reduction). The thorough source assessment is posted above. Greptile's exact-head check succeeded with no concrete blocker; its limited external comparisons are covered by the primary-source and nearest-library checks documented in the PR/review. Configured GPT review was requested with /review and has not returned a verdict yet.

The external validation blocker is observable: GitHub reports mergeable: null, mergeable_state: unknown, and merge_commit_sha: null; refs/pull/745/head exists but refs/pull/745/merge does not. Only the successful metadata advisory pull_request_target workflow ran; the protected pull_request workflows have not been scheduled. A local merge-tree calculation against main 01e7db404c7902d0ac652dc1a726a63208b67374 is conflict-free. This is not evidence that protected CI passed.

The branch remains unchanged and auto-merge is disabled. Resume validation/review at this head when GitHub creates the merge revision; enter the validated native queue only after all independent required checks and reviews pass. Daily documentation publishing is asynchronous and is not part of this blocker.

[Vilin97]

{
"summary": "Exact-head source assessment at a13503a. All 12 published files and the complete public import closure were available; the five dimensions were reviewed independently. The six card endpoints are supported, including higher MB symmetry, the normed Frechet comparison, completeness-dependent weak integration and bounded-below reflection. The pinned upstream port, Apache attribution and AI provenance are preserved. The closest inspected Mathlib/Tau Ceti and pooled results have materially different hypotheses or conclusions: Mathlib already has general TVS first-derivative definitions, while this project adds the higher MB and weak-integration framework. External overlap coverage was bounded and is recorded in the novelty verdict. Author-reported private builds, declaration audits and timings were not independently credited.",
"verdict": "approve",
"reviewed_commit": "a13503aaaae23ab5c50c08ff334757694d192f9d",
"dimensions": {
"faithfulness": {
"verdict": "pass",
"bottom_line": "All six headlines and the mathematical summary match the published real locally convex calculus and disclose their substantive hypotheses.",
"proves_the_claim": "proves_it",
"claim_note": "The Lean proves MB chain rules and symmetric higher differentials, smooth equivalence on real normed spaces, the stated weak-integral and Mackey-completeness results, and finite-order reflection under a uniform positive derivative lower bound.",
"assumed_inputs": "The card discloses real Hausdorff locally convex settings, open domains and mapping hypotheses; sequential or Mackey completeness for the corresponding integrals; and a Banach source, smooth j, fixed m > 0, continuous γ and γ(W) ⊆ U for bounded-below reflection. These are ordinary input hypotheses, not undisclosed assumptions of the claimed conclusions.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "This is a substantial graduate-level development of Michal–Bastiani calculus, with named differential and integration theorems and a reusable theory.",
"fit": "good_fit",
"level": "graduate",
"branch": "functional analysis",
"mode": "theory_building",
"significance_one_sentence": "The project develops Michal–Bastiani calculus on real locally convex spaces through the chain rule, Schwarz symmetry, weak integration and Mackey completeness, with Fréchet comparison and a bounded-below derivative regularity theorem.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The pinned upstream formalization is credited and preserved by the port, and the checked Glöckner–Neeb references support the explicitly stated real, open-domain calculus claims.",
"source_match": "matches",
"findings": []
},
"code_quality": {
"verdict": "pass",
"bottom_line": "Shared derivative interfaces, a completeness-parametric integral induction, and a reused linear bootstrap make the full calculus development maintainable without material duplication.",
"code_quality": 4,
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "The general locally convex MB and weak-integration development is a genuine extension of the inspected derivative, normed-calculus and pooled analytic results.",
"already_formalized": "",
"novelty_note": "The new contribution is higher MB regularity, its Frechet compatibility bridge and completeness-sensitive weak integration on locally convex spaces; the bounded searches do not establish exhaustive semantic absence in uninspected sources.",
"findings": []
}
},
"findings": [],
"integration_status": "Source acceptance only. The existing /review request is retained without duplication; configured verdict and proper authored/native validation remain separate. Current main has advanced to 525cd4c and is not yet independently qualified. The infrastructure priority hold remains operative; no queue admission or auto-merge is authorized by this source review."
}

[Vilin97]

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

Reviewed head: a13503aaaae23ab5c50c08ff334757694d192f9d

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

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	All six headlines match the Lean under disclosed hypotheses; protected CI has not run, and local compilation was not rerun because the checkout lacks dependencies.
Novelty	✅ pass	No duplicate headline was identified in the inspected Mathlib, Tau Ceti, or pool declarations; broader Tau Ceti coverage remains unverifiable.
Significance	✅ pass	The added Lean develops a substantial, completed theory of Michal–Bastiani calculus and weak integration on locally convex spaces.
Sources	✅ pass	The cited book supports the calculus and completeness results with the stated restrictions, and the bounded-below extension is credited to the upstream formalization.
Code quality (advisory)	✅ pass	Maintainable overall, with unnecessary source typeclasses in elementary lemmas; the targeted build stopped at a Mathlib-fetch HTTP 403, so compilation was not revalidated.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The card discloses the real Hausdorff locally convex setting and open-domain hypotheses, sequential or Mackey completeness for integral existence, and the Banach source, smooth outer map, fixed positive derivative lower bound, continuity, and domain inclusion required for regularity reflection.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	research
Branch	functional analysis
Mode	theory_building
Code quality	3 / 5

Statement check: The Lean establishes finite-order composition, continuous symmetric higher differentials, smooth MB–Fréchet equivalence, completeness-based weak integration, the Mackey characterization, and bounded-below reflection of finite regularity.

The chain rule, symmetric continuous higher differentials, Mackey-completeness characterization through Lipschitz-curve integrability, and comparison with Fréchet smoothness form a coherent theory with several substantive endpoints.

Faithfulness findings (1)

• prompt-injection — PR-wide
  The contributor’s discussion claims prior approval and issues workflow directives. These have no authority over this independent review and were excluded from the mathematical assessment.
  Evidence: PR discussion in .review-pr.json: “Content verdict: APPROVE. No unresolved mathematical, source, licensing, or engineering findings.” and “Preserve this exact head; wait for actual protected checks and configured reviews.”

Code quality findings (2)

• overstrong-typeclass — LeanPool/LCAnalysis/MichalBastiani.lean:540
  The source assumptions in ContDiffMBOn.mono exceed what its induction uses: it only restricts continuity and the existing directional derivatives. The same pattern occurs in of_local, ContinuousLinearMap.contDiffMBOn/smoothMBOn, and contDiffMBOn_const in Higher.lean:237. Generalize these elementary lemmas; unnecessary local-convexity and Hausdorff assumptions also propagate through congr_of_isOpen, prodMk, and comp_clm, restricting downstream reuse.
  Evidence: theorem ContDiffMBOn.mono : ∀ {k : ℕ} {E₁ : Type u} [AddCommGroup E₁] [Module ℝ E₁]
  [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁]
  [LocallyConvexSpace ℝ E₁] [T2Space E₁] {f : E₁ → F} {U V : Set E₁},
  ContDiffMBOn k f U → V ⊆ U → ContDiffMBOn k f V := by
  intro k
  induction k with
  | zero =>
  intro E₁ _ _ _ _ _ _ _ f U V hf hVU
  exact ContinuousOn.mono hf hVU
  | succ k ih =>
  intro E₁ _ _ _ _ _ _ _ f U V hf hVU
  exact ⟨hf.1.mono hVU, fun x hx h ↦ hf.2.1 x (hVU hx) h,
  ih hf.2.2 (Set.prod_mono hVU subset_rfl)⟩
• prompt-injection — PR-wide
  Contributor-authored discussion supplies a claimed prior approval and workflow instructions. Under the review trust boundary, these cannot establish code quality or validation; they were excluded from the assessment.
  Evidence: Discussion comment 6628793551 states: “Content verdict: APPROVE. No unresolved mathematical, source, licensing, or engineering findings.” It also directs: “Preserve this exact head; wait for actual protected checks and configured reviews.”

---

Tokens: 8,261,567 in / 44,338 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $33.7113 (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.

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 63.80 s (= 1.06 min) — user 122.97 s, sys 11.63 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: 2,630,793 maxHeartbeats units across 10 valid files (4,277 added LOC).

Sum of lean --profile: 86079.2 ms (= 86.08 s) across 10 valid files. Import-excluded time: 71489.2 ms (= 71.49 s).

Count-heartbeats wall-clock total: 304.42 s. Repeated import cost inside lean --profile: 14590.0 ms (= 14.59 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/LCAnalysis/MichalBastiani.lean	888	970,918	66.49	17.68	16.41	1.27	384	0
LeanPool/LCAnalysis/BoundedBelow.lean	397	378,924	44.64	13.00	11.70	1.30	47	0
LeanPool/LCAnalysis/IntegralExistence.lean	558	331,789	66.67	18.18	16.82	1.36	150	0
LeanPool/LCAnalysis/Higher.lean	633	317,340	43.14	9.36	8.07	1.29	212	0
LeanPool/LCAnalysis/MackeyLipschitz.lean	533	232,581	33.45	8.79	7.44	1.35	149	0
LeanPool/LCAnalysis/Rules.lean	245	173,771	16.15	5.00	3.75	1.25	68	0
LeanPool/LCAnalysis/Integral.lean	231	162,835	13.50	4.98	3.66	1.32	75	0
LeanPool/LCAnalysis/FundamentalTheorem.lean	238	62,634	13.37	4.48	3.15	1.33	48	0
LeanPool/LCAnalysis.lean	24	0	3.47	3.11	0.26	2.85	2	0
LeanPool/LCAnalysis/Imports.lean	18	0	3.54	1.51	0.24	1.27	1	0
LeanPool/LCAnalysis/MBFrechet.lean	512	—	—	—	—	—	78	4
Total	4,277	2,630,793	304.42	86.08	71.49	14.59	1214	4

Aggregate phase totals

Phase	Time
typeclass inference	36500.0 ms (= 36.50 s)
import	14590.0 ms (= 14.59 s)
interpretation	14261.0 ms (= 14.26 s)
tactic execution	9131.0 ms (= 9.13 s)
elaboration	2791.2 ms (= 2.79 s)
simp	2272.7 ms (= 2.27 s)
type checking	2189.9 ms (= 2.19 s)
linting	843.6 ms (= 0.84 s)
norm_num	722.2 ms (= 0.72 s)
ring	584.3 ms (= 0.58 s)
process pre-definitions	418.9 ms (= 0.42 s)
parsing	378.6 ms (= 0.38 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.LCAnalysis.MichalBastiani	13.00 s
LeanPool.LCAnalysis.BoundedBelow	12.00 s
LeanPool.LCAnalysis.IntegralExistence	11.00 s
LeanPool.LCAnalysis.MBFrechet	10.00 s
LeanPool.LCAnalysis.Higher	8.50 s
LeanPool.LCAnalysis.Rules	7.70 s
LeanPool.LCAnalysis.Integral	5.60 s
LeanPool.LCAnalysis.MackeyLipschitz	4.00 s
LeanPool.LCAnalysis.FundamentalTheorem	3.40 s
LeanPool.LCAnalysis	1.50 s
LeanPool.LCAnalysis.Imports	1.50 s

Per-file `lean --profile` output

LeanPool/LCAnalysis.lean

import took 2.85s
cumulative profiling times:
	declTypeLinter 0.399ms
	elaboration 0.13ms
	import 2.85s
	initialization 37.1ms
	interpretation 220ms
	linting 0.68ms
	module linting 0.0103ms
	parsing 0.0481ms
	tacticAnalysis 0.467ms
real 3.93
user 1.42
sys 1.30

LeanPool/LCAnalysis/BoundedBelow.lean

import took 1.3s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 140ms
tactic execution of Lean.Parser.Tactic.refine took 980ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 274ms
cumulative profiling times:
	attribute application 0.138ms
	blocked (unaccounted) 2.41ms
	congr simp thm 8.46ms
	declTypeLinter 19.5ms
	dsimp 12.4ms
	elaboration 171ms
	fix level params 10ms
	import 1.3s
	initialization 32ms
	instantiate metavars 15.7ms
	interpretation 1.62s
	let-to-have transformation 0.475ms
	linting 98ms
	module linting 0.011ms
	norm_num 104ms
	parsing 46.2ms
	process pre-definitions 59.9ms
	ring 49.1ms
	share common exprs 42.3ms
	simp 290ms
	tactic execution 2.61s
	tacticAnalysis 11.6ms
	type checking 385ms
	typeclass inference 6.11s
real 6.81
user 12.64
sys 1.16

LeanPool/LCAnalysis/FundamentalTheorem.lean

import took 1.33s
cumulative profiling times:
	attribute application 0.188ms
	blocked (unaccounted) 0.365ms
	congr simp thm 3.06ms
	declTypeLinter 16.7ms
	dsimp 1.88ms
	elaboration 133ms
	fix level params 2.71ms
	import 1.33s
	initialization 32.2ms
	instantiate metavars 4.25ms
	interpretation 823ms
	let-to-have transformation 0.321ms
	linting 49.8ms
	module linting 0.0133ms
	norm_num 11.2ms
	parsing 21.4ms
	process pre-definitions 23.5ms
	ring 68.8ms
	share common exprs 19ms
	simp 121ms
	tactic execution 324ms
	tacticAnalysis 9.38ms
	type checking 106ms
	typeclass inference 1.38s
real 4.08
user 4.27
sys 1.07

LeanPool/LCAnalysis/Higher.lean

import took 1.29s
cumulative profiling times:
	attribute application 6.75ms
	blocked (unaccounted) 0.0569ms
	compilation (IR) 0.35ms
	compilation (LCNF base) 8.01ms
	compilation (LCNF impure) 1.46ms
	compilation (LCNF mono) 3.91ms
	congr simp thm 11.2ms
	declTypeLinter 46ms
	dsimp 13.8ms
	elaboration 513ms
	fix level params 10.2ms
	import 1.29s
	initialization 32.5ms
	instantiate metavars 16.2ms
	interpretation 784ms
	let-to-have transformation 1.02ms
	linting 122ms
	module linting 0.0113ms
	parsing 58ms
	process pre-definitions 73.7ms
	share common exprs 30.4ms
	simp 444ms
	tactic execution 923ms
	tacticAnalysis 21.9ms
	type checking 363ms
	typeclass inference 4.59s
real 6.01
user 9.17
sys 1.14

LeanPool/LCAnalysis/Imports.lean

import took 1.27s
cumulative profiling times:
	declTypeLinter 0.13ms
	elaboration 0.0947ms
	import 1.27s
	initialization 34.3ms
	interpretation 205ms
	linting 0.255ms
	module linting 0.0118ms
	parsing 0.0017ms
	tacticAnalysis 0.145ms
real 2.32
user 1.34
sys 1.03

LeanPool/LCAnalysis/Integral.lean

import took 1.32s
cumulative profiling times:
	attribute application 0.129ms
	congr simp thm 3.19ms
	declTypeLinter 12.1ms
	dsimp 17.4ms
	elaboration 153ms
	fix level params 3.49ms
	import 1.32s
	initialization 32.7ms
	instantiate metavars 3.66ms
	interpretation 566ms
	let-to-have transformation 0.253ms
	linting 52.5ms
	module linting 0.0133ms
	norm_num 10.2ms
	parsing 25.7ms
	process pre-definitions 21.2ms
	ring 27.2ms
	share common exprs 11.5ms
	simp 142ms
	tactic execution 456ms
	tacticAnalysis 7.38ms
	type checking 89.9ms
	typeclass inference 2.02s
real 4.10
user 4.78
sys 1.10

LeanPool/LCAnalysis/IntegralExistence.lean

import took 1.36s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 559ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 589ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 602ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 409ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 363ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 364ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 207ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 625ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 661ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 338ms
tactic execution of Mathlib.Tactic.nlinarith took 332ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 119ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 116ms
cumulative profiling times:
	attribute application 1.33ms
	congr simp thm 25.1ms
	declTypeLinter 34.4ms
	elaboration 437ms
	fix level params 9.16ms
	import 1.36s
	initialization 36.5ms
	instantiate metavars 24.3ms
	interpretation 6.83s
	let-to-have transformation 0.796ms
	linting 165ms
	module linting 0.015ms
	norm_num 273ms
	parsing 64.8ms
	process pre-definitions 84.7ms
	ring 227ms
	share common exprs 109ms
	simp 509ms
	tactic execution 1.79s
	tacticAnalysis 21.3ms
	type checking 373ms
	typeclass inference 5.8s
real 8.00
user 17.90
sys 1.18

LeanPool/LCAnalysis/MBFrechet.lean

import took 1.33s
LeanPool/LCAnalysis/MBFrechet.lean:358:6: error: Type mismatch
  ContDiff.comp_contDiffOn (LinearIsometryEquiv.contDiff ?m.2024) hBcC
has type
  ContDiffOn ℝ (↑k) (⇑?m.2024 ∘ Bc) U
but is expected to have type
  ContDiffOn ℝ (↑k) D U

Note: The following definitions were not unfolded because their definition is not exposed:
  Real.instOne ↦ 8
  Real.instZero ↦ 100
LeanPool/LCAnalysis/MBFrechet.lean:358:6: error: Application type mismatch: The argument
  continuousMultilinearCurryLeftEquiv ℝ (fun x => E) F
has type
  @LinearIsometryEquiv ℝ ℝ Field.toSemifield.toSemiring Field.toSemifield.toSemiring (RingHom.id ℝ) (RingHom.id ℝ) ⋯ ⋯
    (ContinuousMultilinearMap ℝ (fun x => E) F) (E →L[ℝ] E [×m]→L[ℝ] F) ContinuousMultilinearMap.seminormedAddCommGroup
    ContinuousLinearMap.toSeminormedAddCommGroup ContinuousMultilinearMap.instModule ContinuousLinearMap.module
but is expected to have type
  @LinearIsometryEquiv ℝ ℝ Field.toSemifield.toSemiring Field.toSemifield.toSemiring (RingHom.id ℝ) (RingHom.id ℝ) ⋯ ⋯
    (E [×m + 1]→L[ℝ] F) ?m.2028 NormedAddCommGroup.toSeminormedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup
    ContinuousMultilinearMap.normedSpace'.toModule NormedSpace.toModule
in the application
  LinearIsometryEquiv.contDiff (continuousMultilinearCurryLeftEquiv ℝ (fun x => E) F)
simp took 107ms
simp took 101ms
tactic execution of Lean.Parser.Tactic.refine took 2.49s
cumulative profiling times:
	attribute application 1.58ms
	compilation (IR) 0.0473ms
	compilation (LCNF base) 1.26ms
	compilation (LCNF impure) 0.258ms
	compilation (LCNF mono) 0.353ms
	congr simp thm 20.4ms
	declTypeLinter 27ms
	dsimp 8.23ms
	elaboration 333ms
	fix level params 9.18ms
	import 1.33s
	initialization 38ms
	instantiate metavars 9.06ms
	interpretation 1.03s
	let-to-have transformation 0.843ms
	linting 112ms
	module linting 0.0123ms
	norm_num 9.68ms
	parsing 59.6ms
	process pre-definitions 51.2ms
	ring 9.72ms
	share common exprs 27.3ms
	simp 689ms
	tactic execution 4.36s
	tacticAnalysis 17.1ms
	type checking 451ms
	typeclass inference 7.66s
real 11.27
user 16.91
sys 1.17
error: profile command exited with status 1

LeanPool/LCAnalysis/MackeyLipschitz.lean

import took 1.35s
cumulative profiling times:
	attribute application 0.543ms
	congr simp thm 8.57ms
	declTypeLinter 31.7ms
	dsimp 7.49ms
	elaboration 294ms
	fix level params 7.34ms
	import 1.35s
	initialization 38.3ms
	instantiate metavars 11.5ms
	interpretation 1.49s
	let-to-have transformation 0.6ms
	linting 107ms
	module linting 0.0138ms
	norm_num 281ms
	parsing 54.9ms
	process pre-definitions 60.7ms
	ring 166ms
	share common exprs 66.9ms
	simp 209ms
	tactic execution 1.17s
	tacticAnalysis 23.1ms
	type checking 357ms
	typeclass inference 3.05s
real 5.61
user 8.51
sys 1.18

LeanPool/LCAnalysis/MichalBastiani.lean

import took 1.27s
typeclass inference of DiscreteTopology took 146ms
typeclass inference of DiscreteTopology took 134ms
typeclass inference of DiscreteTopology took 172ms
typeclass inference of DiscreteTopology took 114ms
cumulative profiling times:
	attribute application 0.611ms
	congr simp thm 10.8ms
	declTypeLinter 58.1ms
	dsimp 24.9ms
	elaboration 860ms
	fix level params 15.1ms
	import 1.27s
	initialization 32.6ms
	instantiate metavars 16.7ms
	interpretation 1.19s
	let-to-have transformation 1.19ms
	linting 207ms
	module linting 0.0136ms
	norm_num 5.86ms
	parsing 89.1ms
	process pre-definitions 78.7ms
	ring 19.9ms
	share common exprs 43.8ms
	simp 464ms
	tactic execution 1.47s
	tacticAnalysis 29.3ms
	type checking 395ms
	typeclass inference 11.4s
real 10.33
user 17.48
sys 1.18

LeanPool/LCAnalysis/Rules.lean

import took 1.25s
cumulative profiling times:
	attribute application 0.105ms
	congr simp thm 4.83ms
	declTypeLinter 13.9ms
	dsimp 3.26ms
	elaboration 230ms
	fix level params 3.82ms
	import 1.25s
	initialization 38.4ms
	instantiate metavars 4.64ms
	interpretation 533ms
	let-to-have transformation 0.441ms
	linting 41.4ms
	module linting 0.0136ms
	norm_num 36.9ms
	parsing 18.5ms
	process pre-definitions 16.5ms
	ring 26.3ms
	share common exprs 14.7ms
	simp 93.7ms
	tactic execution 388ms
	tacticAnalysis 7.39ms
	type checking 121ms
	typeclass inference 2.15s
real 4.28
user 4.77
sys 1.12

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