WIP: Import Coarse-graining theory for elliptic equations

[Vilin97]

Imports scottnarmstrong/coarsegraining at 28ca42c02fd286c8f63a45be3344f6f82d026db3 into LeanPool.CoarseGraining.

Develops the function-space, deterministic, probabilistic, and homogenization-scale machinery of quantitative stochastic homogenization. Includes the quenched minimal-scale theorem and a uniformly elliptic specialization of the homogenization comparison estimate in dimensions d ≥ 2, for stationary unit-range isotropic laws invariant under adjoints.

All 1,590 production and required source modules remain included, with 1,640 destination files. The compatibility layer preserves the raw integral and cube-norm formulas even for nonmeasurable inputs, and proves bridges to current Mathlib seminorms under the required measurability hypotheses. The endpoint descriptions retain the dimension, structural-law, adjoint-invariance and force-regularity assumptions.

Work remains in progress; the existing PR lifecycle is preserved. No checks, gates, compiler budgets or repository settings have been weakened.

• The latest targeted raw-norm/transport build passed 3,192 jobs. Full17 was interrupted; the complete current entry has not passed yet.
• The current scoped static audit reports 83 remaining proof-size findings across 1,640 files, reduced from the original 137 findings.
• The previous ten failing modules passed in the latest CI build. Six new frontier modules exposed public/private interface and raw-versus-measurable norm compatibility errors. Repairs are checkpointed at 714ad4426 and await kernel validation.
• The raw integral seminorm now has a generic scalar-scaling lemma for every exponent, including zero and infinity, without a measurability assumption. Supporting proof refactors retain all public mathematical contracts. Further downstream compiler repairs, size cleanup, warning cleanup, scoped linters and compiled audits remain.

Please leave this PR unmerged.

[Vilin97]

Changes requested by automated review

Reviewed exact head 78d00ae926b802f814dcefbc2bff1152e930dceb. The exact-head CoarseGraining build fails in multiple proof-bearing modules: rewrite failures and type mismatches in Besov/ProjectionCharacterization.lean, fractional Sobolev bridge and instance errors, CubePoisson solver rewrite/type errors, and unknown MeasureTheory.Measure.isProbabilityMeasure_map in HighContrast/Corridor/FixedPhase/EfronSteinAE.lean. Repair the imported closure, then rerun complete protected CI. Do not change the gates.

[Vilin97]

/review

[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 risk] Adds mathematical library code for coarse-graining theory.

No new or outstanding review finding blocks the PR, but it should remain unmerged while the complete entry build and required audits are unfinished.

Findings

1.  Headline overstates comparison ▶
2.  Annealed headline omits assumptions ▶

Summary

Imports the CoarseGraining formalization, exposes its modules through LeanPool.lean, and registers its homogenization results.

• The registered comparison claim now names the compatibility defect and the force-regularity condition.
• The registered annealed claim now names the structural-law and dimension assumptions.
• The complete current entry build has not passed; the PR remains work in progress.

