Expand description
Settled-answer replay — the residual certificate for physics-solved linear systems.
The trust covenant: the physical solver (or its behavioral model) is UNTRUSTED by
construction — no trajectory, no convergence argument, no producer arithmetic is believed.
The claim is neutral data: A, b, the settled readout x̂, and a declared ∞-norm bound
ε — all exact rationals. check_relax_claim re-multiplies r = A·x̂ − b with THIS
crate’s own exact arithmetic (crate::linalg::matvec) and demands ‖r‖∞ ≤ ε,
component by component. Fail-closed: a malformed shape, a negative ε, or an empty system
is a rejection, never a pass.
The same mathematics will judge the thermal map (G·ΔT = P) — one residual checker,
two physical planes.
Structs§
- Ising
Claim - The Ising candidate’s neutral claim: the instance, the returned spins, the claimed exact energy, and the claimed 1-flip stability verdict. BY DESIGN there is no optimality field — a soft-spin settle returns an attractor, and this type cannot express more.
- Minimize
Claim - The neutral claim a convex-quadratic settle emits:
minimize ½xᵀQx + bᵀx, the settled readout, a claimed strong-convexity parameter, and a claimed suboptimality bound. Everything exact; nothing trusted. - Relax
Claim - The neutral claim a settling run emits. Everything exact; nothing trusted.
Functions§
- check_
ising_ claim - Judge an Ising candidate: recompute the exact energy and the exact 1-flip stability with this crate’s own arithmetic and demand agreement with BOTH claims. Fail-closed on shape garbage (asymmetry, nonzero diagonal, non-±1 spins).
- check_
minimize_ claim - Judge a minimize claim by THEOREM, not trust: for symmetric Q with spectrum ≥ μ > 0
(verified against the exact Gershgorin row bound, which this checker recomputes itself),
strong convexity gives
f(x̂) − f* ≤ ‖∇f(x̂)‖² / (2μ)— the gradient is re-derived with this crate’s own arithmetic and the inequality checked exactly. Fail-closed throughout. - check_
relax_ claim - THE judge. Recomputes the residual with this crate’s own exact multiplication and checks the declared bound. Rejects malformed claims outright.