WIP: Remove blanket section exposure across Lean Pool

[Vilin97]

This draft removes blanket @[expose] public section exports across Lean Pool. It keeps ordinary public section declarations and adds individual @[expose] attributes where imported clients require a definition's body. The main module-system migration merged separately in #517.

The scope remains the full module migration: preserve all projects, mathematical statements, assumptions and intended APIs; review the individual exposure edits and any narrowly scoped proof repairs; reconcile accepted changes on Main through the review owner's integration process. No project removal, theorem weakening, warning suppression, waiver or gate change is proposed.

Draft — do not merge yet. Published and locally validated source remain distinct. The published PR head is 4e51cbbfd4a1b908ffbd333044bcda2df9697870. Earlier full-pool attempts used local H52 3823d12e542bef70447bd5a801ef3c0b717db54b; the current local, unpublished checkpoint in the dated observation below is Source70 ec202b6ce0c4e64cf2d0f0cb9d956631e92b4021.

Main was verified as 15542c175fbeeb83666dc46fc20c4f18f0783e12 at the 2026-10-20, 08:40:02 UTC publication. The same immutable SHA inherits Root's 07:36 UTC primary metadata comparison against 2aaa7220788257635be774b855528c4f0be6f3bd: twenty Git-object observations established identical object types and IDs for all ten protected compiler/dependency, gate and review paths. Other intervening Main content was not inspected or integrated with Source70. Final integration with moving Main remains with the review owner.

Saved H52 structure checks covered 14,216 Lean files, with zero missing module declarations and zero blanket-exposure sections. These structural checks do not establish compilation or final-gate acceptance. The later reviewed exposure repairs preserve all other statement, assumption, definition-body, proof, import, option and header bytes.

Retained N45/N59 Brill compilation passes at H52, including their recorded Row04/Row06 coverage, remain valid within their named scope. The earlier Regts/Stafford incremental batch passed using replayed artifacts and supplies no fresh-compilation credit; the separate Carlson Relations qualification freshly compiled and passed. Interrupted H52 full-pool attempts and later targeted runs retain their original outcomes, logs and caches. None is relabeled a completed full-pool build.

Retained earlier local history. Source53–68 supplied scoped passing targets while later EllipticPDE project runs still failed. Original outcomes, byte-preservation reviews, logs and caches remain retained, with the default 200,000-heartbeat limit, proofs, options and gates preserved. Source60's 600-second coordination stop occurred before its remaining targets; its separate continuation remains separate evidence.

Dated validation observation — 2026-10-20, 09:14:21 UTC. The current local, unpublished source is Source70 ec202b6ce0c4e64cf2d0f0cb9d956631e92b4021, saved at 18:18:25 UTC. Its two individual exposures in GrothendieckVanishing/CohomologyAPI add 20 bytes; independent preservation and actual commit/map reviews matched the exact change. All other statement, type, hypothesis, definition-body, proof, import, option and header bytes remain unchanged.

Source69's EllipticPDE target 64108 passed at 16:50:28 UTC (project 0, outer 0, no guard stop), with 13 fresh Built records. That scoped pass remains separate from full-pool acceptance.

Source69’s full LeanPool attempt 78968 remains an output-guarded failure: outer exit 1, target exit −15, no normal terminal. Its 1,095 fresh Built records remain progress only. Its closed written log retained ten CohomologyAPI source-error headers, including the original 200,000-heartbeat timeout; unwritten stdout may have remained undrained. The old failure and separate operational Source release are not relabeled successes.

On Source70, attempt 75079 completed LeanPool.GrothendieckVanishing at 18:31:26 UTC, with project exit 0, outer exit 0 and no guard stop. Its independently reviewed closed log contains 13 fresh Built records, including CohomologyAPI in 230 seconds and the project root in 3.0 seconds, without error, warning or crash markers. The ten earlier source-error headers cleared with the original heartbeat limit and options unchanged. This establishes the named retained-cache project result; it does not isolate which exposure caused the improvement or establish a full-pool pass.

Three later full-LeanPool attempts stopped at their output-growth guards:

