WIP: Remove blanket section exposure across Lean Pool

[Vilin97]

Blanket @[expose] public section exports implementation bodies throughout Lean Pool. This WIP removes blanket section exposure while retaining the named computational interfaces and public equations that callers require.

Compilation failures remain. This PR is a draft and is not ready to merge. This update contains repairs in 164 source files; main is integrated through 30ac0ffae.

Progress at 2026-09-26 10:35 UTC:

• 7,995 tracked LeanPool, Challenge, and Solution sources and generated indexes: zero missing module headers and zero blanket exposed sections. These source counts do not imply a successful build.
• 175 projects / 3,880 sources have clean local builds and audited source coverage. Newly verified since the previous update: ACMax, MRiscX, QuasiBorelSpaces, OSforGFF, BollobasNikiforov, DomainTheory, Wallace, PhaseRetrieval, PoincareThreeBody, and AsymptoticTrianglePacking. Source hashes, compiled artifacts, import coverage, and source diffs were checked, including otherwise unimported files.
• Scoped declaration linters pass for 175 projects, style checks for 3,880 sources, and separate axiom and option audits for 55 projects. MRiscX now passes after replacing two bv_decide steps with UInt64 kernel lemmas. The earlier Erdos97ConvexOctagon verification includes all 267 source modules and 1,998 audited declarations.
• Hosted CI for preceding snapshot ed1f25d59 had nine failing build shards and one passing shard. Fresh CI must validate this update. Larger-project repairs remain in progress. BrauerGroupNew now builds, with independent review pending; it is not yet counted. SardMoreira built before a review correction restored its original generated public APIs and simp metadata; its rebuild is pending and it is also excluded. More Navier/Euler leaf batches pass, including H6NonlinearProduct, FiveProfileMoments, TerminalCompensation, NaturalEntrance, UniformFourierAlias, and PeriodicResidualLimits; the whole project remains unverified.
• Four unchanged static quality checks (headers, forbidden text, file sizes, and proof sizes) pass for the repair snapshot, and added lines meet the 100-character limit. Of the 164 files, 121 change only exposure attributes, 15 also normalize reflexivity proofs, and 28 contain reviewed proof/API repairs. No check, gate, or waiver changed.
• Heavy local commands use the shared VM lock, a 22 GiB memory limit, explicit two-thread Lean invocations, bounded compiler concurrency, and timeouts. Declaration-linter entries run separately with an 18 GiB address-space limit and 60-second timeout. Each worker queues at most one batch and freezes its source closure until completion.

Progress is updated at least hourly while work continues.

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

✅ No statements changed — all 1 tracked declaration across 1 modified file kept their type; only proofs / definition bodies changed.

Statements are compared textually against the merge base (comments and whitespace ignored; by proof terms embedded in a type are treated as proof-irrelevant), the same method as physlib's /check-golf. Anonymous instances and examples are not tracked.

Compile cost of modified files — base → head

Heartbeats: 0 → 0 (+0, —). Declarations: 0 → 0.

