feat(ErdosProblems/114): add finite n <= 14 EHP certificate variant

[bengoechea]

Summary

This adds Erdős Problem 114, the Erdős--Herzog--Piranian lemniscate-length conjecture.

The all-degree conjecture is stated as open. A separate finite-degree sibling statement records the current certificate-backed range 1 ≤ n ≤ 14:

• n = 1: elementary translated-circle case
• n = 2: MacLane / Eremenko--Hayman degree-two case
• 3 ≤ n ≤ 14: Mendoza finite-degree IEEE-1788 interval certificate packet

The external certificate pipeline is not formalized in this Lean file, so the finite statement remains a sorry rather than being discharged by imported certificate axioms.

References

• Erdős problem page: https://www.erdosproblems.com/114
• Zenodo version DOI for the corrected v3.1.0 certificate packet: https://doi.org/10.5281/zenodo.20087919
• Zenodo concept DOI, which resolves to the latest version: https://doi.org/10.5281/zenodo.19184467
• Source release for the n=13 corrected certificate: https://github.com/MendozaLab/erdos-experiments/releases/tag/v3.1.0

Notes

This supersedes the older #3712 approach. That branch encoded per-degree certificate conclusions as axioms; this PR instead keeps the finite result as an externally certificate-backed statement with a sorry, making the boundary between Lean formalization and external computation explicit.

Validation

• Earlier clean-worktree validation: lake build FormalConjectures completed successfully before the DOI-version update.
• DOI-version update commit 713d3fa: lake build FormalConjectures.ErdosProblems.«114» completed successfully.
• A wording/proof-integrity scan found no imported certificate axioms and no claim that the all-degree conjecture is resolved.
• DOI wording now cites version DOI 10.5281/zenodo.20087919 for the corrected v3.1.0 packet and concept DOI 10.5281/zenodo.19184467 for the latest-version family.

[bengoechea]

Follow-up after the Zenodo manual version was published: commit 713d3fa updates the Lean reference to pin the corrected v3.1.0 certificate packet at version DOI 10.5281/zenodo.20087919, while keeping the concept DOI 10.5281/zenodo.19184467 for the latest-version family.

Targeted validation for this DOI-only commit: lake build FormalConjectures.ErdosProblems.«114» completed successfully in a clean PR worktree.