• 18780 was recorded GUARDED_STOP at 19:21:37 UTC: outer exit 1, target exit −15, no normal terminal; 438 fresh Built records in its closed written log.
• 23771 was recorded GUARDED_STOP at 19:37:44 UTC: outer exit 1, target exit −15, no normal terminal; 142 fresh Built records in its 59,450-byte closed written log.
• 82298 was recorded GUARDED_STOP at 19:50:13 UTC: outer exit 1, target exit −15, no normal terminal; 35 fresh Built records in its 50,225-byte closed written log.

Subsequent independent review — 19:52:43 UTC. Reviews of all three entire written logs found no error, warning, heartbeat-timeout or crash markers in these written logs, including after ANSI removal. These observations cover written EOF only: stdout may not have fully drained, so unwritten output remains unknown. The missing normal terminals prevent complete compiler-capture or peak-resource claims. Per-run Built counts are retained progress, not unique-module totals, completion percentages or full-pool acceptance.

Before/after Source70 checks matched all 14,216 files against the same map, with clean tracked source. Empty groups and Source release were recorded separately; release supplies no build acceptance.

Closed continuation — 21:59:29 UTC. Attempt 23766 stopped at its finite 7,200-second target timeout: LeanPool exit −15, outer exit 0, with fullpool_build_passed and all_targets_passed both false. Its independently reviewed 145,865-byte closed written log contains 1,116 fresh Built records and 28 replay records, with zero findings across all fourteen raw/ANSI diagnostic scans. These are written progress records, not unique-module totals, completion percentages or a full-pool pass; unwritten stdout is not established complete.

For 23766, both Source70 before/after checks matched 14,216 files / 271,053,191 bytes against the same map with clean tracked source. The owned group was empty and normal Source release was independently verified. All 512 captured compiler samples matched the pinned executable and final -j1 flags; these bounded samples do not establish continuous or universal compiler telemetry.

Closed continuation — 2026-10-20, 00:09:43 UTC. Attempt 54848 stopped at its finite 7,200-second target timeout: LeanPool exit −15, outer exit 0, with fullpool_build_passed and all_targets_passed both false. Its independently reviewed 116,398-byte closed written log contains 708 fresh Built records and 38 replay records, with zero findings across all fourteen raw/ANSI diagnostic scans. Written EOF does not prove unwritten stdout complete; these records establish no global unique-module total, graph percentage or full-pool acceptance.

For 54848, both Source70 checks matched 14,216 files / 271,053,191 bytes against the same map with clean tracked source. Normal Source release and an empty owned group were independently verified at 00:14:06 UTC. The recorded RSS maximum was 14,777,171,968 bytes, with at most two recorded compiler processes and 512 pinned final-flag samples; the samples supply no continuous or universal telemetry claim.

Closed project continuation — 2026-10-20, 02:25:02 UTC. Attempt 59420 reached normal CLOSED after its finite 7,200-second target timeout: LeanPool.MovingSofa exit −15, outer exit 0, with project and full-pool results both false. Root’s whole-written-log scan covered 2,365 bytes at stable EOF/SHA, recording 24 fresh Built records, zero replay records, zero findings across its ten broad raw/ANSI diagnostic scans, and no partial written tail. The independent fourteen-pattern closed review completed at 02:28:06 UTC, finding zero markers across all fourteen raw/ANSI scans and independently verifying the normal Source release and empty owned group. Written EOF does not prove unwritten stdout complete; these records establish no global unique-module count, graph percentage or acceptance. Both Source70 checks matched 14,216 files / 271,053,191 bytes with clean tracked source. The terminal recorded a maximum RSS of 19,341,033,472 bytes, at most two compiler processes and 26 pinned final-flag compiler samples; these bounded observations do not establish continuous or universal telemetry.

Project pass — 2026-10-20, 03:17:29 UTC. Attempt 85718 completed the sole target LeanPool.MovingSofa in normal CLOSED, with target exit 0, no stop reason and outer exit 0. Root’s whole-written-log scan covered 1,549 bytes at stable EOF/SHA, recording 16 fresh Built records, zero replay records, zero findings across its ten broad raw/ANSI diagnostic scans, and no partial written tail; the root module built in 3.2 seconds. The independent fourteen-pattern closed review completed at 03:21:49 UTC, finding zero markers across all fourteen raw/ANSI scans and verifying the exact Source70 checks, normal release and empty owned group. Both Source70 checks matched 14,216 files / 271,053,191 bytes with clean tracked source, and Root verified normal guards, Source release and an empty owned group. The terminal recorded a maximum RSS of 12,833,685,504 bytes, at most two compiler processes and 16 pinned final-flag compiler samples; these bounded observations do not establish continuous or universal telemetry. Written EOF does not prove unwritten stdout complete; these records establish no global unique-module count or graph percentage. This is project C0 only; it supplies no full-pool, gate, current-Main, CI, final-review or merge acceptance.