Per-file wall sum: 0.7 s → 0.8 s (+13.7%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal.

Files: 1 compared — 0 cheaper, 0 costlier, 1 within noise (threshold: |Δ heartbeats| ≥ 1,000 and ≥ 1%). Measurement errors: 1 base-side / 1 head-side file(s), marked ⚠; their heartbeat counts are partial.

Both sides are elaborated against the merge-base build of the pool — sound when only proofs and definition bodies change; a file whose statements changed may fail there and is flagged ⚠. Heartbeats come from Mathlib's linter.countHeartbeats, in maxHeartbeats units. Δ lines counts added/deleted lines from this PR diff.

File	Δ lines	HB base	HB head	Δ HB	Δ HB %	Wall base (s)	Wall head (s)
LeanPool/Basic.lean ⚠	+1/-1	0	0	+0	—	0.73	0.83
Total	+1/-1	0	0	+0	—	0.7	0.8

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

[Vilin97]

Reviewed f7e0dbc3d904410e145e075e1b3508466331e798 under the refactor rubric. The current one-line change removes definition-body exposure from LeanPool.Basic while retaining the public hello declaration and its signature. The change is consistent with the stated API goal; I found no actionable defect in this increment.

This review covers the committed Basic.lean change only. The PR body describes a pool-wide migration that is still in progress, so it should remain a draft until that implementation is finished and the final head has passed the full build, linters, and quality checks. Current full-pool CI is still running.

[Vilin97]

🤖 LLM review — refactor (gpt-6-astra)

Reviewed head: 57dabce33a6bb7e0c687ebffaa7e7dce4428839d

Verdict: 🛑 request_changes

This refactor removes blanket exposure from 862 files across 107 projects, preserving selected definitions and adding projection lemmas. The proof adjustments generally retain structure and clarify dependencies, but the exported interfaces remain incomplete: public computational checkers and the Birkhoff theorem’s conditional-expectation interface lose necessary unfolding access. An isolated Lean 4.34 import test reproduces the computational regression; aggregate builds were not rerun.

Aspect	Value
Scope	module exposure/API refactor
Introduces tech debt	🛑 yes
Maintainability	🛑 regressed
Brittleness	🛑 more_brittle
Risk	🟡 medium

The selective interfaces improve some dependencies, but remaining public API gaps need fixing before merge.

Findings (2)

• reusability-lost — LeanPool/RungeKuttaOrderConditions/ButcherOrder.lean:29
  The public butcherCheck and gaussCheck macros still explicitly unfold Phi, gamma, order, the tableaux, and related definitions, whose bodies this change hides. An importing-module test using the exact tree definitions passes with the original exposure and fails after removal: decide +kernel gets stuck on order leaf, and simp only rejects gamma and its dependencies. Restoring targeted exposure makes the test pass. Preserve exposure for the checkers’ computational dependencies and verify both macros from a separate importing module; certificates inside this file do not exercise that boundary.
• reusability-lost — LeanPool/PointwiseBirkhoff/Main.lean:19
  Removing exposure hides invCondexp without providing an equation identifying it with μ[φ | invariants f]. Both main Birkhoff theorems conclude convergence to this wrapper, so ordinary importing callers can no longer unfold it to obtain the conditional-expectation conclusion or apply Mathlib’s conditional-expectation lemmas. This follows Lean’s module visibility rules. Expose invCondexp individually or export its defining equality, then check the conditional-expectation formulation from an importing module.

---

Tokens: 1,753,751 in / 9,513 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $35.7885 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
request_changes is an ask, not a close: of the reviewer's past request_changes verdicts, 39% were merged after a human looked. Read the findings before acting on the verdict.

[Vilin97]

Changes requested by automated review

Reviewed head f0c226ed3a52eacf077c499456bca752269b9e30.

The exposure cleanup breaks the exported Runge–Kutta proof API. A separate module importing LeanPool.RungeKuttaButcherOrder and running open RungeKuttaOrderConditions.Butcher followed by example : orderCond eulerA eulerB t1 := by butcherCheck fails: the macro tries to simplify with unexposed bodies (Phi, phiVec, phiForest, dot, pmul, mulMatVec, gamma, the trees and the method tables). I reproduced this with the pinned toolchain after compiling the imported module. The same example in legacy, non-module mode succeeds, so compiling internal examples does not establish the exported API still works.

Acceptance condition: expose the definitions intentionally used by the public macros, or rewrite the macros against public equation lemmas, and verify both butcherCheck and gaussCheck from a separate module client. Keep the reduced default exposure elsewhere. This is an actionable compatibility defect even while the PR is a draft; no maintainer decision is needed.

The large exposure delta was audited file by file with a reproducible inventory; the remaining proof/API edits were inspected separately. The finding is a reproduced client failure, not an objection to the diff's size.

[Vilin97]

Changes requested by automated review

Reviewed exact head ac89e8bb07d66286226f89bfdaa6a07cbe58b4e1; this comment is updated to reconcile the latest 301-file repair, rather than repeat the older shard failures as current evidence.

The exported Runge–Kutta checker API still fails from an importing module. After compiling LeanPool/RungeKuttaOrderConditions/ButcherOrder.lean at this head, a separate module importing it and running open RungeKuttaOrderConditions.Butcher fails for both example : orderCond eulerA eulerB t1 := by butcherCheck and example : orderCond gaussA gaussB t1 := by gaussCheck. Lean reports Invalid simp theorem Phi: Expected a definition with an exposed body, likewise for phiVec, phiForest, dot, pmul, mulMatVec, gamma, the trees and tableaux. The macros at lines 293/316 still unfold these hidden definitions. Internal certificates do not test this module boundary. The macro client also reports missing exported norm_num implementation; verify its tactic imports as part of the client API.

Acceptance condition: give the public checkers access to the intended computational definitions (targeted exposure or public equations), export the required tactic implementation, and make both separate-module examples pass. Obtain all build shards and the unchanged aggregate lint/quality/trust gates at the resulting head. The current build is pending; the preceding head's nine failed shards are historical, not proof that these new repairs fail.

The complete follow-up was partitioned into 454 mechanically compared attribute/by rfl hunks and 41 remaining API/proof hunks, all inspected, across 301 files. The explicit projection equations and consumer repairs are valid progress and should be preserved. No new mathematical solution is claimed, and the blocking finding is a reproduced public API failure, independent of draft status or diff size.

[Vilin97]

Changes requested by automated review

Reviewed exact head 41625603d7c2cf879e6d6849c9621d66064fd793. The previous full diff, declaration/dependency and source review was reconciled with all current changed files, intervening edits, review threads, and available CI; preceding-head failures remain applicable to unchanged source. Valid earlier repairs are preserved.

The selective-exposure migration still breaks computational public interfaces and required CI. The Runge–Kutta butcherCheck/gaussCheck client failure remains applicable because the relevant implementation is unchanged; the current nine failed shards independently show hidden-body/definitional-equality failures, including Euler/Foundations/MollifierUniform.lean:85,89,208.

Acceptance condition: Restore the exported computation and tactic implementation interfaces, add or retain separate-module client checks, and make all ten migration shards pass under the unchanged gates. Draft status does not excuse these defects.

Preceding completed CI on unchanged project source evidence: full job log.

Formal self-review is unavailable for this account; this is the changes-requested disposition, not an approval.

Successor-head reconciliation (41625603d7c2cf879e6d6849c9621d66064fd793): The successor only integrates the already independently reviewed main changes; the submitted project source and the cited blocker/repair evidence are unchanged. Current observed gates: Build project=pending, Documentation preflight=SUCCESS, Content / non-content separation=SUCCESS. The disposition remains changes requested. This updates the existing review rather than adding a duplicate comment.