Import Conway refinement for omnific integers

[Vilin97]

Imports Conway's multiplicative refinement theorem for omnific integers from gaearon/conway-refinement at 264445c93b78554c408e99e4e7f663693b4e91ab, together with the generalized power-series factorization theory, standalone formulations and CombinatorialGames dependency.

All 682 upstream production/dependency modules are retained in 774 destination files. Original authorship and license notices remain. The import keeps 161 SourceIndex signature checks, two instance checks and fourteen UpstreamReuse fixtures. Long proofs are factored into mathematical lemmas, and the port uses Lean/Mathlib 4.34.0.

The imported quotient-game namespace is isolated as ConwayGame, and its OfSets tactic has a project-specific spelling to avoid aggregate pool collisions. The module-migration checkpoint a4932bf82 preserves the automated main merge and migrates all 91 remaining legacy import aggregators to the required module system. Its complete warning-free build (3176 jobs), all 15 declaration linters, style and module-index checks pass. Recursive size/static and compiled public-axiom/environment audits also pass across all 774 files. The fresh metadata gate also passes. A combined import with the existing Brouwer game formalization passed before the aggregator-only migration.

The latest head 03255d3a2 preserves the subsequent citation correction. Its aggregate pool job passes module/index generation, compilation, declaration linters, text style and repository quality checks. Auxiliary documentation/metadata checks and independent review are tracked separately. The PR’s existing ready-for-review state is preserved. No checks, limits or waivers were changed; do not merge.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

Changes requested by automated review

Reviewed exact head c1d5bd8d7420c2791f567eb18147d713fc9370ed. The exact-head full build fails because the imported ConwayRefinement and existing MisereGames files declare the tactic of_sets_tactic more than once (reported in ConwayRefinement/CombinatorialGames/Game/Player.lean:146 and MisereGames/OfSets.lean:39). Resolve the duplicate declaration/integration conflict and rerun all gates at the new head.

[Vilin97]

/review

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low risk] Adds a large mathematical library for combinatorial game theory.

No blocking issue was established, but this review does not independently establish that the entire large import is safe to merge.

Summary

The PR imports Conway refinement and its supporting formalization, adds a catalog entry, and exposes the headline theorem through a focused project module. Since the previous review, it has replaced an inlined surreal support model with the shared CombinatorialGames model and narrowed unrelated Erdős 367 imports.

• The two previous Greptile threads are resolved: the project is registered, and its focused umbrella imports Solution rather than the entire development.
• No new actionable issue was established. The full 776-file contribution was not independently checked declaration by declaration in this review, so headline fidelity, provenance, and cost across the entire import remain unverified.

_{Reviews (18) · Last reviewed commit: "Merge commit 'refs/review-reconcile-2026..."}

[Vilin97]

🤖 LLM review (gpt-6-astra, 5 rubrics)

Reviewed head: c59d7d31cd231f9d4b0392c0b9e111f0bb121d68

Verdict: 🛑 request_changes — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	The exported theorem proves the card’s four-factor refinement claim for omnific integers, including degenerate cases.
Novelty	✅ pass	Searches of pinned Mathlib 4.34.0 and existing pool sources found no duplicate of ConwayRefinement.Palomar.conwayRefinement.
Significance	✅ pass	A research-level theory-building project centered on Conway’s refinement theorem, with substantial supporting Hahn-series factorization theory and no identified generated-bulk concern.
Sources	🛑 block	Correct the remaining LM24 reducedness citation from Definition 8.2.1 to Definition 8.2.6.
Code quality (advisory)	🤔 discuss	The implementation is competent overall, but duplicated foundational APIs and substantial repeated proofs create maintenance debt worth reviewing before merging.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	Only omnific-integer membership and the product equality stated in the card; the internal Hahn-series hypotheses are proved for surreals.
Matches cited source	🛑 mismatch
Fit	✅ good_fit
Level	research
Branch	ordered algebra and surreal numbers
Mode	theory_building
Code quality	3 / 5

