Import high-contrast stochastic homogenization

[Vilin97]

Imports the complete HighContrastHomogenization development into Lean Pool: 2,935 Lean modules covering quantitative stochastic homogenization in high contrast, together with the pinned CoarseGraining dependency closure. The project entry is LeanPool.HighContrastHomogenization, and the generated Imports module includes the complete library.

The source is Scott Armstrong, Tuomo Kuusi and Amélie Loher’s HighContrastHomogenization repository at 7a13dbcd8d6609264a713373f5c69ceeac870472, with CoarseGraining pinned to c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4, accompanying arXiv:2609.27647. Their credits and Apache-2.0 notices are retained; the project card records AI provenance.

The public HCPoly APIs provide polynomial entry into small contrast, algebraic convergence of annealed coarse blocks, uniform and polynomial homogenization, and quenched convergence. These include effective matrices, quantitative random-scale tails, correctors, Liouville classification and large-scale regularity. Dirichlet estimates use the documented negative-Sobolev formulation on adapted cells; theorem documentation records the skew-centered flux convention and scope differences from the paper.

The module tree separates analytic and geometric foundations, multiscale entry arguments, provider proof assemblies, frozen theorem exports and consistency checks. Supporting development uses the isolated HCPolySupport namespace. The import also registers the project and includes the required naming, documentation and warning repairs.

Validation: the complete repository CI passed at a33b2352 (run 37760552806): all ten build shards, aggregate build, declaration lint, text style, and repository quality checks. Local validation also passed the 2,935-module strict build, fresh lint over 46,515 declarations, and the static, axiom, options and index checks.

The corrected endpoint core now publicly imports the seven modules that define its theorem type and keeps eleven proof dependencies local; nine redundant direct imports were removed. Its assembly removes an unused namespace opening. All declaration types, definition computations and proof bodies are unchanged.

Six alternating cached-import pairs with the same assembly source, pinned compiler and two Lean threads measured the endpoint assembly peak RSS at 1,694,534 → 1,638,424 KiB (54.8 MiB lower; all six pairs improved). Consumer CPU was 1.59 → 1.56s, essentially flat. Compiling the core itself cost 29.955 → 30.570s (+2.1%); this is a downstream-memory improvement. Candidates for proof simplification and a four-module split were tested and omitted when they showed noise or a compilation regression.

At optimized commit 6b3b4e14a, the strict complete-project dependency build, fresh lint of 13 changed/dependent modules (178 declarations), full-project text style, index, and all static/compiled quality audits passed locally. Automatic CI 37800426861 passed on that exact commit, including compilation, declaration lint, text style, repository quality, and the final Build project gate. All required PR checks are green.

The optional Proof Profile planner reaches GitHub’s 1 MiB job-output limit on this large PR: its planning steps succeed, but GitHub rejects the exported outputs. The paired measurements above were completed locally; profiling is informational, and all required checks pass.

[Vilin97]

Partial source review at 127f5c130d7c19bb1b6a4afbef96181b2e3bdab5

Please repair these helper contracts while retaining the public mathematical statements:

1. [P1] Bind the threshold assumptions to the parameters used in the conclusion — LeanPool/HighContrastHomogenization/Provider/Quenched/EndpointRelativeEngineData.lean:1252. endpoint_threshold_and_polynomial_costs takes independent theta and mu parameters in hlowFix, hgainFix, habsFix and hrelFix, but concludes bounds for eta / (A + D + 1) and d / 2 - g. The local let mu and let theta at lines 1287–1289 shadow those parameters; they do not rewrite the existing assumptions. Consequently the conversions at 1310, 1316 and 1322 need equalities that the contract does not supply. State the assumptions using the intended expressions, or bind and use both equalities explicitly.

2. [P1] Pass the original-law witness into the cadence helper — LeanPool/HighContrastHomogenization/Provider/Quenched/SmallContrastCorrectedEndpointCore.lean:3213. endpoint_decay_from_corrected_cadence uses hdag to construct original-law finite means and positive annealed blocks at lines 3213–3216, but its complete contract only binds the recentered witness hdagR. There is no local original-law hdag in this declaration. Thread the original witness, or the two required original-law certificates, from the caller into this helper before carrying the decay back.

3. [P1] Thread the radius equality through the uniform-parameter helper — LeanPool/HighContrastHomogenization/Provider/Quenched/SmallContrastCorrectedEndpointCore.lean:3844. corrected_endpoint_decay_of_uniform_parameters passes hRdef to endpoint_burned_maximum_envelope, which requires R = 4 / (1 + cIso). The helper binds R independently and assumes only 1 <= R; its complete contract and local proof do not bind that equality. The public caller creates it at line 3886, so pass it through the intermediate helper and its call.

These are static findings from the exact published blobs, independently checked against the complete affected contracts. They are not a report of a local compiler run.

Independent review has now read all 53 selected lower suppliers, including the eight endpoint producers, seven polynomial/geometry bridges and 38 foundation/analytic files. This supplements the earlier 22 selected entry/setup/result files. Genuine law, energy and test-pairing premises and a concrete nonvacuous identity-law instance were checked. Remaining transitive variational/weak-derivative providers, full strict compilation, linters, trust checks and repaired API/value replay still require validation. This partial review does not approve the whole import.

