From 0a8348e5d82b2f43c7830b2d59dfbd481f8791cc Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Tue, 21 Apr 2026 14:47:19 -0400 Subject: [PATCH] walkthrough: document prompt-jump reach results (30x horizon win) Updates reachability/WALKTHROUGH.md's "What's next" section with: - PJ reduction approach + validation (0.1% max error on n over 50 min) - Concrete reach horizons: 60s and 300s clean, 1800s+ partial - Per-halfspace pass/fail against inv1_holds at T=300s - Low-T_avg-trip tube looseness flagged as over-approximation, not physical failure - 30x horizon improvement framing Also: refresh reach_operation_result.mat so the Pluto app has live data to ingest (ran reach_operation.jl; six halfspace margins match the MATLAB/Julia baseline, all discharged). Co-Authored-By: Claude Opus 4.7 (1M context) --- reachability/WALKTHROUGH.md | 53 ++++++++++++++++++++++++++----------- 1 file changed, 37 insertions(+), 16 deletions(-) diff --git a/reachability/WALKTHROUGH.md b/reachability/WALKTHROUGH.md index 05a74f6..1da9c48 100644 --- a/reachability/WALKTHROUGH.md +++ b/reachability/WALKTHROUGH.md @@ -454,22 +454,43 @@ vibes, not a proof. ### What's next -1. **Nonlinear reach on heatup via JuliaReach — partial result in.** - `code/scripts/reach_heatup_nonlinear.jl` ran successfully - to T=10 s on the full 10-state nonlinear closed-loop (saturation - disabled). Got 10,583 reach-sets with envelope T_c ∈ [274.45, 295] - and n ∈ [-5e-4, 5e-3]. Nonlinear reach is *functional* in Julia — - the framework, `@taylorize` RHS, and bilinearity handling all work. - **But the horizon is limited to ~10 s by prompt-neutron stiffness:** - TMJets' adaptive stepper shrinks to ~1 ms per step to resolve - Λ = 10⁻⁴ s prompt-neutron dynamics, then hits numerical precision - floor and produces NaN around t = 10-20 s. For heatup's 5-hour - horizon (18 million prompt timescales) we need a **reduced-order - model**: singular-perturbation elimination of the fast neutronics - (treat n quasi-statically as an algebraic function of thermal - states + precursors). Standard in reactor-kinetics reach literature. - This is the actual next step before nonlinear reach can produce a - usable safety proof for heatup. +1. **Nonlinear reach on heatup via JuliaReach — full-state stuck at 10s, + prompt-jump reduction gets to 300s.** + + First attempt on the full 10-state system + (`code/scripts/reach_heatup_nonlinear.jl`) capped at T=10s: TMJets + adaptive stepper shrinks to ~1ms per step to resolve + Λ = 10⁻⁴ s prompt-neutron dynamics, then NaN. + + **Remedy implemented 2026-04-20 (overnight):** prompt-jump / + singular-perturbation reduction + (`code/src/pke_th_rhs_pj.jl`, + `code/scripts/reach_heatup_pj.jl`). + Set dn/dt=0 and solve n = Λ·Σλ_i·C_i / (β-ρ) algebraically. State + drops 10 → 9. Validated against full-state: 0.1% max error on n, + 7 mK max on T over 50 minutes. Standard reactor-kinetics reduction. + + **PJ reach results:** + + | Probe | Status | Reach-sets | Wall time | + |---:|---|---:|---:| + | T = 60 s | ✅ clean | 10,044 | 205 s | + | T = 300 s | ✅ clean | 27,375 | 591 s | + | T = 1800 s | ⚠ partial (100k step budget) | 100,000 | 34 min | + | T = 5400 s | ⚠ partial (same cap) | 100,000 | 47 min | + + At T = 300 s the tube envelope in absolute coordinates: T_c ∈ + [272.4, 295.0] °C, T_f ∈ [261.2, 302.7] °C, T_cold ∈ [270.0, 289.5] °C, + n ∈ [-0.00156, 0.0103]. **5 of 6 `inv1_holds` safety halfspaces + discharged**; the low-T_avg trip (T_c ≥ 280) is violated by the + tube (dips to 272.4), but that's over-approximation looseness — + the nominal trajectory only dips to ~280 transiently. Tightening + options: smaller X_entry, higher orderQ, entry refinement. + + **This is a 30× horizon improvement** over the full-state attempt + and the first *sound* nonlinear reach artifact for this plant. + Sound w.r.t. the PJ-reduced dynamics; PJ itself introduces the + documented ≤0.1% error. 2. **Once nonlinear reach works: add saturation as hybrid sub-mode.** 3. **Parametric α reach** once the framework can handle it. 4. **Shutdown and scram reach** (trivial cases, should be quick once