Inverse coeff. |A₄| over Starlike S* · Geometric Function Atlas

← all proofs

Certificate under review. This legacy or incomplete artifact is retained for audit, but cannot carry public proof wording until its v1 replay contract validates.

Stored legacy claim for Inverse coeff. |A₄| over Starlike S*. Its proof wording is withheld pending a valid replayable v1 certificate.

What this rests on

The certificate reduces to these classical lemmas - each checkable by hand, independently of the engine.

1. Schur parametrisation is exact

The Schur recursion maps the closed polydisc \(\overline{\mathbb D}^{m}\) exactly onto the admissible coefficient vectors \((a_2,\dots,a_{m+1})\) of the class. Ranging the Schur parameters over \(\overline{\mathbb D}^{m}\) therefore sweeps every member's coefficients — nothing admissible is missed and nothing spurious is added.

Schur 1917; Foias–Frazho; Simon, OPUC. · schur-onto-coefficient-body
2. Rotation normalisation

The functional is weight-homogeneous under \(f(z)\mapsto e^{-i\theta}f(e^{i\theta}z)\), so its maximum is attained on the rotation-normalised slice \((\gamma_0\ge 0\) real\()\). This removes one real dimension and is verifiable by hand.

Elementary weight homogeneity. · rotation-reduction
3. Floating-point arithmetic is sound

Every float64 operation in the interval evaluation is widened by its IEEE-754 forward-error bound, so each computed interval rigorously encloses the true real value. The numerics are a certified enclosure, not a heuristic estimate.

IEEE-754 rounding; standard interval arithmetic. · ieee754-forward-error
4. The box partition is complete

Boxes are bisected at exactly representable midpoints, so the two children tile the parent with no gap and no overlap. The union of the certified leaf boxes is therefore provably the entire domain — coverage is exhaustive.

Exact dyadic subdivision. · bisection-partition

In the literature

No matching publication turned up via the registry's automated keyword + reconciliation search of the 1,067-paper corpus. That search is imperfect - it can miss a result published under a differently-named class (e.g. SL* vs lemniscate) - so treat this as unconfirmed, not a novelty claim. Confirm with a manual search before claiming priority.

dag engine m = 3 Schur params · 1,809 boxes · 905 certified leaves

Reproduce & raw certificate

Reproduce: python3 -m gft.proofs prove starlike inv_a4 "14" --slack 1e-06
Recheck: python3 -m gft.proofs recheck data/proofs/starlike__inv_a4.json

{
 "status": "PROVED",
 "engine": "dag",
 "statement": "max over S*(starlike) of |inv_a4| <= 14 + 1e-06",
 "class": "starlike",
 "functional": "inv_a4",
 "bound": "14",
 "slack": 1e-06,
 "target_sq_hex": "0x1.880003ab862d5p+7",
 "m": 3,
 "vars": [
  "x0",
  "x1",
  "x2",
  "x3",
  "x4",
  "x5",
  "x6"
 ],
 "boxes_processed": 1809,
 "n_leaves": 905,
 "terms": [],
 "evaluator": {
  "type": "factored-dag",
  "definition": "gft/dag.py (classical factored Schur formulas; symbolically verified against the expanded derivation in tests/test_proofs.py)",
  "code_commit": "see matching prove event in data/proofs/audit.jsonl"
 },
 "lemmas": [
  "schur-onto-coefficient-body",
  "rotation-reduction",
  "ieee754-forward-error",
  "bisection-partition"
 ],
 "failure": null,
 "leaves_parts": [
  "data/proofs/starlike__inv_a4.w2.part0.npz",
  "data/proofs/starlike__inv_a4.w3.part0.npz",
  "data/proofs/starlike__inv_a4.w1.part0.npz",
  "data/proofs/starlike__inv_a4.w0.part0.npz",
  "data/proofs/starlike__inv_a4.final.npz"
 ],
 "sharp": {
  "class": "starlike",
  "functional": "inv_a4",
  "bound": "14",
  "slack": 1e-06,
  "bracket_lo": 14.0,
  "bracket_hi": 14.000001,
  "extremal_gammas": [
   1.0,
   0.0,
   0.0
  ],
  "candidate": {
   "value_exact": "14",
   "value_float": 14.0,
   "method": "declared bound"
  },
  "exact": true,
  "proven": false,
  "note": "Candidate exact constant recognised from the certified bracket and matched to the attained extremal value. Not a proof; sharp closure requires the second-variation certificate."
 },
 "discovery": {
  "max_numeric": 14.0,
  "edge_max": 14.0,
  "de_max": 13.99999999999663,
  "edge_values": [
   14.0,
   0.0,
   0.6666666666666666
  ],
  "candidate_bound": "14",
  "recognition": "edge-rational"
 },
 "m3_status": "CERTIFIED_ENCLOSURE_CANDIDATE",
 "m3_note": "The interval certificate proves the displayed upper enclosure and the explicit extremal supplies the lower endpoint. The recognised constant is a candidate, not a sharp theorem; exact closure needs an independent extremal/second-variation argument."
}