Full-pool guarded stop and subsequent release. Attempt 20650 remains an output-guarded failure, recorded GUARDED_STOP at 04:06:57 UTC: LeanPool target exit −15, outer exit 1, with no normal terminal and no full-pool acceptance. Its independently reviewed 127,878-byte entire closed written log contains 577 fresh Built records and 41 replay records, with zero markers across all fourteen raw/ANSI diagnostic scans and no partial written tail. These are written progress records, not global unique-module totals, graph percentages or completion; unwritten stdout may have remained undrained. The missing normal terminal prevents complete compiler-capture or peak-resource claims. Both Source70 attestations matched 14,216 files / 271,053,191 bytes against the same map. Root’s 04:12:35 UTC snapshot recorded clean tracked source and an empty owned group. The separate operational Source release completed at 04:24:44 UTC, and the independent negative closed-and-released review completed at 04:27:04 UTC. Release supplies no build acceptance.

Full-pool guarded stop — 2026-10-20, 05:45:44 UTC snapshot. Attempt 9170 was recorded GUARDED_STOP at 05:35:09 UTC under its output-growth guard: LeanPool target exit −15, outer exit 1, with no normal terminal and no full-pool acceptance. Its independently reviewed 125,134-byte entire closed written log contains 535 fresh Built records and 50 replay records, with zero findings across all fourteen raw/ANSI diagnostic scans. These are written progress records, not global unique-module totals, graph percentages or completion; written EOF does not establish that unwritten stdout fully drained. The missing normal terminal prevents complete compiler-capture or peak-resource claims. Both Source70 attestations matched 14,216 files / 271,053,191 bytes against the same map. Root’s separate operational release at 05:44:18 UTC recorded clean tracked source, an empty owned group and Source availability restored through a negative CLOSED ledger; the original guarded runtime and ledger remain immutable. This operational release supplies no build acceptance. Source70 remains unpublished and the cache is retained. At this dated snapshot, a possible 15.875 GiB cumulative-stage continuation remains prospective, with no actual adoption or successor invocation credited. All six actual post-build gates remain unexecuted; full-pool, kernel, current-Main, hosted-CI, final-review and merge acceptance remain pending.

Latest full-pool guarded stop — 2026-10-20, 06:33:26 UTC snapshot. Attempt 59598 was recorded GUARDED_STOP at 06:10:00 UTC under its output-growth guard: LeanPool target exit −15, outer exit 1, with no normal terminal and no full-pool acceptance. Its independently reviewed 88,441-byte entire closed written log contains 117 fresh Built records and 51 replay records, with zero findings across all fourteen raw/ANSI diagnostic scans and no partial written tail. These are written progress records, not global unique-module totals, graph percentages or completion; written EOF does not establish that unwritten stdout fully drained. The missing normal terminal prevents complete compiler-capture or peak-resource claims. Both Source70 attestations matched 14,216 files / 271,053,191 bytes against the same map. Root's separate operational release completed at 06:17:34 UTC, and the independent negative closed-and-released review completed at 06:21:53 UTC, verifying clean tracked source, an empty owned group and Source availability restored through a negative CLOSED ledger. The original guarded runtime and ledger remain immutable. Release supplies no build acceptance; Source70 remains unpublished and the cache is retained.

A separate operational qualification committed the 34 GiB disk / 15.5 GiB cumulative stage selection at 04:36:04 UTC, on the same 18,693,206,016-byte baseline within the original 16 GiB reservation, with no increment or new reservation origin. Any continuation remains on the same unpublished Source70 and retained cache, under the finite 7,200-second target bound, actual compiler -j1, at most two compiler processes and unchanged source guards. The prospectively qualified disk envelope is 34 GiB, with 15.5 GiB cumulative stage growth from the same baseline, superseding the earlier operational disk ceiling. RAM remains capped at 25 GiB. No cleanup, baseline reset, refund or new reservation origin is credited.

