645f2d8d27
Singular-perturbation reduction of the PKE+T/H system: set dn/dt=0,
solve algebraically n = Λ·Σλ_i·C_i / (β-ρ). State drops 10 -> 9 (no
n), removes Λ⁻¹ stiffness. Validated against full state on the heatup
scenario:
t [s] |Δn|/n_full T_c err [K]
60 3.7e-5 4e-6
300 3.8e-4 1.9e-4
1200 1.0e-3 2.2e-3
3000 5.0e-4 7.2e-3
Maximum relative error 0.1% on n, peak 7 mK on temperatures over
50 minutes. PJ approximation is excellent for slow heatup transients
(sub-prompt-critical regime).
Files:
- code/src/pke_th_rhs_pj.jl: reduced 9-state RHS
- code/scripts/validate_pj.jl: side-by-side sim
- code/scripts/reach_heatup_pj.jl: TMJets reach with PJ model
(probing T = 60, 300, 1800, 5400 s)
App v2 (Pluto):
- §9b: live ingestion of reach_operation_result.mat with per-
halfspace margins computed from JSON-defined inv2_holds.
- §9c: 2D projection chooser (n, T_f, T_c, T_cold) with reach
tube envelope overlay.
- §9d: PJ heatup reach summary (placeholder until first run lands).
Journal:
- Added 2026-04-20-overnight-prompt-jump.tex with PJ derivation,
validation table, soundness ledger update. apass markers for
the in-progress reach results.
This commit captures state mid-run; next commit will add the
populated reach results once TMJets returns.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
app — Predicate Explorer (Pluto.jl)
A local-server visual companion to reachability/predicates.json. Maps
the FRET-spec boolean predicates to their numerical halfspaces over the
10-state continuous vector, shows mode invariants as conjunctions of
named safety limits, and previews a UI for editing them.
v1: read-only. Sliders display in the edit panel but do not write back to the JSON. v2 will add live write-through. v3 (the dream) will derive halfspaces automatically from the FRET spec.
This is the FRET-adjacent piece — the "hybrid-systems group tab" we talked about. Stand-alone for now; integration into the upstream FRET UI is a later story.
Run
First time:
cd app
julia --project=. -e 'using Pkg; Pkg.instantiate()'
Subsequent:
julia --project=. -e 'using Pluto; Pluto.run()'
A browser window opens (default http://localhost:1234). Pick
predicate_explorer.jl from the file list. The notebook is reactive —
edit any cell, dependent cells re-run.
What you can do today (v1)
- Inspect every operational deadband, safety limit, mode invariant, and mode boundary.
- See the boolean ↔ continuous mapping for each predicate.
- View a 2D projection (T_avg × n) showing the operating polytope.
- Read the reach-status traceability table — which artifact has tried to discharge which obligation, with link.
- Move sliders to feel out the editing workflow.
What lands in v2
- Sliders write back to
predicates.jsonwith an "are you sure" gate. - Diff view: pending changes vs.\ the on-disk version.
- Re-run reach scripts in-place from the notebook.
What's the dream (v3)
- The FRET spec at
../fret-pipeline/pwr_hybrid_3.jsondeclares predicate names without numerical concretization. Could we use a structured ontology of physical bounds (fuel limits, trip setpoints, rate limits) plus the FRET text to derive the concretization? - Round-tripping changes back into the FRET model so the synthesis side stays consistent.
Caveats
- Pluto notebooks aren't great in version control — they're long files with cell UUIDs and order metadata. The notebook is committed because it's small and the cell order matters.
- Manifest.toml is gitignored; regenerate locally.