Foundational theorems in local complex-analytic geometry

This repository formalizes four classical results in Lean 4:

1. Rückert Noetherianity for local holomorphic-germ rings;
2. algebraic and geometric finite projection for a nontrivial hypersurface germ;
3. the holomorphic constant-rank normal form;
4. Rückert's finite-family local analytic Nullstellensatz.

The four compared declarations are:

LocalComplexGeometry.holomorphicGerm_isNoetherian
LocalComplexGeometry.hypersurface_finiteProjection
LocalComplexGeometry.holomorphic_constantRank_normalForm
LocalComplexGeometry.localAnalyticNullstellensatz

Their proved public wrappers are in LocalComplexGeometry/Palomar.lean. Detailed mathematical formulations and fidelity notes are in MATHEMATICAL_STATEMENTS.md.

Mathematical content

Write

and let be the subring of germs which have a representative analytic at the origin.

1. Noetherianity

For every natural number , including , the ring is Noetherian.

2. Finite projection

Let be nonzero and vanish at the origin. The theorem returns a continuous complex-linear equivalence , a positive natural number , analytic representatives , and a transformed germ , where represents , represents , and is represented by .

Put , , and let be the quotient map. The result supplies the natural base-coordinate inclusion and the last-coordinate germ . Every has a unique expansion

Thus, for the -algebra structure induced by , the quotient is finite free of rank , with explicit power basis . The compared theorem states uniqueness directly rather than exposing the proof-bearing internal Module.Basis.

The same theorem gives an open preconnected neighborhood , a radius , coefficient functions analytic near every point of , and a factor analytic and nowhere zero on the vertical tube, such that

For every and , it asserts separately that both the prepared polynomial and are nonzero. It also gives finite fibers with at most distinct points and surjectivity and properness of the zero-locus projection to .

3. Constant rank

For an analytic map at , with and

throughout a neighborhood of , the theorem returns source coordinates and target coordinates . It states their four base-point equations, analyticity at the relevant points, all four eventual inverse identities, and

near zero, where for and otherwise.

4. Local analytic Nullstellensatz

If are analytic at zero and, on one neighborhood of zero,

then there are a positive natural number and functions , each analytic at zero, such that near zero

The library also proves the separately audited arbitrary-ideal identity , plus submersion, immersion, and regular-level-set corollaries. These additional results are not part of the four-declaration Comparator surface.

Palomar trust boundary

NullstellensatzPalomarChallenge.lean imports only Mathlib. Its transitive source dependencies contain no substantive project module and no ClassicalComplexWPT source. It locally spells out only the elementary analytic-germ ring needed by the first two statements.

NullstellensatzPalomarSolution.lean imports LocalComplexGeometry.Palomar, whose wrappers derive the same four declarations from the substantive library. The Weierstrass-preparation project is therefore a Solution-only dependency, pinned to the public commit b4a7273fe5c9752753c52e10494097569089642d. Mathlib is pinned through lake-manifest.json at 81a5d257c8e410db227a6665ed08f64fea08e997.

The unique module names are intentional: the WPT dependency has its own generic Challenge and Solution modules, and Palomar resolves modules over the whole Lake source path.

Reproduction

With the pinned Lean toolchain and normal Lake/Git access:

lake build
lake build NullstellensatzPalomarChallenge NullstellensatzPalomarSolution
lake env lean LocalComplexGeometry/AxiomAudit.lean
./scripts/audit-lean-sources.sh
./scripts/verify-comparator.sh

The comparator script pins the current Palomar toolchain components, including Comparator 575674928e239f5bc452aab72d1dd7b0f1326494, and runs Comparator, NanoDa, and Lean's default kernel. VERIFICATION.md records the audit surface.

Repository map

• NullstellensatzPalomarChallenge.lean: Mathlib-only statement module with exactly four deliberate theorem holes.
• NullstellensatzPalomarSolution.lean: proved comparison module.
• LocalComplexGeometry/Palomar.lean: proof-development-to-public-surface wrappers.
• LocalComplexGeometry/: substantive proof development.
• comparator.json: four theorem names, permitted axioms, and NanoDa setting.
• formalization.yaml: Palomar editorial metadata and disclosure.
• MATHEMATICAL_STATEMENTS.md: precise statement-by-statement interpretation.
• PALOMAR_SUBMISSION.md: exact submission instructions.

Sources and disclosure

The principal references are Gunning–Rossi, Analytic Functions of Several Complex Variables; Łojasiewicz, Introduction to Complex Analytic Geometry; and Rückert, “Zum Eliminationsproblem der Potenzreihenideale.” Exact locations and relationships are recorded in formalization.yaml.

Codex agents performed the Lean implementation, wrapper redesign, and automated audits under user direction. No external human mathematical or code review is claimed. The repository is Apache-2.0 licensed; the cited sources retain their own copyrights.

Palomar intake: https://submit.palomar-registry.org/.