Not one domain but a CONTINUUM of them: for every c in [0.845, 0.85] the convex trapezoid A(0,0) B(1,0) C(c,9/10) D(1/4,9/10) — no symmetry axis, outside every analytically proven class — has a simple second Neumann eigenvalue whose eigenfunction attains its extrema on the boundary only. To our knowledge the first certified hot-spots result for a positive-measure FAMILY rather than a single specimen. The domain below, c = 17/20, is the right endpoint and is where the program started. The domain treated in full below is that endpoint: a convex trapezoid with no symmetry axis, whose second Neumann eigenfunction attains its maximum and its minimum on the boundary only. And more precisely: the maximum is attained AT VERTEX A, and only there — certified, with φ̂(A) ∈ [2.126029, 2.193158]. One domain, one theorem, one corollary: μ₁ is simple, its enclosure is [12.020976137, 12.022398349], and every interior point is excluded by a certified cell of an exact partition. Floats propose; interval and rational arithmetic decide.
Every number on this page is decided by interval or exact rational arithmetic unless it is marked, and every printed bound is rounded outward. Underlined dashed: nothing decided it — where the float steering saw the boundary minimum, a float angle, a wall-clock time. The theorem holds given two lemmas of Liu, cited and pinned; what it rests on, and how far each premise was checked, is listed under the certificate chain.
Machine-derived; published from this repository; not peer-reviewed; not independently rerun. The claim is fenced: Judge–Mondal proved all triangles (Annals 2020, after partial acute-triangle results, Siudeja arXiv:1308.3005), lip domains are Atar–Burdzy, certain non-convex L-tiled polygons are Hatcher (arXiv:2405.19508), and symmetric quadrangle subcases are Deng–Gui–Jiang–Yang–Yao–Zou (arXiv:2604.19003) — this domain sits outside each class. In the other direction, in sufficiently high dimension the conjecture is FALSE for convex sets (de Dios Pont, arXiv:2412.06344), so the planar convex case is exactly where it remains expected — and where this domain lives. A validated-numerics route to acute triangles was developed in the Polymath7 project before the analytic triangle proof; it is lineage here, not a fence. The claim is ONE domain, never the quadrilateral conjecture. Race watch: arXiv, weekly. Every number on this page comes from a VERIFIED record in certs/ember-*.json; the chain re-runs in about 2 minutes (its records' own timings).
The interior is partitioned on the 1/100 grid, and the classes are decided in EXACT RATIONALS — depth is concave on a convex domain, so a cell's minimum depth sits at a corner and the core test is exact; a cell goes to a corner sector only when it lies ENTIRELY inside that vertex's 0.11-disk (the max-corner test is exact because distance is convex); domain membership is a separating-axis decision. The theorem record re-decides the whole partition at assembly time, and this figure is drawn from those same decisions — not from an artist's sketch.
Every stage reads its inputs from the upstream record — no constant travels by hand — and each is a falsifiable claim: the batteries mutate a vertex, forge the kernel norm, flip the ladder identity's sign, inflate the flux, and the chain must refuse each one. The two literature inputs (Liu's framework theorem and the Crouzeix–Raviart constant 0.1893·h_K) are assumptions, named in every record's trust base, with the source PDF pinned and re-hashed at certify time.
| stage | what it certifies | the number | record |
|---|---|---|---|
| 1 · spectrum | two-sided localization; μ₁ SIMPLE by the certified gap | μ₁ ∈ [11.892662, 12.041820], μ₂ ≥ 13.955936 | certs/ember-spectrum.json |
| 2 · defect | the frozen Helmholtz trial's boundary flux, by interval Taylor jets | ‖∂νu‖ ≤ 1.24 × 10⁻⁵ | certs/ember-defect.json |
| 3 · eigenpair | μ₁ tightened more than 104×; the eigenfunction enclosure | μ₁ ∈ [12.020976137, 12.022398349] · ‖u − c₁φ₁‖ ≤ 6.54 × 10⁻⁵ | certs/ember-eigenpair.json |
| 4 · pointwise | solid-mean lemma (I₀ = 5/48 exact); witnesses; every core cell killed | φ̂(w₊) ≥ 2.126029 · −φ̂(w₋′) ≥ 1.993810 | certs/ember-pointwise.json |
| 5 · collar | every collar cell killed with reflected boundary bounds | 2272 cells, 0 survivors | certs/ember-collar.json |
| 6 · corners | the four tip sectors, by certified corner expansions | b-coefficients enclosed at TWO annuli; all four tips closed | certs/ember-corner.json |
| cross | independent re-derivations: I₀ rational, C_tr on bigfloat, μ₁ upper on a P1 basis | C_tr ∈ [2.6426189449, 2.6426189450] · P1 upper 12.0642 | certs/ember-cross.json |
| theorem | chain consistency + the partition re-decided in rationals + assembly | 23 checks, all green | certs/ember-theorem.json |
What the theorem rests on, as every record's trust base names it, in the order the chain uses it:
Every stage is interval or exact rational arithmetic over these premises, and the record walk and live re-proofs of instruments/hotspots/battery.js ran at this build; the weakest premise is assumed: two cited lemmas and the textbook facts, which no machine here checked.
In each corner sector the eigenfunction is EXACTLY a Bessel–Fourier series φ̂ = Σ b_k J_{kν}(√μ₁ r) cos(kνθ) (Neumann separation; H¹ regularity excludes the singular family). The b-coefficients are certified by annulus L² extraction and — the chain's most delicate step — re-extracted at a SECOND annulus: the two enclosures of every coefficient must intersect, and do.
| corner | b₀ | b₁ | b₂ | value range on the tip | the argument |
|---|---|---|---|---|---|
| A | [2.109, 2.194] | [2.682, 2.988] | [-2.974, 12.761] | [2.015, 2.194] | max: ∂rφ̂ < 0 (worst ≤ −4.98 × 10⁻²) · min: value |
| B | [0.831, 0.878] | [-4.596, -4.273] | [0.319, 6.552] | [0.756, 0.897] | value kill, both sides |
| C | [-2.021, -1.978] | [-2.046, -1.893] | [-5.305, -3.679] | [-2.027, -1.846] | max: value · min: |∇φ̂| > 0 on the sector + φ̂_nn ≥ 13.0 on the wedge |
| D | [-1.571, -1.546] | [3.418, 3.634] | [-1.525, -0.364] | [-1.665, -1.351] | value kill, both sides |
At corner C — where the float steering puts the boundary minimum, 0.0195 from the vertex — the wedge along the top edge is closed by normal monotonicity, and the second tangential derivative comes from the Bessel ladder:
The polar-split pieces diverge individually like r^{ν−2} with cancelling signs interval arithmetic cannot see; the ladder form is exact and sign-explicit — and the singular term arrives with b₁ < 0 (certified at both annuli), so it HELPS: φ̂_nn ≥ 13.03 on the wedge from r = 0.12 down to r = 10⁻⁶, and ≥ 11.64 inside r ≤ 10⁻⁶; and the exact second-order Taylor from the Neumann edge (the first-order term vanishes by the boundary condition) forces every interior wedge point strictly above the boundary minimum. J_{ν−2} at ν − 2 ≈ −0.19 is a NEGATIVE-ORDER Bessel evaluation — the reason the instrument layer carries fractional and negative orders with their own falsifier battery.
The hot spot is vertex A — certified. The witness w₊ sits inside A's sector (decided in exact rationals); ∂rφ̂ < 0 on the whole punctured sector means φ̂ strictly decreases along every ray from A, so φ̂(A) > φ̂(w₊) ≥ 2.126029; and every point outside the sector — core, collar, tips B/C/D — is certified strictly below that. At the vertex the expansion collapses to φ̂(A) = b₀(A), so φ̂(A) ∈ [2.126029, 2.193158]. For triangles, extrema-only-at-vertices is Judge–Mondal's refinement; the maximum-side analogue now holds, certified, for this quadrilateral.
The cold spot is an open question of enclosure width. φ̂(C) = b₀(C) ∈ [-2.0204, -1.9789] overlaps the observed boundary minimum (float −1.9998, sitting 0.0195 from C along the top edge). Whether the minimum is at vertex C or strictly inside the edge is undecided; a tighter corner extraction would decide it — and an off-vertex answer would contrast with the triangle behaviour, where extrema occur only at vertices.
| what is certified | value | why it is the load-bearing part |
|---|---|---|
| the interval | c ∈ [0.845, 0.85] | a positive-measure family, not a point — the uniqueness wall is crossed on an interval |
| chunk ladder | 17 chunks, no gap | shared endpoints, re-derived here; a gap of 1e-12 would make the interval claim false |
| σ-cell ladder | 738 cells, no gap | every certified quantity is per-cell, so the cells must tile [−1,0] in each stage too |
| uniform simplicity | μ₁ ≥ 11.85157, μ₂ ≥ 13.90773 | the gap never closes, so μ₁ stays simple for every c and the eigenfunction is well defined |
| thinnest margins | 2.47 × 10⁻⁴ / 6.41 × 10⁻⁴ | max and min side, worst over every cell of every chunk — both strictly positive |
| collar survivors outside the corner windows | 0 | zero, everywhere; the corners are closed by exact local expansions instead |
| tip C genericity | sup b₁ ≤ -0.8790 < 0 | the named condition the specimen proof leaned on, re-checked on all 17 chunks by corner position, not by sign |
| zero-width cells found | 51 | an audit finding, not in the producer's summary: cells the σ-refinement emitted at zero width. They certify an empty set, so they cannot affect the covering — and the covering is complete without them in every chunk and every stage |
An interval theorem is a union of chunk theorems, and the way such a union fails is almost never arithmetic — it is COVERING. Two ladders carry the whole result and neither is visible inside any single certificate: the chunks must tile the interval, and inside each chunk the σ-cells must tile [−1,0] in every stage that reports per-cell numbers. Both are re-derived here from the stage records by instruments/emberband/verify-band.js, which shares no code with the producer, and the battery keeps eight red controls that each break the band in a different realistic way — a removed chunk, an endpoint nudged by 1e-5, one missing σ-cell out of 738, a single margin at −1e-9, one escaped collar survivor, a dropped stage, tip C losing its sign, and a ladder that tiles the wrong interval. All 8 must fire or the page does not build: this build ran it (24 checks, 8/8 red controls fired).
The audit also turned up something the producing summary does not mention: 51 of the σ-cells are zero-width, emitted where the ratio-1.3 refinement toward σ = 0 bottoms out and duplicates a shared endpoint. They certify an empty set, so they cannot bridge a gap or affect the conclusion — and the auditor confirms the remaining cells still tile [−1,0] in every chunk and every stage. It is reported rather than dropped because a certificate covering nothing is worth counting, and because the check that excludes them is also the check that stops one from papering over a real hole.
Scope, stated plainly. The six-stage chain was executed on the bench that produced it, not re-executed here — about 10 hours, on the producer's own figure in the band record. What this page adds is the independent audit: the covering ladders and every band-wide value re-derived from per-cell data by a checker that shares no code with the producer, over records sha-pinned in corpus/emberband. That is the genre of this repository's lower-bound audit, not of its from-scratch theorems. The convex-quadrilateral conjecture itself remains open: this is a family, not the census.
What the band rests on, beyond the premises the specimen names above:
The audit is exact over what the records hold; the weakest premise is assumed: the per-cell arithmetic of a chain this repository did not re-execute.
The whole chain re-runs from this repository, deterministically:
node tools/run-ember-chain.js # all 8 stages, ~2 min, records in certs/ node tools/run-ember-chain.js corner # any single stage node instruments/hotspots/battery.js # record walk, live re-proofs: 32 checks, 8 reds node instruments/ivspecial/battery.js # the Γ/Bessel layer: 75 checks, 6 reds make test # every battery in the machine
Sources: instruments/hotspots/ + instruments/ivspecial/ · literature input pinned at corpus/sources/liu2018_arxiv-1808-08148.pdf with its transcription beside it. Refutations and independent re-runs are invited: carlos@carlostoledo.co.
cert-machine · built 2026-10-30 · git d049222f · every number from a VERIFIED record · Liu pin fb867aa5ab93… · archived: DOI 10.5281/zenodo.22225860