[Vilin97]

Reviewer follow-up at a33b2352f235f59366331ebd7c919ecff0e1ba7c

All three helper-contract findings in my earlier review at 127f5c1 are resolved in the current source:

1. endpoint_threshold_and_polynomial_costs now states its assumptions using the canonical eta / (A + D + 1) and d / 2 - g expressions.
2. The cadence helper receives distinct original-law hdag and recentered-law hdagR certificates, in the correct order at the actual midpoint-exponent caller.
3. The uniform-parameter route carries R = 4 / (1 + cIso) into the maximum-envelope proof.

Independent review checked the affected current contracts and complete selected proof contexts. Both public written theorem headers remain byte-identical to the earlier headers.

The current headline review also traced HCPoly.polynomial_homogenization through its frozen wrapper and root composition, then read both current triangle producers. The weighted triangle is derived from a.e. ellipticity and actual square-integrable pullbacks. The documented scope is adapted triadic-cell Dirichlet comparison, an existential effective matrix and X ≥ 1; it does not assert X ≥ S, identify that matrix with the annealed limit, or cover every Lipschitz domain. Broader imported corrector, Dirichlet, Liouville and regularity makers remain outside this current review's proof-body coverage.

The failed required job reports shard=cancelled finalize=cancelled and then fails its aggregate outcome check. That job contains no Lean compilation step; it supplies no observed proof error or proof-success evidence. The cancellation cause remains unverified, and exact-head required CI still needs recovery and successful completion.

This remains a partial current-head review, with the draft and protected checks pending. Earlier local validation is retained as historical evidence and is not transferred across changed dependency closures. The current-main CI priority hold remains active; no merge, auto-merge or author-branch update was performed.

[Vilin97]

Scoped review at 6b3b4e14: absorption and producer chain

The exact a33b2352…6b3b4e14 comparison changes only the core imports and assembly namespace opening. Reconstructed blobs match GitHub’s full identities; written declaration and proof texts are unchanged. Import visibility still needs current CI validation.

The two scalar absorption files are unchanged from a33b2352. At that head, both compiled with the four current Lean options and zero warnings/errors; their selected theorem axioms were only propext, Classical.choice, and Quot.sound. Official Mathlib text and module-name checks passed on exactly these files with zero errors.

I traced the lag caller, both Young applications, the whole one-step hub, and primal/adjoint cutoff-row composition. No local circular final-estimate premise emerged. Finite blocks, Schur data, smallness, cell integrability and weak finiteness remain explicit.

The primary paper supports the card’s documented restricted endpoint scope; full Theorem D equivalence is not established.

Remaining review covers changed recent-defect/coefficient suppliers and lower analytic definitions, full current-project validation, and global novelty. This is a partial assessment; project approval remains pending.

[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 proof library for homogenization theory.

The accepted finding is non-blocking: sharing the internal endpoint statement would make future changes easier.

Findings

1.  The statement has four copies ▶

Summary

Imports the high-contrast homogenization library and its pinned CoarseGraining support, with five public headline theorems.

• One non-blocking maintenance concern: the long polynomial homogenization statement is repeated across four exports.
• Review coverage is incomplete. The full diff was retrieved, but most of the roughly 47 MB contribution was not inspected. Complete headline proof-chain faithfulness, prior-art overlap, upstream completeness, source support, license and provenance, and repository-wide maintenance and cost remain unverified at this head.
• No runtime or compilation verification was performed. The reported memory measurements were not independently reproduced.

_{Reviews (1) · Last reviewed commit: "Keep corrected endpoint proof imports lo..." · Reviewed by Greptile}

[Vilin97]

Source review accepted at 6b3b4e14a760784ebb02ddddbfc0ed685f24c067.

The earlier helper-contract findings are resolved. The remaining recent-defect constants, physical row suppliers, projection limits and finite response endpoint have now been reviewed against the current source, using independent peers. The actual callers construct the projected estimates and full-pairing limit; Fatou transfers the uniform bounds. The numerical response route obtains finite row/weak caps and proves non-top before converting to real values. It does not obtain a finite bound by treating an infinite ENNReal value as zero.

Acceptance is for the documented mathematical scope: adapted-cell Dirichlet comparison in negative Sobolev norms, an existential effective matrix, and X >= 1. Physical isotropy/reference envelopes, variance budgets, finite means and smallness assumptions remain explicit. This review does not claim literal equivalence to the paper's full introductory theorem or whole-library manual proof coverage.

The retained source notices, pinned upstream/dependency identities, Apache-2.0 card and AI provenance are consistent with the saved source review. Finite current Mathlib/TauCeti checks found no concrete endpoint duplicate; no universal renamed-equivalence claim is made. The contribution is significant at this stated scope.

All eight required checks passed at this exact head. The separate profiling planner failure is informational and does not waive any required check. Author-reported measurements are not independent reviewer benchmarks.

The advisory about four copies of the long endpoint statement is non-blocking. Sharing the internal statement can be a later maintenance improvement while retaining explicit public/frozen contracts and normal validation.

Proceed through the protected native queue after refreshing live head, required checks, discussions and the current-main rollout condition.