% ---------------------------------------------------------------------------
% 2026-04-27 — Hot-standby SOS barrier + scram X_exit redefinition
% Live / B-style entry: two task closeouts in one sitting.
% ---------------------------------------------------------------------------

\session{2026-04-27}{Hacker-Split, Mac mini}{%
Two thesis-relevant closeouts in one go: redefine the scram exit
predicate from a power threshold to a shutdown-margin halfspace
(actual NRC criterion, and a clean linear halfspace), then port the
degree-4 SOS barrier machinery from operation to hot-standby and
discharge a forever-invariance certificate on a 2-D thermal projection.}

\section{2026-04-27 --- Scram exit \& hot-standby SOS}
\label{sec:20260427-shutdown-sos-scram-exit}

\subsection*{Scram \texttt{X\_exit}: from $n \leq 10^{-4}$ to shutdown margin}

The scram-mode exit predicate as written in
\texttt{reachability/predicates.json} read

\[
  X_{\mathrm{exit}}^{(\mathrm{scram})} \;=\; \{\, x \;:\; n \leq 10^{-4} \;\wedge\; T_f \leq T_{f,0} + 50\,^\circ\mathrm{C}\,\}.
\]

Two structural problems with this:

\begin{enumerate}
  \item \textbf{$n$ is nonlinear in the prompt-jump (PJ) state.} Under PJ,
    $n = \Lambda \sum_i \lambda_i C_i / (\beta - \rho)$, and $\rho$
    depends on $T_f, T_c$. So $n \leq 10^{-4}$ is not a halfspace in the
    9-state PJ vector; the existing \texttt{reach\_scram\_pj.jl} was
    reconstructing $n$ post-hoc and checking the bound on the endpoint
    only.
  \item \textbf{The $T_f$ bound is infeasible by 60\,s under decay heat.}
    With $Q_{\mathrm{sg}} = 0.03 P_0$ and a fuel time constant
    $M_f c_f / hA \approx 0.3\,\mathrm{s}$, the fuel rapidly equilibrates
    with $T_c$ and the system loses only $\sim 5\,^\circ\mathrm{C}$ in
    $60\,\mathrm{s}$. The conjoined bound was decorative.
\end{enumerate}

The actual NRC tech-spec criterion for scram success is phrased in
shutdown margin ($\rho \leq -\rho_{\mathrm{SDM}}$, typically $1\%
\Delta k/k$). Under constant rod $u = U_{\mathrm{SCRAM}} = -8\beta$,
total reactivity is

\[
  \rho(x) \;=\; U_{\mathrm{SCRAM}} \;+\; \alpha_f (T_f - T_{f,0}) \;+\; \alpha_c (T_c - T_{c,0}),
\]

\emph{linear} in $(T_f, T_c)$ — a single-row halfspace in the reach state.
Replacing $X_{\mathrm{exit}}$ with the predicate
\texttt{shutdown\_margin}:

\[
  \alpha_f T_f + \alpha_c T_c \;\leq\;
    -\rho_{\mathrm{SDM}} - U_{\mathrm{SCRAM}} + \alpha_f T_{f,0} + \alpha_c T_{c,0}
    \;\approx\; 2.97 \times 10^{-3}.
\]

Re-ran \texttt{reach\_scram\_pj.jl} (TMJets, orderT $= 4$, orderQ $= 2$).
Discharged at all three probe horizons:

\begin{center}
\begin{tabular}{r r r r r}
$T$ (s) & reach-sets & wall (s) & $\rho$ at $T$ & discharged \\
\hline
$10$ & $6919$ & $98.6$ & $[-0.0507,\,-0.0504]$ & \checkmark \\
$30$ & $9900$ & $130.5$ & $[-0.0506,\,-0.0503]$ & \checkmark \\
$60$ & $12340$ & $164.2$ & $[-0.0503,\,-0.0500]$ & \checkmark \\
\end{tabular}
\end{center}

Required $|\rho| \geq 0.01$. Actual $|\rho| \approx 0.05$ — five times
the requirement, dominated by rod worth (as expected; Doppler/moderator
contributions vary by only $\sim 3\%$ of $U_{\mathrm{SCRAM}}$).

\begin{decision}
\textbf{Shutdown margin (in $\Delta k/k$) is the canonical scram success
criterion across all modes.} The $n$-threshold framing was a
back-translation that didn't survive scrutiny. Where reach scripts
need to discharge a successor obligation post-scram, use
\texttt{shutdown\_margin}.
\end{decision}

