Import several complex variables, analytic germs, and extension theory

[Vilin97]

Imports the several-complex-variables library from bjbraams/lean-scv, pinned at caef1ae776ff79933718312357980d46628d3702.

The development includes Reinhardt and Hartogs theory, Weierstrass preparation and division, analytic germs and sets, extension domains, Levi theory, and the completed solution statements. It retains the original copyright and authorship notices and the incoming Lean/Mathlib v4.34.0 module migration.

The project card now names SeveralComplexVariables.analyticOnNhd_of_separately_analytic_locally_bounded for the locally bounded Osgood result. SCV.osgood remains the valid jointly continuous version. Four Boas section references have been corrected against the December 2013 notes, and the theorem catalogue and bibliography link to the exact upstream revision. The documentation explicitly acknowledges the Weierstrass preparation and germ Noetherianity already in LocalComplexGeometry; the broader contribution includes germ unique factorization, relative primality, Hartogs extension, Cartan–Thullen equivalences, and Bochner's tube theorem.

Validation for the latest documentation repair:

• All executable Lean text is unchanged after comment stripping, including the incoming module migration; the repair changes only comments, the registry entry and its generated card.
• Static header, forbidden-source, file/proof-size, required-metadata, metadata-value and card checks pass. The generated root index is unchanged by the repair.
• Main was merged through bf008d9, preserving all 218 existing main cards plus this project.
• Full current-head CI at 07ef38d4c36552bfb21661ff6c4c85fac3463f90 passes the module indexes, project and challenge builds, declaration linters, text-style lint and repository quality checks: verified job. The PR remains unmerged.

Latest verification (2026-09-26): head a3b27d517836961e334f3e0d7e3d08b4189a218f passes the actual CI index, build, challenge/solution build, declaration-linter, text-style and repository-quality steps (job). PR remains unmerged.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

Automation disposition: needs-maintainer

Reviewed exact head 33d31760f09b0c03b0934afb4ffbc1e50addb1c0 for this draft pooled-project/content import, Import several complex variables, analytic germs, and extension theory. The changed tree is a substantial source import (including LeanPool/SeveralComplexVariables.lean) with the pinned upstream source, project metadata, and generated index present. Observed exact-head required checks have no failures; profile evidence: no proof-profile comment was posted for this exact head.

No concrete author-actionable defect was established in this bounded review that would justify an ordinary change request. The PR is still marked draft, so protected merge is not permitted. Maintainer decision required: confirm the headline result's significance, faithfulness, novelty, source/provenance and scope, then ask the author to mark the PR ready (or give scope direction). This is a maintainer disposition, not an approval.

