cert-machine · spectral geometry · rebuilt from certificates at every build

The hot spot stays on the boundary

The second Neumann eigenfunction of a convex trapezoid with no symmetry axis — to our knowledge the first certified hot-spots domain outside every analytically proven class — 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.

the domain
A B C D
(0,0) · (1,0) · (17/20, 9/10) · (1/4, 9/10) — exact rationals; convex, side slopes 6 and 18/5, no symmetry axis, not a lip domain
μ₁ enclosure
1.42e-3
μ₁ ∈ [12.020976137, 12.022398349], simple (certified spectral gap: μ₂ ≥ 13.9559)
the partition
6,962 cells
core 4690 + collar 2272 on the 1/100 grid, classes decided in exact rationals; four corner sectors close the rest — zero surviving cells
trust base
2 inputs
two quoted lemmas of Liu (arXiv:1808.08148, pinned sha256 fb867aa5ab93…) — named in every record; everything else re-derives here

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 (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 two minutes.

the zone map

Every interior point is somebody's problem

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.

A (0, 0) B (1, 0) C (17/20, 9/10) D (1/4, 9/10) w₊ · φ̂ ≥ 2.1260 w₊ · φ̂ ≥ 2.1260 w₋′ · −φ̂ ≥ 1.9938 w₋′ · −φ̂ ≥ 1.9938 boundary max (at A) boundary min → CORE — 4690 cells, depth ≥ 3/40 everywhere (killed by witness vs sup + solid-mean bound) COLLAR — 2272 cells (killed with reflected boundary bounds) CORNER SECTORS r ≤ 0.11 — the four tip lemmas
Core cells die by comparison against the interior witnesses (diamonds): certified sup + solid-mean error stays below the witness value on both sides (margins 3.93e-2 max side, 5.61e-4 min side). Collar cells die the same way with REFLECTED error bounds across their nearest open edge. The hatched sectors are where the corner expansions take over. Zero cells survive anywhere.
the certificate chain

Six stages, two cross-checks, one record each

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.

stagewhat it certifiesthe numberrecord
1 · spectrumtwo-sided localization; μ₁ SIMPLE by the certified gapμ₁ ∈ [11.892662, 12.041820], μ₂ ≥ 13.955936certs/ember-spectrum.json
2 · defectthe frozen Helmholtz trial's boundary flux, by interval Taylor jets‖∂νu‖ ≤ 1.24e-5certs/ember-defect.json
3 · eigenpairμ₁ tightened 105×; the eigenfunction enclosureμ₁ ∈ [12.020976137, 12.022398349] · ‖u − c₁φ₁‖ ≤ 6.54e-5certs/ember-eigenpair.json
4 · pointwisesolid-mean lemma (I₀ = 5/48 exact); witnesses; every core cell killedφ̂(w₊) ≥ 2.126029 · −φ̂(w₋′) ≥ 1.993811certs/ember-pointwise.json
5 · collarevery collar cell killed with reflected boundary bounds2272 cells, 0 survivorscerts/ember-collar.json
6 · cornersthe four tip sectors, by certified corner expansionsb-coefficients enclosed at TWO annuli; all four tips closedcerts/ember-corner.json
crossindependent re-derivations: I₀ rational, C_tr on bigfloat, μ₁ upper on a P1 basisC_tr ∈ [2.6426189450, 2.6426189450] · P1 upper 12.0642certs/ember-cross.json
theoremchain consistency + the partition re-decided in rationals + assembly19 checks, all greencerts/ember-theorem.json
the corner sectors

The tips, and the ladder identity

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.

cornerb₀b₁b₂value range on the tipthe argument
A[2.109, 2.194][2.682, 2.988][-2.974, 12.761][2.015, 2.194]max: ∂rφ̂ < 0 (worst -4.99e-2) · 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 boundary minimum lives, 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:

∂t²[J_ν(kr)cos(νθ)] = (k²/4)[ J_{ν+2}cos((ν+2)θ) + J_{ν−2}cos((ν−2)θ) − 2 J_ν cos(νθ) ]

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.04 on the whole wedge, down to 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 corollary, and its open twin

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.

the method

Rules the instruments enforce

reproduce

Reproduce

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 + 8 red controls
node instruments/ivspecial/battery.js    # the Γ/Bessel layer: 69 checks, 5 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.