Statement check: For arbitrary cut-defined omnific integers with ab = cd, the theorem supplies omnific e, f, g, h satisfying all four claimed equations modulo Conway equivalence.

The project proves multiplicative refinement for omnific integers—a named problem documented in L’Innocente–Mantova, §1.1—and develops supporting algebraic-independence, polynomial-presentation, and factorization results.

Sources findings (1)

• source-mismatch — LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/RealLeadingSplit.lean:37
  The source pointer for isReduced_mapRealDomainToSurreal identifies the wrong numbered result: LM24 8.2.1 is a proposition about divisibility under truncation, while reducedness is Definition 8.2.6. This misdirects readers checking the definition used by the theorem. Replace the reference with Definition 8.2.6, consistent with the imported Reduced.lean and LM24 §8.2.
  Evidence: The diff says: “is reduced in the sense of LM24, Definition 8.2.1, after the embedding.” Its theorem is theorem isReduced_mapRealDomainToSurreal {a : Nonpositive ℝ R} (haOrder : (mapRealDomainToSurreal a : R⟦Surreal.{u}⟧).order ≠ 0) (haConstant : constantCoeff a = 1) : IsReduced (mapRealDomainToSurreal a : Nonpositive Surreal.{u} R) := by. The imported HahnSeries/IntegerPart/Reduced.lean instead explicitly attributes def IsReduced to “LM24, Definition 8.2.6”.

Code quality findings (2)

• duplicate-definition — LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/ConvexQuotient.lean:41
  This recreates Algebra/Order/ConvexQuotient.lean's convexity class, quotient-order instances, and proofs under another namespace. The parallel implementation extends through Support/ArchimedeanQuotient, ConvexQuotientSplitting, OrderedAddGroup, and HahnLimitTailQuotient, duplicating their counterparts in Algebra/Order, Algebra/Order/Module, Topology/Order, and HahnSeries/LimitTailQuotient. The standalone OneRowExample and DegreeTwoExample similarly copy Examples/OmnificInteger/OneRowNormalForm and DegreeTwoNormalForm. Maintaining these independent copies requires repeating API changes and risks divergence. Keep the shared constructions in dependency-light modules and preserve the alternate public namespaces with aliases or thin wrappers; that can retain the standalone import boundary without duplicating implementations.
  Evidence: Both ConvexQuotient files add class IsConvex (H : AddSubgroup G) : Prop where with ordConnected : (H : Set G).OrdConnected, and independently add instance instLE : LE (G ⧸ H) where le x y := ∃ a b : G, (a : G ⧸ H) = x ∧ (b : G ⧸ H) = y ∧ a ≤ b. Both ArchimedeanQuotient files also define def tailKernel (T : Set (FiniteArchimedeanClass G)) : AddSubgroup G := ⨅ c : T, ArchimedeanClass.closedBallAddSubgroup c.1.1 and repeat its supporting proofs.
• duplicate-proof — LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/DerivAtInjective.lean:96
  The successor-case theorem repeats the substantial support-tail argument already proved generally in UnboundedTruncations.lean:109, including an identical private translatedTruncation_not_mem_negativeMonomialIdeal_of_mem_support helper. Its proof can instead apply the general theorem with rho := beta, upper exponent beta + 1, and lt_add_one beta; the import graph permits this reuse without a cycle. Related private-helper duplication occurs for truncGE_zero_eq_single and supportOrderType_truncGE_zero_eq_zero_or_one in Factorization/DegreeTwo/DegreeTwo.lean and Factorization/GermLike.lean. Consolidating these proofs would avoid maintaining multiple versions of the same truncation arguments.
  Evidence: The specialized declaration assumes (hu : ordinalValue u = ω^ (beta + 1)) and concludes ∃ γ : ℝ, θ < γ ∧ γ < 0 ∧ ordinalValue (translatedTruncation (u : K⟦ℝ⟧) γ) = ω^ beta. The general declaration is theorem exists_ordinalValue_translatedTruncation_eq_wpow_of_lt {beta rho : NatOrdinal} (hrho : rho < beta) (u : Series K) (hu : ordinalValue u = ω^ beta) {θ : ℝ} (hθ : θ < 0) : ∃ γ : ℝ, θ < γ ∧ γ < 0 ∧ ordinalValue (translatedTruncation (u : K⟦ℝ⟧) γ) = ω^ rho := by. Both proofs independently construct set S : Set ℝ := B ∩ Set.Iio y with hSdef, prove have hSpwo : S.IsPWO := hBpwo.mono Set.inter_subset_left, and set set γ : ℝ := sSup S with hγdef before repeating the singleton and limit cases.

