Repository navigation
Conversation
…ibution and complete production scope
Changes requested by automated reviewReviewed exact head |
|
/review |
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Low risk] Mathematical library code for coarse-graining theory. The accepted finding is non-blocking: the two comparison proofs should share their norm conversion. Findings
SummaryAdds
Reviews (3) · Last reviewed commit: "Merge current main and migrate PR #507 t..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
# Conflicts: # LeanPool.lean
Changes requested by automated reviewReviewed exact current head |
This comment has been minimized.
This comment has been minimized.
Changes requested by automated reviewReviewed head
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. |
Preserve authored mathematics and metadata; regenerate public project indexes.
| have hB_le_H : B ≤ Kpos * H := by | ||
| dsimp [B, H, Kpos] | ||
| exact Ch03.Legacy.scaleNormalizedPositiveBesovVectorSeminormTwo_le_const_mul_sobolev | ||
| (originCube d m) (s := fixedComparisonS) g hs_pos hs_le_one hg | ||
| have hdata : E + B ≤ Kdata * (E + H) := by |
There was a problem hiding this comment.
homogenizationComparison_uniformEllipticity repeats the force-norm conversion and final estimate assembly from homogenizationComparison_uniformEllipticity_variableExponents. Changes to the compatibility bounds require the same repair in two proofs.
Extract the shared conversion into a helper that takes the exponent and the existing Besov estimate. Keep the law-independent choice of constants in the fixed-exponent theorem.
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!
| ∃ sigmaBar : ℝ, | ||
| 0 < sigmaBar ∧ |
There was a problem hiding this comment.
The returned sigmaBar is constrained only by positivity. Neither ComparisonPair nor the estimate uses this witness; they use barSigmaLimit through S instead. A caller cannot identify the returned value with the homogenized coefficient from this theorem's type.
Remove the unused witness, or add sigmaBar = Ch05.Section57.barSigmaLimit S.hP S.hStruct.
| have hB_le_H : B ≤ Kpos * H := by | ||
| dsimp [B, H, Kpos] | ||
| exact Ch03.Legacy.scaleNormalizedPositiveBesovVectorSeminormTwo_le_const_mul_sobolev | ||
| (originCube d m) (s := fixedComparisonS) g hs_pos hs_le_one hg | ||
| have hdata : E + B ≤ Kdata * (E + H) := by |
There was a problem hiding this comment.
homogenizationComparison_uniformEllipticity repeats the constant bounds and Besov-to-Sobolev conversion from homogenizationComparison_uniformEllipticity_variableExponents. Both proofs establish hdata, apply the same two bridge lemmas, and finish with the same inequality chain. Maintainers must repair both copies when these dependencies change.
Extract a shared conversion lemma parameterized by the exponent and the internal estimate. Keep each theorem's choice of constants separate so the fixed theorem still chooses them before the law.
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!
| ∃ sigmaBar : ℝ, | ||
| 0 < sigmaBar ∧ |
There was a problem hiding this comment.
homogenizationComparison_uniformEllipticity returns sigmaBar, but its statement only says that number is positive. Neither the comparison pair nor the estimate refers to it; both use the coefficient already fixed by S. Callers cannot prove that the returned number is that coefficient and must unpack an extra witness that gives them no useful information.
Remove this witness, or state that it equals Ch05.Section57.barSigmaLimit S.hP S.hStruct.
| have hB_le_H : B ≤ Kpos * H := by | ||
| dsimp [B, H, Kpos] | ||
| exact Ch03.Legacy.scaleNormalizedPositiveBesovVectorSeminormTwo_le_const_mul_sobolev | ||
| (originCube d m) (s := fixedComparisonS) g hs_pos hs_le_one hg | ||
| have hdata : E + B ≤ Kdata * (E + H) := by | ||
| have hE_le : E ≤ Kdata * E := by | ||
| calc | ||
| E = 1 * E := by ring | ||
| _ ≤ Kdata * E := | ||
| mul_le_mul_of_nonneg_right hKdata_ge_one hE_nonneg | ||
| have hB_le_Kdata : B ≤ Kdata * H := by | ||
| exact hB_le_H.trans | ||
| (mul_le_mul_of_nonneg_right hKpos_le_Kdata hH_nonneg) | ||
| calc | ||
| E + B ≤ Kdata * E + Kdata * H := add_le_add hE_le hB_le_Kdata | ||
| _ = Kdata * (E + H) := by ring |
There was a problem hiding this comment.
homogenizationComparison_uniformEllipticity repeats the Besov-to-legacy conversion inside homogenizationComparison_uniformEllipticity_variableExponents: the same constants, data bound, negative-defect bound, and final multiplication. Changes to either bridge will need the same repair in both proofs.
Extract a shared conversion lemma parameterized by s and the incoming Besov bound. Keep each theorem's constant selection separate so the fixed-exponent theorem still chooses constants before the law.
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!
This branch has not been deployed
1 participant
Imports scottnarmstrong/coarsegraining at
28ca42c02fd286c8f63a45be3344f6f82d026db3intoLeanPool.CoarseGraining.The development covers function spaces, deterministic and probabilistic estimates, and quantitative stochastic homogenization, including the quenched minimal-scale theorem and a uniformly elliptic homogenization comparison estimate. All 1,590 production and required source modules remain included, with 1,640 destination files. The compatibility layer retains raw integral and cube-norm formulas for nonmeasurable inputs and proves bridges to current Mathlib seminorms under the appropriate measurability hypotheses. Endpoint descriptions retain their dimension, structural-law, adjoint-invariance, and force-regularity assumptions.
Current head (2026-10-02): Published
b41b4be7f97cf915519120859baf1ec93825ca10, reconciled with the current bot branch and mainc57dde95469483aaab58f4fac461f625468ebc29. The last complete, source-hash-guarded Lean 4.35.0-rc3 project build passed all 4,912 jobs with zero Lean errors; it still reported 2,456 distinct source warnings. Subsequent proof and formatting batches were validated with source-guarded scoped builds. The generated index checks (mk_all --checkand the Python project-root check) and content-only diff against main pass. Fresh hosted CI on this head is running; Plan build has passed and Build pool is queued.Open work: The zero-warning gate remains red on the previous hosted head, and the latest full local warning inventory is not yet refreshed after these scoped batches. Static-only quality still flags imported proofs above the 200-code-line limit. These source findings require proof and formatting changes before merge. No check, gate, waiver, compiler budget, or repository setting has been changed. Keep this PR WIP and unmerged.
Part of the requested 42-project import batch.