feat(ErdosProblems): add Problem 114 (Erdős–Herzog–Piranian conjecture)

[bengoechea]

Summary

Adds FormalConjectures/ErdosProblems/114.lean — the Erdős–Herzog–Piranian conjecture (#114).

• erdos_114: Full open conjecture (all n) — body is sorry
• erdos_114_small_n: Solved for 3 ≤ n ≤ 14 via twelve axiom declarations (one per degree, each encoding the IEEE 1788 interval-arithmetic certificate for that n) and interval_cases n discharge

Context

Moritz Firsching confirmed a standalone PR is welcome:
Zulip message

This PR is intentionally separate from #3422.

On the axiom shape

The current shape is twelve axioms ehp_cert_3 ... ehp_cert_14, each typed as (p : ℂ[X]) (hp : p.Monic) (hd : p.natDegree = n) → arcLength p ≤ arcLength (X^n - C 1) for the corresponding n. The theorem then dispatches via interval_cases n, one axiom per case. A single axiom over the range would be tighter — open to refactoring if reviewers prefer. Posting a discussion on #Formal-conjectures to ask for the repo convention.

Certificates

Each n case is verified by branch-and-bound over the parameter space of monic degree-n polynomials, with IEEE 1788-2015 interval arithmetic:

• n = 3–12: Python/mpmath
• n = 13–14: Rust/inari (MPFR-backed)

Results, B&B box counts, runtimes, and Hessian negative-definiteness checks at the extremizer for each degree are deposited with SHA-256 checksums:

doi:10.5281/zenodo.19480329 (v5; supersedes v3 at doi:10.5281/zenodo.19322367 referenced earlier)

Reproduction: python verify_ehp.py --degree N (n ≤ 12) or cargo run --release -- --degree N (n ≤ 14).

Definitions

Name	Description
levelCurveUnit p	Lemniscate {z ∈ ℂ : ‖p(z)‖ = 1}
arcLength p	1-dimensional Hausdorff measure of the level curve

Future work

• Discharge axiom ehp_cert_n declarations once Mathlib has a verified IEEE 1788 library
• Uniqueness theorem (erdos_114_small_n_unique)
• Extension to n = 15+ as compute budget allows

Tooling

The Lean source was prepared with assistance from Anthropic's Claude (Claude Code CLI) for proof drafting, Mathlib API search, and tactic iteration. The IEEE 1788 verification (Python/mpmath, Rust/inari) was author-written. All axiom statements, lemma signatures, and proof tactics are author-verified against Mathlib's current master source. The author is responsible for the final content.

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[Smetalo]

Is this a duplicate of #3708?

[bengoechea]

Not a duplicate — #3708 was the first attempt but had CLA issues and a messy commit history, so I closed it and opened this one clean. Same content, cleaner PR. #3708 can be ignored.

[bengoechea]

For context on what changed from #3708: CLA was failing because the original PR came from a personal fork before I'd signed it. Also fixed the Apache 2.0 license header (http → https in the license URL, which was failing CI) and updated the AI disclosure section. This PR is from the MendozaLab org fork with a clean single commit. The mathematical content in 114.lean is identical.

[bengoechea]

Build was failing because hausdorffMeasure 1 left the 1 at universe level (Type) instead of ℝ. Fixed in 53d30b1 — annotated as hausdorffMeasure (1 : ℝ). CI should be green on the next run.

[bengoechea]

Note on the fix commits: the initial submission compiled locally against a slightly older Mathlib snapshot. CI's pinned toolchain exposed type class resolution differences — specifically around hausdorffMeasure elaboration. We've since set up a local environment mirroring upstream's exact lake-manifest.json so future submissions compile clean against CI on the first push.

[bengoechea]

The CLA issue is resolved now, and I’ve reconciled my local state to the exact PR head for this branch (MendozaLab:erdos-problem-114), rather than the older erdos-114-small-n attempt from #3708.

This PR is intended to add only FormalConjectures/ErdosProblems/114.lean, and the follow-up fixes discussed earlier are already on the branch, including the μH[1] notation change and the Classical elaboration fix.

At this point it looks like the remaining blocker on GitHub is that the fork-triggered workflows have not been approved to run yet. When convenient, could someone approve the pending Actions workflows for the current head commit so the full CI can execute? If CI surfaces anything real after that, I’ll address it directly on this branch.

[bengoechea]

Closing this as superseded by #3958.

The newer PR uses the v13 finite-degree formulation: it records the contiguous 1 ≤ n ≤ 14 certificate-backed range, includes the corrected n=13 release/audit trail, and keeps the all-degree EHP conjecture explicitly open. It also avoids the older approach here of discharging the finite statement via per-degree certificate axioms; the external certificate pipeline is cited but not formalized in Lean.

Thanks for the earlier triage on this one.