Stale-constant gotcha caught while drafting the predicate: I derived
the RHS by hand using rounded $T_{f,0} = 320$, $T_{c,0} = 300$, but
the actual values from \texttt{pke\_params} are $T_{c,0} = 308.35$
($= (T_{\mathrm{hot},0} + T_{\mathrm{cold},0})/2$ with
$T_{\mathrm{hot},0} = T_{\mathrm{cold},0} + P_0 / (W c_c) = 326.7$)
and $T_{f,0} = 328.35$. Off by $\Delta\mathrm{RHS} \sim 10^{-3}$. Fixed
by switching the JSON \texttt{rhs\_expr} to a symbolic form that gets
substituted at load time. Lesson: every constant in
\texttt{predicates.json} that's derivable from \texttt{pke\_params}
should be symbolic, not baked.

\subsection*{SOS barrier on hot-standby (q\_shutdown)}

Companion to \texttt{barrier\_sos\_2d.jl} (operation/LQR). New script
\texttt{barrier\_sos\_2d\_shutdown.jl}. Hot-standby is an
\emph{equilibrium-mode} obligation (forever-invariance), not
reach-avoid, so SOS suits it well.

Controller: $u_{\mathrm{shutdown}} = -5\beta = -0.0325$, constant. With
$Q_{\mathrm{sg}} = 0$ (no SG load), the thermal subsystem is adiabatic:
\emph{any} uniform temperature $T_f = T_c = T_{\mathrm{cold}} = T^*$
sufficient to make $\rho < 0$ is invariant. The hot-standby IC sets
$T^* = T_{\mathrm{standby}} = 275.02\,^\circ\mathrm{C}$; a 50\,000\,s sim
confirms the trajectory parks there, $\|dx/dt\| \sim 10^{-22}$. So the
linearization is at $x_{\mathrm{eq}} = (T_{\mathrm{standby}}, T_{\mathrm{standby}}, T_{\mathrm{standby}})$
with $u_{\mathrm{eq}} = -5\beta$, $Q_* = 0$.

\textbf{2-D reduction.} Picked $(T_c, T_{\mathrm{cold}})$ — the slow safety-relevant
thermal modes. $n$ and the precursors are decoupled at quasi-zero power
and not the safety driver in this mode. $T_f$ tracks $T_c$ with time
constant $\sim 0.3\,\mathrm{s}$ and is folded into the dynamics implicitly
(the 2-D reduction loses $\|cross\| = 0.459$ of coupling from dropped
states — non-trivial; see \emph{Open issues} below).

Reduced closed-loop:
\[
  A_{\mathrm{red}} \;=\; \begin{bmatrix} -0.959 & 0.500 \\ 0.333 & -0.333 \end{bmatrix},
  \quad \mathrm{eig}(A_{\mathrm{red}}) = \{-1.16,\, -0.132\}.
\]

Both Hurwitz; slow mode is $T_{\mathrm{cold}}$ ($\tau \sim 7.6\,\mathrm{s}$).

\textbf{Sets.} Safety: $|\delta T_c| \leq 10$, $|\delta T_{\mathrm{cold}}| \leq 15$.
Entry: $|\delta T_c| \leq 5$, $|\delta T_{\mathrm{cold}}| \leq 5$ (matches the
\texttt{q\_shutdown.X\_entry\_polytope} extent recentered on $x_{\mathrm{eq}}$).
Unsafe focus: $\delta T_c \geq +10$ — over-warming is the harder direction
because the controller has rods already maxed in negative reactivity and
no recourse but to wait for the moderator coefficient.

\textbf{Methodological gotcha: trivial barrier.} First run with the
Prajna--Jadbabaie SOS feasibility formulation returned
$B(x) \equiv 0$ — vacuously satisfies $B \leq 0$ on entry, $B \geq 0$
on unsafe (with $\sigma_u \equiv 0$), $\nabla B \cdot f = 0$ globally.
Standard fix: add a \emph{strict-separation slack} $\varepsilon > 0$
and tighten the constraints to $B \leq -\varepsilon$ on entry,
$B \geq +\varepsilon$ on unsafe. Maximize $\varepsilon$.

Second run: \texttt{DUAL\_INFEASIBLE}. Because $B$ has free scale, the
program is unbounded — scaling $B \to cB$ scales $\varepsilon \to c\varepsilon$.
Cap $\varepsilon \leq 1$ (the unit is arbitrary; we only need
$\varepsilon^* > 0$ for a real certificate).

