Lemniscate length of monic cubics

../

_proof: Root identities give exact length integrals; a comparison with z^3-c and box-uniform ball bounds over two parameter regimes prove the family inequality.

evidence/: Box-uniform arb bounds cover the whole parameter range of the cubic family in two regimes, with a coverage join and a two-sided control.

The proof and its ball-arithmetic evidence are by Plasma AI. The whole-claim examination and distinct PASS grade warrant tier 1 for the complete statement, including uniqueness. The external-source and arithmetic qualifications below remain in force; no Lean proof is claimed. The family inequality is proved here: a written analysis reduces it to explicit integrals, and the evidence program bounds those integrals uniformly over boxes that cover the whole parameter range, including both ends. The consequence for every cubic also consumes two source results of a refereed paper: Lemma 4, the existence of a maximizer in each degree, and Lemma 5, that some maximizer has all its critical points on its lemniscate; the uniqueness clause also uses the deformation constructed in the proof of Lemma 5. Their library accounts record the statements as read on the print and the proof of Lemma 5 as read in outline; for this claim the whole proof of Lemma 5 (pp. 5--7 of the corrected preprint) was read on the page images. Tao's Proposition 1.2 restates them.

The claim is the degree-3 case of the question of Problem 114, with uniqueness: $z^3-1$ maximizes the length, and up to rotation and translation it is the only maximizer. The uniqueness argument uses the quasiconformal deformation in the proof of Lemma 5, which the paper carries out for every extremal polynomial, together with the strict family inequality. It settles no other degree. The research sketch records how the reduction, the deformation and the family inequality compose.

Verification. Read the proof and run, from the repository root,

uv run --no-sync python wiki/theory/polynomials/L144_cubic_lemniscate_length/evidence/main.py

which takes about five minutes on one thread. The verification record retains the whole-statement report, distinct grade, exact executable inputs and independent derivations. An initial identity-only import exposure was ruled immaterial by the distinct grader; the later eligibility assessment found no demonstrated unrelated-status exposure to that grader. Four failed auxiliary endpoint-equality assertions remain failed and have no successful-calibration weight. The accepted source interface retains Lemma 4 as an external theorem with only partial verification of its supplied proof, and the cited Beltrami book theorem remains an unread original-source boundary.