Attempt 59598 used the later 15.875 GiB cumulative stage / 34 GiB disk selection on that same baseline within the original 16 GiB reservation, without an increment or new reservation origin. At the 06:33:26 UTC checkpoint, the next B preparation remains prospective and unadopted: it would separately register a 2 GiB increment, bringing the retained reservation to 18 GiB, and select a 17.75 GiB cumulative stage / 36 GiB disk envelope with the aggregate minimum-free requirement increased from 73,668,755,456 to 75,816,239,104 bytes. No B adoption or successor invocation is credited by this dated snapshot. RAM remains capped at 25 GiB, with the original 2 GiB margin, address space remains 22 GiB, and the at-most-two-compiler, final-flag, finite-target, heavy-lock, Source, proof and gate safeguards remain unchanged. This preparation supplies no full-pool, post-build-gate, kernel, current-Main, hosted-CI, final-review or merge acceptance.

Current registered continuation — 2026-10-20, 07:33:08 UTC snapshot. B was actually registered at 06:37:11 UTC, adding 2 GiB to the original 16 GiB reservation for 18 GiB retained in total. The current selection is 17.75 GiB cumulative stage / 36 GiB disk, on the same 18,693,206,016-byte baseline, with no new reservation origin, baseline reset, refund or cleanup credited. The earlier 06:33:26 UTC prospective-B paragraph records its historical snapshot. Actual retained-cache attempt 91674 has been BUILDING since 06:45:45 UTC, on the same unpublished Source70, with the sole target LeanPool and the finite 7,200-second target bound; the final compiler -j1, at-most-two-compiler, 25 GiB RAM plus 2 GiB margin, 22 GiB address-space, heavy-lock, Source, proof and gate safeguards remain unchanged. Root's reviewed active written prefix at 07:33:08 UTC covers 124,733 bytes, 1,646 complete lines, 533 fresh Built records and 51 replay records, with no partial written tail and zero findings across all fourteen raw/ANSI diagnostic scans. This is a live prefix, not final written EOF or proof that unwritten stdout is complete; the records supply no global unique-module count, percentage, graph completion or acceptance. The 07:32:57 UTC bounded sample recorded 2,832 seconds elapsed, 9,672,978,432 bytes RSS, two compiler processes and 37,206,790,144 allocated bytes, below the selected 37,752,123,392-byte allocation stop. These are dated samples, not continuous or peak-resource observations. No normal terminal, full-pool result or post-build-gate acceptance is credited by this snapshot.

2026-10-20, 08:22:25 UTC update. Prior B18 full-pool attempt 91674 was recorded as guarded at 07:49:50.608421 UTC for output growth cap: outer exit 1, target exit −15, and no normal terminal. Its complete written 144,464-byte log contained 762 fresh Built and 51 Replayed records across 1,875 complete lines, with no partial tail and zero matches in all fourteen canonical diagnostic categories, both raw and ANSI-stripped. The two source attestations matched 14,216 files / 271,053,191 bytes exactly. Root released the source at 07:53 UTC, and the independent negative closed-and-released review passed; this supplied no full-pool or post-gate acceptance. The next reservation was actually registered at 08:02:14 UTC: original 16 GiB + B's 2 GiB + C's 1 GiB = 19 GiB, with a selected 18.75 GiB stage and 37 GiB disk envelope from the same growth basis, without a new reservation origin, baseline reset, refund or cleanup credit. Retained-cache full-pool attempt 57779 has been BUILDING since 08:09:52.963409 UTC, on unchanged, unpublished Source70 ec202b6ce0c4e64cf2d0f0cb9d956631e92b4021. The finite 7,200-second bound, final -j1, at most two compiler processes, RSS + 2 GiB < 25 GiB, 22 GiB address-space bound, heavy lock, source/proof safeguards and gates remain intact. Root's 08:22:25 UTC active-prefix observation covered 89,162 written bytes / 1,229 complete lines, no partial tail, 116 fresh Built / 51 Replayed records, and zero matches in all fourteen raw and ANSI-stripped diagnostic categories. These dynamic records describe a partial written prefix; they establish no final EOF, unwritten-output completeness, global unique count, completion percentage, graph completion, full-pool pass or post-gate, CI, Main-integration, review or merge acceptance.

