Expand description
The relaxation lane — continuous-time state evolution as a compute primitive
(Solve A·x = b by settling).
The four-fabric thesis, mechanized at its first rung: the SAME Sum tiles that compute
results in the dataflow lane here generate FORCES — ẋ = b − A·x is one weighted-sum tile
per state variable, and capacitor state integrates it. Gradient flow on the strongly convex
quadratic ½xᵀAx − bᵀx converges for admissible A (symmetric + positive definite;
Hirsch–Smale, gradient systems), and the admission gate PROVES membership over exact ℚ —
strict diagonal dominance with a positive diagonal (Gershgorin ⇒ SPD for symmetric A) or
all leading principal minors positive (Sylvester’s criterion). Anything else refuses TYPED.
The trust covenant: the settle (here, a deterministic explicit-Euler behavioral model with
an optional fixed-seed noise injection — the future chip replaces it wholesale) is
UNTRUSTED. Only the settled answer counts: the readout is ADC-quantized on the target’s
converter grid, the exact residual r = A·x̂ − b is computed in ℚ, and the emitted
RelaxClaim is judged by the INDEPENDENT logicaffeine_proof::relax_replay checker.
Settling time is a performance knob, not a correctness one: an under-settled run exceeds
the demanded budget and refuses — it cannot emit a certificate it does not meet.
Structs§
- DynSystem
- A configured dynamical system: one force tile per state variable, built from the EXISTING
tile vocabulary (
AnalogCell::Sum— the tiles stop computing results and start generating the forces that move state). - Ising
Outcome - One Ising candidate: an attractor of the soft-spin flow, certified for WHAT IT IS — its exact energy and its exact 1-flip stability — and nothing more (the claim type has no optimality field to lie with).
- Minimize
Outcome - One settled, certified quadratic minimization.
- Relax
Outcome - One settled, certified solve.
- Settle
Opts - The deterministic settle knobs.
eps_requiredis the demanded certificate budget — the hard admission line for the emitted claim;noise_amp/seedinject a fixed-seed disturbance per step (the model’s stand-in for the physical noise floor, and R3’s future annealing ramp).
Functions§
- gradient_
flow_ system - Build the gradient-flow force network for
ẋ = b − A·x. Purely structural — admission issolve_by_settling’s job. - ising_
by_ soft_ spin - The R3 attempt:
minimize H(s) = −Σ J_ij·s_i·s_j − Σ h_i·s_iby SOFT-SPIN relaxation (Hopfield 1984): continuous statesx ∈ [−1,1]ⁿfollowẋ = −x + tanh(β·(J·x + h))with the annealing schedule as a NOISE-AMPLITUDE RAMP (opts.noise_ampdecaying linearly to zero — the noise floor as a resource) while β ramps up. The trajectory and the tanh live in the UNTRUSTED model tier; the readoutsign(x̂)is certified digitally and exactly: recomputed energy and 1-flip stability, judged byproof::relax_replay::check_ising_claim. A candidate that is not even 1-flip stable is polished greedily (each flip strictly lowers H — a certified descent, not a search). - minimize_
by_ settling minimize ½xᵀQx + bᵀxby settlingẋ = −(Q·x + b)— the SAME force network with the signs flipped (the tiles generate the negative gradient). The admission gate is R1’s; the CERTIFICATE is R2’s theorem: for spectrum ≥ μ > 0 (exact Gershgorin row bound over ℚ),f(x̂) − f* ≤ ‖∇f(x̂)‖²/(2μ)— a gradient residual becomes a distance-to-optimum bound.Candidatesemantics: the bound is the claim; no optimality field exists to lie with.- solve_
by_ settling Solve A·x = bby settling the gradient-flow system, fail-closed end to end.- with_
penalty - Fold one soft equality constraint
gᵀx = cinto the quadratic as a virtual spring:f(x) + λ(gᵀx − c)²⇒Q += 2λ·ggᵀ,b −= 2λc·g. Stiffer springs pull the settled answer closer to the constraint surface — the quadratic-penalty form (primal-dual dynamics are the ledgered future).