---

Tokens: 5,966,873 in / 37,026 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $122.1144 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/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.

CI was not green for this commit at review time; this review does not replace CI.

[Vilin97]

Changes requested by automated review

Reviewed exact current head 85b7729e30a137424902ef1bb821534c1e0f71d4. The full build still reports duplicate declaration of of_sets_tactic between ConwayRefinement and MisereGames. Resolve the integration conflict and rerun all gates.

[Vilin97]

Changes requested by automated review

Reviewed head 7a56eb0d65d306307c8cac5f566a0752bb330ee6. Substantial four-factor omnific-integer refinement, with concrete signed/support models.

1. Complete the pinned-toolchain integration. The previous source-identical build failed at bbe32e0b1cc94909c4a24f362fff44860be07555. The same source-level blocker is present at this reviewed head; its error includes:

   error: LeanPool.lean:1:0: cannot import non-`module` LeanPool.ConwayRefinement from `module`
   

   The file/dependency audit finds 91 changed Lean files without the required module form. Repair the affected dependency closure, regenerate the module index, and obtain a warning-free full pool build plus the unchanged linter, quality and axiom gates. A project-only or previous-head build does not resolve this failure.

Review coverage: complete changed-file inventory and full diff retained; 774 changed project files, 154,107 lines, import reachability and executable trust-token scan; advertised endpoints and supporting definitions examined with bounded implementation sampling and existing review findings reconciled. Potential reusable value: Surreal and ordered-algebra interfaces. Source/provenance and prior-art evidence were considered separately from CI; these findings do not assert that every proof line was manually read. Earlier automated scores are advisory and are not approval of this failing head.

Exact-head reconciliation: the automatic main merge left all project Lean source and the pinned toolchain unchanged. This run restored the original parsed project card after the rebase parser dropped the title-first entry; parsed-card equality and the generated module-index check pass. The restoration is a narrowly scoped fast-forward commit from an isolated worktree. It does not repair the substantive blockers above; new CI is not assumed green.

[Vilin97]

{
"review_type": "current-head reconciliation with prior complete rubric review",
"recommendation": "approve subject to fresh required CI",
"mandatory_gates": "Pending on this new documentation-only head; no waiver or gate change.",
"validation": "Executable Lean is unchanged by the repair. Current-main integration preserves every one of the 218 main cards plus this project; metadata/card and complete module-index checks pass.",
"prior_review": "#509 (comment)",
"scope": "All 774 project files were byte-identical to the fully reviewed a4932bf before the comment-only repair. The prior passing faithfulness, novelty, significance, and code-quality assessments carry forward.",
"statement": "For arbitrary omnific integers with ab = cd, the theorem supplies four omnific factors satisfying the advertised refinement equations, including degenerate cases; membership and the product equality are the disclosed assumptions.",
"repair": "Corrected the standalone explanation to characteristic-zero ordinal-value multiplicativity v_J(bc) = v_J(b) \u2299 v_J(c), citing Berarducci Theorem 9.7 and LM24 Fact 2.7.1. Natural addition is correctly applied to the exponent degrees. This resolves the prior source-blocking finding without changing any definition or proof.",
"source": "https://arxiv.org/html/1710.07304v5#S2.SS7",
"quality_disposition": "The remaining shared-lemma and umbrella-scope suggestions concern maintenance/build organization, not the faithful research theorem. They remain advisory; no proof consolidation or reduced build scope is claimed.",
"reviewed_head": "03255d3a20ebe0dfb95e7ba5dbd28b9039246dd3"
}

