diff --git a/STATUS.md b/STATUS.md index 4083355..60df929 100644 --- a/STATUS.md +++ b/STATUS.md @@ -3,7 +3,7 @@ The live ledger: where every problem stands, what is queued next, and what has already been ruled out. Read this before starting work. -## TL;DR (updated 2026-07-31) +## TL;DR (updated 2026-08-04) **Open for contributions. No automated loop is currently running** — the hourly cycle that produced these records was stopped once its in-flight work closed @@ -17,8 +17,21 @@ hourly routine with that file as the prompt. Everything needed is in this directory. New attempts are welcome as pull requests; see `CONTRIBUTING.md`, and `AGENTS.md` for whether to work blind or informed. -Current standing. HEADLINE: the second 2026-07-31 cycle ran the -two-track billiards plan (old queue 11+12); all four records are +Current standing. HEADLINE (2026-08-04): maxwell-equilibria onboarded +(new problem, E&M round per docs/PLAN-em-problems.md) and its first +attempt closed the marquee target: an explicit rational five-charge +configuration — units at e₁,e₂,e₃, charges 4367/1000000 at +(1/3,1/3,1/3) ± (17/200)(1,1,1) — is CERTIFIED to have exactly 24 +nondegenerate equilibria, > (5−1)² = 16: a concrete machine-checkable +instance of the six-day-old arXiv:2607.27197 refutation of Maxwell's +1873 conjecture, which the asymptotic preprint itself does not supply. +Complete census (472k boxes, all-positive localization, index sum −4), +independently re-verified leaf-by-leaf by the second engine (different +arithmetic + fixed-point theorem), both PASS. Escalation per contract: +skeptic review of the shared subdivision driver queued (new queue 16) +before this counts as settled. Float side-finding: the 24-count window +needs ε ≲ 0.18 and is ~0.5% wide in q. Previous headline (2026-07-31): +the two-track billiards plan (old queue 11+12); all four records are skeptic-confirmed, six corrections total, none load-bearing. Conservative track (005+008): the W(a,b) death law is closed on both sides — the half word composes in closed form to @@ -63,6 +76,7 @@ attempts (queue; run blind). | Triangular billiards | death law CLOSED both sides: parametric necessity all (a,b), death = γ_d exactly for 20 members (005/008); 135° stall dissolved, birth law + exact-135 certificates (006/007) | high | next: parametric sufficiency + birth-law theorem (queue 11); coverage conjecture + sampler blind spot (queue 12) | | Mahler in ℝ⁴ | census done blind (skeptic-confirmed) | medium | next: close k=12–20 (falsifiable: no proper mask with P<11); run the same pipeline on {0,±1}³ for the n=3 spectrum comparison | | Crouzeix | onboarded, no attempts | medium | harness ready, certification risk retired; first attempt is the dim-3 landscape (run blind) | +| Maxwell equilibria | explicit 24-equilibria witness VERIFIED (001, both engines) | high | next: skeptic review of the driver (queue 16, escalation), certified window/fold brackets + exact centroid Hessian (001 leads 2, 5); n=3 census (queue 17) untouched | ## Attempt queue (next cycles pull from the top) @@ -80,6 +94,9 @@ attempts (queue; run blind). 12. [billiards-triangles] **The coverage conjecture, and the sampler blind spot** (from 006/007, 2026-07-31; absorbs the old pinch-gap item — its motivating gap [135.000°, 135.049°] is CLOSED, W(4,3) is certified alive inside it): 006 reduced "every obtuse angle has an alive W member" to an elementary Diophantine statement (unproven; float-checked at 157 + 25 arcs over 90.5°–165°, zero failures). Prove it, using the birth law as a labelled input where needed. Note the certificates so far are POINTWISE (007's C2): window-interval continuity on sub-arcs is float + SPECULATION law only, and per-triangle coverage of a whole arc is a different (open) question — the windows are x-slivers at the corners. Separately falsifiable (007 lead): every sampler in use accumulates only at the 90/j window edges, so an interior-pinch alive window would hide from ALL current designs — build one targeted interior-accumulation test before trusting any negative screen again. 13. [mahler-4d] Close the {0,±1}⁴ universe: k = 12–20 pairs (~30M orbits at k=12, improper fraction already 77% at k=9). Falsifiable: no proper mask with k ≥ 12 has P < 11. Needs the improper-detection shortcut or a streaming canonicalizer; see 001 lead 1. Cheap side quest, same pipeline: the {0,±1}³ census for the n=3 spectrum comparison (13 pairs, trivial) — does the non-Hanner gap grow or shrink with n? 14. [billiards-triangles] Coverage self-test: re-derive the acute and right-triangle cases as a scoped attempt record. Low value now that the harness self-test covers Fagnano and the orthic geometry and 001 mapped the obtuse side — take it only if something turns up that the certificate machinery cannot express. +15. [maxwell-equilibria] **Run blind.** First attempt: certified counts for structured 3-charge families beyond the harness self-test knowns — collinear with unequal charges (does the count stay 2 or drop?), isoceles families, a coarse (shape × charge-ratio) sweep. Deliverable is the count strata map, `EVIDENCE` scoped by grid and region. Every complete count must pass the index-sum identity; treat a violation as a harness bug, not a finding. +16. [maxwell-equilibria] ~~Explicit certified witness for the arXiv:2607.27197 refutation~~ **DONE in 001** (witness certified, both engines PASS). Replacement item — the escalation the contract demands: **skeptic review of 001**, fresh eyes on the shared subdivision driver (the residual common-mode risk: both engines re-check the same leaf tree, so a driver bug that produced a wrong tree AND self-consistent leaves would slip through). Concrete: re-run the census at different precision/min-width/box offsets (tree changes wholesale; certified count must not), verify the 24 enclosures pairwise disjoint exactly, audit the Krawczyk-verdict and leaf-emission code paths by hand. Cheap add-ons that bracket the structure: certified counts at q = 4360/1000000 (expect 12) and 4400/1000000 (expect 16) — 001 lead 2 — and the exact rational centroid-Hessian fold analysis (001 lead 5). +17. [maxwell-equilibria] Three-positive-charge census hunting the open 4-vs-6 gap: after 15's strata map, target the strata boundaries (where counts jump) with unequal charges. Win condition kept in view by every run: any configuration certified with ≥ 5 isolated equilibria refutes the conjectured max 4 and is a result people have sought since 1873 — it must survive verify_equilibria.py and be reported as requiring escalation. Equal-magnitude configurations are settled (Tsai 2015, max 4) — spend no effort there. ## Verified results @@ -312,6 +329,22 @@ attempts (queue; run blind). was a relabeling. Corrections: length-30 universe is 566 words (not 811); gap certificates are pointwise, not "alive throughout". +- **[maxwell-equilibria] Explicit five-charge witness: exactly 24 + nondegenerate equilibria, certified (both engines)** (2026-08-04, + attempt 001): unit charges at e₁, e₂, e₃ plus charges 4367/1000000 at + (1/3,1/3,1/3) ± (17/200)(1,1,1) — a rational embedding of the + arXiv:2607.27197 family at ε ≈ 0.18, charge within 2·10⁻⁸ of their law — + has exactly 24 isolated equilibria, all nondegenerate with certified + index signs (10/−14, sum −4 = 1−n as Poincaré–Hopf demands). Complete + census: 472k boxes tile the localization ball, zero unresolved leaves, + enclosure widths 5·10⁻⁷–2·10⁻⁴; independently re-verified leaf-by-leaf + (different arithmetic, interval Newton vs Krawczyk), PASS in 924 s. + 24 > (5−1)² = 16: an explicit, checkable instance of the refutation of + Maxwell's conjecture — the preprint's own result is asymptotic with no + explicit ε. Float `EVIDENCE`, sampled grids: the 24-count window exists + only for ε ≲ 0.18 and spans ~0.5% in q. Escalation open: skeptic review + of the shared driver (queue 16) before this is settled library fact. + ## Insights / cross-problem notes - Infrastructure (2026-07-27): cross-pollination layer added. `mechanisms.json` @@ -441,6 +474,24 @@ attempts (queue; run blind). relabeling. Any law fitted over family members must first quotient by the word-canonicalization symmetry. +- Onboarding (2026-08-04): maxwell-equilibria added per `docs/PLAN-em-problems.md`, + and the Phase-0 literature check changed the framing mid-plan: Maxwell's + general (n−1)² conjecture was refuted by a preprint SIX DAYS before + onboarding (arXiv:2607.27197, ≥ 24 nondegenerate equilibria from 5 charges; + companion 2607.28785 takes 3 positive charges from 12 to 6). The refutation + is perturbative with no explicit certified witness — queue 16 targets + exactly that gap, which our certificate machinery is unusually suited to. + Frame all attempts against the surviving questions (n=3 max 4-vs-6, + explicit witnesses, growth of the max), never against the dead statement. + thomson-sphere (second problem in the plan) deferred to a follow-up + onboarding session. New harness pattern worth reusing: certificate = + subdivision tree with split paths + per-leaf certificates, so the + independent checker can re-establish every leaf AND verify the tiling + combinatorially (prefix-freeness + Kraft equality) — coverage claims stop + being trust-me. Also: decimal's squareRoot ignores context rounding + (always half-even, per spec) — directed sqrt bounds must be established + by hand; caught by the verifier's own validation suite. + ## Dead ends - **[union-closed] Pointwise Plackett odds-ratio control (gap (a) as diff --git a/docs/PLAN-em-problems.md b/docs/PLAN-em-problems.md new file mode 100644 index 0000000..eeb5659 --- /dev/null +++ b/docs/PLAN-em-problems.md @@ -0,0 +1,230 @@ +# Plan: onboard electricity-and-magnetism problems + +Status: **plan only — nothing below is implemented.** Written 2026-08-04 as a +handoff for an onboarding session. Branch: +`claude/electrical-magnetism-exploration-o4nztc`. Companion to +`docs/PLAN-physics-problems.md` (2026-07-28), which onboarded the first three +physics-flavored problems; the same phase structure applies and is not +repeated in full here. + +This file is **not tier 0** (see `tiers.json`): it contains this lab's framing +and route ideas, so it must never be copied into a blind checkout or cited in +`PROBLEM.md` prose. + +## Scoping decision + +The request: open mathematics around electric fields and magnetism, attacked +in the hope of something physics-relevant. Same selection filter as the July +round — the open frontier must be attackable with this lab's methodology: +exact or certified arithmetic in stdlib Python (+ optional C kernels), +census-shaped falsifiable first steps, honest `EVIDENCE` framing. + +**Expectation-setting, stated up front so the ledger stays honest.** None of +these problems will produce "new physics" in the discovery sense; they are +open *mathematics* whose statements are physical. The realistic deliverables +are the usual ones — approach library, dead ends with reasons, `EVIDENCE` +over stated ranges — plus one genuine long-shot upside: several of the +candidates below are refutable by a single certified finite object (a charge +configuration, a point configuration), and a refutation of a 150-year-old +electrostatics conjecture would be a real result with physical content +(trapping geometries, Earnshaw-adjacent structure). That is the honest +version of "physics-impacting": possible, census-shaped, and not the +expected outcome. + +## Recommended: one problem now, one second + +### 1. `maxwell-equilibria` — Maxwell's conjecture on points of equilibrium + +- **Conjecture** (J.C. Maxwell, *Treatise on Electricity and Magnetism*, + 1873, §113 footnote). The electrostatic field of N fixed point charges in + ℝ³ in general position has at most (N−1)² isolated equilibrium points + (zeros of the field). **Open even for N = 3**, where the conjectured + maximum is 4. Best published bound for three charges is 12, via Khovanskii + fewnomial theory (Gabrielov–Novikov–Shapiro, "Mystery of point charges", + Proc. LMS 2007). Sharper still: whether the equilibrium set is always + *finite* is itself open in general. **Verify all of this precisely during + PROBLEM.md drafting** — GNS 2007 is the anchor citation; search for + post-2007 improvements (planar/collinear special cases, two-charge and + symmetric-configuration results) and cite the exact current frontier. +- **Physics lens.** This *is* electrostatics: equilibria of Coulomb fields, + Earnshaw's theorem (every such equilibrium is a saddle — no stable trap), + Morse theory of the potential. Ion-trap adjacent. Fills the E&M gap in the + lab's physics coverage with the most literal candidate available. +- **Key structure.** Equilibria are critical points of V(x) = Σ qᵢ/|x−xᵢ|. + The system is not polynomial, but adjoining rᵢ = |x−xᵢ| as variables with + rᵢ² = |x−xᵢ|², rᵢ > 0 makes it semi-algebraic — so exact-arithmetic and + certified-enclosure machinery applies. For rational configurations + everything lives over ℚ. A complete certified count over a bounded region + is the shape of the work: enclose each equilibrium (interval Newton / + Krawczyk), certify the rest of the region equilibrium-free (exclusion + boxes), and derive per-configuration a-priori bounds that confine all + equilibria to a computable ball (for all-positive charges they lie in the + convex hull of the charges; the mixed-sign bound needs its own small lemma + — a harness design item, not an afterthought). The affine-forms lesson + from the billiards harness (STATUS insights, 2026-07-28) applies verbatim: + iterated/recombined interval geometry must start from first-order forms. +- **Harness** (`harness/maxwell-equilibria/`): + - *equilibria.py* — reference implementation. Input: rational charges and + positions. Output: a certified equilibrium count — disjoint isolating + boxes each certified to contain exactly one nondegenerate zero, plus a + covering family of exclusion boxes for the remainder of the a-priori + ball, plus the certified a-priori ball derivation itself. Stdlib only. + - *verify_equilibria.py* — independent checker by a *different* method: + re-certify isolating boxes via topological degree (sign analysis on box + faces) rather than Krawczyk, and re-derive the count for coplanar + configurations by an independent reduction. No shared code with + equilibria.py beyond `fractions.Fraction`. + - Verification contract for PROBLEM.md: a count claim states the + configuration exactly (rational data), the a-priori ball and its proof, + the isolation and exclusion certificates, and the arithmetic used. + Floating point locates candidates; it never certifies. Degenerate + (non-isolated or near-degenerate) configurations are reported as + UNRESOLVED at stated tolerance, never silently skipped. +- **First attempts (queue lines):** + 1. Self-test: three collinear charges (the classical, fully analyzable + case) and symmetric triangle configurations — reproduce known counts + with certificates end to end. Expected `VERIFIED`, scope = those + families. Run blind by design (nearly free before prior art exists). + 2. Census: 3-charge configurations, quotiented by similarity (2 shape + parameters + 2 charge ratios, rational grid). Distribution of + certified equilibrium counts; map the strata where the count changes. + **Win condition, kept in view by every run: any configuration + certified with ≥ 5 isolated equilibria refutes Maxwell's N=3 count + outright.** `EVIDENCE` scoped by grid and tolerance. + 3. Later: N = 4 (conjectured max 9), guided by whatever the N=3 strata + map shows about where counts jump. + - Kill conditions to record at queue time: (i) if certified counting near + the degenerate strata (where equilibria merge) forces resolution costs + that grow without bound, the full-census route dies — record the + reachable margin instead; (ii) if the mixed-sign a-priori ball lemma + resists elementary proof, scope the census to all-positive charges and + say so. +- **Budget: high.** Best physics-lens fit, decidable-over-ℚ certificates, + century-old open statement with a one-object refutation path. + +### 2. `thomson-sphere` — minimal Coulomb energy on the sphere + +- **Conjecture / problem** (J.J. Thomson, 1904). N unit charges on S² + minimizing Coulomb energy Σ 1/|xᵢ−xⱼ|. Global minimizers are **proven** + only for N = 2, 3, 4, 6, 12 (linear-programming / universal-optimality + methods) and N = 5 (R. Schwartz 2013, computer-assisted interval + arithmetic). **N = 7 is open** — conjectured minimizer the pentagonal + bipyramid. Related but distinct: Smale's 7th problem (logarithmic energy, + algorithmic formulation) — keep the two separated in PROBLEM.md. **Verify + the exact proven-N list and the N=7 status during drafting** (the N=5 + proof is the methodological anchor: it shows a stdlib-style + interval-arithmetic optimality proof is a real, if heavy, object). +- **Physics lens.** Electron shells on a sphere; realized physically in + multi-electron bubbles in liquid helium and (as a family of energies) + colloidosomes/capsid structure. Electrostatics of confined charge. +- **Key structure.** Finite-dimensional certified global optimization. + Energies are algebraic; comparisons between configurations reduce to + certified enclosures. Symmetry reduction cuts the domain; the honest + deliverable is a *landscape census*: all local minima for N = 7 (and + neighbors) under a stated search design, certified energy enclosures, and + the gap between the best two — `EVIDENCE` about the design, plus the + building blocks a Schwartz-style N=7 proof would need. +- **Harness sketch** (`harness/thomson-sphere/`): *energy.py* (certified + energy enclosures for exact/near-exact configurations; certified local + minimality via interval Hessian) and *verify_energy.py* (independent + re-computation, different parametrization). Contract: every reported + energy is an interval; "global minimum" is never claimed, only "least + found under design D" plus certified local minimality. +- **First attempts:** self-test on N ≤ 6, 12 knowns; then the N=7 landscape + census. Kill condition: if enclosure widths near the putative minimizer + cannot be driven below the energy gap to the second-best basin at + affordable cost, the certification route dies at N=7 — measure and record + the cost curve first, as with Crouzeix. +- **Budget: medium.** Heavier certification load than maxwell-equilibria; + the full-optimality moonshot is real but expensive. + +## Watch list (needs Phase-0 literature verification before any commitment) + +- **Sendov's conjecture / Smale's mean value conjecture.** Both are exactly + 2D electrostatics of unit charges (critical points of the logarithmic + potential of polynomial roots). By far the best exact-arithmetic fit on + this page — pure polynomial algebra, censuses over rational-coefficient + families are trivial to make exact. Sendov: proved for degree ≤ 8 and for + sufficiently large degree (Tao 2020); open in between. Smale MVC: factor 4 + known since 1981, conjectured (n−1)/n. Reason not recommended now: the + physics lens is the thinnest here (the electrostatic reading is an + interpretation, not the subject), and the request was E&M. If a later + round wants a near-guaranteed-tooling win, start here. +- **Almost Mathieu / Hofstadter spectral questions ("dry ten martini", + critical coupling).** The one candidate whose physics is genuinely + *magnetic* (Bloch electrons in a magnetic field). Transfer-matrix spectra + admit certified enclosures in stdlib. But the open/solved boundary has + moved fast (Ten Martini: Avila–Jitomirskaya 2009; dry-version and + critical-case claims in 2023–2025 preprints) and this plan's author could + not pin the current frontier from memory with tier-0-grade confidence. + Do not onboard without a careful literature pass; if the dry problem + stands in a census-able form, it becomes a strong third problem. + +## Candidates that lost (recorded so the next sweep doesn't re-tread) + +- **Yang–Mills mass gap.** No finite falsifiable step exists at any budget; + nothing census-shaped to do. Out. +- **Pólya–Szegő plate-capacity conjecture** (the disk minimizes capacity + among convex plates of given area, 1951 — open). Certified capacity needs + certified PDE/integral-equation numerics in stdlib Python; loses for + exactly the reason hot-spots lost in the July round. +- **Magnetic relaxation / helicity energy bounds (Arnold; Freedman–He + asymptotic crossing number).** Frontier is geometric analysis; anything + we could compute reproduces knowns. Out. +- **Anisotropic Calderón problem (EIT uniqueness).** Purely analytic + frontier; no computational census touches it. Out. +- **2D crystallization / Abrikosov lattice / universal optimality in d=2** + (triangular lattice as Coulomb-gas minimizer; open — solved in d = 8, 24 + by Fourier-interpolation machinery). The missing piece is sharp analytic + machinery, not evidence; a census would reproduce what everyone already + believes. Out, with regret — it is the best "magnetism" story of the + losers (superconductor vortex lattices). + +## Implementation phases + +Same as `docs/PLAN-physics-problems.md` phases 0–4, with these deltas: + +- **Phase 0 (literature check, no repo changes).** The load-bearing items: + exact statement and best bounds for Maxwell's conjecture (GNS 2007 + + successors; the finiteness question's status); the proven-N list and N=7 + status for Thomson; the two watch-list frontiers if pursued. Nothing + enters PROBLEM.md that is not literature. +- **Phase 1–2 (scaffolding + harness).** Slugs `maxwell-equilibria` (now) + and `thomson-sphere` (second, or deferred if the first round's harness + work uncovers shared certified-optimization infrastructure worth + extracting into `harness/common/` first — decide there, record the + decision). Existing tiers.json globs cover new slugs automatically. +- **Phase 3 (registry + ledger).** No new field lens needed: `analysis` + (potential theory), `geometry-topology`, and `computation` cover both + problems; mechanism tags arrive with attempts, not preemptively. STATUS + rows: maxwell-equilibria budget high, thomson-sphere medium. Queue + entries as listed above, kill conditions inline, appended — never + renumber the existing queue. +- **Phase 4.** `python -m pytest tests/ -q`, `scripts/blind.sh` smoke test + per new slug, push. + +## Execution addendum (2026-08-04, same branch) + +Phases 0–4 for `maxwell-equilibria` were executed the day after this plan +was written, and Phase 0 materially changed the framing: **the general +Maxwell conjecture was refuted between planning and execution** — +arXiv:2607.27197 (July 29, 2026) constructs five charges with ≥ 24 +nondegenerate equilibria (> 16), and arXiv:2607.28785 sharpens the +three-positive-charge bound to 6 unconditionally. The problem was onboarded +*reframed* around the surviving open questions (n = 3 max between 4 and 6; +explicit certified witness for the refutation, which is asymptotic-only; +growth of the max; finiteness) rather than the dead statement. See +PROBLEM.md and STATUS queue items 15–17. + +Decision recorded per the Phase 1–2 delta above: `thomson-sphere` is +**deferred** to a follow-up onboarding session — the maxwell harness came +out problem-specific (its certificates lean on the charge-field structure), +so no shared certified-optimization infrastructure fell out to extract, and +the refutation shifted the value toward starting maxwell attempts sooner. + +## Non-goals for the onboarding session + +Identical to the July plan: onboarding only — no attempt records, no census +runs, no edits to existing problems or attempt records, no lab findings in +tier-0 files. First attempts run **blind by design** via +`scripts/new_attempt.py` in separate sessions. diff --git a/harness/maxwell-equilibria/equilibria.py b/harness/maxwell-equilibria/equilibria.py new file mode 100644 index 0000000..7c407f7 --- /dev/null +++ b/harness/maxwell-equilibria/equilibria.py @@ -0,0 +1,738 @@ +#!/usr/bin/env python3 +"""Certified equilibrium counting for point-charge fields (reference tool). + +Setting. Distinct points x_1..x_n in R^3 carry nonzero rational charges +q_1..q_n. The field of interest is + + F(x) = sum_i q_i * (x - x_i) / |x - x_i|^3 (= E, minus grad of + V(x) = sum q_i/|x-x_i|) + +and an equilibrium is a zero of F away from the charges. This tool takes a +configuration with rational data and produces a *certificate* for the number +of equilibria in a search region: a binary-subdivision tree of the region in +which every leaf is one of + + excluded-sign interval evaluation of F over the (closed) leaf box + proves some component is bounded away from 0; + excluded-newton the Krawczyk image K(B) is disjoint from B, so B + contains no zero (any zero lies in K(B), by the + mean-value form); + excluded-ball the leaf lies inside a punctured ball around charge i + on which the domination lemma below proves F != 0; + excluded-outside the leaf lies outside the localization sphere of the + all-positive lemma below; + isolated the Krawczyk operator proves the leaf contains exactly + one zero of F, in its interior; + unresolved nothing above succeeded at the minimum width (reported, + never dropped: the count is then a lower bound). + +Leaves are interior-disjoint by construction, so if no leaf is unresolved the +number of equilibria in the region is exactly the number of isolated leaves. + +Arithmetic. Outward-rounded interval arithmetic with dyadic rational +endpoints (fractions.Fraction; products/quotients/roots are rounded outward +to a fixed 2^-PREC_BITS grid, sums and differences are exact). Square roots +use integer isqrt enclosures: for f = p/q >= 0 and S = 2^PREC_BITS, with +s = isqrt(p*q*S^2), (s/(qS))^2 <= f <= ((s+1)/(qS))^2. Squaring is its own +operation so that squares of intervals straddling 0 stay nonnegative. + +Krawczyk certificate (standard; see A. Neumaier, "Interval Methods for +Systems of Equations", CUP 1990, section 5.2, or R. Moore, R. Kearfott, +M. Cloud, "Introduction to Interval Analysis", SIAM 2009, chapter 8). For a +box B with midpoint m, an arbitrary rational matrix Y, interval Jacobian +enclosure J(B) and interval evaluation F(m): + + K(B) = m - Y*F(m) + (I - Y*J(B)) * (B - m). + +If K(B) is contained in the interior of B, then F has exactly one zero in B +(existence by Brouwer via the mean-value extension, uniqueness because the +contraction forces every matrix in J(B) to be nonsingular). If K(B) and B +are disjoint, F has no zero in B. Y is a floating-point approximate inverse +of the midpoint Jacobian, rationalized; the *certificate* does not depend on +Y being accurate, only the success rate does. + +Localization lemma (all charges positive). If q_i > 0 for all i then every +equilibrium satisfies |x| < R_0 := max_i |x_i|: for |x| >= R_0 and x not a +charge point, + + x . F(x) = sum_i q_i * x.(x - x_i) / |x - x_i|^3 > 0, + +because x.(x - x_i) >= |x| (|x| - |x_i|) >= 0 with equality in every term +simultaneously only if x equals every x_i. So a complete census may take +the search region to be any box containing the closed ball of radius R_0. +(Mixed-sign configurations get no automatic region; the caller must supply +one, and completeness claims are then scoped to it.) + +Domination lemma (any signs). Let d_ij = |x_i - x_j| and pick rho_i with +0 < rho_i < min_j d_ij such that + + |q_i| / rho_i^2 > sum_{j != i} |q_j| / (d_ij - rho_i)^2. + +Then F has no zero x with 0 < |x - x_i| <= rho_i: writing r = |x - x_i|, +the i-th term of F has magnitude |q_i|/r^2 >= |q_i|/rho_i^2 while the others +sum to at most the right-hand side (|x - x_j| >= d_ij - rho_i). The tool +finds such rho_i by halving from min_j d_ij / 2, instantiating the +inequality in exact rational arithmetic (with certified lower bounds for +d_ij). Without this lemma, subdivision near a charge would never terminate: +interval evaluations blow up as the singularity is approached. + +Index-sum identity (all charges positive; classical Poincare-Hopf/degree +argument). On a large sphere F points radially outward (localization lemma +computation), so its degree is +1; around each positive charge F is locally +q_i*(x-x_i)/r^3, degree +1. Hence if all equilibria are nondegenerate, + + sum over equilibria of sign det DF = 1 - n. + +A complete census with certified index signs must satisfy this; the tool +checks it and records the outcome. A violation means a missed zero or a +wrong sign somewhere -- treat it as an error in the run, never as a finding. + +Face-alignment note. Certified zeros that lie exactly on a subdivision face +can never acquire an isolation certificate (they are interior to no leaf). +Symmetric configurations have zeros at symmetric points, and grids love to +put faces through those points, so the automatic search region is offset by +the non-dyadic rationals (1/97, 1/101, 1/103): every face coordinate is then +offset + dyadic, which no symmetric rational point of small height hits. + +Output. JSON certificate (see --help) with the configuration, lemma +instantiations, full leaf list including split paths (so an independent +checker can rebuild every box exactly and verify the tiling), isolation +boxes, det-signs, and the index-sum check. Written under $MATHLAB_OUT +(default ./out). + +Usage: + equilibria.py --validate run the validation suite + equilibria.py --config FILE.json [--out F] count equilibria of a config + config: {"charges": [{"q": "1", "pos": ["1", "0", "0"]}, ...], + "region": optional [[lo,hi],[lo,hi],[lo,hi]] as strings} +Options: --min-width-bits K (default 30), --prec-bits P (default 128), + --max-boxes N (default 400000). + +Standard library only. +""" + +from __future__ import annotations + +import argparse +import json +import os +import sys +import time +from fractions import Fraction +from math import isqrt + +# --------------------------------------------------------------------------- +# outward-rounded dyadic interval arithmetic +# --------------------------------------------------------------------------- + +PREC_BITS = 128 +_SCALE = 1 << PREC_BITS + + +def set_precision(bits: int) -> None: + global PREC_BITS, _SCALE + PREC_BITS = bits + _SCALE = 1 << bits + + +def _rdn(x: Fraction) -> Fraction: + """Round down to the 2^-PREC_BITS grid.""" + return Fraction((x.numerator * _SCALE) // x.denominator, _SCALE) + + +def _rup(x: Fraction) -> Fraction: + """Round up to the 2^-PREC_BITS grid.""" + return Fraction(-((-x.numerator * _SCALE) // x.denominator), _SCALE) + + +def _sqrt_dn(f: Fraction) -> Fraction: + """Certified lower bound for sqrt(f), f >= 0.""" + if f < 0: + raise ValueError("sqrt of negative") + p, q = f.numerator, f.denominator + s = isqrt(p * q * _SCALE * _SCALE) + return Fraction(s, q * _SCALE) + + +def _sqrt_up(f: Fraction) -> Fraction: + """Certified upper bound for sqrt(f), f >= 0.""" + if f < 0: + raise ValueError("sqrt of negative") + p, q = f.numerator, f.denominator + t = p * q * _SCALE * _SCALE + s = isqrt(t) + if s * s == t: + return Fraction(s, q * _SCALE) + return Fraction(s + 1, q * _SCALE) + + +class IV: + """Closed interval [lo, hi] with Fraction endpoints.""" + + __slots__ = ("lo", "hi") + + def __init__(self, lo: Fraction, hi: Fraction | None = None): + if hi is None: + hi = lo + if lo > hi: + raise ValueError("empty interval") + self.lo = lo + self.hi = hi + + # -- exact operations --------------------------------------------------- + + def __add__(self, o: "IV") -> "IV": + return IV(self.lo + o.lo, self.hi + o.hi) + + def __sub__(self, o: "IV") -> "IV": + return IV(self.lo - o.hi, self.hi - o.lo) + + def __neg__(self) -> "IV": + return IV(-self.hi, -self.lo) + + def sub_point(self, p: Fraction) -> "IV": + return IV(self.lo - p, self.hi - p) + + # -- rounded operations ------------------------------------------------- + + def __mul__(self, o: "IV") -> "IV": + cands = (self.lo * o.lo, self.lo * o.hi, self.hi * o.lo, self.hi * o.hi) + return IV(_rdn(min(cands)), _rup(max(cands))) + + def scale(self, c: Fraction) -> "IV": + if c >= 0: + return IV(_rdn(self.lo * c), _rup(self.hi * c)) + return IV(_rdn(self.hi * c), _rup(self.lo * c)) + + def sq(self) -> "IV": + """Interval square, preserving nonnegativity (never a generic product).""" + a, b = abs(self.lo), abs(self.hi) + hi = _rup(max(a, b) ** 2) + if self.lo <= 0 <= self.hi: + return IV(Fraction(0), hi) + return IV(_rdn(min(a, b) ** 2), hi) + + def div(self, o: "IV") -> "IV": + """self / o, requiring o.lo > 0 (the only case this tool needs).""" + if o.lo <= 0: + raise ZeroDivisionError("divisor interval must be strictly positive") + cands = (self.lo / o.lo, self.lo / o.hi, self.hi / o.lo, self.hi / o.hi) + return IV(_rdn(min(cands)), _rup(max(cands))) + + def sqrt(self) -> "IV": + return IV(_sqrt_dn(self.lo), _sqrt_up(self.hi)) + + # -- predicates & helpers ----------------------------------------------- + + def contains0(self) -> bool: + return self.lo <= 0 <= self.hi + + def mid(self) -> Fraction: + return _rdn((self.lo + self.hi) / 2) + + def width(self) -> Fraction: + return self.hi - self.lo + + def inside_open(self, o: "IV") -> bool: + return o.lo < self.lo and self.hi < o.hi + + def disjoint(self, o: "IV") -> bool: + return self.hi < o.lo or o.hi < self.lo + + +IV0 = IV(Fraction(0)) + + +# --------------------------------------------------------------------------- +# configuration +# --------------------------------------------------------------------------- + +class Config: + """Charges with exact rational data.""" + + def __init__(self, charges: list[tuple[Fraction, tuple[Fraction, Fraction, Fraction]]]): + if len(charges) < 2: + raise ValueError("need at least two charges") + seen = set() + for q, p in charges: + if q == 0: + raise ValueError("zero charge") + if p in seen: + raise ValueError("coincident charges") + seen.add(p) + self.charges = charges + + @property + def n(self) -> int: + return len(self.charges) + + def all_positive(self) -> bool: + return all(q > 0 for q, _ in self.charges) + + @staticmethod + def from_json(obj: dict) -> "Config": + return Config([ + (Fraction(c["q"]), tuple(Fraction(v) for v in c["pos"])) + for c in obj["charges"] + ]) + + def to_json(self) -> dict: + return {"charges": [{"q": str(q), "pos": [str(v) for v in p]} + for q, p in self.charges]} + + +# --------------------------------------------------------------------------- +# interval field and Jacobian +# --------------------------------------------------------------------------- + +def field_iv(cfg: Config, box: tuple[IV, IV, IV]) -> tuple[IV, IV, IV] | None: + """Interval enclosure of F over box, or None if box may contain a charge.""" + out = [IV0, IV0, IV0] + for q, p in cfg.charges: + d = [box[k].sub_point(p[k]) for k in range(3)] + r2 = d[0].sq() + d[1].sq() + d[2].sq() + if r2.lo <= 0: + return None + r = r2.sqrt() + r3 = r * r2 + for k in range(3): + out[k] = out[k] + d[k].scale(q).div(r3) + return tuple(out) + + +def jac_iv(cfg: Config, box: tuple[IV, IV, IV]) -> list[list[IV]] | None: + """Interval enclosure of DF over box (DF_kl = dF_k/dx_l), or None.""" + J = [[IV0, IV0, IV0] for _ in range(3)] + three = Fraction(3) + for q, p in cfg.charges: + d = [box[k].sub_point(p[k]) for k in range(3)] + r2 = d[0].sq() + d[1].sq() + d[2].sq() + if r2.lo <= 0: + return None + r = r2.sqrt() + r3 = r * r2 + r5 = r3 * r2 + inv_r3 = IV(Fraction(1)).div(r3) + for k in range(3): + for l in range(3): + if k == l: + term = inv_r3 - d[k].sq().div(r5).scale(three) + else: + term = -((d[k] * d[l]).div(r5).scale(three)) + J[k][l] = J[k][l] + term.scale(q) + return J + + +def det3_iv(J: list[list[IV]]) -> IV: + a, b, c = J[0] + d, e, f = J[1] + g, h, i = J[2] + return a * (e * i - f * h) - b * (d * i - f * g) + c * (d * h - e * g) + + +# --------------------------------------------------------------------------- +# floating-point helpers (candidate machinery only -- never certifies) +# --------------------------------------------------------------------------- + +def _field_float(cfg: Config, x: tuple[float, float, float]) -> list[float] | None: + out = [0.0, 0.0, 0.0] + for q, p in cfg.charges: + d = [x[k] - float(p[k]) for k in range(3)] + r2 = d[0] * d[0] + d[1] * d[1] + d[2] * d[2] + if r2 <= 0.0: + return None + r3 = r2 ** 1.5 + for k in range(3): + out[k] += float(q) * d[k] / r3 + return out + + +def _jac_float(cfg: Config, x: tuple[float, float, float]) -> list[list[float]] | None: + J = [[0.0] * 3 for _ in range(3)] + for q, p in cfg.charges: + d = [x[k] - float(p[k]) for k in range(3)] + r2 = d[0] * d[0] + d[1] * d[1] + d[2] * d[2] + if r2 <= 0.0: + return None + r3 = r2 ** 1.5 + r5 = r3 * r2 + for k in range(3): + for l in range(3): + t = (1.0 / r3 if k == l else 0.0) - 3.0 * d[k] * d[l] / r5 + J[k][l] += float(q) * t + return J + + +def _inv3_float(J: list[list[float]]) -> list[list[Fraction]] | None: + a, b, c = J[0] + d, e, f = J[1] + g, h, i = J[2] + A = e * i - f * h + B = -(d * i - f * g) + C = d * h - e * g + det = a * A + b * B + c * C + if det == 0.0 or abs(det) < 1e-300: + return None + adj = [[A, -(b * i - c * h), b * f - c * e], + [B, a * i - c * g, -(a * f - c * d)], + [C, -(a * h - b * g), a * e - b * d]] + try: + return [[Fraction(adj[r][s] / det) for s in range(3)] for r in range(3)] + except (OverflowError, ValueError): + return None + + +# --------------------------------------------------------------------------- +# Krawczyk certificate +# --------------------------------------------------------------------------- + +def krawczyk(cfg: Config, box: tuple[IV, IV, IV]): + """Return ("unique", K) / ("empty", None) / ("unknown", None) for box.""" + m = tuple(box[k].mid() for k in range(3)) + Fm = field_iv(cfg, tuple(IV(mi) for mi in m)) + if Fm is None: + return ("unknown", None) + J = jac_iv(cfg, box) + if J is None: + return ("unknown", None) + Jf = _jac_float(cfg, tuple(float(mi) for mi in m)) + if Jf is None: + return ("unknown", None) + Y = _inv3_float(Jf) + if Y is None: + return ("unknown", None) + + # K_k = m_k - (Y Fm)_k + sum_l (I - Y J)_kl (box_l - m_l) + K = [] + for k in range(3): + acc = IV(m[k]) - (Fm[0].scale(Y[k][0]) + Fm[1].scale(Y[k][1]) + Fm[2].scale(Y[k][2])) + for l in range(3): + # (I - Y J)_kl as an interval + yj = J[0][l].scale(Y[k][0]) + J[1][l].scale(Y[k][1]) + J[2][l].scale(Y[k][2]) + ent = IV(Fraction(1 if k == l else 0)) - yj + acc = acc + ent * box[l].sub_point(m[l]) + K.append(acc) + K = tuple(K) + + if all(K[k].inside_open(box[k]) for k in range(3)): + return ("unique", K) + if any(K[k].disjoint(box[k]) for k in range(3)): + return ("empty", None) + return ("unknown", None) + + +def det_sign(cfg: Config, box: tuple[IV, IV, IV]) -> int: + """Certified sign of det DF over box: +1, -1, or 0 (= undecided).""" + J = jac_iv(cfg, box) + if J is None: + return 0 + det = det3_iv(J) + if det.lo > 0: + return 1 + if det.hi < 0: + return -1 + return 0 + + +# --------------------------------------------------------------------------- +# lemmas +# --------------------------------------------------------------------------- + +def localization_radius_sq(cfg: Config) -> Fraction: + """R_0^2 for the all-positive localization lemma (exact).""" + if not cfg.all_positive(): + raise ValueError("localization lemma requires all-positive charges") + return max(p[0] ** 2 + p[1] ** 2 + p[2] ** 2 for _, p in cfg.charges) + + +def domination_radii(cfg: Config) -> list[Fraction]: + """Certified rho_i for the domination lemma, exact rational arithmetic.""" + rhos = [] + for i, (qi, pi) in enumerate(cfg.charges): + d_lo = [] # certified lower bounds on distances to the other charges + for j, (qj, pj) in enumerate(cfg.charges): + if j == i: + continue + d2 = sum((pi[k] - pj[k]) ** 2 for k in range(3)) + d_lo.append((abs(qj), _sqrt_dn(d2))) + rho = min(d for _, d in d_lo) / 2 + ok = False + for _ in range(80): + # |q_i|/rho^2 > sum |q_j|/(d_ij - rho)^2, all in Q + if all(d - rho > 0 for _, d in d_lo): + rhs = sum(aq / (d - rho) ** 2 for aq, d in d_lo) + if abs(qi) / rho ** 2 > rhs: + ok = True + break + rho = rho / 2 + if not ok: + raise RuntimeError(f"no domination radius found for charge {i}") + rhos.append(rho) + return rhos + + +def box_inside_ball(box, center, rho_sq: Fraction) -> bool: + """Exact test: is the box contained in the closed ball around center?""" + s = Fraction(0) + for k in range(3): + s += max(abs(box[k].lo - center[k]), abs(box[k].hi - center[k])) ** 2 + return s <= rho_sq + + +def box_min_norm_sq(box) -> Fraction: + s = Fraction(0) + for k in range(3): + if box[k].lo > 0: + s += box[k].lo ** 2 + elif box[k].hi < 0: + s += box[k].hi ** 2 + return s + + +# --------------------------------------------------------------------------- +# the census driver +# --------------------------------------------------------------------------- + +# non-dyadic offsets so subdivision faces avoid symmetric rational points +_OFFSETS = (Fraction(1, 97), Fraction(1, 101), Fraction(1, 103)) + + +def auto_region(cfg: Config) -> tuple[tuple[IV, IV, IV], Fraction]: + """Search box covering the localization ball, offset off symmetric points.""" + r0_sq = localization_radius_sq(cfg) + r_up = _sqrt_up(r0_sq) + half = r_up + Fraction(1, 16) + box = tuple(IV(_OFFSETS[k] - half, _OFFSETS[k] + half) for k in range(3)) + return box, r0_sq + + +def count_equilibria(cfg: Config, region=None, min_width_bits: int = 30, + kraw_start: Fraction = Fraction(1, 2), + max_boxes: int = 400_000, progress_every: int = 0) -> dict: + """Run the certified census; return the certificate as a JSON-able dict.""" + t0 = time.time() + complete = region is None + r0_sq = None + if region is None: + region, r0_sq = auto_region(cfg) + + rhos = domination_radii(cfg) + rho_sqs = [r ** 2 for r in rhos] + min_width = Fraction(1, 1 << min_width_bits) + + leaves = [] # (path, kind, extra) + isolated = [] + unresolved = 0 + excl_counts = {"excluded-sign": 0, "excluded-newton": 0, + "excluded-ball": 0, "excluded-outside": 0} + stack = [(region, "")] + processed = 0 + + while stack: + box, path = stack.pop() + processed += 1 + if progress_every and processed % progress_every == 0: + print(f" ... {processed} boxes, {len(stack)} queued, " + f"{len(isolated)} isolated, {unresolved} unresolved, " + f"{round(time.time() - t0)}s", file=sys.stderr) + if processed > max_boxes: + raise RuntimeError(f"box budget exceeded ({max_boxes}); " + f"raise --max-boxes or shrink the region") + + # 1. outside the localization sphere (complete mode only) + if r0_sq is not None and box_min_norm_sq(box) >= r0_sq: + leaves.append((path, "excluded-outside", None)) + excl_counts["excluded-outside"] += 1 + continue + + # 2. inside a domination ball around a charge + ball = next((i for i, (_, p) in enumerate(cfg.charges) + if box_inside_ball(box, p, rho_sqs[i])), None) + if ball is not None: + leaves.append((path, "excluded-ball", ball)) + excl_counts["excluded-ball"] += 1 + continue + + # 3. sign exclusion by interval evaluation + F = field_iv(cfg, box) + if F is not None and any(not F[k].contains0() for k in range(3)): + leaves.append((path, "excluded-sign", None)) + excl_counts["excluded-sign"] += 1 + continue + + wmax = max(box[k].width() for k in range(3)) + + # 4. Krawczyk isolation + if F is not None and wmax <= kraw_start: + verdict, K = krawczyk(cfg, box) + if verdict == "empty": + leaves.append((path, "excluded-newton", None)) + excl_counts["excluded-newton"] += 1 + continue + if verdict == "unique": + enc = tuple(IV(max(K[k].lo, box[k].lo), min(K[k].hi, box[k].hi)) + for k in range(3)) + s = det_sign(cfg, enc) + if s == 0: + s = det_sign(cfg, box) + leaves.append((path, "isolated", None)) + isolated.append({"path": path, + "box": _box_json(box), + "enclosure": _box_json(enc), + "det_sign": s}) + continue + + # 5. give up or split + if wmax <= min_width: + leaves.append((path, "unresolved", None)) + unresolved += 1 + continue + axis = max(range(3), key=lambda k: box[k].width()) + mid = (box[axis].lo + box[axis].hi) / 2 # exact + for side, part in enumerate((IV(box[axis].lo, mid), IV(mid, box[axis].hi))): + child = tuple(part if k == axis else box[k] for k in range(3)) + stack.append((child, path + f"{axis}{side}")) + + # index-sum check (complete all-positive census, no unresolved leaves) + index_sum = None + index_sum_ok = None + if complete and unresolved == 0: + signs = [it["det_sign"] for it in isolated] + if all(s != 0 for s in signs): + index_sum = sum(signs) + index_sum_ok = (index_sum == 1 - cfg.n) + + return { + "tool": "equilibria.py", + "config": cfg.to_json(), + "prec_bits": PREC_BITS, + "min_width_bits": min_width_bits, + "region": _box_json(region), + "complete": complete, + "localization_r0_sq": str(r0_sq) if r0_sq is not None else None, + "domination_rhos": [str(r) for r in rhos], + "count": len(isolated), + "unresolved": unresolved, + "excluded": excl_counts, + "isolated": isolated, + "leaves": [{"path": p, "kind": k, "ball": b} for p, k, b in leaves], + "index_sum": index_sum, + "index_sum_ok": index_sum_ok, + "boxes_processed": processed, + "seconds": round(time.time() - t0, 3), + } + + +def _box_json(box) -> list[list[str]]: + return [[str(box[k].lo), str(box[k].hi)] for k in range(3)] + + +# --------------------------------------------------------------------------- +# validation suite +# --------------------------------------------------------------------------- + +def _mk(charges) -> Config: + return Config([(Fraction(q), tuple(Fraction(v) for v in p)) for q, p in charges]) + + +def validate() -> int: + failures = 0 + + def check(name, cond): + nonlocal failures + print((" ok " if cond else " FAIL ") + name) + if not cond: + failures += 1 + + print("interval primitives") + x = IV(Fraction(-1, 3), Fraction(1, 5)) + check("sq nonnegative on straddling interval", x.sq().lo == 0 and x.sq().hi >= Fraction(1, 9)) + two = IV(Fraction(2)) + r = two.sqrt() + check("sqrt(2) enclosure", r.lo < r.hi and r.lo ** 2 <= 2 <= r.hi ** 2 + and r.hi - r.lo < Fraction(1, 1 << 100)) + q = IV(Fraction(1)).div(IV(Fraction(3))) + check("1/3 enclosure", q.lo <= Fraction(1, 3) <= q.hi and q.hi - q.lo < Fraction(1, 1 << 100)) + + print("two unit charges at (+-1,0,0): exactly 1 equilibrium, index -1") + cert = count_equilibria(_mk([(1, (1, 0, 0)), (1, (-1, 0, 0))])) + check("count == 1", cert["count"] == 1) + check("no unresolved leaves", cert["unresolved"] == 0) + check("index sum == 1-n", cert["index_sum_ok"] is True) + if cert["count"] == 1: + enc = cert["isolated"][0]["enclosure"] + check("equilibrium at the midpoint (origin)", + all(Fraction(enc[k][0]) <= 0 <= Fraction(enc[k][1]) for k in range(3))) + + print("three collinear unit charges at x = -1, 0, 1: exactly n-1 = 2") + cert = count_equilibria(_mk([(1, (-1, 0, 0)), (1, (0, 0, 0)), (1, (1, 0, 0))])) + check("count == 2", cert["count"] == 2) + check("no unresolved leaves", cert["unresolved"] == 0) + check("index sum == 1-n", cert["index_sum_ok"] is True) + + print("unit charges at an equilateral triangle (e1,e2,e3): exactly 4") + cert = count_equilibria(_mk([(1, (1, 0, 0)), (1, (0, 1, 0)), (1, (0, 0, 1))])) + check("count == 4", cert["count"] == 4) + check("no unresolved leaves", cert["unresolved"] == 0) + check("index sum == 1-n", cert["index_sum_ok"] is True) + if cert["count"] == 4: + c = Fraction(1, 3) + centroid_hits = sum( + 1 for it in cert["isolated"] + if all(Fraction(it["enclosure"][k][0]) <= c <= Fraction(it["enclosure"][k][1]) + for k in range(3))) + check("one equilibrium at the centroid", centroid_hits == 1) + + print("FAILURES:", failures) + return 1 if failures else 0 + + +# --------------------------------------------------------------------------- +# cli +# --------------------------------------------------------------------------- + +def main() -> int: + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("--validate", action="store_true") + ap.add_argument("--config", help="JSON file with charges (and optional region)") + ap.add_argument("--out", help="output path (default $MATHLAB_OUT/maxwell-cert-.json)") + ap.add_argument("--min-width-bits", type=int, default=30) + ap.add_argument("--prec-bits", type=int, default=128) + ap.add_argument("--max-boxes", type=int, default=400_000) + ap.add_argument("--progress-every", type=int, default=0, + help="print a progress line to stderr every N boxes") + args = ap.parse_args() + + set_precision(args.prec_bits) + + if args.validate: + return validate() + if not args.config: + ap.error("need --validate or --config") + + with open(args.config, encoding="utf-8") as fh: + obj = json.load(fh) + cfg = Config.from_json(obj) + region = None + if obj.get("region"): + region = tuple(IV(Fraction(lo), Fraction(hi)) for lo, hi in obj["region"]) + cert = count_equilibria(cfg, region=region, + min_width_bits=args.min_width_bits, + max_boxes=args.max_boxes, + progress_every=args.progress_every) + + out = args.out + if not out: + outdir = os.environ.get("MATHLAB_OUT", "./out") + os.makedirs(outdir, exist_ok=True) + out = os.path.join(outdir, f"maxwell-cert-{int(time.time())}.json") + with open(out, "w", encoding="utf-8") as fh: + json.dump(cert, fh, indent=1) + print(f"count={cert['count']} unresolved={cert['unresolved']} " + f"index_sum={cert['index_sum']} boxes={cert['boxes_processed']} " + f"secs={cert['seconds']} -> {out}") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/harness/maxwell-equilibria/verify_equilibria.py b/harness/maxwell-equilibria/verify_equilibria.py new file mode 100644 index 0000000..008c070 --- /dev/null +++ b/harness/maxwell-equilibria/verify_equilibria.py @@ -0,0 +1,771 @@ +#!/usr/bin/env python3 +"""Independent checker for point-charge equilibrium certificates. + +This tool re-verifies a certificate produced by the reference counting tool +in this directory. It shares no code with it beyond fractions.Fraction, and +deliberately uses different machinery for every layer of the claim: + + arithmetic directed-rounding decimal interval arithmetic (the decimal + module's ROUND_FLOOR / ROUND_CEILING contexts; Decimal + add/mul/div/sqrt are correctly rounded per IBM's decimal + specification), with a precision-doubling retry ladder -- + instead of dyadic rational intervals; + isolation the preconditioned interval Newton operator with interval + Gaussian elimination: N(B) = m - IGA(Y*J(B), Y*F(m)) for a + rational approximate midpoint-Jacobian inverse Y. If the + interval Gauss algorithm succeeds (no pivot straddles 0) + and N(B) lies in the interior of B, then B contains exactly + one zero of F -- existence via the mean-value extension and + Brouwer, uniqueness because IGA success forces every matrix + in Y*J(B), hence in J(B), to be nonsingular; the + certificate is valid for ANY fixed Y, so the float-computed + Y is not part of the trust chain. See A. Neumaier, + "Interval Methods for Systems of Equations", CUP 1990, + chapter 5 -- instead of the Krawczyk operator; + tiling an exact combinatorial check that the leaf boxes partition + the search region: leaf split paths must be prefix-free and + satisfy the Kraft equality sum 2^-depth(leaf) = 1, which + for a binary subdivision tree holds iff the leaves tile the + root; every leaf box is rebuilt exactly (Fraction midpoint + splitting) from its path; + lemmas re-derived, not trusted. Localization (all-positive + charges): an equilibrium x satisfies |x| < R_0 = max|x_i|, + since x.F(x) = sum q_i x.(x-x_i)/|x-x_i|^3 is positive for + |x| >= R_0 (each term is q_i(|x|^2 - x.x_i)/... >= 0, not + all zero). Domination (any signs): if 0 < rho < min_j d_ij + and |q_i|/rho^2 > sum_{j!=i} |q_j|/(d_ij - rho)^2 then no + zero of F has 0 < |x - x_i| <= rho, by the triangle + inequality on the field terms. Both inequalities are + re-instantiated here in exact rational arithmetic with this + tool's own certified square-root bounds (integer isqrt). + +Every leaf of the certificate is re-checked according to its kind, the +count is recomputed, and for complete all-positive censuses the index-sum +identity (sum of certified signs of det DF over the equilibria = 1 - n, a +classical Poincare-Hopf/degree computation) is re-verified with this tool's +own interval determinant. + +Verdict: PASS means every leaf certificate was independently re-established. +FAIL lists every leaf that could not be re-established -- which does not by +itself mean the claim is false, but does mean the certificate cannot be +cited. A certificate that PASSES here at a record-adjacent count is to be +reported as requiring escalation, not accepted (see the problem's +verification contract). + +Usage: + verify_equilibria.py --cert CERT.json re-verify a certificate + verify_equilibria.py --validate run the validation suite + +Standard library only. +""" + +from __future__ import annotations + +import argparse +import json +import sys +import time +from decimal import Context, Decimal, ROUND_CEILING, ROUND_FLOOR +from fractions import Fraction +from math import isqrt + +# --------------------------------------------------------------------------- +# directed-rounding decimal interval arithmetic +# --------------------------------------------------------------------------- + +class DCtx: + """A pair of decimal contexts rounding down / up at a given precision.""" + + def __init__(self, digits: int): + self.digits = digits + self.dn = Context(prec=digits, rounding=ROUND_FLOOR) + self.up = Context(prec=digits, rounding=ROUND_CEILING) + + def from_fraction(self, x: Fraction) -> "DIV": + n = Decimal(x.numerator) + d = Decimal(x.denominator) + return DIV(self.dn.divide(n, d), self.up.divide(n, d), self) + + +class DIV: + """Closed interval with Decimal endpoints and outward rounding.""" + + __slots__ = ("lo", "hi", "ctx") + + def __init__(self, lo: Decimal, hi: Decimal, ctx: DCtx): + if lo > hi: + raise ValueError("empty interval") + self.lo = lo + self.hi = hi + self.ctx = ctx + + def __add__(self, o: "DIV") -> "DIV": + c = self.ctx + return DIV(c.dn.add(self.lo, o.lo), c.up.add(self.hi, o.hi), c) + + def __sub__(self, o: "DIV") -> "DIV": + c = self.ctx + return DIV(c.dn.subtract(self.lo, o.hi), c.up.subtract(self.hi, o.lo), c) + + def __neg__(self) -> "DIV": + return DIV(-self.hi, -self.lo, self.ctx) + + def __mul__(self, o: "DIV") -> "DIV": + c = self.ctx + lo = min(c.dn.multiply(a, b) for a in (self.lo, self.hi) for b in (o.lo, o.hi)) + hi = max(c.up.multiply(a, b) for a in (self.lo, self.hi) for b in (o.lo, o.hi)) + return DIV(lo, hi, c) + + def sq(self) -> "DIV": + c = self.ctx + a, b = abs(self.lo), abs(self.hi) + hi = c.up.multiply(max(a, b), max(a, b)) + if self.lo <= 0 <= self.hi: + return DIV(Decimal(0), hi, c) + m = min(a, b) + return DIV(c.dn.multiply(m, m), hi, c) + + def div(self, o: "DIV") -> "DIV": + if o.lo <= 0: + raise ZeroDivisionError("divisor interval must be strictly positive") + c = self.ctx + lo = min(c.dn.divide(a, b) for a in (self.lo, self.hi) for b in (o.lo, o.hi)) + hi = max(c.up.divide(a, b) for a in (self.lo, self.hi) for b in (o.lo, o.hi)) + return DIV(lo, hi, c) + + def sqrt(self) -> "DIV": + # The decimal spec rounds squareRoot half-even REGARDLESS of the + # context rounding, so directed bounds must be established by hand: + # take the correctly-rounded root and step it by ulps until the + # bound is proved by exact rational comparison of squares. + c = self.ctx + if self.lo < 0: + raise ValueError("sqrt of negative") + lo = c.dn.sqrt(self.lo) + while _dec_to_frac(lo) ** 2 > _dec_to_frac(self.lo): + lo = c.dn.next_minus(lo) + hi = c.up.sqrt(self.hi) + while _dec_to_frac(hi) ** 2 < _dec_to_frac(self.hi): + hi = c.up.next_plus(hi) + return DIV(lo, hi, c) + + def contains0(self) -> bool: + return self.lo <= 0 <= self.hi + + def mig(self) -> Decimal: + """Mignitude: min |y| over the interval (0 if it straddles 0).""" + if self.contains0(): + return Decimal(0) + return min(abs(self.lo), abs(self.hi)) + + def inside_open_frac(self, lo: Fraction, hi: Fraction) -> bool: + """Is this interval strictly inside the rational interval (lo, hi)?""" + return (Fraction(self.lo.as_integer_ratio()[0], self.lo.as_integer_ratio()[1]) > lo + and Fraction(self.hi.as_integer_ratio()[0], self.hi.as_integer_ratio()[1]) < hi) + + +def _zero(ctx: DCtx) -> DIV: + return DIV(Decimal(0), Decimal(0), ctx) + + +def _dec_to_frac(d: Decimal) -> Fraction: + return Fraction(*d.as_integer_ratio()) + + +# --------------------------------------------------------------------------- +# certified rational square-root bounds (for the exact lemma re-derivations) +# --------------------------------------------------------------------------- + +_LEMMA_BITS = 96 + + +def sqrt_lower(f: Fraction) -> Fraction: + """Certified rational lower bound for sqrt(f), f >= 0.""" + p, q = f.numerator, f.denominator + s = 1 << _LEMMA_BITS + r = isqrt(p * q * s * s) + return Fraction(r, q * s) + + +def sqrt_upper(f: Fraction) -> Fraction: + p, q = f.numerator, f.denominator + s = 1 << _LEMMA_BITS + t = p * q * s * s + r = isqrt(t) + if r * r != t: + r += 1 + return Fraction(r, q * s) + + +# --------------------------------------------------------------------------- +# field and Jacobian in decimal intervals (independently written) +# --------------------------------------------------------------------------- + +def d_field(charges, box, ctx: DCtx): + """Enclosure of F over box; box is a triple of DIV. None if r^2 may be 0.""" + acc = [_zero(ctx), _zero(ctx), _zero(ctx)] + for q, pos in charges: + qi = ctx.from_fraction(q) + d = [box[k] - ctx.from_fraction(pos[k]) for k in range(3)] + r2 = d[0].sq() + d[1].sq() + d[2].sq() + if r2.lo <= 0: + return None + r3 = r2.sqrt() * r2 + for k in range(3): + acc[k] = acc[k] + (qi * d[k]).div(r3) + return acc + + +def d_jac(charges, box, ctx: DCtx): + one = DIV(Decimal(1), Decimal(1), ctx) + three = DIV(Decimal(3), Decimal(3), ctx) + J = [[_zero(ctx) for _ in range(3)] for _ in range(3)] + for q, pos in charges: + qi = ctx.from_fraction(q) + d = [box[k] - ctx.from_fraction(pos[k]) for k in range(3)] + r2 = d[0].sq() + d[1].sq() + d[2].sq() + if r2.lo <= 0: + return None + r3 = r2.sqrt() * r2 + r5 = r3 * r2 + for k in range(3): + for l in range(3): + if k == l: + t = one.div(r3) - (three * d[k].sq()).div(r5) + else: + t = -((three * d[k] * d[l]).div(r5)) + J[k][l] = J[k][l] + qi * t + return J + + +def d_det3(J): + a, b, c = J[0] + d, e, f = J[1] + g, h, i = J[2] + return a * (e * i - f * h) - b * (d * i - f * g) + c * (d * h - e * g) + + +# --------------------------------------------------------------------------- +# interval Newton via interval Gaussian elimination +# --------------------------------------------------------------------------- + +def interval_gauss_solve(A, b, ctx: DCtx): + """Enclosure of {x : Mx = r, M in A, r in b} by interval Gaussian + elimination with mignitude pivoting. None if a pivot straddles 0 + (in which case nothing is certified).""" + A = [row[:] for row in A] + b = b[:] + n = 3 + perm = list(range(n)) + for col in range(n): + piv = max(range(col, n), key=lambda r: A[r][col].mig()) + if A[piv][col].mig() == 0: + return None + if piv != col: + A[col], A[piv] = A[piv], A[col] + b[col], b[piv] = b[piv], b[col] + perm[col], perm[piv] = perm[piv], perm[col] + for r in range(col + 1, n): + m = _div_signed(A[r][col], A[col][col]) + for cc in range(col, n): + A[r][cc] = A[r][cc] - m * A[col][cc] + b[r] = b[r] - m * b[col] + x = [None] * n + for r in range(n - 1, -1, -1): + s = b[r] + for cc in range(r + 1, n): + s = s - A[r][cc] * x[cc] + x[r] = _div_signed(s, A[r][r]) + return x + + +def _div_signed(a: DIV, b: DIV) -> DIV: + """a / b for an interval b not containing 0 (either sign).""" + if b.lo > 0: + return a.div(b) + if b.hi < 0: + return (-a).div(-b) + raise ZeroDivisionError("pivot straddles zero") + + +def _float_jac(charges, x): + """Plain floating-point midpoint Jacobian (candidate machinery only).""" + J = [[0.0] * 3 for _ in range(3)] + for q, pos in charges: + d = [float(x[k]) - float(pos[k]) for k in range(3)] + r2 = d[0] * d[0] + d[1] * d[1] + d[2] * d[2] + if r2 <= 0.0: + return None + r3 = r2 ** 1.5 + r5 = r3 * r2 + for k in range(3): + for l in range(3): + t = (1.0 / r3 if k == l else 0.0) - 3.0 * d[k] * d[l] / r5 + J[k][l] += float(q) * t + return J + + +def _float_inv3(J): + a, b, c = J[0] + d, e, f = J[1] + g, h, i = J[2] + A = e * i - f * h + B = -(d * i - f * g) + C = d * h - e * g + det = a * A + b * B + c * C + if det == 0.0 or abs(det) < 1e-300: + return None + adj = [[A, -(b * i - c * h), b * f - c * e], + [B, a * i - c * g, -(a * f - c * d)], + [C, -(a * h - b * g), a * e - b * d]] + return [[adj[r][s] / det for s in range(3)] for r in range(3)] + + +def newton_certify_unique(charges, box_frac, ctx: DCtx): + """Preconditioned interval Newton certificate that box (rational + endpoints) contains exactly one zero of F. Returns True only on full + success. + + Preconditioning is sound: for a fixed rational matrix Y, any zero x* of + F in B satisfies Y*F(m) + (Y*M)(x* - m) = 0 for some M in J(B) (mean + value theorem row by row), so x* lies in m - IGA(Y*J(B), Y*F(m)); and + success of the interval Gauss algorithm on Y*J(B) makes every Y*M -- + hence every M -- nonsingular, which forbids two zeros in B. The + certificate does not depend on the quality of Y, only its success rate + does.""" + N = _newton_image(charges, box_frac, ctx) + if N is None: + return False + for k in range(3): + if not N[k].inside_open_frac(box_frac[k][0], box_frac[k][1]): + return False + return True + + +def newton_certify_empty(charges, box_frac, ctx: DCtx): + """Mean-value exclusion: every zero of F in B lies in N(B); if some + component of N(B) is disjoint from B, then B contains no zero.""" + N = _newton_image(charges, box_frac, ctx) + if N is None: + return False + for k in range(3): + lo, hi = box_frac[k] + if _dec_to_frac(N[k].hi) < lo or _dec_to_frac(N[k].lo) > hi: + return True + return False + + +def krawczyk_certify_empty(charges, box_frac, ctx: DCtx): + """Krawczyk-image exclusion: K(B) = m - Y*F(m) + (I - Y*J(B))(B - m) + contains every zero of F in B (mean-value form, valid for any fixed Y, + with no regularity requirement); if a component of K(B) is disjoint + from B, then B has no zero. This mirrors the reference tool's exclusion + OPERATOR -- it is used here only for emptiness, where the interval + Newton form is structurally weaker (a straddling pivot aborts the + Gaussian elimination, while the Krawczyk image needs no linear solve). + Isolation certificates never use it; independence for emptiness rests + on the different arithmetic and implementation.""" + m = [(lo + hi) / 2 for lo, hi in box_frac] + box = [DIV(ctx.from_fraction(lo).lo, ctx.from_fraction(hi).hi, ctx) + for lo, hi in box_frac] + Fm = d_field(charges, [ctx.from_fraction(mi) for mi in m], ctx) + if Fm is None: + return False + J = d_jac(charges, box, ctx) + if J is None: + return False + Jf = _float_jac(charges, m) + if Jf is None: + return False + Yf = _float_inv3(Jf) + if Yf is None: + return False + Y = [[ctx.from_fraction(Fraction(Yf[r][s])) for s in range(3)] for r in range(3)] + one = DIV(Decimal(1), Decimal(1), ctx) + for k in range(3): + acc = ctx.from_fraction(m[k]) - ( + Y[k][0] * Fm[0] + Y[k][1] * Fm[1] + Y[k][2] * Fm[2]) + for l in range(3): + yj = Y[k][0] * J[0][l] + Y[k][1] * J[1][l] + Y[k][2] * J[2][l] + ent = (one - yj) if k == l else -yj + acc = acc + ent * (box[l] - ctx.from_fraction(m[l])) + lo, hi = box_frac[k] + if _dec_to_frac(acc.hi) < lo or _dec_to_frac(acc.lo) > hi: + return True + return False + + +def _newton_image(charges, box_frac, ctx: DCtx): + """N(B) = m - IGA(Y*J(B), Y*F(m)) as a list of DIV, or None.""" + m = [(lo + hi) / 2 for lo, hi in box_frac] + box = [DIV(ctx.from_fraction(lo).lo, ctx.from_fraction(hi).hi, ctx) + for lo, hi in box_frac] + Fm = d_field(charges, [ctx.from_fraction(mi) for mi in m], ctx) + if Fm is None: + return None + J = d_jac(charges, box, ctx) + if J is None: + return None + Jf = _float_jac(charges, m) + if Jf is None: + return None + Yf = _float_inv3(Jf) + if Yf is None: + return None + Y = [[ctx.from_fraction(Fraction(Yf[r][s])) for s in range(3)] for r in range(3)] + # precondition: YJ = Y * J(B), Yb = Y * F(m), as interval enclosures + YJ = [[Y[r][0] * J[0][s] + Y[r][1] * J[1][s] + Y[r][2] * J[2][s] + for s in range(3)] for r in range(3)] + Yb = [Y[r][0] * Fm[0] + Y[r][1] * Fm[1] + Y[r][2] * Fm[2] for r in range(3)] + try: + delta = interval_gauss_solve(YJ, Yb, ctx) + except ZeroDivisionError: + return None + if delta is None: + return None + return [ctx.from_fraction(m[k]) - delta[k] for k in range(3)] + + +# --------------------------------------------------------------------------- +# certificate re-verification +# --------------------------------------------------------------------------- + +def _parse_box(bx) -> list[tuple[Fraction, Fraction]]: + return [(Fraction(lo), Fraction(hi)) for lo, hi in bx] + + +def _rebuild_box(root, path: str) -> list[tuple[Fraction, Fraction]]: + """Rebuild a leaf box from its split path, mirroring midpoint bisection.""" + box = list(root) + if len(path) % 2: + raise ValueError(f"odd-length path {path!r}") + for i in range(0, len(path), 2): + axis = int(path[i]) + side = int(path[i + 1]) + lo, hi = box[axis] + mid = (lo + hi) / 2 + box[axis] = (lo, mid) if side == 0 else (mid, hi) + return box + + +def _min_norm_sq(box) -> Fraction: + s = Fraction(0) + for lo, hi in box: + if lo > 0: + s += lo ** 2 + elif hi < 0: + s += hi ** 2 + return s + + +def _max_dist_sq(box, center) -> Fraction: + s = Fraction(0) + for (lo, hi), c in zip(box, center): + s += max(abs(lo - c), abs(hi - c)) ** 2 + return s + + +def verify(cert: dict, base_digits: int = 60, max_digits: int = 480, + progress: bool = False) -> dict: + t0 = time.time() + charges = [(Fraction(c["q"]), tuple(Fraction(v) for v in c["pos"])) + for c in cert["config"]["charges"]] + n = len(charges) + all_positive = all(q > 0 for q, _ in charges) + root = _parse_box(cert["region"]) + complete = bool(cert.get("complete")) + failures: list[str] = [] + + # --- lemma re-derivations (exact) ------------------------------------- + r0_sq = None + if complete: + if not all_positive: + failures.append("completeness claimed but charges are not all positive") + else: + r0_sq = max(p[0] ** 2 + p[1] ** 2 + p[2] ** 2 for _, p in charges) + r_up = sqrt_upper(r0_sq) + for k in range(3): + if not (root[k][0] <= -r_up and r_up <= root[k][1]): + failures.append("search region does not contain the localization ball") + break + + rhos = [Fraction(r) for r in cert["domination_rhos"]] + if len(rhos) != n: + failures.append("wrong number of domination radii") + else: + for i, (qi, pi) in enumerate(charges): + rho = rhos[i] + ok = rho > 0 + rhs = Fraction(0) + for j, (qj, pj) in enumerate(charges): + if j == i: + continue + d_lo = sqrt_lower(sum((pi[k] - pj[k]) ** 2 for k in range(3))) + if d_lo - rho <= 0: + ok = False + break + rhs += abs(qj) / (d_lo - rho) ** 2 + if not (ok and abs(qi) / rho ** 2 > rhs): + failures.append(f"domination inequality fails for charge {i}") + + # --- structural: leaves tile the region ------------------------------- + leaves = cert["leaves"] + paths = [lf["path"] for lf in leaves] + if len(set(paths)) != len(paths): + failures.append("duplicate leaf paths") + spaths = sorted(paths) + for a, b in zip(spaths, spaths[1:]): + if b.startswith(a): + failures.append(f"leaf {a!r} is a prefix of leaf {b!r}") + break + kraft = sum(Fraction(1, 1 << (len(p) // 2)) for p in paths) + if kraft != 1: + failures.append(f"Kraft sum is {kraft}, not 1: leaves do not tile the region") + + # --- per-leaf re-verification ----------------------------------------- + iso_by_path = {it["path"]: it for it in cert["isolated"]} + unresolved = 0 + counted = 0 + index_signs = [] + kinds = {"excluded-sign": 0, "excluded-newton": 0, "excluded-ball": 0, + "excluded-outside": 0, "isolated": 0, "unresolved": 0} + + for idx, lf in enumerate(leaves): + if progress and idx % 2000 == 0 and idx: + print(f" ... {idx}/{len(leaves)} leaves", file=sys.stderr) + kind = lf["kind"] + kinds[kind] = kinds.get(kind, 0) + 1 + box = _rebuild_box(root, lf["path"]) + + if kind == "excluded-outside": + if r0_sq is None: + failures.append(f"leaf {lf['path']!r}: outside-exclusion without " + f"a localization lemma in force") + elif _min_norm_sq(box) < r0_sq: + failures.append(f"leaf {lf['path']!r}: outside-exclusion is wrong") + continue + + if kind == "excluded-ball": + i = lf["ball"] + if not (isinstance(i, int) and 0 <= i < n + and _max_dist_sq(box, charges[i][1]) <= rhos[i] ** 2): + failures.append(f"leaf {lf['path']!r}: ball-exclusion is wrong") + continue + + if kind == "excluded-sign": + digits = base_digits + ok = False + while digits <= max_digits: + ctx = DCtx(digits) + dbox = [DIV(ctx.from_fraction(lo).lo, ctx.from_fraction(hi).hi, ctx) + for lo, hi in box] + F = d_field(charges, dbox, ctx) + if F is not None and any(not F[k].contains0() for k in range(3)): + ok = True + break + digits *= 2 + if not ok: + failures.append(f"leaf {lf['path']!r}: sign-exclusion not reproduced") + continue + + if kind == "excluded-newton": + digits = base_digits + ok = False + while digits <= max_digits: + ctx = DCtx(digits) + dbox = [DIV(ctx.from_fraction(lo).lo, ctx.from_fraction(hi).hi, ctx) + for lo, hi in box] + F = d_field(charges, dbox, ctx) + if F is not None and any(not F[k].contains0() for k in range(3)): + ok = True # sign exclusion is an acceptable re-derivation too + break + if newton_certify_empty(charges, box, DCtx(digits)): + ok = True + break + if krawczyk_certify_empty(charges, box, DCtx(digits)): + ok = True + break + digits *= 2 + if not ok: + failures.append(f"leaf {lf['path']!r}: emptiness not reproduced") + continue + + if kind == "unresolved": + unresolved += 1 + continue + + if kind == "isolated": + it = iso_by_path.get(lf["path"]) + if it is None: + failures.append(f"leaf {lf['path']!r}: isolated leaf missing record") + continue + claimed = _parse_box(it["box"]) + if claimed != box: + failures.append(f"leaf {lf['path']!r}: recorded box mismatches path") + continue + digits = base_digits + ok = False + while digits <= max_digits: + if newton_certify_unique(charges, box, DCtx(digits)): + ok = True + break + digits *= 2 + if not ok: + failures.append(f"leaf {lf['path']!r}: interval Newton could not " + f"re-establish isolation") + continue + counted += 1 + # det sign over the claimed enclosure + s_claim = it.get("det_sign", 0) + enc = _parse_box(it["enclosure"]) + for k in range(3): + if not (box[k][0] <= enc[k][0] and enc[k][1] <= box[k][1]): + failures.append(f"leaf {lf['path']!r}: enclosure not inside box") + s_here = 0 + digits = base_digits + while digits <= max_digits and s_here == 0: + ctx = DCtx(digits) + dbox = [DIV(ctx.from_fraction(lo).lo, ctx.from_fraction(hi).hi, ctx) + for lo, hi in enc] + J = d_jac(charges, dbox, ctx) + if J is not None: + det = d_det3(J) + if det.lo > 0: + s_here = 1 + elif det.hi < 0: + s_here = -1 + digits *= 2 + if s_claim != 0 and s_here != 0 and s_claim != s_here: + failures.append(f"leaf {lf['path']!r}: det sign disagrees") + index_signs.append(s_here) + continue + + failures.append(f"leaf {lf['path']!r}: unknown kind {kind!r}") + + if counted != cert["count"]: + failures.append(f"recount: {counted} isolated leaves re-established, " + f"certificate claims {cert['count']}") + if unresolved != cert["unresolved"]: + failures.append(f"unresolved recount: {unresolved} vs claimed " + f"{cert['unresolved']}") + + index_sum = None + index_sum_ok = None + if complete and all_positive and unresolved == 0 and counted and \ + all(s != 0 for s in index_signs): + index_sum = sum(index_signs) + index_sum_ok = (index_sum == 1 - n) + if not index_sum_ok: + failures.append(f"index-sum identity fails: {index_sum} != {1 - n}") + + return { + "verdict": "PASS" if not failures else "FAIL", + "failures": failures, + "count": counted, + "unresolved": unresolved, + "kinds": kinds, + "index_sum": index_sum, + "index_sum_ok": index_sum_ok, + "seconds": round(time.time() - t0, 3), + } + + +# --------------------------------------------------------------------------- +# validation suite +# --------------------------------------------------------------------------- + +def validate() -> int: + failures = 0 + + def check(name, cond): + nonlocal failures + print((" ok " if cond else " FAIL ") + name) + if not cond: + failures += 1 + + print("decimal interval primitives") + ctx = DCtx(40) + third = ctx.from_fraction(Fraction(1, 3)) + check("1/3 outward", Fraction(str(third.lo)) <= Fraction(1, 3) <= Fraction(str(third.hi)) + and third.lo != third.hi) + two = ctx.from_fraction(Fraction(2)) + r = two.sqrt() + check("sqrt(2) outward", Fraction(str(r.lo)) ** 2 <= 2 <= Fraction(str(r.hi)) ** 2) + x = DIV(Decimal("-1"), Decimal("0.5"), ctx) + check("sq nonnegative on straddling interval", x.sq().lo == 0) + + print("certified rational sqrt bounds") + check("sqrt_lower/upper bracket sqrt(2)", + sqrt_lower(Fraction(2)) ** 2 <= 2 <= sqrt_upper(Fraction(2)) ** 2 + and sqrt_upper(Fraction(2)) - sqrt_lower(Fraction(2)) < Fraction(1, 1 << 90)) + + print("interval Newton core: two unit charges at (+-1,0,0)") + charges = [(Fraction(1), (Fraction(1), Fraction(0), Fraction(0))), + (Fraction(1), (Fraction(-1), Fraction(0), Fraction(0)))] + box = [(Fraction(-1, 40), Fraction(1, 48))] * 3 # off-center box at origin + check("unique zero certified near origin", + newton_certify_unique(charges, box, DCtx(60))) + far = [(Fraction(1, 3), Fraction(1, 2))] * 3 + check("no false certificate away from the zero", + not newton_certify_unique(charges, far, DCtx(60))) + + print("tamper detection on synthetic certificates") + cfg2 = {"charges": [{"q": "1", "pos": ["1", "0", "0"]}, + {"q": "1", "pos": ["-1", "0", "0"]}]} + # (a) a region that truly contains the origin equilibrium, declared + # sign-excluded in one leaf: must be caught. + bad = { + "config": cfg2, + "region": [["-9/64", "1/8"], ["-1/8", "1/8"], ["-1/8", "1/8"]], + "complete": False, + "domination_rhos": ["1/4", "1/4"], + "count": 0, "unresolved": 0, "isolated": [], + "leaves": [{"path": "", "kind": "excluded-sign", "ball": None}], + } + res = verify(bad, max_digits=120) + check("wrong sign-exclusion detected", res["verdict"] == "FAIL" + and any("sign-exclusion" in f for f in res["failures"])) + # (b) a genuinely field-positive region away from zeros and charges: + # the same claim must be accepted. + good = dict(bad) + good["region"] = [["2", "9/4"], ["0", "1/4"], ["0", "1/4"]] + res = verify(good) + check("correct sign-exclusion accepted", res["verdict"] == "PASS") + # (c) a leaf list with a hole: the Kraft check must catch it. + gap = dict(good) + gap["leaves"] = [{"path": "00", "kind": "excluded-sign", "ball": None}] + res = verify(gap) + check("coverage gap detected (Kraft sum)", + any("Kraft" in f for f in res["failures"])) + + print("FAILURES:", failures) + return 1 if failures else 0 + + +# --------------------------------------------------------------------------- +# cli +# --------------------------------------------------------------------------- + +def main() -> int: + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("--cert", help="certificate JSON to re-verify") + ap.add_argument("--validate", action="store_true") + ap.add_argument("--digits", type=int, default=60, + help="starting decimal precision (doubles on retry)") + ap.add_argument("--progress", action="store_true") + args = ap.parse_args() + + if args.validate: + return validate() + if not args.cert: + ap.error("need --cert or --validate") + + with open(args.cert, encoding="utf-8") as fh: + cert = json.load(fh) + res = verify(cert, base_digits=args.digits, progress=args.progress) + print(json.dumps(res, indent=1)) + return 0 if res["verdict"] == "PASS" else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/problems/maxwell-equilibria/PRIOR-ART.md b/problems/maxwell-equilibria/PRIOR-ART.md new file mode 100644 index 0000000..edea1bd --- /dev/null +++ b/problems/maxwell-equilibria/PRIOR-ART.md @@ -0,0 +1,82 @@ +# Maxwell equilibria — prior art from this lab + +> **Tier 1.** Reading this file makes an attempt `informed`. + +Machine-readable index: `prior-art.json`. + +## Attempts + +- **001 — Explicit certified witness for the five-charge Maxwell + counterexample** (2026-08-04, informed, `VERIFIED`). The configuration + with unit charges at e₁,e₂,e₃ and charges 4367/1000000 at + (1/3,1/3,1/3) ± (17/200)(1,1,1) has exactly 24 isolated nondegenerate + equilibria — a complete certified census, re-established leaf-by-leaf by + the independent checker, index sum −4. Since 24 > (5−1)² = 16 this is an + explicit machine-checkable instance of the arXiv:2607.27197 refutation, + at a concrete witness the (asymptotic) preprint does not supply. Float + side-findings: the 24-count window exists only for t ≤ 0.085 + (ε ≲ 0.18) and is about half a percent wide in q. Escalation per the + contract: a skeptic review of the shared subdivision driver is queued + (leads 1–2 of the record) before the ledger treats this as settled. + +## Editorial view of the attack surface + +This problem was onboarded days after the general conjecture was claimed +false (arXiv:2607.27197, July 29 2026), which is exactly why the budget is +high rather than why it should be low. What died is the (n−1)² count at +n = 5; what the refutation *opened* is a set of questions shaped like this +lab's tooling: + +- **The refutation has no explicit witness.** The perturbation argument + holds "for all sufficiently small ε" and certifies no concrete + configuration. Producing a fully rational instance and certifying ≥ 24 + isolated equilibria in exact arithmetic would be the first independent + verification of the counterexample — and would either confirm it or find a + gap in a days-old result. Route note: the equilateral triangle embeds + rationally in ℝ³ as e₁, e₂, e₃ (pairwise distances √2, plane x+y+z = 1, + symmetry axis along (1,1,1)), so the whole five-charge configuration can + be taken with rational coordinates and rational charges — the axial pair + at (1/3, 1/3, 1/3) ± t·(1,1,1) with rational t, and a rational charge + near the scaled (3/4)ε³ law. Everything the harness needs is then in ℚ. + Expect the 21 bifurcated equilibria to be nearly degenerate for small t + (they merge as t → 0): the certification cost grows as t shrinks and the + equilibria may vanish for t large, so the work is finding the Goldilocks + window. Kill condition: if no rational t admits certification at + affordable subdivision depth, record the cost curve and the tightest + bracketing achieved — that is a finding about the window, and `EVIDENCE` + that the asymptotic regime is narrower than the preprint's framing + suggests. +- **n = 3 is open between 4 and 6.** The community's intuition about this + problem was just proven wrong at n = 5; the conjectured max 4 at n = 3 + deserves suspicion too. A census over three positive charges — two shape + parameters and two charge ratios after similarity reduction — hunting for + a configuration with ≥ 5 certified equilibria is self-policing in the + same way the Mahler volume-product search is: a single certified witness + settles a question people have worked on since 1873. The equal-magnitude + case is closed (Tsai 2015, max 4), so weight the census toward unequal + charges; near-degenerate strata (where equilibria merge and the count + jumps) are both where new equilibria appear and where certification is + most expensive. +- **The index-sum identity (Σ indices = 1 − n) is a completeness alarm.** + Any complete census that fails it has missed an equilibrium or + miscounted an index. It is implemented in the harness as a mandatory + self-check; treat a violation as a bug until proven otherwise. + +Concrete lines, if you want them: + +- Self-test first (blind): collinear positive charges (exactly n−1 + equilibria, classical) and unit charges at an equilateral triangle + (exactly 4, Tsai). Purpose is validating the certification machinery + against known answers — a mismatch is a bug in our enclosures, not a + finding. +- Then the explicit five-charge witness (informed; it consumes the + arXiv:2607.27197 construction as a labelled input). +- Then the three-charge census. + +Methodological warning carried over from the rest of the lab: the equilibria +of symmetric configurations sit at symmetric points, and subdivision grids +love to put cell faces through symmetric points. The harness offsets its +root box by non-dyadic rationals so certified zeros never land on cell +faces; keep that property if you modify the search design, or isolation +certificates will fail forever at the symmetric equilibria and the run will +report spurious UNRESOLVED regions. diff --git a/problems/maxwell-equilibria/PROBLEM.md b/problems/maxwell-equilibria/PROBLEM.md new file mode 100644 index 0000000..fdf4b51 --- /dev/null +++ b/problems/maxwell-equilibria/PROBLEM.md @@ -0,0 +1,146 @@ +# Maxwell's problem on points of equilibrium + +> **Tier 0.** Published background only. Nothing below reflects what this lab +> has tried. See `AGENTS.md`. + +**Setting.** Fix n distinct points x₁, …, xₙ ∈ ℝ³ carrying nonzero charges +q₁, …, qₙ. The electrostatic potential is + + V(x) = Σᵢ qᵢ / |x − xᵢ|, + +harmonic away from the charges. A **point of equilibrium** is a critical point +of V — equivalently a zero of the field E = −∇V — away from the charges. By +Earnshaw's theorem (harmonicity), V has no local extrema, so every +nondegenerate equilibrium is a saddle. + +**Maxwell's claim** (*A Treatise on Electricity and Magnetism*, 1873, §113 +and footnote). The number of equilibrium points of n point charges, when they +are finite in number, is at most (n−1)². Maxwell gave a Morse-theoretic +sketch, not a proof. The statement splits into the questions that are actually +studied: + +1. Is the number of equilibria always finite (say, for generic + configurations)? +2. What is the sharp upper bound on the number of isolated (or nondegenerate) + equilibria, as a function of n? +3. What is the sharp bound for small n — in particular n = 3? + +## Published status + +- **Finiteness is open in general.** Gabrielov, Novikov and Shapiro (*Mystery + of point charges*, Proc. London Math. Soc. 95, 2007) — the modern reference + — prove via Khovanskii's fewnomial theory that the number of *isolated* + equilibria admits a bound depending only on n (not on the dimension), but + whether the equilibrium set of a positive-charge configuration in ℝ³ is + always finite remains unproved. Their bound for three charges is 12. +- **Three charges.** Conjectured sharp bound: (3−1)² = 4. For three charges of + **equal magnitude**, the sharp bound 4 is a theorem (Ya-Lun Tsai, + *Maxwell's conjecture on three point charges with equal magnitudes*, + Physica D 309, 2015): the possible counts of isolated equilibria are 0, 2, + 3, 4, and unit charges at the vertices of an equilateral triangle attain + exactly 4 (one central, three edge-adjacent). For three **positive** charges + of arbitrary magnitudes, a July 2026 preprint (arXiv:2607.28785, *From 12 + to 6: sharpening the three-charge bound in Maxwell's problem*) claims an + unconditional improvement of the Gabrielov–Novikov–Shapiro bound from 12 to + 6 nondegenerate equilibria. **Whether 4 is the true maximum for general + three positive charges is open**: the gap is between 4 and 6. +- **The general conjecture is claimed false** (preprint). Arathoon, Ball and + Kvalheim, *The Maxwell Conjecture is False* (arXiv:2607.27197, July 2026), + construct five positive charges whose potential has at least 24 + nondegenerate critical points, exceeding (5−1)² = 16. The configuration: + three unit charges at the vertices of an equilateral triangle, plus two + charges of magnitude q_ε = (3/4)ε³ − (5/32)ε⁵ at height ±ε on the + triangle's symmetry axis. The three edge equilibria of the triangle persist + and the central equilibrium bifurcates into 21 equilibria. The proof is a + rigorous perturbation/bifurcation argument valid "for all sufficiently + small ε > 0"; **no explicit value of ε is certified**, and the supporting + computations are computer-algebra, not certified numerics. As a preprint of + days ago at the time of writing, it has not been peer-reviewed. +- **Lower-bound constructions.** Maxwell's count is attained for small n in + the plane: four point charges in a plane can produce nine equilibrium + points (Physica D / Appl. Math. Letters literature, 2022). Which counts + between the known constructions and the upper bounds are realizable is + open. +- **Restricted geometries are classical.** For n collinear positive charges, + all equilibria lie on the line and there is exactly one in each of the n−1 + open segments between consecutive charges (the on-axis field is strictly + decreasing between consecutive charges and blows up with opposite signs at + the endpoints); the count n−1 is exact and elementary. For coplanar + positive charges all equilibria lie in the plane of the charges (the normal + field component is z·Σqᵢ/rᵢ³, which vanishes only at z = 0). +- **Degree/index identity** (classical, Poincaré–Hopf for the field E = −∇V + on a large ball minus small balls around the charges). If all charges are + positive and all equilibria are nondegenerate, the indices (sign det DE) + of the equilibria sum to 1 − n. This is an unconditional consistency + constraint on any claimed complete census. + +**What is open, concretely.** The sharp maximum for three positive charges +(4, 5, or 6); certified explicit witnesses for the five-charge refutation +(the preprint's construction is asymptotic in ε); the true growth of the +maximum in n now that (n−1)² is claimed dead; finiteness. + +## Verification contract + +Any claim recorded against this problem must meet the bar in +`CONTRIBUTING.md`. The equilibrium equations are not polynomial, but for +rational charge data the system becomes semi-algebraic after adjoining the +distances rᵢ = |x − xᵢ|, so every quantity in a certificate is decidable over +ℚ; the contract exploits that: + +- **A count claim is a certificate, not a number.** It states the + configuration exactly (rational charges and positions), the search region, + and produces: (i) a list of pairwise interior-disjoint **isolating boxes**, + each certified to contain exactly one equilibrium by a stated + fixed-point/interval-Newton criterion evaluated in outward-rounded rational + interval arithmetic; (ii) **exclusion certificates** covering the entire + remainder of the region (sign-definite field component, charge-neighborhood + domination, or an a-priori localization lemma, each with its inequality + instantiated in exact rational arithmetic). +- **A complete count** (a claim about *all* equilibria of a configuration, + not just those in a stated region) additionally requires a proved a-priori + localization: for all-positive charges, no equilibrium lies at radius ≥ + max |xᵢ| from the origin (radial-component lemma); mixed-sign + configurations need their own recorded localization argument before any + completeness language is used. +- **Floating point locates candidates; it never certifies.** Approximate + Newton iterates and float scans may steer the subdivision; every counted + equilibrium and every excluded region must carry a rigorous certificate. +- **Nondegeneracy and index claims** require a certified sign of det DE over + the isolating box. A complete census of an all-positive configuration must + check the index-sum identity (Σ indices = 1 − n) and report the check. +- **Unresolved regions are reported, never dropped.** A run that cannot + certify a subregion (near-degenerate equilibria, insufficient precision) + states the unresolved boxes; its count is then a lower bound plus an + explicit gap, not a count. +- **Record-adjacent counts escalate.** A configuration certified with a + count that contradicts a published bound, or that would set a record + (e.g., ≥ 5 isolated equilibria for three positive charges), must be + re-verified by the independent checker (different arithmetic, different + fixed-point criterion) before it is recorded anywhere outside the attempt + record, and reported as requiring escalation rather than accepted. +- **Censuses are `EVIDENCE`**, scoped by the sampled family, grid, region + and precision, all of which must be stated. Perturbation arguments valid + "for small ε" without a certified ε are `SPECULATION` at the instantiation + step no matter how rigorous the asymptotics. + +## Harness (tier 0) + +- `harness/maxwell-equilibria/equilibria.py` — the reference implementation. + Certified equilibrium counting for rational configurations: adaptive + bisection with exclusion tests in outward-rounded rational interval + arithmetic (dyadic endpoints, exact integer square-root enclosures), + Krawczyk-operator isolation certificates, the localization and + charge-neighborhood lemmas instantiated in exact arithmetic, certified + det-sign indices, and the index-sum consistency check. Emits a JSON + certificate with the full leaf decomposition (split paths), so the covering + is independently re-checkable. Standard library only. +- `harness/maxwell-equilibria/verify_equilibria.py` — the independent + checker. Re-verifies a claimed certificate with different machinery: + directed-rounding floating-point interval arithmetic (with an exact + rational fallback), interval Newton with interval Gaussian elimination + instead of the Krawczyk operator, its own derivations of the localization + and domination lemmas, and an exact combinatorial check (Kraft equality + + prefix-freeness) that the leaf boxes tile the search region. Run it on any + certificate you intend to cite; a count confirmed by both routes at a + record-adjacent value is reported as requiring escalation rather than + accepted. diff --git a/problems/maxwell-equilibria/attempts/001-abk-explicit-witness.md b/problems/maxwell-equilibria/attempts/001-abk-explicit-witness.md new file mode 100644 index 0000000..2170bec --- /dev/null +++ b/problems/maxwell-equilibria/attempts/001-abk-explicit-witness.md @@ -0,0 +1,229 @@ +# 001 — Explicit certified witness for the five-charge Maxwell counterexample + +- **Problem:** maxwell-equilibria, `problems/maxwell-equilibria/PROBLEM.md` +- **Date:** 2026-08-04 +- **Mode:** informed +- **Type:** computational search + certification +- **Tools:** `problems/maxwell-equilibria/explore/abk_witness_scan.py` (float + candidate census; deterministic, seeded RNG, ~10 s per parameter point); + `harness/maxwell-equilibria/equilibria.py` (certified complete census; + exact/outward-rounded arithmetic at 64 dyadic bits, run at + `--max-boxes 3000000`); `harness/maxwell-equilibria/verify_equilibria.py` + (independent re-verification). Runtimes in the body. +- **Sources:** arXiv:2607.27197 (Arathoon–Ball–Kvalheim, *The Maxwell + Conjecture is False*, July 2026) [T — abstract and HTML body via web + fetch, not the PDF]; arXiv:2607.28785 (three-charge bound 12 → 6) [T]; + both consumed as labelled inputs per STATUS queue item 16. + +## Approach + +The ABK refutation proves that five positive charges can have ≥ 24 +nondegenerate equilibria — but only asymptotically: their configuration +family is valid "for all sufficiently small ε" with no explicit ε named, and +their supporting computations are computer-algebra, not certified. Queue +item 16: produce an *explicit rational* configuration and certify its exact +equilibrium count, making the counterexample a concrete checkable object. + +Why this rather than the obvious alternative (certifying at their literal +coordinates): their triangle has vertices at irrational coordinates +(circumradius 1 in the xy-plane), while the equilateral triangle embeds +rationally in ℝ³ as e₁, e₂, e₃ (pairwise distance √2, symmetry axis along +(1,1,1)). Since equilibrium counts are similarity-invariant and charge +values are scale-invariant (F_λ(λx) = λ⁻²F(x)), the family maps to + + unit charges at e₁, e₂, e₃; charges q at (1/3,1/3,1/3) ± t·(1,1,1) + +with everything in ℚ once t, q are rational. The dictionary to ABK's frame: +ε = 3t/√2, and their charge law is q_ε = (3/4)ε³ − (5/32)ε⁵. + +## What was done + +**Statement under test.** The configuration + + q₁ = q₂ = q₃ = 1 at (1,0,0), (0,1,0), (0,0,1); + q₄ = q₅ = 4367/1000000 at (251/600, 251/600, 251/600) + and (149/600, 149/600, 149/600) + +(t = 17/200, i.e. ε ≈ 0.18031; q within 2·10⁻⁸ of the ABK law value) +has ≥ 17 isolated equilibria — refuting Maxwell's (5−1)² = 16 — and in fact +exactly 24, all nondegenerate, matching ABK's count. + +**Step 1 — parameter hunt (floats; locate, never certify).** +`explore/abk_witness_scan.py --scan` sweeps (t, λ) with q = λ·q_ε. Findings +of record, all at float precision with a seeded global Newton census +(cluster seeds around the centroid + global seeds in the localization +ball), reproducible via the flags in the file: + +- The full 24-count window exists only for t ≤ 0.085 (ε ≲ 0.18): at + t = 0.0875 the maximum observed count is 18, and at t ≥ 0.1 the counts + run 6 → 18 → 10 as q crosses the ABK law with no 24 anywhere on the + sampled grid. "Sufficiently small ε" is doing real work — at ε ≈ 0.19 + the bifurcation has not yet released all 21 equilibria. +- At t = 17/200 the 24-window in q is roughly (4.366, 4.389)·10⁻³ — about + half a percent wide, λ ∈ (1.000, 1.005) — with conditioning best at the + low edge and count falling 24 → 16 past the high edge. Below the window + the count is 12. +- Chosen witness: q = 4367/1000000, the low-edge sweet spot, which happens + to sit within 2·10⁻⁸ of the exact ABK law value (3/4)ε³ − (5/32)ε⁵ at + ε = (3/√2)(17/200). Float diagnostics there: 24 zeros, minimum pairwise + separation 1.51·10⁻³ (centroid to each of the three nearest cluster + points), minimum |det DF| ≈ 1.3·10⁻⁵, float index sum −4 = 1 − n. +- Structure of the 24 (float positions, D₃ₕ-symmetric): the exact centroid + (1/3,1/3,1/3) — a rational equilibrium by symmetry, at all (t, q) — plus + 17 more within 0.0152 of it (orbits of sizes 3+3+6+2+3), plus two outer + orbits of 3 (|z−c| ≈ 0.110 and 0.147), the latter being the persisted + edge equilibria of the bare triangle. + +**Step 2 — certified complete census.** Command: + + python harness/maxwell-equilibria/equilibria.py \ + --config problems/maxwell-equilibria/data/abk-witness-config.json \ + --out problems/maxwell-equilibria/data/abk-witness-cert.json \ + --prec-bits 64 --max-boxes 3000000 --progress-every 20000 + +All five charges are positive, so the localization lemma applies and the +census is complete (search region ⊇ ball of radius max|xᵢ| = 1): the +certificate covers every equilibrium of the configuration, not a sampled +region. + +Result: **exactly 24 isolated equilibria, zero unresolved leaves**, in +471,985 boxes / 235,993 leaves / 1984 s (single core, 64 dyadic bits, +minimum width 2⁻³⁰ never reached — deepest leaf at 58 total splits ≈ 19 +per axis). Leaf breakdown: 7,262 sign-exclusions, 228,674 Krawczyk-empty +exclusions, 18 charge-ball exclusions, 15 outside-localization exclusions, +24 Krawczyk isolation certificates. Every one of the 24 has a certified +det-sign (10 positive, 14 negative — all nondegenerate); enclosure widths +run 4.7·10⁻⁷ to 1.9·10⁻⁴. Certified positions agree with the float census +to ~9 digits. Artifacts in `problems/maxwell-equilibria/data/`: +`abk-witness-cert.json.gz` (full 34 MB certificate, 680 KB gzipped — +gunzip before re-verifying), `abk-witness-summary.json` (counts, lemma +data and the 24 enclosures, human-readable), and the run is +deterministic, so the certificate regenerates exactly from +`abk-witness-config.json` with the command above. + +**Step 3 — independent re-verification.** Command: + + python harness/maxwell-equilibria/verify_equilibria.py \ + --cert problems/maxwell-equilibria/data/abk-witness-cert.json + +Different arithmetic (directed-rounding decimal vs dyadic rational), +different isolation certificate (preconditioned interval Newton / interval +Gauss vs Krawczyk), independently re-derived lemmas, exact tiling check. + +Result: **PASS, zero failures, 924 s.** All 235,993 leaves re-established: +the 24 isolation certificates by preconditioned interval Newton, all +235,969 exclusions, both lemmas re-derived from the configuration, the +Kraft-equality tiling check exact, det-signs matching, and the index-sum +identity re-confirmed. + +**Cross-checks.** + +- Index-sum identity: a complete nondegenerate census of 5 positive charges + must have Σ sign det DF = 1 − 5 = −4. Holds: 10 positive and 14 negative + certified det-signs, in both engines. +- The float census (independent implementation, different algorithm) found + the same count and positions to ~9 digits before any certification ran. +- Harness validation suite (classical two-charge, collinear, equilateral + knowns) passes before and after the run. + +## Outcome + +**VERIFIED** (scope: the single explicit configuration above, and nothing +else). The configuration + + q₁ = q₂ = q₃ = 1 at e₁, e₂, e₃; + q₄ = q₅ = 4367/1000000 at (251/600,251/600,251/600), (149/600,149/600,149/600) + +has **exactly 24 isolated equilibrium points, all nondegenerate** — a +complete certified census over a region provably containing every +equilibrium, established by two independent implementations using different +arithmetic and different fixed-point theorems. Since 24 > 16 = (5−1)², this +is an explicit, machine-checkable refutation of Maxwell's conjecture for +n = 5, and an independent confirmation of the count in arXiv:2607.27197 at +a concrete witness the preprint itself does not supply (its theorem is +asymptotic in ε with no ε₀ named). + +Per the verification contract this is a record-adjacent count: it passed +both routes and is hereby **reported as requiring escalation** — a separate +skeptic-review attempt (fresh eyes on the harness itself, not just the +certificate) is queued before the ledger treats the refutation as settled +library fact. + +**Not claimed:** that 24 is the maximum for five charges; anything about +any other (t, q), including ABK's asymptotic theorem itself (one instance +is certified, not the family); the float-level window observations in +step 1 (those are `EVIDENCE` at float precision, sampled grids only); and +nothing about the n = 3 gap, which stays open at 4-vs-6. The ABK preprint +is six days old and not peer-reviewed; this attempt confirms its headline +count at one explicit point, which is evidence for the paper, not a review +of its proof. + +## Why it failed / what survived + +Nothing failed. What remains unproven, labelled: + +- The parameter-window observations (24-count window exists only for + t ≤ 0.085, window ≈ half a percent wide in q) are float-level + `EVIDENCE`; certified window boundaries are lead 2. +- `SPECULATION`: the 24-count window's low edge is a fold bifurcation + (12 → 24, six zeros born in three symmetric pairs) and the high edge + another (24 → 16). Consistent with the observed count sequence and + separations; not certified. + +Reusable: + +- The witness configuration itself: five rational charges realizing 24 + equilibria — the hard-instance family for any future counting work. +- The rational equilateral embedding trick (e₁,e₂,e₃ + diagonal axis) + turns any D₃-symmetric planar-triangle construction rational; it will + serve every future triangle-based configuration here. +- Cost calibration for the harness at a near-degenerate instance: + ~472k boxes / 33 min to certify a cluster with min separation 1.5·10⁻³ + and min |det DF| ≈ 1.3·10⁻⁵ at 64 bits; verification ~15 min. Deepest + isolation at ~19 splits per axis. This prices lead 2 and queue item 17. +- The exploration scanner (`explore/abk_witness_scan.py`) as the + candidate-hunting front end for any configuration family. + +## Leads generated + +1. **Skeptic review of this attempt** (required by the contract's + escalation clause): independently audit the harness's Krawczyk and + covering logic — the two engines share the subdivision tree, so a bug + in the *driver* (not the certificates) is the residual common-mode + risk. Concrete check: re-run the census at different precision, + min-width, and box offsets (the tree changes wholesale; the count must + not), and verify the 24 enclosures pairwise-disjoint by exact + comparison. Outcome either way is recordable. +2. **Certify the window boundaries.** Run the census at q = 4360/1000000 + (expect 12) and q = 4400/1000000 (expect 16): certified counts on both + sides bracket the two folds. Cost: ~2 × 35 min by the calibration + above. Turns the float window into certified bifurcation brackets. +3. **Certified ε₀ probe.** Binary-search t ∈ (0.085, 0.0875) with + certified censuses: the largest t with count 24 gives a certified + lower bound on how far ABK's "sufficiently small" actually reaches — + a quantitative datum the preprint leaves open. +4. **n = 4 variant.** Whether a triangle plus ONE axial charge (n = 4, + Maxwell bound 9) can beat 9 by the same bifurcation mechanism. + Falsifiable by the same pipeline: scan, then certify. If it can, the + refutation extends to n = 4; if not, the mechanism's n-dependence is + itself informative. +5. **Exact centroid equilibrium.** (1/3,1/3,1/3) is an equilibrium of + every member of the family by symmetry — a rational point where the + full Hessian is computable in ℚ exactly. The fold structure of lead 2 + should be decidable in exact arithmetic at that point alone + (eigenvalue sign changes of a rational matrix), no census needed. + +## References + +## References + +- P. Arathoon, G. Ball, M. D. Kvalheim, *The Maxwell Conjecture is False*, + arXiv:2607.27197 (July 2026). [T] +- *From 12 to 6: Sharpening the Three-Charge Bound in Maxwell's Problem*, + arXiv:2607.28785 (July 2026). [T] +- A. Gabrielov, D. Novikov, B. Shapiro, *Mystery of point charges*, Proc. + London Math. Soc. 95 (2007). [T — abstract level only] +- Ya-Lun Tsai, *Maxwell's conjecture on three point charges with equal + magnitudes*, Physica D 309 (2015). [T — abstract level only] +- This repo: `problems/maxwell-equilibria/PROBLEM.md` (verification + contract), STATUS queue item 16 (route framing). diff --git a/problems/maxwell-equilibria/data/abk-witness-cert.json.gz b/problems/maxwell-equilibria/data/abk-witness-cert.json.gz new file mode 100644 index 0000000..8a7287d Binary files /dev/null and b/problems/maxwell-equilibria/data/abk-witness-cert.json.gz differ diff --git a/problems/maxwell-equilibria/data/abk-witness-config.json b/problems/maxwell-equilibria/data/abk-witness-config.json new file mode 100644 index 0000000..5e353ce --- /dev/null +++ b/problems/maxwell-equilibria/data/abk-witness-config.json @@ -0,0 +1,10 @@ +{ + "_comment": "Explicit ABK-type witness candidate: unit charges at e1,e2,e3, charges q=4367/1000000 at (1/3,1/3,1/3) +- (17/200)(1,1,1) = (251/600 and 149/600 on the diagonal). Rational embedding of the arXiv:2607.27197 five-charge configuration (their eps = 3t/sqrt(2) ~ 0.1803; q matches their charge law to ~2e-8).", + "charges": [ + {"q": "1", "pos": ["1", "0", "0"]}, + {"q": "1", "pos": ["0", "1", "0"]}, + {"q": "1", "pos": ["0", "0", "1"]}, + {"q": "4367/1000000", "pos": ["251/600", "251/600", "251/600"]}, + {"q": "4367/1000000", "pos": ["149/600", "149/600", "149/600"]} + ] +} diff --git a/problems/maxwell-equilibria/data/abk-witness-summary.json b/problems/maxwell-equilibria/data/abk-witness-summary.json new file mode 100644 index 0000000..3dcb126 --- /dev/null +++ b/problems/maxwell-equilibria/data/abk-witness-summary.json @@ -0,0 +1,855 @@ +{ + "tool": "equilibria.py", + "config": { + "charges": [ + { + "q": "1", + "pos": [ + "1", + "0", + "0" + ] + }, + { + "q": "1", + "pos": [ + "0", + "1", + "0" + ] + }, + { + "q": "1", + "pos": [ + "0", + "0", + "1" + ] + }, + { + "q": "4367/1000000", + "pos": [ + "251/600", + "251/600", + "251/600" + ] + }, + { + "q": "4367/1000000", + "pos": [ + "149/600", + "149/600", + "149/600" + ] + } + ] + }, + "prec_bits": 64, + "min_width_bits": 30, + "region": [ + [ + "-1633/1552", + "1665/1552" + ], + [ + "-1701/1616", + "1733/1616" + ], + [ + "-1735/1648", + "1767/1648" + ] + ], + "complete": true, + "localization_r0_sq": "1", + "domination_rhos": [ + "1836551021563074506914973/4427218577690292387840000", + "1836551021563074506914973/4427218577690292387840000", + "1836551021563074506914973/4427218577690292387840000", + "13579046637201137836337/737869762948382064640000", + "13579046637201137836337/737869762948382064640000" + ], + "count": 24, + "unresolved": 0, + "excluded": { + "excluded-sign": 7262, + "excluded-newton": 228674, + "excluded-ball": 18, + "excluded-outside": 15 + }, + "isolated": [ + { + "path": "0111210010200111210010200110200011210011210011210110200011210011210111210011210110210110210011210110200011", + "box": [ + [ + "35316445/101711872", + "70634539/203423744" + ], + [ + "71500009/211812352", + "35750863/105906176" + ], + [ + "18228649/54001664", + "36459049/108003328" + ] + ], + "enclosure": [ + [ + "6405090803762556163/18446744073709551616", + "6405177360805284493/18446744073709551616" + ], + [ + "6227010338702533891/18446744073709551616", + "3113510106457667163/9223372036854775808" + ], + [ + "778376327315829647/2305843009213693952", + "6227019924598346053/18446744073709551616" + ] + ], + "det_sign": -1 + }, + { + "path": "011121001020011121001020011020001121001121001121001020001121001121011121001021011020011120011020001020", + "box": [ + [ + "17447975/50855936", + "34897599/101711872" + ], + [ + "8931277/26476544", + "35726825/105906176" + ], + [ + "2277049/6750208", + "36434535/108003328" + ] + ], + "enclosure": [ + [ + "3164424561262277951/9223372036854775808", + "6329114749228546371/18446744073709551616" + ], + [ + "6222800091501748581/18446744073709551616", + "6222822356935232345/18446744073709551616" + ], + [ + "3111400068800879615/9223372036854775808", + "6222822305878599023/18446744073709551616" + ] + ], + "det_sign": 1 + }, + { + "path": "011121001020011121001020001120011021011021011021001120011021011121001021011021011021001121001121011020", + "box": [ + [ + "34333641/101711872", + "17167645/50855936" + ], + [ + "18386239/52953088", + "36774195/105906176" + ], + [ + "18228649/54001664", + "36459049/108003328" + ] + ], + "enclosure": [ + [ + "3113502199600737021/9223372036854775808", + "6227026125605813943/18446744073709551616" + ], + [ + "1601258275592933377/4611686018427387904", + "1601308716641569087/4611686018427387904" + ], + [ + "3113502194744884259/9223372036854775808", + "194594566549979909/576460752303423488" + ] + ], + "det_sign": -1 + }, + { + "path": "0111210010200111210010200011200110210110210110210010200110210111210010210010210110200011200111200111200111", + "box": [ + [ + "68622759/203423744", + "8578051/25427968" + ], + [ + "72671003/211812352", + "4542045/13238272" + ], + [ + "2277049/6750208", + "36434535/108003328" + ] + ], + "enclosure": [ + [ + "6222805899961907395/18446744073709551616", + "1555704133709130357/4611686018427387904" + ], + [ + "6328925082074877075/18446744073709551616", + "3164519027130278565/9223372036854775808" + ], + [ + "777850812171998339/2305843009213693952", + "1555703979547970891/4611686018427387904" + ] + ], + "det_sign": 1 + }, + { + "path": "0111210010200111210010200010210111200111200111200010210111200111210011200111210110200010200011210110200111", + "box": [ + [ + "68668931/203423744", + "17167645/50855936" + ], + [ + "71500009/211812352", + "35750863/105906176" + ], + [ + "18750447/54001664", + "37502645/108003328" + ] + ], + "enclosure": [ + [ + "1556752551881680341/4611686018427387904", + "6227020427693030661/18446744073709551616" + ], + [ + "1556752541126784887/4611686018427387904", + "6227020414527290055/18446744073709551616" + ], + [ + "3202542108446182061/9223372036854775808", + "6405184395501162407/18446744073709551616" + ] + ], + "det_sign": -1 + }, + { + "path": "0111210010200111210010200010210111200111200111200010200111200111210011200010210110200011200110210110210111", + "box": [ + [ + "68622759/203423744", + "8578051/25427968" + ], + [ + "71451933/211812352", + "35726825/105906176" + ], + [ + "37054389/108003328", + "9264035/27000832" + ] + ], + "enclosure": [ + [ + "6222806309642432699/18446744073709551616", + "1555704026905152217/4611686018427387904" + ], + [ + "1555701571822246361/4611686018427387904", + "1555704037297871321/4611686018427387904" + ], + [ + "791114322407916853/2305843009213693952", + "1582262346265064305/4611686018427387904" + ] + ], + "det_sign": 1 + }, + { + "path": "011121001020011121001020001020011121011121011121011121001020001020001021001120001120001021011121001121", + "box": [ + [ + "17200625/50855936", + "34402899/101711872" + ], + [ + "35819543/105906176", + "8955315/26476544" + ], + [ + "36529089/108003328", + "4566355/13500416" + ] + ], + "enclosure": [ + [ + "3119565215249166813/9223372036854775808", + "6239231776023307469/18446744073709551616" + ], + [ + "1559782608320469949/4611686018427387904", + "6239231537419074003/18446744073709551616" + ], + [ + "6239130454783151173/18446744073709551616", + "779903968151411317/2305843009213693952" + ] + ], + "det_sign": -1 + }, + { + "path": "011121001020011121001020001020011121011121001121011020011020001020001020001121011021001021001121001121", + "box": [ + [ + "4222241/12713984", + "33779577/101711872" + ], + [ + "35366255/105906176", + "8841993/26476544" + ], + [ + "36066825/108003328", + "1127143/3375104" + ] + ], + "enclosure": [ + [ + "3063039988254282045/9223372036854775808", + "3063120111604273549/9223372036854775808" + ], + [ + "3080118046607932067/9223372036854775808", + "6160347942151018233/18446744073709551616" + ], + [ + "770029518442285957/2305843009213693952", + "6160347765788240851/18446744073709551616" + ] + ], + "det_sign": -1 + }, + { + "path": "0111210010200111210010200010200111210111210011200110210110210110200110210111200110210010210111200011", + "box": [ + [ + "16982957/50855936", + "33967563/101711872" + ], + [ + "35366255/105906176", + "8841993/26476544" + ], + [ + "8966365/27000832", + "17934481/54001664" + ] + ], + "enclosure": [ + [ + "770024294496851799/2305843009213693952", + "6160389778562778091/18446744073709551616" + ], + [ + "6160193974912849381/18446744073709551616", + "6160389948825147889/18446744073709551616" + ], + [ + "1531501548264665295/4611686018427387904", + "1531578454585421151/4611686018427387904" + ] + ], + "det_sign": -1 + }, + { + "path": "0111210010200111210010200010200111210111210010210111200111200110200111200110210110210010210110210011", + "box": [ + [ + "16982957/50855936", + "33967563/101711872" + ], + [ + "35170517/105906176", + "17586117/52953088" + ], + [ + "18032537/54001664", + "1127143/3375104" + ] + ], + "enclosure": [ + [ + "6160185933012099695/18446744073709551616", + "385024841648344059/1152921504606846976" + ], + [ + "95719077485239321/288230376151711744", + "765787503367256701/2305843009213693952" + ], + [ + "385012075433034901/1152921504606846976", + "192512206443809353/576460752303423488" + ] + ], + "det_sign": -1 + }, + { + "path": "011121001020011121001020001020011121011121001020011121011121011121001121011021001121011120001020001121", + "box": [ + [ + "8475813/25427968", + "33904901/101711872" + ], + [ + "35301009/105906176", + "17651363/52953088" + ], + [ + "36000287/108003328", + "18001019/54001664" + ] + ], + "enclosure": [ + [ + "6004702795367627/18014398509481984", + "1537253427856989771/4611686018427387904" + ], + [ + "1537203819053564381/4611686018427387904", + "6149014196459287253/18446744073709551616" + ], + [ + "3074407763259039489/9223372036854775808", + "6149013774341998165/18446744073709551616" + ] + ], + "det_sign": 1 + }, + { + "path": "011121001020011121001020001020011121011121001020011020001020011020001020011021001120001021011020011121011121", + "box": [ + [ + "67382711/203423744", + "8423045/25427968" + ], + [ + "68941679/211812352", + "17235849/52953088" + ], + [ + "70307357/216006656", + "17577277/54001664" + ] + ], + "enclosure": [ + [ + "3055195951869756855/9223372036854775808", + "190950774713983735/576460752303423488" + ], + [ + "6004202855654004115/18446744073709551616", + "6004272782307387533/18446744073709551616" + ], + [ + "6004202843830971217/18446744073709551616", + "3002136404315700139/9223372036854775808" + ] + ], + "det_sign": 1 + }, + { + "path": "011121001020011121001020001020011121011121001020001020011121001021011120001120001121011120011121001121", + "box": [ + [ + "16702627/50855936", + "33406903/101711872" + ], + [ + "34782475/105906176", + "543503/1654784" + ], + [ + "35471485/108003328", + "8868309/27000832" + ] + ], + "enclosure": [ + [ + "6058597888744979215/18446744073709551616", + "3029349413910681845/9223372036854775808" + ], + [ + "6058597867359574539/18446744073709551616", + "6058698607042204737/18446744073709551616" + ], + [ + "6058597907491905497/18446744073709551616", + "6058698801091224537/18446744073709551616" + ] + ], + "det_sign": -1 + }, + { + "path": "01112100102001112100102000102001112101102000112101112101102000112100102101112000112001102100112101112101", + "box": [ + [ + "67600379/203423744", + "16900507/50855936" + ], + [ + "34171223/105906176", + "8543235/26476544" + ], + [ + "34848129/108003328", + "4356235/13500416" + ] + ], + "enclosure": [ + [ + "6130163989357751181/18446744073709551616", + "3065105085182445529/9223372036854775808" + ], + [ + "5951997038267935217/18446744073709551616", + "2976069613689314759/9223372036854775808" + ], + [ + "2975998499104631715/9223372036854775808", + "5952139234975134213/18446744073709551616" + ] + ], + "det_sign": -1 + }, + { + "path": "011121001020011121001020001020011121001121011020011120011020011120011120011021001120001121001020001021011121", + "box": [ + [ + "66211921/203423744", + "33106785/101711872" + ], + [ + "70160749/211812352", + "35081233/105906176" + ], + [ + "70307357/216006656", + "17577277/54001664" + ] + ], + "enclosure": [ + [ + "6004202773912714451/18446744073709551616", + "6004272755628061343/18446744073709551616" + ], + [ + "6110391899283235149/18446744073709551616", + "3055212427567488115/9223372036854775808" + ], + [ + "3002101391703327161/9223372036854775808", + "6004272753828748429/18446744073709551616" + ] + ], + "det_sign": 1 + }, + { + "path": "011121001020011121001020001020011121001121011020011021011020011021011021011021001121001020001020001120011121", + "box": [ + [ + "66211921/203423744", + "33106785/101711872" + ], + [ + "68941679/211812352", + "17235849/52953088" + ], + [ + "71550567/216006656", + "35776159/108003328" + ] + ], + "enclosure": [ + [ + "3002101442441584347/9223372036854775808", + "1501068215532974433/4611686018427387904" + ], + [ + "750525363269209899/2305843009213693952", + "1501068208490550651/4611686018427387904" + ], + [ + "3055195935546761087/9223372036854775808", + "6110424773825967207/18446744073709551616" + ] + ], + "det_sign": 1 + }, + { + "path": "01112100102001112100102000102001112100112001102101112100112001102100112100102000112000112101112100102100112000112101", + "box": [ + [ + "262547329/813694976", + "131274489/406847488" + ], + [ + "140776503/423624704", + "35194555/105906176" + ], + [ + "139394267/432013312", + "69698009/216006656" + ] + ], + "enclosure": [ + [ + "2976031971879655211/9223372036854775808", + "372004531896557579/1152921504606846976" + ], + [ + "3065092845397525543/9223372036854775808", + "6130188406533945325/18446744073709551616" + ], + [ + "744007988294789637/2305843009213693952", + "5952072537746043271/18446744073709551616" + ] + ], + "det_sign": -1 + }, + { + "path": "011121001020011121001020001020011121001021011120011121001021011120001021001121001121001020011121001120001021", + "box": [ + [ + "16409105/50855936", + "65638069/203423744" + ], + [ + "34171223/105906176", + "68344163/211812352" + ], + [ + "71781699/216006656", + "35891725/108003328" + ] + ], + "enclosure": [ + [ + "2976021745110275009/9223372036854775808", + "5952092942466194839/18446744073709551616" + ], + [ + "5952043494303735213/18446744073709551616", + "5952092925105580845/18446744073709551616" + ], + [ + "6130179157887373587/18446744073709551616", + "766274365949659147/2305843009213693952" + ] + ], + "det_sign": -1 + }, + { + "path": "01112100102001112000102101112101112100102000102000102001112000112101102000102100102001102101102000", + "box": [ + [ + "19235491/50855936", + "38472631/101711872" + ], + [ + "625919/1654784", + "20031125/52953088" + ], + [ + "6574499/27000832", + "13150749/54001664" + ] + ], + "enclosure": [ + [ + "1744362247739751735/4611686018427387904", + "6977459099450669141/18446744073709551616" + ], + [ + "6977448920963318289/18446744073709551616", + "872182395725580725/2305843009213693952" + ], + [ + "2245912733915662123/9223372036854775808", + "2245923250120498873/9223372036854775808" + ] + ], + "det_sign": 1 + }, + { + "path": "01112100102001112000102101112101112001112000102000102100102001112000112000102100102001", + "box": [ + [ + "9999489/25427968", + "5000569/12713984" + ], + [ + "1301631/3309568", + "5208241/13238272" + ], + [ + "1440071/6750208", + "2881893/13500416" + ] + ], + "enclosure": [ + [ + "3627604944912416235/9223372036854775808", + "1813828802076970559/4611686018427387904" + ], + [ + "7255210586527560063/18446744073709551616", + "1813828595484525413/4611686018427387904" + ], + [ + "123003706090274611/576460752303423488", + "3936319450411628329/18446744073709551616" + ] + ], + "det_sign": -1 + }, + { + "path": "0111210010200110210011200111210111210010200010200010200110210011210110200010", + "box": [ + [ + "1201909/3178496", + "2405467/6356992" + ], + [ + "402709/1654784", + "1612553/6619136" + ], + [ + "637989/1687552", + "1277729/3375104" + ] + ], + "enclosure": [ + [ + "1744162509141282423/4611686018427387904", + "3489128375554312183/9223372036854775808" + ], + [ + "4490126239401053787/18446744073709551616", + "4493548490234137339/18446744073709551616" + ], + [ + "218019887044950387/576460752303423488", + "6978271163473220705/18446744073709551616" + ] + ], + "det_sign": 1 + }, + { + "path": "01112100102001102100112001112101102101102100102000112000102001102100102100", + "box": [ + [ + "624865/1589248", + "2501109/6356992" + ], + [ + "88229/413696", + "707549/3309568" + ], + [ + "1326757/3375104", + "332127/843776" + ] + ], + "enclosure": [ + [ + "7254421238089834793/18446744073709551616", + "7256116766574481559/18446744073709551616" + ], + [ + "1967293337942289031/9223372036854775808", + "246114005928101911/1152921504606846976" + ], + [ + "7254432529209451027/18446744073709551616", + "907013047076714555/2305843009213693952" + ] + ], + "det_sign": -1 + }, + { + "path": "011121001020001121011020011121011121001020001020001020001121001121011020001020011021011020011021", + "box": [ + [ + "12382247/50855936", + "1547987/6356992" + ], + [ + "625919/1654784", + "20031125/52953088" + ], + [ + "20424403/54001664", + "10213077/27000832" + ] + ], + "enclosure": [ + [ + "4491820780971254589/18446744073709551616", + "4491850385066937285/18446744073709551616" + ], + [ + "6977447167034991167/18446744073709551616", + "436091334938909085/1152921504606846976" + ], + [ + "6977447116740003531/18446744073709551616", + "6977461318903876457/18446744073709551616" + ] + ], + "det_sign": 1 + }, + { + "path": "01112100102000112101102001112100112100112100102000102001102001112101112100102001", + "box": [ + [ + "2711757/12713984", + "1356703/6356992" + ], + [ + "1301631/3309568", + "2604979/6619136" + ], + [ + "1326757/3375104", + "2655265/6750208" + ] + ], + "enclosure": [ + [ + "3935832682777309391/18446744073709551616", + "3936635189886338515/18446744073709551616" + ], + [ + "3627520559382277989/9223372036854775808", + "3627734962071894251/9223372036854775808" + ], + [ + "3627519806844975131/9223372036854775808", + "3627734828647057173/9223372036854775808" + ] + ], + "det_sign": -1 + } + ], + "index_sum": -4, + "index_sum_ok": true, + "boxes_processed": 471985, + "seconds": 1984.317, + "_comment": "Summary of abk-witness-cert.json.gz (full certificate with all 235993 leaf paths; gunzip before running verify_equilibria.py). Regenerable deterministically from abk-witness-config.json." +} \ No newline at end of file diff --git a/problems/maxwell-equilibria/explore/abk_witness_scan.py b/problems/maxwell-equilibria/explore/abk_witness_scan.py new file mode 100644 index 0000000..572d51f --- /dev/null +++ b/problems/maxwell-equilibria/explore/abk_witness_scan.py @@ -0,0 +1,218 @@ +#!/usr/bin/env python3 +"""Float exploration for an explicit ABK-type witness configuration. + +Candidate machinery ONLY (contract: floats locate, never certify). Searches +the two-parameter family + + unit charges at e1, e2, e3; charges q at (1/3,1/3,1/3) +- t*(1,1,1) + +which is the arXiv:2607.27197 configuration mapped onto the rational +equilateral embedding (their frame has circumradius 1 and axial height eps; +ours has circumradius sqrt(6)/3, so eps = 3t/sqrt(2), and charges are +scale-invariant). Their charge law: q_eps = (3/4)eps^3 - (5/32)eps^5. + +For a grid of (t, lambda) with q = lambda * q_eps(3t/sqrt(2)), runs a global +Newton census of equilibria (dense seeds near the centroid cluster + coarse +global seeds in the localization ball), dedups converged zeros, and reports +count, minimum pairwise separation, minimum distance to a charge, worst +Jacobian conditioning, and the float index sum (should be 1-n = -4 if the +census is complete and everything is nondegenerate). + +Usage: + abk_witness_scan.py --scan coarse (t, lambda) table + abk_witness_scan.py --probe T LAMBDA heavy census at one point + abk_witness_scan.py --probe-q T Q heavy census at explicit q +""" + +import argparse +import math +import random +import sys + +C = (1.0 / 3.0, 1.0 / 3.0, 1.0 / 3.0) + + +def make_charges(t: float, q: float): + return [ + (1.0, (1.0, 0.0, 0.0)), + (1.0, (0.0, 1.0, 0.0)), + (1.0, (0.0, 0.0, 1.0)), + (q, (C[0] + t, C[1] + t, C[2] + t)), + (q, (C[0] - t, C[1] - t, C[2] - t)), + ] + + +def q_law(t: float) -> float: + eps = 3.0 * t / math.sqrt(2.0) + return 0.75 * eps ** 3 - (5.0 / 32.0) * eps ** 5 + + +def field(ch, x): + out = [0.0, 0.0, 0.0] + for q, p in ch: + d = [x[k] - p[k] for k in range(3)] + r2 = d[0] * d[0] + d[1] * d[1] + d[2] * d[2] + if r2 < 1e-24: + return None + r3 = r2 ** 1.5 + for k in range(3): + out[k] += q * d[k] / r3 + return out + + +def jac(ch, x): + J = [[0.0] * 3 for _ in range(3)] + for q, p in ch: + d = [x[k] - p[k] for k in range(3)] + r2 = d[0] * d[0] + d[1] * d[1] + d[2] * d[2] + if r2 < 1e-24: + return None + r3 = r2 ** 1.5 + r5 = r3 * r2 + for k in range(3): + for l in range(3): + J[k][l] += q * ((1.0 / r3 if k == l else 0.0) - 3.0 * d[k] * d[l] / r5) + return J + + +def solve3(J, b): + # Gaussian elimination with partial pivoting; returns None if singular. + A = [row[:] + [b[i]] for i, row in enumerate(J)] + for col in range(3): + piv = max(range(col, 3), key=lambda r: abs(A[r][col])) + if abs(A[piv][col]) < 1e-300: + return None + A[col], A[piv] = A[piv], A[col] + for r in range(col + 1, 3): + m = A[r][col] / A[col][col] + for cc in range(col, 4): + A[r][cc] -= m * A[col][cc] + x = [0.0] * 3 + for r in range(2, -1, -1): + s = A[r][3] - sum(A[r][cc] * x[cc] for cc in range(r + 1, 3)) + x[r] = s / A[r][r] + return x + + +def det3(J): + a, b, c = J[0] + d, e, f = J[1] + g, h, i = J[2] + return a * (e * i - f * h) - b * (d * i - f * g) + c * (d * h - e * g) + + +def newton(ch, x0, iters=80, tol=1e-13): + x = list(x0) + for _ in range(iters): + F = field(ch, x) + if F is None: + return None + J = jac(ch, x) + if J is None: + return None + step = solve3(J, F) + if step is None: + return None + # damping for large steps + s = max(abs(v) for v in step) + lam = 1.0 if s < 0.1 else 0.1 / s + for k in range(3): + x[k] -= lam * step[k] + if s < tol: + F = field(ch, x) + if F is not None and max(abs(v) for v in F) < 1e-10: + return tuple(x) + return None + return None + + +def census(t, q, n_cluster=6000, n_global=1500, seed=20260804): + ch = make_charges(t, q) + rng = random.Random(seed) + zeros = [] + + def add(z): + if z is None: + return + if sum(v * v for v in z) > 1.0: # localization ball |x| < R0 = 1 + return + for q2, p in ch: + if sum((z[k] - p[k]) ** 2 for k in range(3)) < 1e-12: + return + for w in zeros: + if sum((z[k] - w[k]) ** 2 for k in range(3)) < 1e-16: + return + zeros.append(z) + + # dense seeds around the centroid cluster (radius ~ 6t) + rad = max(6.0 * t, 0.05) + for _ in range(n_cluster): + u = [rng.gauss(0, 1) for _ in range(3)] + nrm = math.sqrt(sum(v * v for v in u)) + r = rad * rng.random() ** (1.0 / 3.0) + add(newton(ch, [C[k] + r * u[k] / nrm for k in range(3)])) + + # coarse global seeds in the ball + for _ in range(n_global): + u = [rng.gauss(0, 1) for _ in range(3)] + nrm = math.sqrt(sum(v * v for v in u)) + r = rng.random() ** (1.0 / 3.0) + add(newton(ch, [r * u[k] / nrm for k in range(3)])) + + # diagnostics + minsep = min((math.dist(a, b) for i, a in enumerate(zeros) + for b in zeros[i + 1:]), default=float("inf")) + mindch = min((math.dist(z, p) for z in zeros for _, p in ch), default=float("inf")) + dets = [det3(jac(ch, z)) for z in zeros] + idxsum = sum(1 if d > 0 else -1 for d in dets) + mindet = min((abs(d) for d in dets), default=0.0) + return { + "count": len(zeros), "minsep": minsep, "min_dist_charge": mindch, + "index_sum": idxsum, "min_abs_det": mindet, "zeros": sorted(zeros), + } + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--scan", action="store_true") + ap.add_argument("--probe", nargs=2, type=float, metavar=("T", "LAMBDA")) + ap.add_argument("--probe-q", nargs=2, type=float, metavar=("T", "Q")) + ap.add_argument("--ts", default="0.25,0.2,0.15,0.125,0.1,0.075") + ap.add_argument("--lams", default="0.6,0.8,0.9,1.0,1.1,1.2,1.4") + args = ap.parse_args() + + if args.scan: + ts = [float(v) for v in args.ts.split(",")] + lams = [float(v) for v in args.lams.split(",")] + print(f"{'t':>7} {'lam':>5} {'q':>12} {'count':>5} {'minsep':>9} " + f"{'mind(chg)':>9} {'idxsum':>6} {'min|det|':>10}") + for t in ts: + for lam in lams: + q = lam * q_law(t) + r = census(t, q, n_cluster=2500, n_global=600) + print(f"{t:7.4f} {lam:5.2f} {q:12.6e} {r['count']:5d} " + f"{r['minsep']:9.5f} {r['min_dist_charge']:9.5f} " + f"{r['index_sum']:6d} {r['min_abs_det']:10.3e}") + print() + return 0 + + if args.probe or args.probe_q: + if args.probe: + t, lam = args.probe + q = lam * q_law(t) + else: + t, q = args.probe_q + r = census(t, q, n_cluster=20000, n_global=5000) + print(f"t={t} q={q!r} count={r['count']} minsep={r['minsep']:.6f} " + f"min_dist_charge={r['min_dist_charge']:.6f} " + f"index_sum={r['index_sum']} min|det|={r['min_abs_det']:.3e}") + for z in r["zeros"]: + d = math.dist(z, C) + print(f" ({z[0]:+.9f}, {z[1]:+.9f}, {z[2]:+.9f}) |z-c|={d:.6f}") + return 0 + + ap.error("need --scan, --probe or --probe-q") + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/problems/maxwell-equilibria/prior-art.json b/problems/maxwell-equilibria/prior-art.json new file mode 100644 index 0000000..168c69d --- /dev/null +++ b/problems/maxwell-equilibria/prior-art.json @@ -0,0 +1,25 @@ +{ + "problem": "maxwell-equilibria", + "route_status": "VERIFIED", + "route_summary": "Explicit rational five-charge witness certified with exactly 24 nondegenerate equilibria (> 16 = (5-1)^2) by two independent engines - a concrete, machine-checkable instance of the arXiv:2607.27197 refutation. Escalation: a skeptic review of the harness driver is queued before this is treated as settled. The n=3 gap (4 vs 6) is untouched.", + "attempts": [ + { + "id": "001", + "file": "attempts/001-abk-explicit-witness.md", + "date": "2026-08-04", + "mode": "informed", + "status": "VERIFIED", + "mechanism": [ + "certified-box-coverage", + "exact-rational-arithmetic", + "independent-reimplementation" + ], + "one_line": "Five rational charges (units at e1,e2,e3; 4367/1000000 at centroid +- (17/200)(1,1,1)) certified to have exactly 24 nondegenerate equilibria - explicit refutation instance of Maxwell (n-1)^2 at n=5, both engines PASS, index sum -4.", + "leak_terms": [ + "4367/1000000", + "abk-witness", + "24-count window" + ] + } + ] +} diff --git a/site/explainers/maxwell-equilibria.md b/site/explainers/maxwell-equilibria.md new file mode 100644 index 0000000..f0e1df5 --- /dev/null +++ b/site/explainers/maxwell-equilibria.md @@ -0,0 +1,82 @@ +--- +title: Maxwell's problem on points of equilibrium +short: Maxwell equilibria +order: 11 +tagline: Fix a handful of electric charges in space. How many places can a test charge sit with no force on it? +posed: James Clerk Maxwell, 1873 +--- + +## In plain terms + +Pin a few positive electric charges at fixed points in space. Between them +the electric field pushes and pulls, and at certain special points the pushes +cancel exactly: a test charge placed there feels nothing. These are the +points of equilibrium. A famous theorem of Earnshaw says none of them is +stable — every one is a saddle, a mountain pass rather than a valley — which +is why you cannot levitate a charge with static fields alone. + +Maxwell, in a footnote of his 1873 *Treatise on Electricity and Magnetism*, +claimed that n charges can never produce more than (n−1)² such points. Two +charges give at most one equilibrium; three should give at most four; five at +most sixteen. He sketched an argument and moved on. A century and a half +later, nobody had proved it — and for three charges, nobody has even proved +that the answer is four rather than five or six. + +## What is known + +Remarkably little, for how old and concrete the question is. It is not even +known that the number of equilibrium points is always finite. The modern +benchmark is a 2007 paper of Gabrielov, Novikov and Shapiro, which used deep +results about systems with few monomials to prove the first general bounds — +for three charges, at most twelve equilibria, against Maxwell's predicted +four. For three charges of *equal* strength the answer really is four +(Tsai, 2015), with the equilateral triangle attaining it: one equilibrium at +the center, three more near the edges. + +Then, days before this problem was onboarded, the story broke open: a July +2026 preprint of Arathoon, Ball and Kvalheim constructs five charges with at +least twenty-four equilibria — eight more than Maxwell's sixteen. The +construction is delicate: an equilateral triangle of unit charges plus two +minuscule charges hovering just above and below its center. As the small +charges switch on, the central equilibrium shatters into twenty-one. If the +preprint holds up, the conjecture as Maxwell stated it is false, and the +true growth of the maximum is wide open. A companion preprint sharpens the +three-charge bound from twelve to six — leaving the original small case, +four versus five versus six, still unresolved. + +## Why it is hard + +The equilibrium equations look tame but are not algebraic — distances enter +through square roots — so the polynomial machinery that counts solutions of +polynomial systems does not apply directly, and what replaces it +(fewnomial theory) gives bounds that are almost certainly far from sharp. +The saddle points also interact: Morse theory constrains their indices +globally, so you cannot add equilibria one at a time; new ones must appear +in coordinated families, which is exactly what makes both counting them and +constructing many of them delicate. + +And the new counterexample illustrates a second difficulty: it exists only +"for sufficiently small ε". Such proofs are rigorous as asymptotics yet name +no actual configuration, and pinning one down is genuinely hard — the +twenty-one new equilibria are born nearly merged, so any explicit instance +sits close to degeneracy, where both numerics and certification are at their +worst. + +## What a breakthrough would mean + +The equilibrium structure of Coulomb fields is textbook physics — ion traps, +charged-particle optics and levitation arguments all live in it — and it is +genuinely startling that the count of force-free points for five charges was +mispredicted for 150 years. Settling the three-charge case would close the +first open case of a question Maxwell thought obvious. An independently +certified explicit counterexample would turn a fresh asymptotic claim into a +concrete, checkable object. And any new record configuration would redraw +the map of what static charge arrangements can do. + +**In this lab it carries a high budget.** Everything the contract needs is +decidable in exact rational arithmetic once the right variables are chosen, +the first targets are concrete and self-policing — a single certified +configuration with five equilibria from three charges, or twenty-four from +five, decides something — and the fresh refutation means the terrain has +just shifted, which is when independent certified searches earn the most. +Nothing has been tried here yet. diff --git a/tiers.json b/tiers.json index c9b47a1..9ea5a20 100644 --- a/tiers.json +++ b/tiers.json @@ -21,6 +21,7 @@ "docs/IDEATE.md", "docs/RIPPLE.md", "docs/PLAN-physics-problems.md", + "docs/PLAN-em-problems.md", ".claude/**/*", "problems/*/PRIOR-ART.md", "problems/*/prior-art.json",