Erdős–Herzog–Piranian conjecture — proof for d=3

This text is a demonstrative write-up of a retained analytic chain for the critical-onfamily in degree , conditional on a domain reduction cited from the literature(Part I: Eremenko–Hayman; Tao, Prop. 1.2, arXiv:2512.12455). It is not anunconditional, self-contained proof of EHP for every monic cubic from first principles.Domain reduction (Part I) — Tao Prop. 1.2 / EH99, valid for all including (no hidden large- restriction); used, not reproved-Analytic chainParts II–VII: , , , V1–V3, quadratures, rationalconstants. Closure of on uses Route 1 on and Route 2 (chord) on .-A posteriori only Python scripts (Appendix A), floating-point checks, grid sweeps — outside the logical chain-MachinecheckedLean (Appendix B) checks Route 1 fully, plus a Route-2fragment without Lean holes in DeltaRoute2/Chord/Lambda/Gap:algebraic chord core; chord lemma (1-x)^{-1/2}≤1+x/2+μ(a)x²;Λ/Λ♯ and Beta recurrence Beta32/Beta52; change-of-variables forincomplete Beta slices; uniform gap≥41/25⇒19/5