[Vilin97]

Approve the focused public-umbrella repair at dcb473579a7188c55309767316b3630ff78841f9, subject to all required fresh CI. COMMENT is used because this account authored the PR.

LeanPool.ConwayRefinement now publicly imports only Solution, which already publicly exports the advertised ConwayRefinement.Palomar.conwayRefinement theorem and its standalone statement/proof API. All 773 descendant source files, every declaration/proof, the complete project card, and LeanPool.lean remain byte-identical. The aggregate root still imports all 773 descendants directly, retaining full repository reachability. The prior completed mathematical review therefore carries forward.

The complete source import graph shrinks the entry closure from 683 to 379 project modules, with no Tests or Fixtures remaining in that closure. Some Standalone modules remain because they implement the advertised theorem. These are source-derived dependency counts; no compile-time saving was measured.

All four existing scoped source checks pass across 774 project files, the generated card and entry-import checks pass, and the actual pinned mk_all --module --check reports no update necessary. A bounded optional compiled export probe could not acquire the shared build lock, so no compiler was run and no dependency rebuild was started. Fresh CI must validate compilation and the remaining repository gates. No checks, configuration, main refresh, or waiver changed.

[Vilin97]

Daily disposition: needs maintainer — protected merge operation

Reviewed exact head 3010605384a7f3e0b6e99c6a94a3d8ec86a92ff8. The four-factor omnific-integer refinement is substantive. Duplicate inline development was removed, and the public entry imports the solution closure while the aggregate index retains every imported file for gates. The complete source/dependency review and recovered repairs were reconciled through the lossless main integration; fresh protected CI remains the integration authority.

Build project: pending/not yet reported, Content / non-content separation: SUCCESS, Documentation preflight: IN_PROGRESS. These are observed check states, not an assertion that unfinished checks passed.

The remaining authority boundary is operational: this repository has allow_auto_merge=false, and GitHub rejected enablePullRequestAutoMerge with “Auto merge is not allowed for this repository.” The maintainer must make protected queuing available through an authorized repository-setting decision, or remove this label and perform a normal squash merge after the required checks and current-base integration pass. This cycle does not change repository settings or bypass protection. No unresolved substantive author-actionable finding justifies another change request or closure; the label is not for draft status, missing profiling, or an old advisory score.

[Vilin97]

/review

[Vilin97]

Reviewed exact head c59d7d31cd231f9d4b0392c0b9e111f0bb121d68. The concurrently completed repair bridges indexed games directly to the shared CombinatorialGames IGame/Surreal. It removes the copied foundations and second conversion layer (111 inserted, 3734 deleted lines), preserves the first-principles statement and headline theorem, and passes the recovered full-project build, linters, style, index and scoped quality/trust audit.

The complete prior review was carried forward after checking the project source/card and inspecting the repair delta; prior local validation is inherited evidence. Previous rubric review. The original maintainer blocker is resolved; clearing needs-maintainer. Current-base integration and successful required checks remain conditions for a normal protected merge.

Observed checks: Build project: not yet reported; Content / non-content separation: SUCCESS; Documentation preflight: IN_PROGRESS. Unfinished checks are not passes.

[Vilin97]

Disposition: needs-maintainer — protected merge operation. Reviewed head c59d7d31cd231f9d4b0392c0b9e111f0bb121d68. The substantive review and valid repairs are preserved. A concurrent run cleared the operational label, but this PR remains open with no auto-merge request. GitHub still reports allow_auto_merge=false, and the protected auto-merge attempt was rejected.

The remaining maintainer decision is to authorize normal protected auto-merge or arrange serialized current-main integration and protected merging. No mathematical blocker justifies requested changes or closure; no protected merge is queued. This label records the unresolved operational authority/coordination decision and must be removed before merge. Repository settings and protection were not changed.