2026-10-20, 09:14:21 UTC update. C19 full-pool attempt 57779 was recorded as guarded at 08:41:35.585432 UTC for output growth cap: outer exit 1, target exit −15, and no normal terminal. Its complete written 111,324-byte log contained 376 fresh Built / 51 Replayed records across 1,493 complete lines, no partial tail, and zero matches in all fourteen canonical diagnostic categories, both raw and ANSI-stripped. Both source attestations matched 14,216 files / 271,053,191 bytes exactly. Root's separate source-release invocation succeeded, and Storage's independent negative closed-and-released review passed at 08:54:16.916399 UTC; no full-pool or post-gate credit follows. The next reservation was actually registered at 08:56:51 UTC: original 16 GiB + B's 2 GiB + C's 1 GiB + D's 1 GiB = 20 GiB, selecting a 19.5 GiB stage with strict allocation stop 39,631,171,584 bytes and a 37.125 GiB disk envelope, from the same growth basis and within the original 25 GiB net-output scope, without a new reservation origin, baseline reset, refund, cleanup credit or cache deletion. Retained-cache full-pool attempt 7557 has been BUILDING since 09:09:24.357406 UTC on unchanged, unpublished Source70 ec202b6ce0c4e64cf2d0f0cb9d956631e92b4021. The finite 7,200-second bound, final -j1, at most two compiler processes, RSS + 2 GiB < 25 GiB, 22 GiB address-space bound, heavy lock, source/proof safeguards and gates remain intact. Root's 09:14:21.889113 UTC active-prefix observation covered 83,470 written bytes / 1,173 complete lines, no partial tail, 55 fresh Built / 52 Replayed records, and zero matches in all fourteen raw and ANSI-stripped diagnostic categories. This partial written prefix establishes no final EOF, unwritten-output completeness, global unique count, completion percentage, graph completion, full-pool pass or post-gate, CI, Main-integration, final-review or merge acceptance.

All six post-build gates remain pending and unexecuted. Their current static preparation is inert, with no actual execution plan or gate credit. Execution still requires successful current-source full-pool closure, independent closed review, warning-free written output and fresh source/resource bindings. Final published-head CI and independent final review remain required.

Source58 also restored three legacy product-instance names as public aliases to canonical Mathlib structures, without adding duplicate instance-search registrations. Historical registration/reducibility behavior and compatibility with every external client are not claimed identical.

The twelve-file RemovalExtremalStability source proposal from earlier Main 374a940b17712eab49f6dfc0bbe754b8ff55e76b remains unapplied and uncompiled. Its static preservation review and prepared runner do not supply latest-Main integration or kernel acceptance; full-pool/post-build prerequisites and reviewer integration remain pending.

The published head's observed CI still fails in Lean Action CI run 37186446631. Those historical diagnostics do not determine the later unpublished local outcomes. Fresh hosted CI must validate the final published head.

Before this PR can leave draft status and merge, the final integrated source must:

• Preserve the complete project scope and pass module-index generation/checks.
• Complete a warning-free full LeanPool build.
• Pass all applicable declaration linters, text-style checks and repository-quality gates, including compiled axiom and environment/option audits.
• Be published at a reviewed final SHA and pass fresh hosted CI tied to that exact head.
• Receive a fresh favorable independent final review and satisfy applicable branch protection, with integration and merge retained by the review owner.

Targeted local successes or static reviews supply no full-pool, final quality, hosted-CI or merge acceptance. This PR remains draft while those requirements are pending.

