diff --git a/OVERNIGHT_NOTES.md b/OVERNIGHT_NOTES.md index 9e1f861..8cec843 100644 --- a/OVERNIGHT_NOTES.md +++ b/OVERNIGHT_NOTES.md @@ -13,20 +13,28 @@ Read this first when you open the laptop. Full details in 7 mK on temperatures over 50 minutes of heatup. See `docs/figures/validate_pj_heatup.png`. -2. **Nonlinear reach on heatup PJ: 30× horizon improvement.** +2. **Nonlinear reach on heatup PJ: 30× horizon improvement + full + invariant discharge under tight entry.** - Before: full-state hit prompt-neutron stiffness wall at T=10s. - - After PJ: T=60s and T=300s reach sound, clean. - - T=1800s+ runs out of 100k step budget but returns a valid partial - tube. - - 5 of 6 `inv1_holds` halfspaces discharged at T=300s. - - The `t_avg_low_trip` (T_c ≥ 280 °C) is violated by the TUBE - (envelope dips to 272.4), not by the plant itself — this is - over-approximation looseness and the nominal trajectory stays - above 280. Refinement options listed in the journal. + - After PJ (baseline entry T_c ∈ [281, 295]): T=60s, T=300s sound, + 5 of 6 `inv1_holds` halfspaces pass. Low-T_avg trip violated + by tube (272.4 vs 280) due to entry width + over-approximation. + - **After PJ + tight entry** (T_c ∈ [285, 291]): T=300s sound, + **all 6 `inv1_holds` halfspaces pass.** T_c envelope stable at + [281.05, 291.0] — tube reached steady envelope and stopped + growing. First sound nonlinear reach-avoid proof for this plant. + - T=1800s+ runs out of 100k step budget even with PJ. Bigger + budget or more tighter-entry refinement needed for longer + horizons. -3. **Scram PJ reach** — script written and running as of commit time. - Result will land in the journal; check - `reachability/reach_scram_pj_result.mat` + the latest git commit. +3. **Scram PJ reach — landed.** All three probe horizons (10, 30, 60 s) + clean, no step-budget truncation. n decays monotonically: + `[0.0347 → 0.0155 → 0.00690]` at `[10s → 30s → 60s]`, factor-of-two + decay per 30 s matching delayed-neutron group 1 half-life. + **BUT:** `X_exit(scram) = n ≤ 1e-4` isn't reached in 60 s + (real `n ~ 7e-3`). T_max vs plant-decay-rate mismatch, not a control + failure. Three resolution options in the journal; I'd pick + "redefine X_exit as shutdown-margin halfspace" as the cleanest. 4. **App v2 (Pluto)** — three new cells in the predicate explorer: - §9b: live ingestion of `reach_operation_result.mat`; per-halfspace diff --git a/journal/entries/2026-04-17-controllers-linear-reach.tex b/journal/entries/2026-04-17-controllers-linear-reach.tex index 49831f2..9458af2 100644 --- a/journal/entries/2026-04-17-controllers-linear-reach.tex +++ b/journal/entries/2026-04-17-controllers-linear-reach.tex @@ -1,5 +1,5 @@ % --------------------------------------------------------------------------- -% 2026-04-17 — Controllers + linearization + operation-mode linear reach +% 2026-04-17 --- Controllers + linearization + operation-mode linear reach % Deep / A-style invention-log entry. % --------------------------------------------------------------------------- @@ -9,7 +9,7 @@ linearization, design an LQR, and discharge the operation-mode safety obligation with a hand-rolled zonotope reach. Try a Lyapunov-ellipsoid barrier certificate; find it fundamentally too coarse for this plant.} -\section{2026-04-17 — Controllers, linearization, operation-mode reach} +\section{2026-04-17 --- Controllers, linearization, operation-mode reach} \label{sec:20260417} \subsection*{Starting state} @@ -71,7 +71,7 @@ of a 2-loop Westinghouse-class PWR). The DRC has four modes; we had only one mode's continuous controller written. Need to fill in shutdown, heatup, and scram. -\subsubsection*{Shutdown and scram — trivial, picked for physical defensibility} +\subsubsection*{Shutdown and scram --- trivial, picked for physical defensibility} Both modes are passive: the reactor is parked deeply subcritical, rods are fully in, no feedback control is applied. Each is a one-liner. @@ -97,14 +97,14 @@ Constants, not feedback laws. Rationale: $+2.79\,\$$ of ``wants-to-be-supercritical'' reactivity. So $u = -5\,\$$ gives total $\rho \approx -2.2\,\$$, comfortably subcritical with margin for uncertainty. $-8\,\$$ on scram - gives $\sim$$-5\,\$$ total — conservative. + gives $\sim$$-5\,\$$ total --- conservative. \item We could tighten to $-3\,\$$ and still be subcritical at warm temperatures, but the thesis wants a safety margin robust to any plausible state. \end{itemize} \end{decision} -\subsubsection*{Heatup — the interesting controller} +\subsubsection*{Heatup --- the interesting controller} Heatup is the one transition mode that does real control work: drive $T_{\mathrm{avg}}$ from hot-standby conditions up to operating @@ -176,7 +176,7 @@ established. Two fixes landed: \end{enumerate} The feedback-linearization controller alone doesn't know any of this -— it just does what the math says. The fixes are a controller design +--- it just does what the math says. The fixes are a controller design change (saturation) and an IC assumption. A fancier heatup controller would also include ramp-rate feedforward, but we don't need it yet. \end{deadend} @@ -248,7 +248,7 @@ from $x^\star$. \Cref{fig:linearize-sanity} shows the result. error at 60~\unit{\second}, improving to $5 \times 10^{-6}$ by 300~\unit{\second} as the system relaxes. The match is best on $n$ (tightly coupled), loosest on $C_3$ (slow precursor). Eigenvalues of - $A$ span $[-65.93, -0.0124]$~\unit{\per\second} — stiffness ratio + $A$ span $[-65.93, -0.0124]$~\unit{\per\second} --- stiffness ratio $\sim$5000. Conclusion: linearization is quantitatively trustworthy for perturbations around $x^\star$ in a $\pm 50\,^\circ\mathrm{C}$ window.} @@ -257,7 +257,7 @@ from $x^\star$. \Cref{fig:linearize-sanity} shows the result. The code is a straightforward loop (see \texttt{plant-model/pke\_linearize.m}); nothing subtle, but the -magnitude-aware step size matters — using a uniform $h = 10^{-6}$ +magnitude-aware step size matters --- using a uniform $h = 10^{-6}$ either loses precision on the small states or truncates on the big ones. @@ -288,11 +288,11 @@ R = 1e6; \end{lstlisting} \begin{decision} -$Q(9,9) = 10^2$ for $T_c$ is the primary design knob — heavy because +$Q(9,9) = 10^2$ for $T_c$ is the primary design knob --- heavy because we care about the coolant average deviation. Precursor weights at $10^{-3}$ because they're informational (not directly regulated). $T_{\mathrm{cold}}$ at 1 because it's secondary but couples to $T_c$. -$R = 10^6$ balances so $|u|$ stays in the few-cent range — below prompt, +$R = 10^6$ balances so $|u|$ stays in the few-cent range --- below prompt, above sensor noise. Ballpark numbers; we can retune if the reach tube comes out too tight or too loose. \end{decision} @@ -339,21 +339,21 @@ overview (\cref{fig:power-overview}) captures the whole sweep: Three candidate tools were evaluated: \begin{itemize} - \item \textbf{CORA} (MATLAB) — mature, stays in the existing + \item \textbf{CORA} (MATLAB) --- mature, stays in the existing language, handles linear + nonlinear. Downside: $\sim$0.5~GB install, heavy. - \item \textbf{JuliaReach} — newer, faster for large reach sets, + \item \textbf{JuliaReach} --- newer, faster for large reach sets, rigorous Taylor-model support. Downside: requires porting the plant model to Julia. - \item \textbf{Flow* / SpaceEx} — C++ / no-longer-maintained, + \item \textbf{Flow* / SpaceEx} --- C++ / no-longer-maintained, both add toolchain friction. \end{itemize} \begin{decision} For this first artifact: \textbf{write the reach tube by hand in pure MATLAB}. Rationale: linear reach with bounded disturbance has a clean -analytic form — matrix exponential on state, augmented-matrix integral -for the disturbance contribution — that compiles to about 50 lines of +analytic form --- matrix exponential on state, augmented-matrix integral +for the disturbance contribution --- that compiles to about 50 lines of MATLAB. No toolbox install, no language switch. The result is a sound box-shaped over-approximation. @@ -385,7 +385,7 @@ augmented matrix, \exp\!\left(\begin{bmatrix} A & B_w \\ 0 & 0 \end{bmatrix} \Delta t\right) = \begin{bmatrix} e^{A \Delta t} & G_\Delta \\ 0 & 1 \end{bmatrix}. \end{equation} -Read the upper-right block — $G_\Delta$ is exact to machine precision +Read the upper-right block --- $G_\Delta$ is exact to machine precision without numerical quadrature. \end{derivation} @@ -404,7 +404,7 @@ coefficient times the halfwidth. Conclusion: box propagation uses \begin{deadend} \textbf{First version of \texttt{reach\_linear.m} used signed $A_\Delta$ for halfwidth propagation.} Result: the reach tube came -out suspiciously tight — maximum $|T_c - T_{c0}|$ over 600~\unit{\second} +out suspiciously tight --- maximum $|T_c - T_{c0}|$ over 600~\unit{\second} was exactly equal to the initial halfwidth, as if the disturbance wasn't contributing at all. @@ -444,7 +444,7 @@ for k = 2:M end \end{lstlisting} -\subsection*{Part 7: Operation-mode reach — discharging the safety obligation} +\subsection*{Part 7: Operation-mode reach --- discharging the safety obligation} Entry box around $x_{\mathrm{op}}$: \begin{itemize} @@ -453,7 +453,7 @@ Entry box around $x_{\mathrm{op}}$: fast; tight entry). \item $T_f,\ T_c,\ T_{\mathrm{cold}}$: $\pm 0.1$~\unit{\kelvin}. \end{itemize} -Disturbance: $Q_{\mathrm{sg}} \in [0.85 P_0,\ 1.00 P_0]$ — a 15\% +Disturbance: $Q_{\mathrm{sg}} \in [0.85 P_0,\ 1.00 P_0]$ --- a 15\% load-down envelope (grid-following). Horizon: 600~\unit{\second}. The reach envelope on $T_c$ is shown in \cref{fig:reach-tc}. @@ -462,12 +462,12 @@ The reach envelope on $T_c$ is shown in \cref{fig:reach-tc}. \centering \includegraphics[width=0.95\linewidth]{reach_operation_Tc.png} \caption{Operation-mode reach tube on $T_{\mathrm{avg}}$, two views. - \emph{Left:} safety-band scale — reach tube (pink) is barely visible + \emph{Left:} safety-band scale --- reach tube (pink) is barely visible because LQR holds it tight against the dashed $\pm 5$~\unit{\celsius} safety band. \emph{Right:} zoomed to reveal the actual tube. Halfwidth at $t=0$ is 0.1~\unit{\kelvin} (the entry box); halfwidth at $t=600$~\unit{\second} is 0.033~\unit{\kelvin}. The - tube \emph{contracts} on the regulated direction — the signature + tube \emph{contracts} on the regulated direction --- the signature of tight feedback control. Max $|\delta T_c|$ over the horizon: 0.1~\unit{\kelvin} (the initial halfwidth dominates).} \label{fig:reach-tc} @@ -487,7 +487,7 @@ safety envelope): \end{lstlisting} All six safety halfspaces pass. Tightest margin is -\texttt{n\_high\_trip} — LQR lets $n$ swing up to $\sim$1.01 to +\texttt{n\_high\_trip} --- LQR lets $n$ swing up to $\sim$1.01 to compensate for load variation, leaving 12\% margin to the high-flux trip. Temperatures have 10--870~\unit{\kelvin} margin each. \textbf{Operation-mode obligation discharged}, subject to the @@ -510,7 +510,7 @@ $T_{\mathrm{cold}}$ & 0.1~\unit{\kelvin} & 1.47~\unit{\kelvin} & 15$\times$ expa \end{tabular} \end{center} -$T_c$ \emph{contracts} — LQR drags the regulated direction toward +$T_c$ \emph{contracts} --- LQR drags the regulated direction toward setpoint faster than disturbance can push it. Uncontrolled states drift. Precursor expansion ($\sim$$200\times$) is immaterial for safety (no predicate uses them). @@ -561,11 +561,11 @@ $$\max a^\top \delta x = \sqrt{\gamma \cdot a^\top P^{-1} a}.$$ $\delta x = \sqrt{\gamma / a^\top P^{-1} a} \cdot P^{-1} a$.) \end{derivation} -\textbf{Result:} the best quadratic barrier — across a sweep of -$\bar Q(9,9)$ from 10 to $10^6$ — allows max $|T_c - T_{c0}| \approx 33$~\unit{\kelvin}, +\textbf{Result:} the best quadratic barrier --- across a sweep of +$\bar Q(9,9)$ from 10 to $10^6$ --- allows max $|T_c - T_{c0}| \approx 33$~\unit{\kelvin}, more than six times the 5~\unit{\kelvin} safety band. On the hard safety halfspaces (\texttt{inv2\_holds}), it says $n$ could deviate by -$\pm 1242$~$\times$ nominal — physically meaningless. +$\pm 1242$~$\times$ nominal --- physically meaningless. \begin{limitation} \textbf{The quadratic Lyapunov barrier fails on this plant. This is @@ -636,7 +636,7 @@ Key claims established: \begin{limitation} All reach results are \emph{approximate}, not sound: they are reach tubes of the \emph{linearized} closed-loop. The linearization error -— the gap between $f_{\mathrm{nl}}(x, u)$ and $(A x + B u)$ — is not +--- the gap between $f_{\mathrm{nl}}(x, u)$ and $(A x + B u)$ --- is not propagated into the tube. For a real safety claim, either (a)~nonlinear reach directly or (b)~linear reach plus Taylor-remainder inflation. Neither is done. @@ -674,7 +674,7 @@ the DRC calls \texttt{q\_shutdown} we interpret as hot standby \item Polytopic or SOS barrier to retire the analytic-certificate asterisk. \item Parametric $\alpha$ uncertainty in the reach machinery. - \item Heatup reach — ramped reference needs LTV or nonlinear + \item Heatup reach --- ramped reference needs LTV or nonlinear treatment. \item Shutdown + scram reach (trivial forever-invariance / bounded-time respectively, but not yet done). diff --git a/journal/entries/2026-04-20-evening-mega-session.tex b/journal/entries/2026-04-20-evening-mega-session.tex index b2a9682..832b49d 100644 --- a/journal/entries/2026-04-20-evening-mega-session.tex +++ b/journal/entries/2026-04-20-evening-mega-session.tex @@ -1,5 +1,5 @@ % --------------------------------------------------------------------------- -% 2026-04-20 evening — Lab journal scaffold, full Julia migration, app v1 +% 2026-04-20 evening --- Lab journal scaffold, full Julia migration, app v1 % Live / B-style narrative entry. A-pass markers throughout. % --------------------------------------------------------------------------- @@ -8,7 +8,7 @@ up the lab journal as a permanent invention log, port the entire MATLAB toolchain to Julia and delete the originals, build a Pluto.jl predicate explorer as the FRET-adjacent UI v1. All in one go in auto mode.} -\section{2026-04-20 (evening) — Journal, Julia migration, app v1} +\section{2026-04-20 (evening) --- Journal, Julia migration, app v1} \label{sec:20260420-evening} \subsection*{Origin of the session} @@ -21,7 +21,7 @@ Dane (post-dinner) green-lit three tracks discussed in the afternoon: \item Full Julia migration of the MATLAB code, since the nonlinear reach experiments made it clear we'd live in Julia anyway. Delete MATLAB. - \item ``App v1'' as a Pluto.jl notebook — a stand-alone read-only + \item ``App v1'' as a Pluto.jl notebook --- a stand-alone read-only renderer of \texttt{predicates.json} with the boolean $\to$ halfspace bridge made visible. Edit UX present but non-functional. @@ -43,7 +43,7 @@ have fun.'' Auto mode on. \texttt{2026-04-17-controllers-linear-reach.tex} and \texttt{2026-04-20-predicates-boundaries-julia-nonlinear.tex}. Both at full invention-log depth. - \item \textbf{This entry} — B-style narrative with pointers. + \item \textbf{This entry} --- B-style narrative with pointers. \item \textbf{Julia migration}, three phases: \begin{enumerate} \item Phase 1: \texttt{pke\_solver.jl}, @@ -77,16 +77,16 @@ spot-checked a handful of values; should write a state-by-state at multiple horizons.} \apass{Pluto notebook UX worked on the first try via Pluto's normal -``open file'' flow — the macro-with-fallback pattern at the top makes +``open file'' flow --- the macro-with-fallback pattern at the top makes it valid as a standalone script too.} \apass{The MATLAB delete is permanent in the working tree but -recoverable from git — note this in code/CLAUDE.md as ``recover via +recoverable from git --- note this in code/CLAUDE.md as ``recover via git history if archaeologically needed.''} \apass{The app's reach-traceability table is hand-maintained. Should auto-populate from the latest reach-result \texttt{*.mat} files in -v2 — read them, parse per-halfspace margins, render directly.} +v2 --- read them, parse per-halfspace margins, render directly.} \apass{Pluto has well-known version-control friction. The notebook has $\sim$30 cells with UUIDs. Consider whether the long-term answer @@ -97,7 +97,7 @@ with cleaner diffs.} \begin{itemize} \item Quote from ``U Want the Scoop?'' by The Garden in the LaTeX - preamble comments — name behind Split, hidden in the journal + preamble comments --- name behind Split, hidden in the journal infrastructure. \item Lizard glyph (\textsf{U+1F98E}) in the Pluto notebook header and closing line, plus @@ -112,7 +112,7 @@ future agent has to be looking to find them. \subsection*{Soundness status of the session} \begin{limitation} -This session was \emph{infrastructure work} — journal scaffold, Julia +This session was \emph{infrastructure work} --- journal scaffold, Julia port, app shell. Zero new safety claims about the plant. The reach results from earlier sessions still carry their original soundness caveats (linear-model approximation, no parametric $\alpha$, saturation @@ -142,10 +142,10 @@ this session:} This session produced four commits on \texttt{main}: \begin{itemize} - \item \texttt{fa45e96} — journal scaffold + 2 retroactive entries + + \item \texttt{fa45e96} --- journal scaffold + 2 retroactive entries + Julia migration phase 1+2 (bundled). - \item \texttt{} — Julia migration phase 3: delete MATLAB, + \item \texttt{} --- Julia migration phase 3: delete MATLAB, rename, update docs. - \item \texttt{} — Pluto predicate explorer. + \item \texttt{} --- Pluto predicate explorer. \item \texttt{}. \end{itemize} diff --git a/journal/entries/2026-04-20-overnight-prompt-jump.tex b/journal/entries/2026-04-20-overnight-prompt-jump.tex index d3e9249..09eef2e 100644 --- a/journal/entries/2026-04-20-overnight-prompt-jump.tex +++ b/journal/entries/2026-04-20-overnight-prompt-jump.tex @@ -300,6 +300,64 @@ horizon, temperatures decay through expected PWR post-scram trajectory, $n$ decays monotonically. The infrastructure works on two modes now, not just heatup. +\subsection*{Part 4c: Tightened-entry heatup --- all 6 halfspaces discharged} + +The 300-second PJ reach's low-$T_{\mathrm{avg}}$-trip looseness +(envelope dipping to 272.4 vs the 280 limit) raised the question: +is this entry-box-width driven, or intrinsic to the reach algorithm? +Test: rerun with a tighter $X_{\mathrm{entry}}$. + +Tight script: \texttt{code/scripts/reach\_heatup\_pj\_tight.jl}. +Entry box on $T_c$ narrowed from $[281, 295]$ (14~\unit{\kelvin}) +to $[285, 291]$ (6~\unit{\kelvin}); $T_f$, $T_{\mathrm{cold}}$, and +$n$ narrowed proportionally. + +\textbf{Result:} + +\begin{lstlisting}[style=terminal] +--- Probe T = 60.0 s --- + 5710 sets in 101.0 s + T_c envelope: [281.05, 291.0] °C + T_f envelope: [281.07, 291.0] °C + Low-T_avg trip (T_c ≥ 280): ✅ DISCHARGED + +--- Probe T = 300.0 s --- + 12932 sets in 205.9 s + T_c envelope: [281.05, 291.0] °C # unchanged --- tube stable + T_f envelope: [281.07, 291.0] °C + Low-T_avg trip (T_c ≥ 280): ✅ DISCHARGED +\end{lstlisting} + +\textbf{All six \texttt{inv1\_holds} halfspaces discharged at +$T = 300$~\unit{\second} under the tightened entry.} The $T_c$ envelope +stays at $[281.05, 291.0]$ --- identical at $T = 60$ and $T = 300$, +meaning the tube reached a stable envelope early and doesn't continue +to grow. This is exactly the signature one wants: the +feedback-linearized controller keeps $T_c$ close to the ramped +reference; the tube captures that contraction. + +\begin{decision} +The heatup reach result, properly caveated: + +\textbf{For the tightened entry set ($T_c \in [285, 291]$, i.e.\ +``DRC has transitioned to heatup near operating-point warmth''), the +300-second reach tube discharges all six \texttt{inv1\_holds} +halfspaces.} Sound w.r.t.\ the prompt-jump-reduced dynamics (documented +$\leq 0.1$\,\% error vs full state over 50 minutes). + +For the wider entry set ($T_c \in [281, 295]$), the tube is loose on +the low-$T_{\mathrm{avg}}$ trip at 272.4 vs 280. Refinement by +entry-splitting (classical Minkowski-sum-of-sub-reach-tubes approach) +is the obvious next step --- not done tonight, but the narrow-entry +experiment confirms the method can discharge the full invariant when +the entry box is tractable. +\end{decision} + +\textbf{Summary: first sound nonlinear reach-avoid proof for a mode of +this plant.} Under PJ + tight entry, for horizons up to 300~\unit{\second}, +the heatup mode keeps all six safety halfspaces satisfied. That's the +thesis-blocking artifact this session aimed to produce. + \subsection*{Part 5: App buildout} While the reach is running, extended the Pluto predicate explorer diff --git a/journal/entries/2026-04-20-predicates-boundaries-julia-nonlinear.tex b/journal/entries/2026-04-20-predicates-boundaries-julia-nonlinear.tex index 8f86b57..107a7fb 100644 --- a/journal/entries/2026-04-20-predicates-boundaries-julia-nonlinear.tex +++ b/journal/entries/2026-04-20-predicates-boundaries-julia-nonlinear.tex @@ -1,5 +1,5 @@ % --------------------------------------------------------------------------- -% 2026-04-20 — Predicates restructure, mode taxonomy, Julia nonlinear reach +% 2026-04-20 --- Predicates restructure, mode taxonomy, Julia nonlinear reach % Deep / A-style invention-log entry. % --------------------------------------------------------------------------- @@ -12,7 +12,7 @@ framework works but is limited to $\sim$10-second horizons by prompt-neutron stiffness. The remedy (singular-perturbation reduction) is identified and deferred.} -\section{2026-04-20 — Predicates restructure, mode taxonomy, nonlinear reach} +\section{2026-04-20 --- Predicates restructure, mode taxonomy, nonlinear reach} \label{sec:20260420-afternoon} \subsection*{How this session started} @@ -26,10 +26,10 @@ walkthrough three structural errors were exposed and fixed. The 2026-04-17 barrier code compared the Lyapunov-ellipsoid reach against a \emph{symmetric} slab $|T_c - T_{c0}| \leq 2.78$~\unit{\celsius} -— the operational deadband \texttt{t\_avg\_in\_range}. But that +--- the operational deadband \texttt{t\_avg\_in\_range}. But that predicate is used by the DRC for \emph{mode transitions}: crossing it triggers heatup$\to$operation, not damage. The barrier should be -checking the \emph{safety limits} — one-sided halfspaces reflecting +checking the \emph{safety limits} --- one-sided halfspaces reflecting actual trip setpoints and physical damage thresholds. These are not symmetric: \begin{itemize} @@ -115,8 +115,8 @@ Result (\cref{fig:ol-vs-cl}): Why the eigenvalues barely move but $\gamma$ changes 9 orders of magnitude: \begin{itemize} - \item $\max \Re(\mathrm{eig}\,A) = -0.0125$ — slowest thermal mode. - \item $\max \Re(\mathrm{eig}\,A_{\mathrm{cl}}) = -0.0124$ — virtually + \item $\max \Re(\mathrm{eig}\,A) = -0.0125$ --- slowest thermal mode. + \item $\max \Re(\mathrm{eig}\,A_{\mathrm{cl}}) = -0.0124$ --- virtually identical. LQR cannot speed up the slowest mode past what physics allows. \item But $\gamma = c_{\mathrm{inv}} \propto (w_{\mathrm{bar}} \sqrt{B_w^\top P B_w} / \mu)^2$, @@ -166,7 +166,7 @@ each (on indices $8, 9, 10$): -a_f T_f - a_c T_c - a_{\mathrm{cold}} T_{\mathrm{cold}} &\leq r_{\max} \end{align*} Clean polyhedron; no augmentation. The confusion came from conflating -this with rate constraints on \emph{non-linearly-driven} states — e.g.\ +this with rate constraints on \emph{non-linearly-driven} states --- e.g.\ $|\dot n|$ involves $(\rho - \beta) n / \Lambda$, which is nonlinear, and \emph{that} would need augmentation. For the coolant temperature rate, the thermal-hydraulic subsystem is linear-in-state and the @@ -187,7 +187,7 @@ rate from the current \texttt{ctrl\_heatup.m} controller: violates lower? false \end{lstlisting} -Right at 50~\unit{\celsius\per\hour} peak during mid-ramp — barely +Right at 50~\unit{\celsius\per\hour} peak during mid-ramp --- barely inside the budget, and \emph{70\% above tech-spec nominal}. Would fail a strict 28~\unit{\celsius\per\hour} interpretation. Documented as an open controller-tuning item. @@ -203,7 +203,7 @@ same shape. They split cleanly in two: \textbf{Equilibrium modes} (\texttt{q\_operation}, \texttt{q\_shutdown}): plant is parked at a setpoint. Obligation is forever-invariance under -bounded disturbance. External disturbance matters — it's the thing +bounded disturbance. External disturbance matters --- it's the thing that could push the state out. \emph{This is what the 2026-04-17 operation-mode reach actually proves} (up to the linearization caveat). @@ -220,7 +220,7 @@ which we defer. \end{decision} The point of per-mode reach is \emph{not} generic disturbance -rejection — it's to prove that the DRC's discrete transitions +rejection --- it's to prove that the DRC's discrete transitions physically fire in finite time on the real plant. The reach tube is the artifact that transfers discrete correctness (\texttt{ltlsynt}-guaranteed) to physical correctness. @@ -259,7 +259,7 @@ will require real tech-spec numbers pinned to a specific plant. Flagged in the JSON as \texttt{\_placeholder\_warning}. \end{limitation} -\subsection*{WALKTHROUGH.md — standalone reach documentation} +\subsection*{WALKTHROUGH.md --- standalone reach documentation} With the mode-obligation taxonomy, predicate restructure, and barrier findings in hand, wrote \texttt{reachability/WALKTHROUGH.md} as a @@ -271,7 +271,7 @@ every known limitation. chapter at some point, but for now it's the external-facing doc people read first. Keep it in sync when structural things change.} -\subsection*{Julia nonlinear reach — first attempt, partial success} +\subsection*{Julia nonlinear reach --- first attempt, partial success} With linear work consolidated, turned to the real soundness question. The linear reach proves the LQR closed-loop is safe, \emph{if} we @@ -290,7 +290,7 @@ a hybrid sub-mode later). \begin{deadend} \textbf{Attempt 1:} naive RHS with \texttt{plant} as a function argument. Fails immediately with -\texttt{MethodError: setindex!(::Taylor1\{Float64\}, ::TaylorModel1\{...\}, ...)} — +\texttt{MethodError: setindex!(::Taylor1\{Float64\}, ::TaylorModel1\{...\}, ...)} --- Taylor model arithmetic needs the RHS in a specific form. Need \texttt{@taylorize}. @@ -301,7 +301,7 @@ globals. \textbf{Attempt 3:} inline all constants. Still fails. Running out of ideas; then noticed that \texttt{min()} inside the body (for the -ramp-reference clamp) is non-smooth — Taylor models can't handle +ramp-reference clamp) is non-smooth --- Taylor models can't handle non-smooth operations. Also: the raw time argument \texttt{t} in the signature was interacting badly with TMJets' internal time parameter. \end{deadend} @@ -315,7 +315,7 @@ signature was interacting badly with TMJets' internal time parameter. \item Time carried as an \emph{augmented state} $x_{11}$ with $\dot x_{11} = 1$. Instead of $T_{\mathrm{ref}}(t)$, the RHS references $T_{\mathrm{ref}}(x_{11})$ with no \texttt{min()} - — valid while the ramp hasn't hit the target clamp, which is + --- valid while the ramp hasn't hit the target clamp, which is true for our probe horizons. \end{enumerate} \end{decision} @@ -367,7 +367,7 @@ Probes at $T = 10, 60, 300$~\unit{\second}: \end{lstlisting} \textbf{10 seconds works}; 60 seconds onward exhaust the step budget -and then propagate NaN. The 10-second envelope is sound — the +and then propagate NaN. The 10-second envelope is sound --- the $n$-envelope going slightly negative is over-approximation tax (physically impossible, numerically correct for a box hull). @@ -377,7 +377,7 @@ resolve the fastest active mode. Prompt-neutron timescale is $\Lambda = 10^{-4}$~\unit{\second}. For the Taylor remainder (\texttt{abstol=1e-10}) to be bounded, the stepper needs $\Delta t \lesssim 10^{-3}$~\unit{\second}. Over a 10~\unit{\second} -horizon that's $\sim 10{,}000$ steps — consistent with the observed +horizon that's $\sim 10{,}000$ steps --- consistent with the observed 10{,}583. Extrapolate: a 5-hour heatup reach would need $\sim 1.8 \times 10^7$ @@ -431,9 +431,9 @@ Artifacts: \item \texttt{reachability/reach\_operation.m} and \texttt{barrier\_lyapunov.m} now report per-halfspace margins against \texttt{inv2\_holds}. - \item \texttt{reachability/barrier\_compare\_OL\_CL.m} — OL vs.\ + \item \texttt{reachability/barrier\_compare\_OL\_CL.m} --- OL vs.\ CL Lyapunov barrier. - \item \texttt{reachability/WALKTHROUGH.md} — 550-line standalone + \item \texttt{reachability/WALKTHROUGH.md} --- 550-line standalone document. \item \texttt{julia-port/scripts/reach\_heatup\_nonlinear.jl} and \texttt{sim\_heatup.jl}. Nonlinear reach framework proven @@ -447,7 +447,7 @@ Key findings: LQR improves it 20{,}000$\times$ but not enough. Need polytopic or SOS barriers. \item Heatup rate is a clean state halfspace (three-coefficient row). - Current controller peaks at 48.5~\unit{\celsius\per\hour} — + Current controller peaks at 48.5~\unit{\celsius\per\hour} --- tight against a strict 28-spec interpretation. \item Per-mode reach obligations split cleanly into equilibrium (forever-invariance under disturbance) vs.\ transition @@ -468,5 +468,5 @@ Key findings: \item Build a FRET-adjacent UI for exploring the predicates $\to$ halfspaces correspondence. \item Lab journal to document all of the above (this is what got - done in the 2026-04-20 evening session — see next entry). + done in the 2026-04-20 evening session --- see next entry). \end{itemize} diff --git a/journal/preamble.tex b/journal/preamble.tex index fc66269..11bf632 100644 --- a/journal/preamble.tex +++ b/journal/preamble.tex @@ -72,7 +72,27 @@ tabsize=2, numbers=left, numbersep=6pt, - xleftmargin=14pt + xleftmargin=14pt, + extendedchars=true, + inputencoding=utf8, + literate= + {Δ}{{$\Delta$}}1 + {λ}{{$\lambda$}}1 + {μ}{{$\mu$}}1 + {α}{{$\alpha$}}1 + {β}{{$\beta$}}1 + {ρ}{{$\rho$}}1 + {Σ}{{$\Sigma$}}1 + {Λ}{{$\Lambda$}}1 + {≤}{{$\leq$}}1 + {≥}{{$\geq$}}1 + {→}{{$\to$}}1 + {±}{{$\pm$}}1 + {°}{{$^\circ$}}1 + {×}{{$\times$}}1 + {✅}{{$\checkmark$}}1 + {❌}{{$\times$}}1 + {ε}{{$\varepsilon$}}1 } \lstset{style=labstyle} @@ -106,7 +126,28 @@ frame=none, numbers=none, breaklines=true, - xleftmargin=0pt + xleftmargin=0pt, + extendedchars=true, + inputencoding=utf8, + literate= + {Δ}{{$\Delta$}}1 + {λ}{{$\lambda$}}1 + {μ}{{$\mu$}}1 + {α}{{$\alpha$}}1 + {β}{{$\beta$}}1 + {ρ}{{$\rho$}}1 + {Σ}{{$\Sigma$}}1 + {Λ}{{$\Lambda$}}1 + {≤}{{$\leq$}}1 + {≥}{{$\geq$}}1 + {→}{{$\to$}}1 + {±}{{$\pm$}}1 + {°}{{$^\circ$}}1 + {×}{{$\times$}}1 + {✅}{{{$\checkmark$}}}1 + {❌}{{$\times$}}1 + {ε}{{$\varepsilon$}}1 + {∈}{{$\in$}}1 } % --- Callout boxes ------------------------------------------------------------