E1040: “Does transfinite diameter at least one force vanishing polynomial sublevel infimum?”

Independent rediscovery

Krishnapur, Lundberg, Ramachandran, On the area of polynomial lemniscates (24 March 2025): for a compact set of unit capacity the minimal lemniscate area tends to zero, answering Erdős–Herzog–Piranian. Found after the closure here, which was made independently

Contributors

@declangessel

@woshuajolk

Verification

Verdict report: artifact 677f4878

CI run: GitHub Actions log

Checks passed: build, axioms, manifest, no new axioms, static policy, anti restatement

Axioms: Classical.choice, Quot.sound, propext

Toolchain: Lean v4.33.0, Mathlib db584cd (Jig's pins)

Solution

import Mathlib.Analysis.Complex.Harmonic.Analytic
import Mathlib.Analysis.Complex.AbsMax
import Mathlib.Topology.Order.Compact
import Mathlib.Tactic
import Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
import Mathlib.Analysis.Calculus.ParametricIntegral
import Mathlib.MeasureTheory.Function.LocallyIntegrable
import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
import Mathlib.Analysis.Normed.Group.Bounded
import Mathlib.Analysis.Complex.OpenMapping
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Integral
import Mathlib.LinearAlgebra.Complex.FiniteDimensional
import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
import Mathlib.MeasureTheory.Group.Integral

CapacityOne.lean

Statement	User	Model	Harness	Time
2)V2One point has no distinct index pair, while the one-root product at zero and two has values zero and two.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V3For every closed infinite F⊆ℂ with transfinite diameter at least one, the infimum of the planar measures of {…	@woshuajolk +1	GPT 5.6 Sol	Cursor	8/25/26

2) V2 One point has no distinct index pair, while the one-root product at zero and two has values zero and two.

kernel-checked, filed Tue Aug 25 2026 07:48:29 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Concrete boundary checks for pair indexing and polynomial root products.

1) V3 For every closed infinite F⊆ℂ with transfinite diameter at least one, the infimum of the planar measures of {|∏(z-r)|<1}, over nonconstant finite root products with roots in F, is zero.

rediscovery, filed Tue Aug 25 2026 07:43:39 GMT+0000 (Coordinated Universal Time) by @woshuajolk, @declangessel

This submission independently machine-verifies the threshold assertion; an earlier public proof by shlummi covers the same full scope.

Priority correction: shlummi’s earlier public manuscript and Lean source cover the same full threshold assertion, including arbitrary compact capacity-one sets and closed unbounded sources. We independently read the complete mathematical proof, audited its formal endpoints, and checked the source hashes against its recorded standard-axiom verification reports; we found no scope restriction or mathematical gap. We have not independently rebuilt that third-party Lean project. The public proof claim at 2026-09-06 02:41:48 precedes our first public proof artifact at 02:48:39.469 UTC; the pinned repository commit is cc27bcde8bbe857d83c6c3b4ae537447739bf409. We therefore withdraw any claim of first public resolution and credit the earlier work. Our independently developed proof and Jig kernel verification remain valid.

Scope. Uses ENNReal for unbounded capacity and area, limsup of the standard Fekete-diameter sequence (known to converge), distinct index pairs, positive-degree root lists, and planar Lebesgue volume.

E1040:Erdős Problem #1040 “Does transfinite diameter at least one force vanishing polynomial sublevel infimum?”

E1040: “Does transfinite diameter at least one force vanishing polynomial sublevel infimum?”