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 2aaa7220788257635be774b855528c4f0be6f3bd in the primary observation at 2026-10-20, 02:14:10 UTC. Fresh metadata comparisons at 02:15:32 UTC against 078c94d9712c98d0e1c0337fcd48999c02ffe76a found identical Git object types and IDs for the ten checked 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, 02:25:16 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 remains pending at the 02:25:16 UTC snapshot. 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; Root recorded normal Source release and an empty owned group. 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. A new 7,200-second same-project retained-cache retry remains proposed only, requiring the independent fourteen-pattern closed review and fresh admission guards; no new actual plan, launch or result is credited. A later project C0 still requires a separate final sole-target 7,200-second full LeanPool run, followed by all six post-build gates and the remaining final requirements. 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 32 GiB, with 14 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.

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.