Hardness map: which coefficient-functional bounds are machine-certifiable today

Companion to METHODS.md. Everything below is measured on the v2 factored-DAG prover (plain intervals + affine arithmetic + second-order Taylor form + monotonicity slide + trig-correlated affine form), not estimated from theory. Date: 2026-06-11.

The dimension table

After the exact Schur reduction and the rotation lemma, the search box for an order-m functional has dimension 2m − 1:

1. Where the open set lives (it is NOT the extremal)

For H₃(1) over S* at bound 0.5 + 1e-3 (true sharp value 4/9 ≈ 0.444), the surviving open set after 4M boxes was probed (experiments/probe_h3_openset.py):

• only 0.1% of open boxes are near the extremal configuration (r₀<0.1, r₁<0.1, r₂>0.9) — the attainment circle is not the obstacle;
• 87% of the root volume was still uncertified: the prover (DFS) had over-resolved one region to width 1e-7 while the bulk interior sat with phase dimensions unsplit;
• median upper-bound excess on open boxes: +3.15 against a target of 0.251 — the bound family overestimates >12× on boxes with whole-circle phase ranges.

2. The certify-rate curve (the quantitative wall)

Uniform grid cells at scaled width 1/k per dimension, 3000-cell samples, H₃(1) over S*, target 0.251:

The bound family only becomes tight near scaled width ~1/32. In 7 dimensions that is 32⁷ ≈ 3.4·10¹⁰ cells — two orders of magnitude past any realistic budget, and adaptivity does not rescue it because the bulk (not a thin critical set) is what fails at coarser scales. The dominating term is the gradient·halfwidth part of the Taylor form, which decays only linearly; affine arithmetic (including the trig-correlated form, where cos tₖ and sin tₖ share the angle's noise symbol — implemented, sound, 0/2000 violation tests) does not change the curve measurably, because the looseness is not phase decorrelation but genuine first-order variation over wide boxes.

In 5 dimensions the same crossover costs 32⁵ ≈ 3.4·10⁷ cells — which is why H₂(2) is feasible and H₃(1) is not. Per-split experiments confirm the gradient-contribution bisection hint is per-box optimal (splitting r₀ beats every other dimension on the measured blocker boxes, and beats "widest dim" by 2.5×), so this is not a split-policy problem.

3a. The two-family tie (measured on the Tier-1 slate)

Of 52 sharp Fekete–Szegő targets, 41 certified (39 at slack 1e-6 — including the algebraic constants −1/2 + √2/2 for S_R and √2/2 for the limaçon at s = 1/√2) and 11 failed even at 40M boxes. The split is exactly predicted by a tie test: evaluate |L| at the two competing extremal families — the tail family ω = z² (γ = (0,1)) and the degenerate face γ₀ = 1 (Koebe-type). For every FAILED combo the two values tie (e.g. nephroid μ=1: both give 1/2; starlike μ=½: both give 1); for every PROVED combo there is a strict gap (e.g. bell μ=1: 1/2 vs 0). A tie means the sharp value is attained on the union of a circle and* a positive-dimensional face, and the certifier must push every box near that whole set below (value + ε)² — which the current bound family cannot do at ε ≤ 1e-3. These 10 carry certified attainment (the constant is right) with the upper-bound certificate recorded as open at fine slack.

3. The attainment-line obstruction for sharp m=2,3 bounds

Sharp Fekete–Szegő and H₂(2) values are attained along faces/lines where the quadratic identity w₀ + r₀² ≡ 1 is active. Affine arithmetic tracks linear correlations exactly but pushes the quadratic part to its remainder, leaving an h-stubborn gap (~10⁻²-scale in the worst measured box). Consequence: bounds certify at slack 1e-3 (sometimes 1e-4) rather than 1e-6 on those lines. The certificates record the achieved slack — "sharp value + 1e-3" is the honest current resolution for those entries. Fixes (not yet implemented): order-2 Taylor models, a w-substitution dual chart, or a γ-phase gauge refix.

4. What closing the m=4 gap actually needs

The 2022 human proof of H₃(1) ≤ 4/9 (Kowalczyk–Lecko–Thomas) does not fight the 7-dimensional box: it reduces to ~3–4 real variables through Carathéodory-coefficient parameterization and analytic elimination (Libera–Złotkiewicz representations, phase optimizations done by hand) before any case analysis. The machine analogue — a certified dimension-reduction chart that eliminates the inner phase variables analytically and hands the optimizer a 3–4 dimensional problem — is the precise prerequisite for machine-certifying H₃(1)/Zalcman-class sharp bounds. That is the next research milestone, and it is the difference between ~10¹⁰ boxes and ~10⁵.

Reproduce

python3 experiments/probe_h3_openset.py        # open-set geography
python3 -m gft.proofs prove CLASS FUNCTIONAL BOUND --slack 1e-3 --workers 4

Every claim above regenerates from the repo at the commit recorded in git.