_{Reviews (30) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..."}

[greptile-apps]

Headline overstates comparison

The project card says the heterogeneous and homogenized solutions satisfy a quantitative comparison estimate. The theorem instead bounds comparisonDefect, which is explicitly a legacy dual-Besov compatibility defect rather than a direct norm of the solutions, and it also requires ForceSobolevRegularity for the forcing term. This makes the registered headline materially broader than the formal result and hides a required hypothesis. Please narrow the card to the actual compatibility-defect statement and condition, or expose a theorem that supports the current claim.

Suggested change

	informal: For a stationary unit-range isotropic uniformly elliptic coefficient law, heterogeneous
	and homogenized elliptic solutions satisfy a quantitative comparison estimate above a random
	minimal scale with stretched-exponential tails.
	informal: For a stationary unit-range isotropic uniformly elliptic coefficient law and a forcing
	term satisfying the required fractional-Sobolev regularity condition, a legacy dual-Besov
	compatibility defect is quantitatively controlled above a random minimal scale with
	stretched-exponential tails.

Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!

[Vilin97]

Changes requested by automated review

Reviewed exact current head 2491831fcf5ee7ebe6b201c364ff992a683ffd81. CoarseGraining still has rewrite/type mismatches across the Besov, fractional-Sobolev, CubePoisson, and high-contrast modules, including the unknown MeasureTheory.Measure.isProbabilityMeasure_map. Repair the dependent closure and rerun full protected CI.

[greptile-apps]

Comments Outside Diff

These findings sit on lines the diff does not cover, so they could not be posted inline. Each one leaves this list once its file changes.

•  Unrelated project bundled LeanPool/projects.yml:2 ▶

  The changes since the previous review register the complete BlockSpectralSensitivity formalization, with its own source, author, main results, and entry module. LeanPool.lean also publicly exports its modules. Because this PR is scoped and documented only as the CoarseGraining import, merging it would silently integrate a second pooled contribution without presenting that project for an independent scope, provenance, headline, and completeness review. Please remove these unrelated changes or move them to a separate PR.

  Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!

[Vilin97]

Changes requested by automated review

Reviewed head 73c0fd1364c20437f071b998b275b63436956e6d. Substantial completed uniformly elliptic specialization; not the entire broader homogenization program.

1. Complete the pinned-toolchain integration. The previous source-identical build failed at a7f9659400e14e6834f3121b046284b32f6d9931. The same source-level blocker is present at this reviewed head; its error includes:

   error: LeanPool/CoarseGraining/Homogenization/Besov/ProjectionCharacterization.lean:63:6: Tactic `rewrite` failed: Did not find an occurrence of the pattern
   

   The file/dependency audit finds 1638 changed Lean files without the required module form. Repair the affected dependency closure, regenerate the module index, and obtain a warning-free full pool build plus the unchanged linter, quality and axiom gates. A project-only or previous-head build does not resolve this failure.

2. Resolve the substantive source/interface defect. The endpoint setup includes 2 ≤ d and the structural law hypothesis includes adjoint invariance as well as stationarity/unit-range/isotropy. Disclose these conditions in the card’s quantitative-homogenization scope, or prove their removal. The current projection/ENNReal/CubePoisson elaboration failures also need repair.

Review coverage: complete changed-file inventory and full diff retained; 1638 changed project files, 575,301 lines, import reachability and executable trust-token scan; advertised endpoints and supporting definitions examined with bounded implementation sampling and existing review findings reconciled. Potential reusable value: Stochastic homogenization, cubes and PDE energy estimates. Source/provenance and prior-art evidence were considered separately from CI; these findings do not assert that every proof line was manually read. Earlier automated scores are advisory and are not approval of this failing head.

Exact-head reconciliation: the automatic main merge left all project Lean source and the pinned toolchain unchanged. This run restored the original parsed project card after the rebase parser dropped the title-first entry; parsed-card equality and the generated module-index check pass. The restoration is a narrowly scoped fast-forward commit from an isolated worktree. It does not repair the substantive blockers above; new CI is not assumed green.

[Vilin97]

Reviewed the incoming refactoring through c5de9ca3c48dea0f60cc6d39c1de11a91e466444 (22 files since 18ae7465931c55a1c3e088e5734a72094d8342b9). Further changes and full validation are required before merge.

The two Basic-module splits preserve the original executable bodies and import lists, and the remaining changes extract the same scalar bounds, descendant translation and stationary-law transport, canonical L² facts, moment normalization, and paired-integral estimates. Existing public endpoint statements, dimension/law/regularity assumptions, constants, and raw cube-norm formulas are preserved. I read all remaining deltas; a second reviewer independently checked both splits, the Caccioppoli extraction, and the Rosenthal/Section 5.2 moment refactoring. No new mathematical blocker was found in this delta.

At this exact commit, the unchanged scoped source gates pass file headers, forbidden-text and file-size checks across 1,640 files. The proof-size check still reports 114 findings. The pinned generated-index and delta whitespace checks pass. This is source review and static validation only; the full current entry, warning-free linting, and compiled audits still need to pass, so leave the PR unmerged.

[Vilin97]

Reviewed all 11 changed files through 014bf816fdab6ec96687621a9d8d9ded8d0b12be against c5de9ca3c48dea0f60cc6d39c1de11a91e466444. The extracted integrability, descendant-measurability, tail and absorption lemmas retain the original moment/stationarity/P4 assumptions, exponents, scale ranges, sigma weights and explicit constants. The two Section 5.2 helper moves preserve their statements and proofs. The original public conclusions are unchanged, and the root index and registry are byte-identical.

The actual pinned index check passes. The unchanged source-quality checks over all 1,640 project files report zero header, forbidden-text or file-size findings, and 102 remaining proof-size findings (previously 114). This is a source-review update, not a completed-port acceptance: finish those remaining proof extractions and obtain a successful complete build, linters and environment/quality audits before merging. No full local compilation is claimed.

[Vilin97]

Changes requested by automated review

Reviewed head 47086bd1111788c72c61aee7a73e3ac1c992bfbd. The completed uniformly elliptic result in dimension at least two is independently significant, with the disclosed stationary, unit-range and adjoint-invariant law assumptions. It is not a claim to formalize the entire broader homogenization program.

The earlier module and scope repairs are preserved, as are the subsequent shared cutoff, matched-trace and Bennett-kernel constructions. The current source still fails the unchanged proof-size gate in 97 declarations. Concrete examples: Book/Ch03/ABK26/LocalCoarseGrainingOneCube.lean:909 has 446 code lines; Book/Ch05/Theorems/Section53/JUpperBoundCoarseFluctuations/PairedSquares.lean:188 has 623. These are measured gate failures, not an objection to the project’s overall size.

Acceptance requires decomposing the remaining long arguments around mathematical interfaces (in particular the one-cube energy estimates and paired-square fluctuation identities), preserving the endpoint contracts, and passing the complete warning-free build, linters, quality and trust checks. The useful completed refactors should be retained; do not add size waivers or change the 200-line gate.

[Vilin97]

Changes requested by automated review

Reviewed 714ad4426c0ebf700eaef916df2131bb1d90f095. The explicitly scoped uniformly elliptic coarse-graining/homogenization results are independently significant. This review does not infer a theorem for every elliptic operator from the broader title.

Blocking finding: Probability/Source/AKL/RegQuotientAdapter.lean:51 lacks an instance; Sobolev/W1p/H1GradientUpgrade.lean:453 cannot resolve memLp_of_gradMemLp_on_isOpenBoundedConvexDomain; Sobolev/PotentialSolenoidalL2Recovery.lean:391,415 cannot resolve blockFstCLM/blockSndCLM. Repair these source failures and the remaining closure failures in CI. The source audit also finds 83 proofs over the 200-code-line limit (down from the previously reported 97), including the 623-line proof in Book/Ch05/Theorems/Section53/JUpperBoundCoarseFluctuations/PairedSquares.lean:188. Preserve the completed repairs and extract meaningful shared/helper arguments for the remaining violations.

Evidence: exact-head build log. Acceptance condition: the complete project, repository quality/axiom gates and required protected checks pass on the repaired head, and the remaining substantive/maintainability findings are resolved. The prior bot verdict does not override these reproduced source/build failures.

[Vilin97]

Changes requested by automated review

Reconciled to exact current head dc985489ab196969da49b049bbab123e5195769a. The main-branch integration leaves this project’s Lean sources byte-identical to the reviewed source; the existing substantive findings and acceptance conditions remain unresolved. The AKL quotient/gradient/potential-solenoidal interfaces still fail to elaborate; 83 proofs still exceed the unchanged 200-line proof cap.

Preserve the valid completed repairs. Merge requires the cited author-actionable defects to be resolved and all protected checks to pass at the resulting head; this is not a needs-maintainer handoff.

[Vilin97]

{
"reviewed_head": "dd37265a64fb1faa45dbb35c864498d0c70c6988",
"scope": "Source reconciliation of the complete 35-file delta (628 added and 990 removed lines) from commit 014bf81, carried unchanged through commit dd37265. Prior mathematical and source assessment retained; this is not a completed-port acceptance.",
"source_delta": "PASS",
"source_evidence": [
"All 515 existing declaration headers and section assumptions are unchanged; no declaration was removed. Read all 13 new helper proofs, all 11 visibility promotions and all 9 definition-body changes. Computational fields are unchanged.",
"The good-scale, tail, Bennett, finite-p Sobolev and matched-trace extractions preserve their assumptions, constants, scale/exponent ranges and public conclusions. Let-bound constants remain definitions in the full theorem types.",
"The reused H10 cutoff chooses the same product witness and exposes the same a.e. gradient identity; scalar-seminorm bridges use measurability evidence already present in the original proof.",
"All 1,640 project modules and the project card and entry are preserved; the internal import graph is unchanged and acyclic."
],
"validation": {
"source_only_headers_forbidden_file_size_findings": 0,
"remaining_proof_size_findings": 83,
"prior_proof_size_findings": 102,
"static_functions_same_as_baseline": true,
"fresh_Lean_compilation": false
},
"limits": [
"83 deterministic proof-size findings remain. Finish those proof extractions and obtain a complete warning-free build, linters and environment/quality audits before merging. No fresh local Lean compilation or native-index pass is claimed."
],
"findings": []
}