[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 mathematical library modules for complex analysis.

No blocking defect was established, but a complete current-head assessment of the imported library’s source fidelity, novelty, and compile cost remains unverified.

Summary

Imports a several-complex-variables formalization covering analytic germs, Hartogs extension, convexity, and related results. Since the previous review, the head also replaces several Erdős 367 proof tactics, removes unused imports from its entry module, and refreshes README statistics.

• Both previous Greptile threads are resolved: the card names the locally bounded Osgood declaration, and the catalogue references point to the pinned upstream revision.
• No new actionable issue was established from the changes since the previous review.

_{Reviews (19) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..."}

[Vilin97]

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

Reviewed head: a472b2cf14e4f5389433ee51dc1ccb432d5d9472

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

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	At the requested commit, the three headline claims match the Lean statements, and the broader summary is supported by proved constructions.
Novelty	✅ pass	This is a genuine extension of existing pool coverage through analytic-germ factorization and global extension theory.
Significance	✅ pass	This coherent graduate-level development contains substantial named theorems and meets the pool’s significance bar.
Sources	✅ pass	The checked Boas references support the labelled results, upstream and prior Lean work are credited, and remaining textbook citations are unverifiable without a demonstrated inconsistency.
Code quality (advisory)	✅ pass	Shared Weierstrass division helpers, germ instances using Mathlib’s algebra hierarchy, and carefully scoped assumptions make this maintainable; no material quality issues identified.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	Standard domain and regularity hypotheses: Cauchy uses positive radii, an interior evaluation point, and continuity/separate analyticity on the closed integration polydisc, yielding the usual formula on smaller polydiscs within a holomorphic domain; the identity theorem requires a nonempty open agreement subset of a connected open domain. No major theorem, extension existence, or germ-factorization result is bundled as an additional assumption.
Already formalized	🛑 ClassicalComplexWPT.classicalComplexWeierstrassPreparation
Matches cited source	🟡 unverifiable
Fit	✅ good_fit
Level	graduate
Branch	several complex variables
Mode	theory_building
Code quality	4 / 5

Statement check: The Osgood headline proves joint analyticity from separate analyticity and local boundedness on an open finite complex coordinate space, without assuming joint continuity.

The project connects Weierstrass division and analytic-germ factorization with Hartogs extension, Cartan–Thullen equivalences, and Bochner’s tube theorem through substantial supporting theory.

---

Tokens: 7,478,217 in / 37,669 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $152.3895 (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.

[Vilin97]

Changes requested by automated review

Reviewed exact current head 6ca2ccff428a14332042f60d4036146cc6382868.

The exact-head Build pool/project checks fail because LeanPool.SeveralComplexVariables is not module-compatible. Port the imported closure, regenerate the index, and rerun all required gates.

Acceptance condition: the named defects are repaired on a new head and all required protected checks are green. Do not change repository policy or add waivers.

[Vilin97]

Changes requested by automated review

Reviewed head 0743324ed346630f0aa934b253029922eac748eb. Substantial SCV package, with supporting overlap in LocalComplexGeometry and a mismatched advertised endpoint.

1. Complete the pinned-toolchain integration. The exact-head build fails. Its concrete error includes:

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

   The file/dependency audit finds 8 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.

2. Resolve the substantive source/interface defect. The card attaches locally bounded Osgood prose to SCV.osgood, whose hypothesis is ContinuousOn. Point it to the actual locally-bounded theorem in LocallyBounded.lean, or correct the prose. Reconcile the section-level Boas references and disclose/reuse the Weierstrass/local-algebra support already in LocalComplexGeometry.

Review coverage: complete changed-file inventory and full diff retained; 163 changed project files, 33,577 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: Holomorphic germs, Weierstrass preparation and local algebra. 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.

[Vilin97]

Review and finding resolution at exact head c5b080873454b0556294fc000c688be7bb0031c0.

The previous faithfulness defect is fixed: the registry now names SeveralComplexVariables.analyticOnNhd_of_separately_analytic_locally_bounded, whose hypotheses are separate analyticity and a local norm bound on an open set, matching the revised prose. The existing SCV.osgood theorem and its joint-continuity hypothesis are preserved.

I checked the actual Boas December 2013 notes: §2.7 contains separate holomorphy and the Osgood/Baire steps (Theorems 6–8), while §2.4 contains Hartogs extension. The four incorrect source locators are corrected accordingly. Catalogue and bibliography links now resolve at the imported revision; the unavailable coverage-ledger link is removed.

The overlap is explicitly disclosed: coordinate-origin Noetherianity and analytic Weierstrass preparation with germ uniqueness already exist in LocalComplexGeometry, and the two analytic-germ constructions use the same Mathlib Filter.Germ representation there. The import's further finite-dimensional transport, germ factoriality/relative-primality and global extension/convexity results give it substantial additional scope. The independent analytic division support is retained with its quotient estimates; no novelty is claimed for the already pooled local endpoints.

The eight-file repair changes no executable Lean text. Static headers, forbidden-source, file/proof sizes, metadata and card synchronization pass; all other registry entries are unchanged, and main integration preserves every existing main card. I did not run a new broad build for a comments/metadata-only repair. The original migration's compilation and trust checks must still be enforced on fresh CI 36179447712.

Substantive fit and the reported documentation/source defects are resolved; approval is conditional on current-head required checks. GitHub prevents an APPROVE review from the PR author, so this verdict is recorded transparently as COMMENT. No workflow, gate, setting or waiver was changed.

[Vilin97]

{
"reviewed_head": "07ef38d4c36552bfb21661ff6c4c85fac3463f90",
"recommendation": "approve subject to fresh required CI and current-main integration",
"review_type": "full-review reconciliation plus independent source and scope revalidation",
"prior_review": "#490 (comment)",
"incoming_changes": "The update preserves the scope/source repairs at c5b0808 and changes only comment wrapping and the compact main-declaration list. Cauchy and identity results remain in main_results and the Lean development. Comparing all changed project files with the prior full-review cf7b403 yields no changed mathematical statements or proofs after accounting for comments, visibility and umbrella import ordering.",
"faithfulness": "The locally bounded headline now names SeveralComplexVariables.analyticOnNhd_of_separately_analytic_locally_bounded, whose actual assumptions are an open domain, separate analyticity, and a local eventual norm bound. Joint continuity is proved internally. The Banach-valued finite-coordinate scope is accurately stated.",
"sources": "Independently checked Boas December 2013 notes: Section 2.7 Theorems 6/7/8 cover separate holomorphy, locally bounded Osgood, and the Baire step; Section 2.4 concerns Hartogs extension. All four corrected locators are retained. The card identifies Boas Theorem 7 as the classical two-variable scalar source, without claiming its statement literally has the stronger formalization scope. The pinned upstream theorem catalogue resolves; the absent local coverage-ledger reference was removed.",
"source_links": [
"https://haroldpboas.gitlab.io/courses/650-2013c/notes.pdf",
"https://github.com/bjbraams/lean-scv/blob/caef1ae776ff79933718312357980d46628d3702/SCVMainTheorems.md"
],
"novelty_disposition": "Accept the explicitly documented partial overlap with LocalComplexGeometry and Mathlib. Independent Weierstrass preparation and germ Noetherianity are disclosed; germ unique factorization, global Hartogs extension, Cartan\u2013Thullen and Bochner tube content justify this coherent additional theory development. The identity theorem is not presented as an independent novelty.",
"quality_and_validation": "Prior full code-quality assessment passes. Importer evidence records a successful 3479-job project build, linter/style, and compiled 1417-declaration trust audit across 163 files. The incoming wrapping change addresses exactly the three line-length warnings in the later CI log. New-head mandatory CI remains pending; no gate is waived."
}

[Vilin97]

Review carried forward to exact commit a3b27d5 from the substantive reconciliation at 07ef38d (prior review). All three required checks passed on that prior head.

This refresh imports only main's attribution and generated metadata updates. All 163 project Lean files, the exact project card and the entire registry remain byte-identical to the reviewed head; all 218 main cards are retained with their values and text. The actual pinned mk_all --module --check passes. The substantive review therefore carries forward, conditional on fresh required CI for this new head. No new local project compilation is claimed.

[Vilin97]

Daily disposition: needs maintainer — protected merge operation

Reviewed exact head 02c40ce28c3d0a03fd7c93cafc54bceb1f9dc015. Global SCV extension/convexity results remain substantial despite disclosed Weierstrass/local-algebra overlap with LocalComplexGeometry. The card points to the actual locally bounded separate-analyticity theorem, and distinguishes its generalization from the cited classical case. 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: SUCCESS. 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]

Reviewed exact head 57033c06f41c3998cfa7f630afef1961e438a0eb. The SCV project source and card are unchanged from the complete review; subsequent main integration preserves the advertised source-scoped results.

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: SUCCESS. Unfinished checks are not passes.

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

[Vilin97]

Disposition: needs-maintainer — protected merge operation. Reviewed head 57033c06f41c3998cfa7f630afef1961e438a0eb. 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.