# 2026-04-28 — Path 1 sketch: SOS on PJ polynomial dynamics **Status:** Sketch only. **Do not run yet.** Dane wants this saved for an overnight session. Closing the soundness gap on operation/hot-standby barriers — moving from linearized SOS to nonlinear-SOS-with-PJ. ## The obstacle Dynamics in `pke_th_rhs_pj.jl` are *rational*, not polynomial, because of the prompt-jump algebraic relation: n(x) = Λ · Σ λᵢ Cᵢ / (β - ρ(x)) with `ρ(x) = u + α_f(T_f - T_f0) + α_c(T_c - T_c0)` affine. `SumOfSquares.jl` only handles polynomials. ## The trick: multiply through by D(x) = β - ρ(x) `D(x)` is affine in `(T_f, T_c)` and strictly positive on the operating envelope (this is exactly the `prompt_critical_margin_*` predicate — already in `predicates.json`). For each PJ state-equation `dxᵢ/dt = fᵢ(x)/D(x) + polynomial`, multiply: D(x) · dxᵢ/dt = fᵢ(x) + D(x) · polynomial The right-hand side is now polynomial. The Lyapunov/barrier condition `dB/dt ≤ 0` becomes (multiplying by `D > 0`): D(x) · ∇B(x) · f(x) ≤ 0 ← polynomial inequality which `SumOfSquares` can handle. Soundness preserved because `D > 0` on the operating envelope (and we discharge that as a separate predicate, already done in current SOS work via the `prompt_critical_margin_*` halfspace). ## Polynomial RHS spelled out PJ state vector: `x = [C₁..C₆, T_f, T_c, T_cold]`, `u` constant per mode. Define `S = Σⱼ λⱼ Cⱼ` (linear in C). Then: D · dCᵢ/dt = βᵢ S - λᵢ Cᵢ D ← deg 2 D · dT_f/dt = (P₀ Λ S - hA (T_f - T_c) D) / (M_f c_f) ← deg 2 D · dT_c/dt = ((hA (T_f - T_c) - 2 W c_c (T_c - T_cold)) D) / (M_c c_c) ← deg 2 D · dT_cold/dt = ((2 W c_c (T_c - T_cold) - Q_sg) D) / (M_sg c_c) ← deg 2 All right-hand sides are degree ≤ 2 in (C, T_f, T_c, T_cold). With B a degree-4 polynomial, the SOS Lie condition `D ∇B · f` is degree ≤ 4 + 1 + 2 = 7. Multipliers degree 2. SDP size scales with monomial count of the relevant degrees in the relevant variables. ## Dimensionality / tractability Full 9-state SOS, degree 4: `C(9+4, 4) = 715` monomials. Big SDP but tractable on modern CSDP/MOSEK with `chordal sparsity`. May need MOSEK rather than CSDP for solver robustness at this scale. Realistic first attempt: **3D projection on (T_f, T_c, T_cold)** with the precursor dynamics treated as bounded uncertainty. Degree 4 in 3 vars = 35 monomials — same scale as the existing 2D scripts. The precursors' contribution to thermal dynamics enters only through `S = Σ λⱼ Cⱼ` in the `T_f` equation, and `S` is bounded on the reach envelope (we have intervals from prior reach runs). Treat `S` as `[S_lo, S_hi]` parametric uncertainty in the SOS — clean Putinar multiplier on `[S - S_lo, S_hi - S]`. This is the pragmatic path: 3D polynomial SOS with bounded `S`. Sound for the nonlinear PJ plant on the operating envelope where `D > 0` and `S ∈ [S_lo, S_hi]`. ## Session plan for the overnight run 1. Add `D(x)` and `S(x)` symbolic primitives to `sos_barrier.jl`. 2. Extend `solve_sos_barrier_2d` → `solve_sos_barrier_nd` with parametric-uncertainty multipliers (Putinar on `S ∈ [S_lo, S_hi]`). 3. Compute `S` envelope from `reach_operation_result.mat` (already exists for operation) and from a long shutdown sim for hot-standby. 4. Build `barrier_sos_3d_pj_operation.jl`: - 3D state `(δT_f, δT_c, δT_cold)` around operation equilibrium - Polynomial RHS via multiply-through - `D > 0` and `S ∈ [S_lo, S_hi]` as Putinar safety multipliers - Same X_entry, X_unsafe as current 2D operation barrier - Run, compare to linearized result. 5. Build `barrier_sos_3d_pj_shutdown.jl` — analogous. 6. If both succeed, write a journal entry making the soundness claim explicit. The new barrier is sound for the PJ-reduced nonlinear plant on `{D > 0} ∩ {S ∈ [S_lo, S_hi]}`. The PJ reduction itself has the Tikhonov error bound (already worked out 2026-04-21). Composing these gives a sound certificate for the *full* nonlinear plant up to the (small, characterized) PJ error. ## Subtleties / things that might bite - **CSDP may not converge at degree 4 in 3D with multiple Putinar multipliers.** If so, switch to MOSEK (license setup needed) or drop to degree 2 with iterative refinement. - **The multiply-through is only valid where D > 0.** If the SOS finds a B that's only valid on a region where the SOS solver's certificate space includes D ≤ 0 points, the result is bogus. Mitigate: use `D` as a Putinar multiplier on the entry/safe sets (so SOS only reasons over `{D > 0}`). - **Precursor coupling not certified.** The 3D projection drops the 6 precursor states. They're bounded in `S` but their individual dynamics aren't certified. If the SOS proves invariance of `(T_f, T_c, T_cold)` while precursors drift outside `[S_lo, S_hi]`, the certificate is invalid. Need to either (a) certify precursor bounds separately as a forward invariant, or (b) include precursor states in the SOS (back to 9D). - **Connection to Tikhonov.** The PJ reduction has error `O(Λ) = O(10⁻⁴)`. Composing PJ-validity-guaranteed barrier + PJ Tikhonov bound = sound certificate for the full plant, modulo the (small) PJ error. Worth working out the full chain rigorously. ## Files that would change - `code/src/sos_barrier.jl` — generalize to ND + parametric uncertainty - `code/scripts/barrier/barrier_sos_3d_pj_operation.jl` — new - `code/scripts/barrier/barrier_sos_3d_pj_shutdown.jl` — new - `journal/entries/YYYY-MM-DD-pj-sos-soundness.tex` — new - `code/CLAUDE.md` — update soundness claim section ## Estimated time 8–12 hours focused work. Realistic overnight run if the SDP is well-conditioned. If MOSEK setup eats time, push to a second night.