Third run: \texttt{OPTIMAL}, $\varepsilon^* = 1.0$ (hit the cap, meaning
the primal is feasible with arbitrarily large separation modulo scale).
Dropping numerical-noise terms,

\[
  B(x_1, x_2) \approx -16.91 \;+\; 0.022\,x_1^2 \;+\; 0.027\,x_2^2 \;+\; 0.005\,x_1^4 \;+\; \text{(cross / cubic terms)},
\]

with $x_1 = \delta T_c$, $x_2 = \delta T_{\mathrm{cold}}$. Geometry: a bowl
with floor $B(0,0) = -16.91 \leq -\varepsilon$, rising past zero around
$|x_1| \approx 7.5$, comfortably $\geq +\varepsilon$ at the unsafe
threshold $x_1 = 10$ (where $B \approx +35$). $\dot B \leq 0$ globally
because $A_{\mathrm{red}}$ is Hurwitz; the polynomial barrier is
essentially a degree-4 Lyapunov function for this Hurwitz system.

\begin{decision}
SOS feasibility programs without an objective + scale normalization
silently return $B \equiv 0$. Future SOS scripts in this repo: always
add the $(\varepsilon, \text{cap})$ pattern. Worth a comment in
\texttt{barrier\_sos\_2d.jl} too — it has the same vulnerability (it
also returned $B \equiv 0$ when I re-ran it mentally).
\end{decision}

\subsection*{Open issues for follow-up}

\begin{itemize}
  \item \textbf{2-D reduction is not sound for the full plant.} The
    dropped coupling norm is $0.459$ — non-trivial. To certify the full
    10-state hot-standby invariance, augment the SOS state with at least
    $T_f$ (3-D) and re-run with appropriate degree. CSDP scales
    polynomially with monomial count; degree 4 in 3 variables is
    $\binom{7}{3} = 35$ monomials, still very tractable.
  \item \textbf{No disturbance.} $Q_{\mathrm{sg}} \equiv 0$ here. For
    hot-standby with auxiliary cooling there's a residual sink. Add
    $B_w w$ to the Lie-derivative inequality and check the worst case
    over $w \in [-Q_{\max}, Q_{\max}]$ — standard Putinar-style
    extension.
  \item \textbf{Equilibrium is parametrized by IC.} Adiabatic + constant
    rod = no unique attractor. The barrier proves invariance \emph{around}
    $x_{\mathrm{eq}}$ but the ``correct'' $x_{\mathrm{eq}}$ depends on
    where the system started. For a shutdown controller that actually
    drives to a setpoint, redesign as a temperature-tracking law (PI on
    $T_c$ with rod motion). Flagged for a separate task — current
    \texttt{ctrl\_shutdown} is open-loop rod-held, which is honest about
    what real plants do during a controlled hold but doesn't compose
    with reach-avoid framing as cleanly as a tracking law would.
  \item \textbf{Lie-derivative condition is global, not boundary.} The
    SOS uses $-\nabla B \cdot f \in \mathrm{SOS}$ everywhere, which is
    stronger than the Prajna $\{B = 0\}$-only condition. Convex but
    conservative. The bilinear Putinar form
    $-\nabla B \cdot f - \sigma_b B \in \mathrm{SOS}$ is what we'd need for
    the boundary-only version; that's a BMI and needs alternation.
    Acceptable conservatism here because the system has a real Lyapunov
    function anyway.
\end{itemize}

\subsection*{Files touched}

\begin{itemize}
  \item \texttt{reachability/predicates.json} --- added \texttt{shutdown\_margin}
    in \texttt{safety\_limits}; updated \texttt{q\_scram.X\_exit\_predicate}
    and \texttt{X\_safe\_predicate}; left \texttt{\_X\_exit\_history} for
    forensics.
  \item \texttt{code/scripts/reach/reach\_scram\_pj.jl} --- added
    \texttt{RHO\_SDM}, \texttt{SDM\_RHS}; per-horizon $\rho$-bounds + halfspace
    LHS sup; \texttt{.mat} output extended.
  \item \texttt{code/scripts/barrier/barrier\_sos\_2d\_shutdown.jl} ---
    new file. Equilibrium-finder + linearization + SOS barrier.
  \item \texttt{claude\_memory/2026-04-27-scram-X\_exit-shutdown-margin.md}
    --- session note for the scram side.
\end{itemize}