---
title: Research & Proof: Papers and Benchmark Results | SpinForge
url: https://spin-forge.com/proof
description: SpinForge research papers and Garmo Solvers benchmark results, with full papers available on request by email.
---

RESEARCH & PROOF

# The evidence behind the work.

Benchmark results and research summaries, in the words of the posters and papers themselves. Each result states its own scope and conditions, including where we did not win. Full posters and papers are available on request by email.

## Garmo Solvers benchmark results

Head-to-head results against established solvers, with every answer re-checked against the original input. Win, tie and loss counts are reported as measured.

GARMO SOLVERS · S01

### Proof-Carrying Max-Cut on a GH200: 67 Biq Mac Optima Proved vs HiGHS's 49

Rigorous SDP and Odd-Cycle LP Bounds in a GPU Branch-and-Bound, Every Proof Re-Checked by an Independent Verifier.

67 vs 49 Biq Mac instances proved optimal, CertCut vs HiGHS (148)

58/83/7 wins / ties / losses vs HiGHS

71/71 Gset upper bounds re-verified by the CPU verifier

L = 9 2-D ±J torus: every seed proved up to n = 81

- Full Biq Mac: 67 vs 49 proved; W/T/L 58/83/7; 0 bound mismatches
- Sparse families (pre-declared 48): 44 vs 40 proved, 33/6/9
- Gset 71/71 rigorous bounds verified VALID; median certified gap 10.05 %
[Request the full poster by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20poster%3A%20Proof-Carrying%20Max-Cut%20on%20a%20GH200%3A%2067%20Biq%20Mac%20Optima%20Proved%20vs%20HiGHS%27s%2049%20%28S01%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

GARMO SOLVERS · S02

### Weighted MaxSAT on a GH200: From 14/33/50 to 33/38/26 Against NuWLS-c-IBR

GPU Local Search, a SAT-Based Improver and a Native Local Search Racing Together. 97 MaxSAT-Evaluation Instances at 60 s; Held-Out 59: 22/34/3.

33/38/26 wins / ties / losses vs NuWLS-c-IBR, 97 instances

22/34/3 on the 59 held-out instances

−36  +7 net wins minus losses, first build to 1.0.2

35/59/3 SAT-based LNS vs the previous default

- 1.0.2 vs NuWLS-c-IBR: 33/38/26 on 97; held-out 59 22/34/3; 93 vs 93 feasible
- SAT-based LNS vs the previous default: 35/59/3 (held-out 10/47/2)
- Still behind on the 38 design instances (11/4/23)
[Request the full poster by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20poster%3A%20Weighted%20MaxSAT%20on%20a%20GH200%3A%20From%2014/33/50%20to%2033/38/26%20Against%20NuWLS-c-IBR%20%28S02%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

GARMO SOLVERS · S03

### Large-Instance TSP on 16 Arm Cores: 0.692 %  0.165 % Mean Gap, Still Behind LKH-3

Sequential 5-Opt Basis Moves, Pi-Alpha Candidates and a Wider Kick Window, Each Confirmed on 8 Held-Out National Instances.

0.165 % mean gap, 8 held-out national TSPs (was 0.692 %)

2/0/6 vs LKH-3 best config, held-out, 30 s

7/7 dev instances improved by 5-opt + pi-alpha

0.020 % d18512 with the LKH-style search (LKH-3: 0.049 %)

- Held-out 8: mean gap 0.692  0.224  0.165 %
- vs LKH-3 still 2/0/6 held-out (wins on ho14473 and ch71009)
- LKH-style variants beat LKH-3 on brd14051, d15112, d18512 (opt-in)
[Request the full poster by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20poster%3A%20Large-Instance%20TSP%20on%2016%20Arm%20Cores%3A%200.692%20%25%20%E2%86%92%200.165%20%25%20Mean%20Gap%2C%20Still%20Behind%20LKH-3%20%28S03%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

GARMO SOLVERS · S04

### A Native QCDCL Solver vs DepQBF: From 0 vs 4 to a 15–15 Tie, Then 15 vs 18 on Fresh Instances

Dependency Learning, Solution-Flip Search and Universal Expansion, Measured on QBFEVAL'22 With Zero Disagreements.

15 vs 18 solved, fresh 100 instances, ours vs DepQBF

0 verdict disagreements in every run

26/36 dev set after tuning (restart base 50, was 20)

3 Organic-Synthesis instances only we solve

- 100-instance set: 15 vs 15 (3 unique each)
- Held-out: 12 vs 16; fresh 100: 15 vs 18: LOSS
- Every DepQBF-only solve is a Hex game: the TRUE side needs short learned cubes
[Request the full poster by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20poster%3A%20A%20Native%20QCDCL%20Solver%20vs%20DepQBF%3A%20From%200%20vs%204%20to%20a%2015%E2%80%9315%20Tie%2C%20Then%2015%20vs%2018%20on%20Fresh%20Instances%20%28S04%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

GARMO SOLVERS · S05

### Vehicle Routing vs PyVRP: a C++ Iterated Local Search Wins 37/26/21 at Equal Budget

CVRPLIB X, Solomon and Gehring–Homberger, One Thread Each, Every Route Set Re-Checked by an Independent Checker.

37/26/21 vs PyVRP, 84 instance-runs, equal budget

25/6/9 on CVRPLIB X

25/66/21 full Solomon set, paired

4.36  0.29 % X mean gap, GPU HGS  ILS

- Subsets: 37/26/21 (X 25/6/9, Homberger 12/3/5)
- Full Solomon 56, both at once: 25/66/21 narrow win
- The 12-instance Solomon subset alone remains a loss (1/16/7)
[Request the full poster by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20poster%3A%20Vehicle%20Routing%20vs%20PyVRP%3A%20a%20C%2B%2B%20Iterated%20Local%20Search%20Wins%2037/26/21%20at%20Equal%20Budget%20%28S05%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

GARMO SOLVERS · S06

### ISPD98 Bisection: a Multilevel FM + Flow Engine Beats KaHyPar and mt-KaHyPar at Equal Budget

Golden-Evaluator Cuts at the TILOS Balance Tiers; 11/6/3 vs mt-KaHyPar on the Largest Instances After a Byte-Identical 1.88× Speedup.

11/6/3 vs mt-KaHyPar, ibm14–18, 60 s, 2 seeds

9/10/1 vs KaHyPar and mt-KaHyPar at 300 s

1.88× engine speedup, partitions byte-identical

20/20 large cells at or below the published leaderboard

- v3 vs KaHyPar 16/43/11, vs mt-KaHyPar 20/40/12
- Large instances: 9/10/1 at 300 s; 11/6/3 at 60 s after the speedup
- GPU-hybrid producer: no gain (6/58/8); hypergraph λ−1 suite still behind
[Request the full poster by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20poster%3A%20ISPD98%20Bisection%3A%20a%20Multilevel%20FM%20%2B%20Flow%20Engine%20Beats%20KaHyPar%20and%20mt-KaHyPar%20at%20Equal%20Budget%20%28S06%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

GARMO SOLVERS · S07

### An Evidence-Driven Solver Router: Regret 0.046 vs 0.190 for the Best Single Backend

Rules Decided on a Training Split, Checked Out of Sample, Every Answer Verified; on the GPU 93/166/11 vs the CPU.

0.046 mean regret vs the oracle, 276 instances

214/276 oracle hits

93/166/11 router on cuda vs cpu

0 planted wrong answers accepted

- Router regret 0.046 (train 0.049, test 0.042) vs 0.190 best single per kind
- Rules HOLD out of sample on 14 of 15
- GPU vs CPU routing: 93/166/11
[Request the full poster by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20poster%3A%20An%20Evidence-Driven%20Solver%20Router%3A%20Regret%200.046%20vs%200.190%20for%20the%20Best%20Single%20Backend%20%28S07%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

GARMO SOLVERS · S08

### A Verified MIP Race: HiGHS, SCIP and GPU Primal Heuristics Against cuOpt on MIPLIB 2017

89 of 94 MIPLIB Instances With a Checker-Accepted Answer at 60 s; GPU Feasibility Jump Helps Early, Not at the End.

89/94 MIPLIB instances with a verified answer

21/42/28 vs the best other engine, final objective

0 checker disagreements with the race

3 modes GPU primal A/B: off / FJ / PDHG

- garmo 89/94 verified feasible vs HiGHS 85, SCIP 83, cuOpt 79
- vs best other engine: 21 better / 42 equal / 28 worse (portfolio view)
- HiGHS and cuOpt cannot run the quadratic suites
[Request the full poster by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20poster%3A%20A%20Verified%20MIP%20Race%3A%20HiGHS%2C%20SCIP%20and%20GPU%20Primal%20Heuristics%20Against%20cuOpt%20on%20MIPLIB%202017%20%28S08%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

GARMO SOLVERS · S09

### Lazy Clause Generation in C++: 39 of 40 Schedules Proved Optimal vs CP-SAT's 20

Explained Propagation, Minimal-Cover Reasons and Energetic Reasoning; One Thread Each, 20 s, Every Answer Re-Checked.

39/1/0 vs CP-SAT, 40 schedules, 20 s

39 vs 20 proved optimal

< 0.1 s every n = 20/24 proof

57/60 XCSP 2024 instances parsed

- Scheduling 39/1/0; proved 39 vs 20
- Every n = 20 and 24 instance proved by us in < 0.1 s, none by CP-SAT
- Queens: faster search, slower end-to-end (Python model translation)
[Request the full poster by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20poster%3A%20Lazy%20Clause%20Generation%20in%20C%2B%2B%3A%2039%20of%2040%20Schedules%20Proved%20Optimal%20vs%20CP-SAT%27s%2020%20%28S09%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

GARMO SOLVERS · S10

### Certified GPU Numerics: Every Answer Carries a Checkable Certificate: and Where It Costs

Conic LP/QP/SOCP, Optimal Transport, Assignment, Krylov CG, MDP Value Iteration and Exact Counting, Each Against Its Reference Solver.

0 failed certificate verifications

6 of 22 DOTmark instances faster than ot.emd

10⁻⁸ certified CG residual, every Poisson run

LOSS on time vs the reference solvers

- Every conic claim re-verified exactly (0 failures), but LOSS on time on every suite
- CertOT: faster than ot.emd on 6 of 22 DOTmark instances; JV slower than scipy
- Exact counts agree with OEIS / independent recounts on every run
[Request the full poster by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20poster%3A%20Certified%20GPU%20Numerics%3A%20Every%20Answer%20Carries%20a%20Checkable%20Certificate%3A%20and%20Where%20It%20Costs%20%28S10%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

GARMO SOLVERS · S11

### LABS on a GH200: Exponent 1.24 to the Proven Optimum, Beside the QAOA Exponents

GPU Memetic Tabu With 4,096 Islands vs lMAts; Exact Branch-and-Bound Matches All 46 Published Optima.

1.240 GPU wall-TTS base b, N = 40–66

46/46 exact optima equal the P&M table

3 of 6 N > 66 best-knowns reached (lMAts 0)

4,096 islands on one GPU

- GPU wall TTS ∝ 1.240N (N 40–66) vs lMAts 1.352N
- Exact B&B: 46/46 optima equal the published table
- N = 67, 71, 75: GPU reaches the best-known value; lMAts at none
[Request the full poster by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20poster%3A%20LABS%20on%20a%20GH200%3A%20Exponent%201.24%20to%20the%20Proven%20Optimum%2C%20Beside%20the%20QAOA%20Exponents%20%28S11%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

GARMO SOLVERS · S12

### UNISOLVE 0.16.1: One Solver Platform, 13 Problem Domains, Every Answer Checked

106 CUDA Gauntlet Cases Passed on One GH200; 8 Real Application Models Answered and Checked; One Airline Optimum Proved Exactly.

106/106 CUDA gauntlet cases passed (one GH200)

14,207 tests passed on Brev (13 skipped)

8/8 real application models answered and checked

gap 0 flugpl airline optimum 1,201,500 proved exactly

- Gauntlet: 106/106 passed; peak memory grows linearly (exponent 0.999–1.002)
- Real-world: 8/8 feasible and checked; 3 independently re-checked; flugpl 1,201,500 proved optimal (gap 0)
- Capacity case: 30 M vertices, 90 M edges, 4.2 GB peak, resident median 0.014 s
[Request the full poster by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20poster%3A%20UNISOLVE%200.16.1%3A%20One%20Solver%20Platform%2C%2013%20Problem%20Domains%2C%20Every%20Answer%20Checked%20%28S12%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

GARMO SOLVERS · S13

### Four Certified Builds: Toroidal Proofs, Unroutability Certificates, CertBQP and a 235× Batch Service

15 of 17 Toroidal Gset Instances Proved Optimal; Routing Infeasibility Certified in Seconds; Every Claim Checked.

15/17 toroidal Gset instances proved optimal

0 false infeasibility certificates

12/12 k-cluster ER n = 40 proved (CertBQP)

235× batched throughput vs one by one

- Toroidal: 15/17 proved optimal, bound gaps closed vs CertCut on every instance
- Unroute: 0 false infeasibility on unmodified files; certificates in 2–76 s
- CertBQP: ER n = 40 12/12 proved; behind HiGHS on MIS and QKP
- Batch: 235× throughput, 200/200 reference hits vs 135/200
[Request the full poster by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20poster%3A%20Four%20Certified%20Builds%3A%20Toroidal%20Proofs%2C%20Unroutability%20Certificates%2C%20CertBQP%20and%20a%20235%C3%97%20Batch%20Service%20%28S13%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

## Search and optimization science

P0

### Ground-State Geometry of Large Random Sparse Max-Cut: σ=ln2 Universality, a Certified Degree Law to d=1024, a T=0 Droplet Link-Overlap Signature, and the Finite-T Spin-Glass Transition at the Bethe Value

We characterize the ground-state geometry of random sparse max-cut (Ising spin glasses on random-degree graphs) at scales to 1.65 × 10¹⁰ variables with a GPU parallel-tempering solver and independent certification. Four results: (1) σ = ln2 universality, independent ground states are mutually orthogonal (per-spin configurational entropy = ln 2, the maximum) across uniform, bimodal ±J, and gaussian couplings and degree d = 3  256, demonstrated at the extreme by the first ground-state overlap matrix ever measured at a billion spins (off-diagonal ⟨q⟩ = 7.5 × 10⁻⁵, folded Hamming 0.49996); (2) a certified degree law c(d) = ½ + a/√d − b/d with the leading constant a = 0.7646 ≈ the Sherrington–Kirkpatrick/Parisi mean-field constant 0.7632 at finite d (b = 0.136); the apparent ≈ln 2 (0.68) value at small d is the −b/d subleading term (α_eff(3) = 0.686 ≈ ln 2 is a coincidence): recount-verified (MATCH=True, relative error ≤ 3.6 × 10⁻⁶) to d = 256 across three generator seeds, cross-checked independently, and extended to d = 1024; (3) a link-overlap droplet signature at T = 0, link overlap pinned at its trivial factorized value with variance shrinking ∝ 1/N toward a delta; (4) a corrected finite-T result: a non-equilibrium cooling-quench decorrelates (⟨q²⟩ ∝ 1/N), but the equilibrated measurement (companion P12) finds the spin-glass transition at the analytically-known T_c = 2.08 for d = 6 ±J ((d−1)tanh²β_c = 1; Binder crossings 2.05/2.13 bracket it); the quench simply fails to equilibrate below T_c, and the T = 0 link-overlap droplet signature (§3.3) and this finite-T transition are different observables, not in tension. We report honest negatives, including the retraction of an earlier finite-T "RSB-like" result that was a within-chain autocorrelation artifact.

[Request the full paper by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20paper%3A%20Ground-State%20Geometry%20of%20Large%20Random%20Sparse%20Max-Cut%3A%20%CF%83%3Dln2%20Universality%2C%20a%20Certified%20Degree%20Law%20to%20d%3D1024%2C%20a%20T%3D0%20Droplet%20Link-Overlap%20Signature%2C%20and%20the%20Finite-T%20Spin-Glass%20Transition%20at%20the%20Bethe%20Value%20%28P0%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

P1

### Classical GPU Parallel Tempering Outscales Quantum Annealing on D-Wave's Own Pegasus Time-to-Solution Benchmark

We test the central empirical claim behind quantum-annealing advantage: favorable time-to-solution (TTS) scaling on hard spin-glass instances, using a classical GPU parallel-tempering solver (SpinForge) run on D-Wave's own Pegasus topology and own TTS metric. Across 60,080 runs on a Pegasus-QAC instance ladder (graph sizes N = 210  3432), SpinForge exhibits a TTS scaling exponent of α = 0.087 (bootstrap 95% CI [0.035, 0.117]), versus the published D-Wave quantum-annealing- correction (QAC) exponent of 1.69 and the classical population-annealing PT-ICM baseline of 1.93 on the same family. A lower exponent is strictly better: it means time-to-solution grows far more slowly with problem size. On 3D Edwards–Anderson spin glasses, the same solver also beats tuned simulated annealing, Toshiba's Simulated Bifurcation Machine (SBM), and Gurobi. We frame the result honestly: the α figure is a point estimate with a wide confidence interval, a strong-but-bounded refutation, not a closed proof, and we detail every place a baseline was under- or over-favorable.

[Request the full paper by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20paper%3A%20Classical%20GPU%20Parallel%20Tempering%20Outscales%20Quantum%20Annealing%20on%20D-Wave%27s%20Own%20Pegasus%20Time-to-Solution%20Benchmark%20%28P1%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

P2

### Certified Maximum-Cut at 16.5 Billion Variables: GPU Parallel Tempering, Independent-Recount Certification, and N-Invariant Solution Quality

We report the solution of maximum-cut (equivalently, ground-state search for an Ising spin glass) at 2.0 × 10¹¹ variables (200 billion), to our knowledge the largest max-cut instance ever solved, reaching a recount-verified near-optimal cut of 0.77419 (degree-6, GPU simulated annealing, ~11.4 h wall), with a graph-analysis proof bundle. At the smaller, fully certified-to-the-Parisi-band scale of 1.65 × 10¹⁰ variables, the largest instance (degree-3, cut 89.4392%) is independently re-counted on CPU (22,136,207,143 cut edges, relative difference 3.2 × 10⁻⁷, MATCH) with the problem and result cryptographically hashed, to our knowledge the largest combinatorial-optimization instance certified at converged optimal-band quality. (The 200 B run is recount-verified, the reported cut is independently recomputed and matches, but it is near-optimal, sitting below the d6 Parisi ceiling 0.796 and above the quench fixed point 0.734, not a converged-band certification.) We establish three systems results: (1) solution quality is N-invariant, the degree-6 family cuts 79.595% from 1 billion to 10.3 billion variables, every record independently recounted; (2) the optimal cooling factor 0.9435 is N-universal (peak at N = 10⁶, 10⁷, and 5×10⁷; a faster 0.950 cool collapses to 76.9% at every size); and (3) bit-packed spins give a 1.41× speedup at bit-identical cut, confirming a prediction that the kernel is memory- latency bound. We document an instructive bug: a quality "dip" at 5 billion variables that was a multi-GPU sharding artifact (a non-annealing temperature ladder), traced by code-diff and fixed. We do not claim 20 billion (it ran out of memory).

[Request the full paper by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20paper%3A%20Certified%20Maximum-Cut%20at%2016.5%20Billion%20Variables%3A%20GPU%20Parallel%20Tempering%2C%20Independent-Recount%20Certification%2C%20and%20N-Invariant%20Solution%20Quality%20%28P2%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

P7

### An Algorithmic Phase Transition Between Annealing and Quench in Large-Scale Parallel Tempering

We identify a sharp algorithmic phase transition in GPU parallel tempering on large random max-cut, controlled by the cooling schedule and sweep budget, with a binary order parameter: the final cut either reaches the equilibrated band (0.7960) or freezes at a quench fixed point (0.7694), with almost nothing in between. On a degree-6, N = 10⁹ instance, varying only the cooling factor gives 0.9435  79.5958%, 0.945  79.5721%, then a cliff at cool_c ≈ 0.947 dropping −2.63 points to a flat quench plateau (0.950  76.9377%, 0.952  76.9380%, 0.965  76.9382%: identical to four digits). The plateau value 0.7694 is a single physical object, the typical greedy / zero-temperature-descent fixed point, and it is the same number behind four previously-separate observations: hardware- invariance (every GPU froze into it), the cooling collapse, a retracted multi-GPU "attractor," and the CERT-009 8-billion-variable placement solve (76.9463%). The transition unifies the campaign's entire errata: every retraction (two-band, "sharded 6× faster," the 5B dip) was a run that quenched instead of annealed, and the data forces a finer picture, a ladder of partial-anneal attractors (the 5B dip froze at 79.4632%, the full quench at 76.94%) set by how early the schedule quenches. We define the annealing gap, 0.7960 − 0.7694 = 0.0266 points, as the measurable worth of equilibrate-to-band over greedy descent. Honest caveat: the much-cited "escape at ~100 sweeps" is the schedule's floor-reach time (k = ln 0.01 / ln cool), not an emergent constant, what survives is that an N-independent sweep budget suffices to reach the band.

[Request the full paper by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20paper%3A%20An%20Algorithmic%20Phase%20Transition%20Between%20Annealing%20and%20Quench%20in%20Large-Scale%20Parallel%20Tempering%20%28P7%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

P9

### Where Is the Hardness? An Empirical Account of Typical-Case vs. Worst-Case Combinatorial Optimization

We give a precise, falsifiable, empirical account of where in instance-space the hardness of NP-hard combinatorial optimization actually lives, backed by solver experiments to 1.65 × 10¹⁰ certified variables. The claim has three parts, each measured. (1) Random large sparse max-cut is maximally degenerate (σ = ln 2, confirmed N = 10⁹–10¹⁰ across uniform/bimodal/gaussian and degree 3  256), and an N-independent sweep budget suffices to reach its optimal band, random instances are not where worst-case hardness bites. (The σ=ln2 / orthogonal-random premise was stress-tested 2026-06-18: an apparent refutation showing a clustered near-optimal manifold was a global-Z2-flip gauge artifact; gauge-fixed against exhaustive ground truth the random near-optimal set decays toward orthogonal, so the "random sits outside the hard regime" premise holds: see P0 §3.6.) (2) Real structured problems (portfolio, NN-quantization, chip-placement, planted) are not σ = ln 2, the Structure Atlas scores all four as structured (basins < K, finite overlap): i.e. they carry exploitable structure and are also outside the adversarial hard regime. (3) Worst-case NP-hardness is therefore carried by a narrow, adversarially-constructed regime that neither random-typical nor real-structured instances occupy, and the Structure Atlas (companion P6) is an instrument that locates any instance relative to it. We state plainly what this is not: not P = NP, not a claim that worst-case instances are easy, not a claim that every real problem is trivial. The disciplined version is both correct and more useful than the aspirational one.

[Request the full paper by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20paper%3A%20Where%20Is%20the%20Hardness%3F%20An%20Empirical%20Account%20of%20Typical-Case%20vs.%20Worst-Case%20Combinatorial%20Optimization%20%28P9%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

P11

### A Dynamical Second Law for Optimization on Sparse Ising: the Entropy–Energy Envelope

the formal object behind "Second Law": Φ = s_eq(e)−s_exp ≥ 0; fixed-T H-theorem dΦ/dt≤0 (proven, demonstrated Φ 0.7350.001); deficit monotone in cooling rate (measured N≤22, ✓; = P7's 0.0266 gap at scale); Clausius form Y ≥ T·X; P10 is its time-reversed special case

[Request the full paper by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20paper%3A%20A%20Dynamical%20Second%20Law%20for%20Optimization%20on%20Sparse%20Ising%3A%20the%20Entropy%E2%80%93Energy%20Envelope%20%28P11%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

P12

### A Statistical Mechanics of Search: State Variables, an Arrow of Time, a Carnot Bound, and the Geometry of Discoverability

We assemble a statistical mechanics for computational search on the σ=ln2 Ising/Max-Cut family and test how far it extends to other domains. The framework has a closed set of macroscopic state variables (the effective dimension of the search state is ~5), a free energy the dynamics minimizes, a proven + measured arrow of time (cooling↔heating hysteresis 2.5–4.1× a reversible control across four landscapes), a proven + measured Carnot-type efficiency bound (no search beats the quasi-static limit; the price of speed is the measured dissipation Φ(τ)), a closed equation of state c*(d,N,W) composed from four independently-measured fragments, a measured effective temperature (fluctuation–dissipation, validated to ~30%), and a measured phase diagram (fluid  critical T_c≈0.596  glassy  frozen, with the explorecommit transition present in spin glasses and in diffusion/language/vision/RL training). From it we give a measurable answer to why finite computation finds structure in nominally-infinite spaces: in the typical case hardness is set by the geometry of the near-optimal manifold, not the size of the space, the manifold is extensively dense (σ=ln2) and reachable in constant work per degree of freedom. We report two clean negatives: there is no conserved Noether invariant of search, and search across domains is not one universality class (exponents split: spin γ=0.64, EDA γ=1.68; cross-modal curves do not collapse, 21×). Results summary figure: P12_search_mechanics_summary, (A) density of states s(e)ln2 (why discovery is possible); (B) equation of state c(d)=½+α/√d; (C) arrow of time (hysteresis vs reversible control); (D) REFUTED single universality class (split exponents); (E) gauge-invariant overlap per domain; (F) the seven-law status board.

[Request the full paper by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20paper%3A%20A%20Statistical%20Mechanics%20of%20Search%3A%20State%20Variables%2C%20an%20Arrow%20of%20Time%2C%20a%20Carnot%20Bound%2C%20and%20the%20Geometry%20of%20Discoverability%20%28P12%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

P13

### P13, Pre-Registered Predictions of the Search-Mechanics Theory

falsifiable forward predictions for the framework with kill-criteria; staged for the first arXiv drop (P0+P12+P13)

[Request the full paper by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20paper%3A%20P13%2C%20Pre-Registered%20Predictions%20of%20the%20Search-Mechanics%20Theory%20%28P13%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

## Applied research

P14

### MATHGEN: Experimental Mathematics via Billion-Scale Ising / Spin-Glass Search

Most extremal combinatorial objects, low-correlation sequences, orthogonal ±1 matrices, extremal graph colorings, optimal rulers, are defined as the solution of an optimization or constraint-satisfaction problem, which is exactly what the SpinForge energy-minimization engine solves at billion-variable scale. MATHGEN turns that engine into an instrument for experimental mathematics: a GPU generator/searcher for mathematical objects, validated against established mathematics before any push to scale. We enforce a three-guarantee discipline (incremental-ΔE self-check = from-scratch recompute; validation against known results; only then scale) and report only what is verified. Verified headline results, all independently re-checked in this draft from the stored result objects: the LABS searcher hits the exhaustive optimum exactly for N = 11, 13, 15, 18 (recomputed energies E = 5, 6, 15, 25; merit factors F = 12.10, 14.083 = the Barker-13 value, 7.50, 6.48), with every incremental-ΔE self-check returning exactly 0.0; a constructive Hadamard generator (Sylvester + Paley I + Kronecker) produces 27/27 matrices validated H Hᵀ = nI exactly (max off-diagonal error 0.0), orders up to n = 8192, including the orders 24, 32, 44 at which naive local search stalled; the Ramsey searcher matches the Goodman monochromatic-triangle minimum for all 12 orders n = 5…16 (verified against OEIS A014557 and confirmed by independent exhaustive brute force for n = 5, 6, 7) and constructs a zero-monochromatic-K₄ coloring of K₁₇, reproducing the bound R(4,4) > 17; the Golomb searcher reproduces optimal rulers for orders 4–12 (nine orders, all rulers independently re-verified to have distinct pairwise differences at the published OGR length). We are explicit about scope: the search-based large-N LABS, OGR ≥ 13, and R(5,5) fronts are honest search results, not records, beating live world records requires the documented specialist algorithms, which we scope precisely. MATHGEN is a working experimental-mathematics engine that reproduces real mathematics across sequences, designs, graphs, and rulers, and is correct by construction in every searcher.

[Request the full paper by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20paper%3A%20MATHGEN%3A%20Experimental%20Mathematics%20via%20Billion-Scale%20Ising%20/%20Spin-Glass%20Search%20%28P14%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

P15

### A Spin-Glass Theory of Innovation: Invention as Frustrated Combinatorial Search on a Rugged Value Landscape

We propose that invention has the mathematical structure of a spin glass: an invention is a subset of reusable building blocks, its value is a mixed-sign frustrated quadratic form over those blocks, and a breakthrough is an escape to a deeper basin of that disordered energy landscape. From this single mapping we derive seven falsifiable laws of innovation: glassiness, bursty (avalanche) breakthroughs, heavy-tailed impact, a recombination degree law, a thermodynamics of search, an emergence (drive × self-modification) condition, and constant-work reachability, each of which inherits a result already proven for the disordered-spin model by the SpinForge program (σ=ln2 near-optimal geometry, the Parisi degree law, the dynamical Second Law, the Emergence Equation). We demonstrate the laws in silico on a recombination landscape run on the SpinForge GPU engine and we test the theory empirically on real bibliometric data: 12,000 OpenAlex articles (4 fields, 2010–2016), with citation impact as the observable. The result is deliberately reported on a four-rung honesty ladder, formal-mapping / proven-for-model / in-silico-measured / empirically-tested, and we preserve the key honest negative: the original conjecture that the heavy tail of impact is the static extreme-value statistics of landscape basin depths is refuted, the static recombination landscape produces Gaussian design values (kurtosis ≈ 3.0). The refuted law forces a sharp refinement: the landscape decides which designs can win; the dynamics (cumulative advantage on that substrate) decides how unequal the winnings are. On real data the refined heavy-tail law is confirmed, impact is power-law in all four fields with exponent α = 2.48 (CS), 2.52 (mathematics), 2.97 (medicine), 2.97 (physics), and a recombination-breadth interior optimum is supported in 3 of 4 fields. We do not assert this as established social science. The contribution is the falsifiable structure: innovation has the form of a spin glass, that form makes specific quantitative predictions, and the predictions are testable today.

[Request the full paper by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20paper%3A%20A%20Spin-Glass%20Theory%20of%20Innovation%3A%20Invention%20as%20Frustrated%20Combinatorial%20Search%20on%20a%20Rugged%20Value%20Landscape%20%28P15%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

P16

### Ghost Collider: A Model-Independent Physics-Discovery Engine on Real CMS Open Data

The frontier in collider physics is increasingly one of inference rather than collision energy: petabytes of public open data already encode physics that has never been exhaustively re-analyzed. We present Ghost Collider, a GPU-ready, model-independent discovery engine that reanalyzes real CMS Open Data and binds every claim to a tamper-evident reproducibility certificate. On 100,000 real 2010 CMS di-muon events (record 545, DOI 10.7483/OPENDATA.CMS.CB8H.MFFA) the engine, with no resonance model supplied, blindly rediscovers three Standard-Model resonances: J/ψ at 3.093 GeV (0.13% from PDG, 135σ local), Υ(1S) at 9.445 GeV (0.16%, 42σ), and Z at 90.76 GeV (0.47%, 92σ). From the eight raw four-momentum components alone, no physics prior, a sparse symbolic regressor recovers the relativistic invariant-mass law with the Minkowski signature (+,−,−,−) at held-out R² = 1.000000. A model-independent anomaly stack (dense autoencoder + RealNVP normalizing flow) concentrates its flagged events in the rare high-mass Drell–Yan tail (flagged-median 32.8 GeV vs 12.4 GeV bulk) and is calibrated by labelled signal injection (0 injected  no false peak; 1000 injected  28.7σ, yield recovered to ~1%). A selected dimuon trigger compiles to both a CUDA kernel and synthesizable Verilog RTL, and the RTL is verified bit-exact against the float selection through real iverilog simulation (0 mismatches). All four pillars are reproduced here from the repository's certificates and re-runs. We are explicit about scope: the resonances and the law are real-data results; no new physics is claimed in this dataset, the correct, honest null, and the injection is the only synthetic input, always labelled as a calibration.

[Request the full paper by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20paper%3A%20Ghost%20Collider%3A%20A%20Model-Independent%20Physics-Discovery%20Engine%20on%20Real%20CMS%20Open%20Data%20%28P16%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

P18

### SAT-Based Combinational Equivalence Checking for a Native EDA Flow: a From-Scratch CDCL Solver with AIG and Tseitin Encoding

A logic-synthesis or timing-restructuring transform is only safe if the transformed circuit computes the same Boolean function as the original. We present the combinational equivalence checker (CEC) used inside the SpinForge EDA flow: a from-scratch CDCL SAT solver, an And-Inverter-Graph (AIG) circuit representation with O(1) structural hashing, and a Tseitin CNF encoding that builds a miter between two circuits. The miter is satisfiable if and only if some input distinguishes the two circuits; proving the miter UNSAT is a sound, complete proof of equivalence. The implementation is pure CPU Rust, we are explicit that the CDCL search is not GPU-accelerated, in contrast to the placement, routing, static-timing-analysis, and placement-DRC stages of the surrounding flow, which run on CUDA. The checker is wired into the flow as a gate on depth-reducing restructuring: a candidate netlist is accepted only if it is both shallower and proven equivalent by the SAT checker, otherwise the baseline is kept, so no transform can introduce a logic regression. We also document a corrected XOR-construction bug (the gate was computing XNOR, which inverts the miter polarity and would have silently passed non-equivalent circuits / failed equivalent ones); the corrected construction is exercised by the test suite. The forge-formal crate passes 31/31 unit tests (14 SAT/CEC-specific, run on CPU in well under one second), including UNSAT proofs of the pigeonhole principle PHP(3,2), SAT model extraction, AND-commutativity, De Morgan's law, and associativity (balanced-vs-linear AND-tree) equivalence.

[Request the full paper by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20paper%3A%20SAT-Based%20Combinational%20Equivalence%20Checking%20for%20a%20Native%20EDA%20Flow%3A%20a%20From-Scratch%20CDCL%20Solver%20with%20AIG%20and%20Tseitin%20Encoding%20%28P18%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

P20

### A Sharp Recovery Threshold for Planted Partitions in Sparse Max-Cut

The SpinForge geometry program (P0) and structure atlas (P6) characterize random sparse Max-Cut, whose near-optimal solutions are orthogonal (σ=ln2) and carry no recoverable structure. Here we ask the complementary question: when a graph contains a planted partition of signal strength f (a fraction f of edges placed to respect a hidden ground-truth assignment σ*, the remaining 1−f uniformly random), at what f does the optimizer recover σ*? We find a sharp recovery threshold that sharpens with system size. Solving for the maximum cut and measuring the gauge-fixed overlap with the planted assignment, the overlap stays at the no-signal null (|⟨s·σ*⟩|/N ≈ 0.01–0.14) for f ≤ 0.5 and jumps to near-perfect recovery (≈0.95–1.00) by f = 0.75; the structure-ratio of the solution against the max-entropy null rises from ≈1.0 to 8.1× at N=2000 and 15.8× at N=8000 across that step: i.e. the transition is N-sharpening, consistent with a sharp threshold f_c in the large-N limit. A finer GPU sweep (N up to 128,000) localizes f_c ≈ 0.49, essentially N-independent, while below f_c the overlap decays toward zero with N and above it the recovery curves collapse, the recovery boundary steepens into a step as N∞. This is the structured counterpart to P0's random-glass result and a concrete recovery boundary the structure atlas (P6) can be calibrated against.

[Request the full paper by email](https://spin-forge.com/contact?product=portfolio&brief=Please%20send%20the%20full%20paper%3A%20A%20Sharp%20Recovery%20Threshold%20for%20Planted%20Partitions%20in%20Sparse%20Max-Cut%20%28P20%29.%0A%0AOur%20organization%20and%20intended%20use%3A%0A)

Results describe the stated inputs, hardware and conditions and are not a guarantee of results in your environment. See the [Terms of Use](https://spin-forge.com/terms).