Skip to main content

Module dynamics

Module dynamics 

Source
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).
IsingOutcome
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).
MinimizeOutcome
One settled, certified quadratic minimization.
RelaxOutcome
One settled, certified solve.
SettleOpts
The deterministic settle knobs. eps_required is the demanded certificate budget — the hard admission line for the emitted claim; noise_amp/seed inject 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 is solve_by_settling’s job.
ising_by_soft_spin
The R3 attempt: minimize H(s) = −Σ J_ij·s_i·s_j − Σ h_i·s_i by SOFT-SPIN relaxation (Hopfield 1984): continuous states x ∈ [−1,1]ⁿ follow ẋ = −x + tanh(β·(J·x + h)) with the annealing schedule as a NOISE-AMPLITUDE RAMP (opts.noise_amp decaying linearly to zero — the noise floor as a resource) while β ramps up. The trajectory and the tanh live in the UNTRUSTED model tier; the readout sign(x̂) is certified digitally and exactly: recomputed energy and 1-flip stability, judged by proof::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ᵀx by 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. Candidate semantics: the bound is the claim; no optimality field exists to lie with.
solve_by_settling
Solve A·x = b by settling the gradient-flow system, fail-closed end to end.
with_penalty
Fold one soft equality constraint gᵀx = c into 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).