# Reproduction — Joseph covariance update — PSD for any gain, 4 DSPs on silicon

The numerically-robust covariance step P+ = (I-K)P(I-K)^T + K R K^T — four 2x2 matrix products — time-multiplexed through ONE shared MAC. Proven to stay PSD for any gain (so recursing it is safe), and the whole four-product update costs 4 DSP48s on real fabric at 100 MHz (vs ~128 unrolled).

| stage | artifact | tier |
|---|---|---|
| emit | 14 compiled targets | LOCAL |
| proof | `kalman2_joseph_psd` — P+ = (I-K)P(I-K)^T + K R K^T stays symmetric positive-semidefinite for ANY gain K (sorryAx-free) | TOOLCHAIN — Lean axiom trail |
| proof | `fxerr_dot2_fullwidth` — the full-width scheduled dot's forward error is a single rounding (<= 2^-FRAC per dot) (sorryAx-free) | TOOLCHAIN — Lean axiom trail |
| simulate | P+ stays PSD over 500 random (P,R,K) = all PSD = PSD (✓) | LOCAL — Q16.16 model, bit-exact to the emitted RTL |
| simulate | P+ off-diagonal symmetry (max |P01-P10|) = 6.10e-05 < 1e-3 (✓) | LOCAL — Q16.16 model, bit-exact to the emitted RTL |
| silicon | `joseph2_update` — WNS +1.350 ns @ 100 MHz on Arty A7-100T | REPLAY |

**Proved, simulated, and on silicon.** The Joseph form is PSD-preserving for any gain (kalman2_joseph_psd, sorryAx-free) — the property that makes recursing the covariance safe — and the whole four-product update runs in 4 DSP48s at 100 MHz. The full-width dot's forward-error bound is re-derived against the scheduled accumulation order (fxerr_dot2_fullwidth, proven); the deployed per-product order is bit-identical to the unrolled matmul. The shared scheduler/operand-mux control is verified bit-exact (Verilator + silicon), not proven — see docs/streaming_kalman_filter.md §4b.

Silicon evidence (REPLAY): `monogate-research/electronics_intake/joseph_arty/evidence/FINDINGS.md`.