[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 e6497e1377c0cc99581411a48d6ee793a67350f4.

The refactor still breaks imported definition visibility. The completed predecessor run on the unchanged affected sources reports failures in ClassificationOfSurfaces/Moise/LocallyFiniteFaceExtension, BooleanMultiplication/N4/SevenGate, MarkovProcess/DenseTime/Trajectory and HardSphereNBC/HardSphereGeometry, among the grouped failures in run 36430792945. The latest two Nikodym batches (13 files, then 9 files) only add targeted @[expose] attributes; it does not repair those other modules.

Acceptance condition: Repair each failing dependency boundary with the needed exposed definitions or public lemmas, remove ineffective exposure attributes reported as warnings, and pass every build shard and unchanged repository gates. Preserve the valid exposure repairs already made.

Prior complete source/dependency/source-attribution audits were reconciled against this head using full diffs, source/card/configuration equality where applicable, and the changed proofs. Fresh pending checks are not represented as green. Formal self-review is unavailable to the PR-author account.

[Vilin97]

Changes requested by automated review

Reviewed exact repaired head ee4c94a4d08f167d498781cebd56d5a7fdd1ad95. All 171 follow-up paths are accounted for in the complete 21,590-line diff and 120 bounded chunks: 131 exposure-only repairs, 38 independently reviewed main-added files and two lossless main integrations. The selective attributes preserve mathematical definitions, proof bodies and theorem hypotheses; this is useful progress, not a new mathematical contribution.

The current public reduction API still breaks downstream consumers. The earlier no-new-failure checkpoint is superseded by this head’s completed shard 01, which has 69 Lean compiler diagnostics. RS/Novel/Skein/ComposeAssoc.lean:916,1151 still fails type/definitional equality; RS/Classical/Super/ColourEval.lean:46,52 cannot establish definitional equality; RS/Novel/Skein/ThroughValue.lean:120,133 cannot unfold/project CoreOddColouring. The diagnostics are current-head evidence; the predecessor’s Brill/NRR failures are not represented as newly confirmed here. Other current shards remain pending.

Acceptance condition: restore the remaining selective exposure or public equation/constructor bridges in the affected RegtsSevenster closure, preserve exported computations and theorem contracts, and pass every build shard plus the unchanged warning, lint, quality and trust gates. Preserve the valid repairs already made. Neither draft status nor the diff’s size is a blocker or reason for a maintainer label.

Additional completed shards at this same reviewed head corroborate the same API defect: shard 02 cannot eliminate OrderConvergesTo in OrderClosures/OrderContinuous/Basic:68 and rejects LLexpr definitional equalities; shard 04 cannot expose seamDivisor in BrillNoetherGraphs/SeamCalculus:124 and later consumers; shard 05 rejects NandakumarRamanaRao/VariableBody/Partition:81; shard 06 cannot eliminate EuclideanGapDynamics/OGMGDynamics in ParameterFreeGradient/V7/Proofs/Euclidean:38/183. These are current-head observations, not historical failures. Restore the narrowly needed constructor/equation reductions for each dependency closure and pass every shard plus the protected aggregate; blanket exposure removal is not safe until its consumers remain kernel-checkable.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[Vilin97]

Independent review — changes requested at da308bab941a6783c135e6fe13b5ab8c98c9bd81

The four declaration-level attributes in Surreal/Basic.lean clear the previous opacity errors there. The current exact-head shard 01 now builds Basic.lean, but fails with five Lean errors in two downstream modules:

• LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Ordinal.lean:37 and :41: the exported rfl theorems cannot validate their claimed definitional equalities after section-wide exposure was removed. At :64, the generated toSurrealRingHom._proof_1 is private but needed by the exported definition. Preserve these exported equations with the necessary targeted exposure or explicit public proofs.
• LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Dyadic.lean:165: rfl cannot reduce through the unexposed Dyadic.mkRat. At :281, the exported toIGameEmbedding_apply equation likewise fails its definitional-equality check. Give these consumers the intended reduction interface or prove the equations through public lemmas.

These are compiler failures in the current head, not a concern about the size of the refactor. The other shards and aggregate lint/quality checks are still running, so they are not claimed as passed. Keep the PR draft, repair these module boundaries, and rerun the complete unchanged protected checks at the resulting head. The prior aggregate-root 10k-line objection is obsolete after the shipped project-root migration; LeanPool.lean is 257 lines here.

Exact-head update — 84a26fc91b5a7e90193d74b97b3714453f929cc4

The four targeted attributes clear all five Ordinal/Dyadic errors above. The new shard 01 now fails with 11 errors, all in LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Real.lean:

• :53, :283, and :347: @[match_pattern] is invalid because Real.toIGame, Real.toGame, and Real.toSurreal are not exposed. Exported rfl equations at :287, :351, and :360 also need those reductions.
• :99, :296, and :369: generated embedding _apply equations fail the exported definitional-equality check. At :337 and :629, generated ring-hom proof constants remain private.

Targeted exposure on the three maps and their three @[simps!] embeddings and two @[simps] homs is a plausible source-only repair, but it has not been compiled. The other shards and aggregate checks are still pending. The review remains changes requested at this head until the full protected run passes.

Exact-head update — 581ecea4c4f363abfcb7b9f85a47e45ec5b4ef9c

The eight declaration-level attributes in Surreal/Real.lean clear the 11 Real errors above. The next shard 01 has now failed with five Invalid rewrite argument errors in two downstream modules:

• LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/NormalFormAdd.lean:168: rw [leadingCoeff] needs the definition from LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Leading.lean:29, but the name is seen as a value of type ℝ across this module boundary.
• LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Support/FinitePowerFamily.lean:456, :476, :537, and :581: rewrites by Oz.IsOrdinaryInteger, Oz.IsReduced, and Oz.HasFiniteDegree need their definitions from Support/OmnificFiniteDegree.lean:26, :31, and :40; they are currently seen as Prop values, not rewriteable definition names.

Targeted exposure on these four definitions is a plausible repair, but it has not been compiled and later downstream errors may surface. Keep the PR draft and run the full unchanged protected checks on the next exact head. The review remains changes requested at this head.

Exact-head update — d3cea7b3aed5462b5b715ebb4f6808343c345f89

The new commit adds @[expose] to exactly those four definitions in Leading.lean and OmnificFiniteDegree.lean. It changes no theorem statement, proof body, or import. This precisely targets the five 581ecea4 shard errors, but the fix still needs compiler confirmation. The fresh exact-head Lean Action run has passed planning and is compiling all ten shards; documentation preflight and content separation passed. The PR remains draft and changes requested pending the full unchanged protected result.

Terminal shard 01 result — d3cea7b3aed5462b5b715ebb4f6808343c345f89

The four new attributes cleared the five 581ecea4 rewrite errors, but the exact-head shard 01 failed with 13 downstream Lean errors in four modules:

• LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Support/ConwayNormalForm.lean:89-90: constructor notation cannot unfold NormalFormIdentifiesOmnificIntegers. Its definition is in Standalone/CombinatorialGames/Examples/OmnificFactorization.lean:51; targeted exposure is needed. The “No goals to be solved” message at :90 follows the first error.
• LeanPool/ConwayRefinement/ConwayRefinement/Examples/OmnificInteger/OneRowPrime.lean:125, :131, :139, :143 and DegreeTwoPrime.lean:162, :170, :179, :184: elaboration cannot unfold the respective exponentAtIndex definitions. They are in Examples/OmnificInteger/OneRowNormalForm.lean:49 and DegreeTwoNormalForm.lean:101; expose those two definitions.
• LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Support/OmegaOmegaBoundary.lean:198, :201, :232: norm_num [scale] cannot unfold scale. Its definition is in Support/FinitePowerFamily.lean:92; expose it or use the existing scale_eq_one_div_three theorem at :95 in these proofs.

These four upstream fixes have not been compiled at this head. Keep the PR draft and rerun the full unchanged protected checks after repair; the review remains changes requested.

Tested-base shard 01 result — 664354de762fe664c7c9314cf070eeb9c5fbc2d6

The four added @[expose] attributes clear the 13 prior errors. On PR head 664354de against its tested base c57dde9, Lean Action shard 01 failed with 23 diagnostics across five downstream proof modules:

• Standalone/Mathlib/Support/InlineConwayRefinementProof.lean:410, :594, :622, :646-647: the proof bridge cannot unfold InlineSurreal.Surreal.ConwayConjecture, singletonIntegerCut, and IsConwayOmnificInteger. Their definitions are in Standalone/Mathlib/Support/InlineSurreal.lean:44, :33, and :40; the final two errors follow the opaque conjecture type.
• Standalone/CombinatorialGames/Support/OmnificFactorizationProof.lean:37, :50, :59: intro cannot see the binders of EveryOmnificIntegerIsPrimal, IrreducibleIsPrime, and IrreducibleFactorizationsAreUnique, defined in Standalone/CombinatorialGames/Examples/OmnificFactorization.lean:57, :61, :66.
• Standalone/CombinatorialGames/Examples/OmegaOmegaBoundaryProof.lean:18: rw [ExistsAtBoundary] needs the definition in Standalone/CombinatorialGames/Examples/OmegaOmegaBoundary.lean:39 exposed.
• Standalone/CombinatorialGames/Examples/DegreeTwoPrimeProof.lean:30, :36, :59, :74, :102, :110-111, :123, :135, and OneRowPrimeProof.lean:28, :38, :49, :61, :84: the display propositions, coefficient functions, and paired normal forms are opaque across their imported modules. Candidate declaration sites are Standalone/CombinatorialGames/Examples/DegreeTwoPrime.lean:48-76, OneRowPrime.lean:37-51, Standalone/CombinatorialGames/Support/DegreeTwoExample.lean:126,153, OneRowExample.lean:71,97, and the corresponding main normal forms in Examples/OmnificInteger/DegreeTwoNormalForm.lean:152 and OneRowNormalForm.lean:98. Some diagnostics cascade from the same hidden definition; each targeted repair needs compilation.

This is tested-base evidence from c57dde9, not a current-main CI result. Canonical main is now 1d7a672f while the PR remains based on c57dde9; latest-main reconciliation and a fresh complete protected run are still required. Keep the PR draft. The review remains changes requested.

Current-main shard 01 result — cd8a838e6119f1ed96dd2faad5ca0718c44155f1

The branch added 36 targeted @[expose] attributes in nine Conway files and made a true two-parent merge of canonical main 1d7a672f. The attributes clear all 23 prior 664354de shard 01 errors. On this exact head and current main, Lean Action shard 01 now fails with one Lean error:

• LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Support/FinitePowerFamilyProof.lean:24: rw [FinitePowerFamily.PrimalFamily] cannot unfold the Prop-valued definition. Its source is Support/FinitePowerFamily.lean:544-545; a targeted @[expose] on def PrimalFamily is the next source-only candidate.

The prior failures are cleared, but this protected run failed and aggregate lint/quality gates are not established as passed. Keep the PR draft and rerun the full unchanged protected checks after the next source repair. The review remains changes requested.

Exact-head repair pending — 4e8c37e318f2d16bb799e59282970af21b07315e

The preceding cd8a838e single-error result is historical evidence from the previous head. This direct child adds exactly one source line: @[expose] on def PrimalFamily in LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Support/FinitePowerFamily.lean:544. No theorem statement, proof body, import, or other file changed. The annotation directly targets the prior FinitePowerFamilyProof.lean:24 rewrite error, but the repair has not yet been confirmed by the compiler.

On canonical main 1d7a672f, fresh exact-head Lean Action CI passed planning and is still building its shards; shard 01 and aggregate lint/quality results are pending. Keep the PR draft and the review changes requested until the full unchanged protected checks pass at this exact head.

Terminal shard 01 result — 4e8c37e318f2d16bb799e59282970af21b07315e

The one-line @[expose] PrimalFamily repair cleared the previous cd8a838e rewrite error. On this exact head and canonical main 1d7a672f, Lean Action shard 01 failed its project build at 06:53 UTC with one new Lean diagnostic:

• LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Examples/FiniteDegreeFamilyProof.lean:19:6: rw [FiniteDegreeExamples.EveryFinitePowerOccurs] reports Invalid rewrite argument because the imported name is seen as a Prop value. Its definition is unexposed in Standalone/CombinatorialGames/Examples/FiniteDegreeFamily.lean:26; a targeted @[expose] on def EveryFinitePowerOccurs is the next source-only candidate.

That candidate has not been compiled. Other build shards were still running when this diagnostic was captured, and aggregate lint/quality gates are not established as passed. Keep the PR draft and the review changes requested; run the full unchanged protected checks at the next exact head.

Exact-head repair pending — abe92ae932cfc4b386e61b08d2029ad2c590673c

The preceding 4e8c37e shard 01 failure is historical evidence from the previous head. This direct child adds exactly one source line: @[expose] on def EveryFinitePowerOccurs in LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Examples/FiniteDegreeFamily.lean:26. No theorem statement, proof body, import, or other file changed. It directly targets the prior FiniteDegreeFamilyProof.lean:19:6 rewrite error, but compiler confirmation is pending.

The new exact-head Lean Action CI run has started against canonical main 1d7a672f; the protected build and aggregate results are pending. Keep the PR draft and the review changes requested until the full unchanged protected checks pass at this exact head.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.