Erdős problem #1041

Adversarially test the degree-five normalized radial-star lemma with an exact certificate path ready.

First action: Run `python3 tools/radial_star_discriminator.py --self-test --trials 0`, then implement a separate rational checker for explicit root configurations and bad-arm t witnesses.

Stop or redirect when: Stop and exact-certify if the second-smallest maximum exceeds 1+1e-4; otherwise stop numerical work after the predefined adversarial families and one fixed-budget optimizer.

• Degree-five normalized minimum-enclosing-disk radial lemma.
  Build the exact rational checker, then optimize the second-smallest arm maximum over a fixed adversarial family portfolio.
• Exact radial-failure certificate format.
  Verify rational points, exact disk support, pair separation, and rational t witnesses using fraction arithmetic and polynomial sign checks.
• Correct the Formal Conjectures length semantics.
  After ensuring at least 8 GB free, rerun bootstrap and identify the mathlib rectifiable-curve or variation API.

• formal statement repair
  Replace range Hausdorff measure with parametrized variation/rectifiable length or restrict to polygonal paths with a proved equivalence.
• exact semialgebraic barrier certification
  Represent {|f|<1} as a real semialgebraic domain and certify barriers or variational lower bounds for all paths between specified roots.
• counterexample and witness search
  Normalize configurations by their minimum enclosing disk, enforce the complement of the elementary close-pair reduction, and compute the maximum product along every radial arm from stationary points of the squared-modulus polynomial.
  Reopen only if: Not applicable to the active radial strategy. For formal compilation, provide at least 8 GB free or a streaming cache bootstrap; for the flow-tree route, satisfy its explicit critical-network and length-estimate condition.

• Treat the current Formal Conjectures file as a proof or exact formal acceptance target.
  Both theorems contain sorry and the length semantics undercount general retracing paths.
  Reopen only if: A successful no-sorry build with corrected parametrized-length semantics or a proved equivalence for the restricted path class.
• Generic gradient-flow lines plus the area integral automatically form a short root-connecting tree.
  Generic flow lines do not form the asserted tree, and removing a sufficiently large critical neighborhood destroys the length budget.
  Reopen only if: Provide an explicit critical-point connection rule and a quantitative length bound that works already for z^2-r^2.
• Use the inherited Terra degree 4-7 samples as evidence for the higher-degree radial lemma.
  It evaluated unnormalized products, omitted the relevant separation condition, and could suppress maxima through the missing scale factor.
  Reopen only if: None; use the corrected normalized implementation or a materially independent encoding.