c5133401e0
Multi-session work bundle on a draft branch. Splits into a clean
sequence of commits later; pushed here so it isn't lost on a reboot.
Reach work
- code/scripts/reach/reach_scram_pj.jl: shutdown_margin halfspace
X_exit (replaces "n <= 1e-4 AND T_f bound" framing); per-step
envelope extraction added.
- code/scripts/reach/reach_scram_pj_fat.jl: per-step envelope
extraction added; shutdown_margin discharge logic mirrored from the
tight scram script. 3 probes (10/30/60s) all discharge from the
fat union polytope.
- code/scripts/reach/reach_scram_full_fat.jl (NEW): full nonlinear
PKE scram reach with fat entry. Hits the stiffness wall at
~1.5 s plant time as expected; saves NaN-tolerant per-step
envelopes. Demonstrates concretely why PJ is the right tool for
the longer-horizon proof.
- code/scripts/reach/reach_heatup_pj.jl: T_REF_START_C constant
(entry-conditioned ramp) replaces T_STANDBY-init that was making
the FL controller command cooling at t=0. Per-step extraction
already in place.
- code/configs/heatup/tight.toml: bumped maxsteps; probe horizon
parameterized.
Hot-standby SOS barrier
- code/scripts/barrier/barrier_sos_2d_shutdown.jl (NEW): mirrors the
operation SOS machinery on the hot-standby thermal projection.
Includes the eps-slack pattern (so feasibility doesn't silently
collapse to B == 0).
- code/scripts/barrier/barrier_sos_2d.jl: refactored to use the same
helper.
- code/src/sos_barrier.jl (NEW): solve_sos_barrier_2d helper module
factoring out the SOS construction; eps-slack with eps_cap=1.0 to
avoid unbounded primal.
Library
- code/src/pke_states.jl (NEW): single source of truth for canonical
initial-condition vectors per DRC mode (op, shutdown, heatup) keyed
off plant + predicates.
- code/scripts/sim/{main_mode_sweep,validate_pj}.jl, code/CLAUDE.md:
migrated to pke_states.
Predicates + invariants
- reachability/predicates.json: new shutdown_margin predicate (1%
dk/k tech-spec floor, expressed as alpha_f*T_f + alpha_c*T_c
halfspace). Used as scram X_exit.
Plot script
- code/scripts/plot/plot_reach_tubes.jl: plot_tubes_scram_pj() with
variant=:fat|:tight knob; plot_tubes_scram_full() for full-PKE
3-panel (T_c, T_f, rho); plot_tubes_heatup_pj() reads results/
not reachability/.
Journal + memory
- journal/entries/2026-04-27-shutdown-sos-and-scram-X_exit.tex (NEW):
long-form entry on the SOS hot-standby barrier and the scram X_exit
refactor.
- journal/journal.tex: input chain updated.
- claude_memory/ — three new session notes:
* 2026-04-27-scram-X_exit-shutdown-margin.md
* 2026-04-28-DICE-2026-conference-intel.md (people, sessions,
strategic notes for the May 12 talk)
* 2026-04-28-path1-sos-pj-sketch.md (sketch of nonlinear-SOS via
polynomial multiply-through; saved for an overnight session)
Docs
- docs/model_cheatsheet.md (NEW): one-page reference of state vector,
dynamics, constants, modes, predicates, sanity numbers — the talk
prep cheatsheet Dane asked for.
- docs/figures/reach_*_tubes.png: regenerated with the new mat data.
- presentations/prelim-presentation/outline.md: revised arc per the
April-28 review pass (cuts: Lyapunov-fails standalone slide,
operation-tube standalone slide, SOS standalone; adds: scopes-of-
control framing, scram on the headline result slide).
- app/predicate_explorer.jl: minor.
Hacker-Split: end-of-session scratch bundle
89 lines
4.2 KiB
Markdown
89 lines
4.2 KiB
Markdown
# 2026-04-27 — Scram `X_exit` redefinition: shutdown-margin halfspace
|
||
|
||
## What changed
|
||
|
||
Replaced the scram-mode `X_exit` predicate from
|
||
`n <= 1e-4 AND T_f <= T_f0 + 50 C` to a single linear halfspace
|
||
`shutdown_margin`:
|
||
|
||
alpha_f * T_f + alpha_c * T_c <= -rho_SDM - U_SCRAM + alpha_f*T_f0 + alpha_c*T_c0
|
||
≈ 0.002972
|
||
|
||
with `rho_SDM = 0.01` (1% Δk/k tech-spec floor).
|
||
|
||
Files touched:
|
||
- `reachability/predicates.json` — added `shutdown_margin` under
|
||
`safety_limits`; updated `mode_definitions.q_scram.X_exit_predicate`
|
||
and `X_safe_predicate`; left a `_X_exit_history` field for forensics.
|
||
- `code/scripts/reach/reach_scram_pj.jl` — added `RHO_SDM`, `SDM_RHS`
|
||
constants; reach loop now reports ρ-bounds and the halfspace LHS sup
|
||
per probe horizon; `.mat` output gets `sdm_lhs_hi`, `rho_max`,
|
||
`sdm_ok` per horizon plus a global `sdm_rhs`, `rho_sdm`.
|
||
|
||
## Why
|
||
|
||
1. **Power threshold was nonlinear in PJ state.** In the prompt-jump
|
||
reduction, `n = Λ * sum(λ_i*C_i) / (β - ρ)` — ρ depends on `T_f`,
|
||
`T_c`. So `n ≤ 1e-4` is *not* a halfspace in the reach state. We
|
||
were reconstructing it post-hoc on every probe, which works for a
|
||
diagnostic check but doesn't compose with halfspace-based discharge.
|
||
2. **`T_f ≤ T_f0 + 50` was infeasible-by-construction at 60 s.** Decay
|
||
heat (`Q_sg = 3% P0`) plus a fuel time constant `M_f*C_f / hA ≈ 0.3 s`
|
||
means `T_f` rapidly equilibrates with `T_c`, but the system loses
|
||
only ~5 °C in 60 s under constant decay — nowhere near the threshold,
|
||
and never going back up either. The bound was dressing, not work.
|
||
3. **Shutdown margin is the actual NRC criterion.** Tech specs phrase
|
||
scram success in Δk/k, not in flux. And ρ is *linear* in
|
||
`(T_f, T_c)` post-scram (constant `u = U_SCRAM`), so it's a clean
|
||
single-row halfspace.
|
||
|
||
## Result
|
||
|
||
`reach_scram_pj.jl` discharges `shutdown_margin` at all three probe
|
||
horizons (10, 30, 60 s), with massive margin:
|
||
|
||
| T (s) | reach-sets | wall (s) | ρ at horizon | discharged |
|
||
|-------|------------|----------|---------------------------|------------|
|
||
| 10 | 6919 | 98.6 | [-0.0507, -0.0504] | ✓ |
|
||
| 30 | 9900 | 130.5 | [-0.0506, -0.0503] | ✓ |
|
||
| 60 | 12340 | 164.2 | [-0.0503, -0.0500] | ✓ |
|
||
|
||
Required: `ρ ≤ -0.01`. Actual: `|ρ| ≈ 5%`. The Doppler/moderator
|
||
contributions vary by ~3% of `U_SCRAM`, so the margin is dominated by
|
||
rod worth — exactly what physical intuition predicts.
|
||
|
||
`.mat` output: `results/reach_scram_pj_result.mat`.
|
||
|
||
## Subtlety I tripped on
|
||
|
||
Hand-derived `SDM_RHS = 0.00402` using rounded `T_F0=320`, `T_C0=300`.
|
||
Actual values from `pke_params`: `T_C0 = 308.35`, `T_F0 = 328.35`
|
||
(because `DT_CORE = P0/(W_M*C_C) = 36.7 °C`, not 20). The script
|
||
computes `SDM_RHS` from constants so the run was correct (0.002972),
|
||
but the predicate JSON had the stale 0.00402. Fixed by switching the
|
||
`rhs_expr` to a symbolic form. **Rule for next time:** if a constant
|
||
in `predicates.json` is derivable from `pke_params`, write it as a
|
||
symbolic expression, not a baked number — that's what `T_cold0`,
|
||
`T_c0`, `T_standby` are for.
|
||
|
||
## What's still open
|
||
|
||
- `X_safe_predicate` still says "fuel_centerline AND cold_leg_subcooled"
|
||
but the reach script doesn't actually discharge those over the
|
||
trajectory — only at the probe horizons. Not a problem for the demo
|
||
(T_f and T_cold are monotone after scram), but the formal obligation
|
||
is reach-AVOID, not just reach. Worth a follow-up: discharge the
|
||
invariant halfspaces over the *full flowpipe*, not the endpoint.
|
||
- `prompt_critical_margin_heatup` is the controller-specific PJ-validity
|
||
predicate. Scram has its own analogous concern (PJ valid only when
|
||
`β - ρ > 0` with margin). Trivially satisfied here (ρ ≈ -0.05, far
|
||
from `β = 0.0065`), but worth a parallel `prompt_critical_margin_scram`
|
||
predicate for completeness — would document the assumption rather than
|
||
leave it implicit.
|
||
|
||
## Graduation candidates
|
||
|
||
- The "rhs_expr should be symbolic when derivable" rule probably belongs
|
||
in `code/CLAUDE.md` near the predicate-loading section. Hold for now —
|
||
one occurrence isn't a pattern yet.
|