Verification

Owner closeout, 4 Nov 2026 (OQ-52): scoped M4 certification, frozen-closure acceptance and reduced-scope M5 physicist sign-off are recorded. Full current-baseline UQ remains incomplete. Earlier pending-gate wording below belongs to the dated research history; unresolved numerical properties retain their original status.

Verification

Scope

M4 separates formal properties over declared domains, statistical calibration and closed-loop comparisons. The owner-selected scope is OQ-22. No M4 certification review has occurred. The transport monotonicity property now has the certificates described below.

Checked exports

tkit.verify.export makes fixed float64 PyTorch copies of the Equinox networks. It includes input transforms, normalization and physical output transforms. Transport’s served response averages members in training space before inverse signed-log; EC clamps the raw mean after averaging. The selected pedestal retains its power-law residual, tanh-GELU, squared outputs and density scaling, with every solution explicit.

check_parity rejects nonfinite arrays, shape differences and a discrepancy beyond the selected numeric criterion. OQ-26 approves mixed relative and absolute parity after the relative-only check exposed cancellation near zero: 13 export checks pass in each mode: all selected members, random box points, local holdouts, physical transforms and served means, with rtol=1e-12 and atol=1e-12 in each declared output unitC-180. Formal proofs may not bypass this gate. The artifact manifests bind model, metadata and explicit box files and allow transport exports to load without opening the large training datasets. They establish storage consistency, not proved physical behavior (OQ-23).

Property contracts

six property contracts load; 14 property-validation tests pass in each mode, including malformed-domain, tolerance and output-schema rejectionC-177. tkit.verify.properties validates model scopes, output names, finite ordered boxes, the declared box data source, robustness tolerances and owner decisions. The existing OQ-20 monotonicity contract is retained.

The formal engine is auto_LiRPA with the input-splitting loop described below, under OQ-24. Bounds target every member; local robustness targets the served ensemble response. Launcher families stay categorical, and complete perturbation boxes that leave a training domain will be reported separately. No training box is silently shrunk to make a property pass.

Closed-loop comparison

tkit.verify.closed_loop reads provenance-bound saved runs and rejects unmatched settings, time/radial grids, nonfinite profiles or unconverged solver records. It checks that a face served by the surrogate was served by TGLF in the reference.

The historical paper eq. 41 convention is retained:

\[ E = 100\frac{\sqrt{\operatorname{mean}((T_{sur}-T_{ref})^2)}} {\operatorname{mean}(T_{sur})}. \]

The guard is defined on faces, while temperatures are cell-centred. Both temperatures are linearly interpolated to the same served faces. Whole-profile errors and a supplementary comparison using cells with both adjacent faces served remain visible. The saved runs’ grids are uniform; the reader rejects other grids without explicit face coordinates.

ITER passes (served-face T_e 7.42%, T_i 8.18%, both passing the 15% limit; whole profile 7.72/9.23%; 34 of 51 final-state faces servedC-178). MAST-U fails (served-face T_e 35.33%, T_i 49.15%, both failing 15%; whole profile 41.51/62.39%; cells with both adjacent faces served give 11.86/23.24%, still failing T_i; 13 of 26 final-state faces servedC-179), with the conservative cell diagnostic also failing ion temperature. Its failure remains ceiling K-030. The mask is only the final accepted state’s guard diagnostic; it does not measure fallback calls throughout the trajectory.

MAST-U scope (OQ-42)

Decided 25 Oct 2026. The MAST-U comparison against a TGLF reference trajectory (remediation step R6) is recorded as not evaluable, and MAST-U is presented for certification review with that limitation stated, alongside K-030 and K-032. ITER’s pass stands. The model, guard, acceptance limits and frozen splits are unchanged, and no further MAST-U reference compute is planned (entry 70).

The evidence is a read-only screen (scripts/m4_mastu_projection_screen.py) of OQ-38’s projection rule: in the reference only, set each negative raw TGLF heat diffusivity to zero, log it, and stop if a projected heat-flux magnitude reaches 1 gB. The single approved projected run stopped on that rule and saved no trajectory. The screen applies the rule to every interior face of the 40 saved states of the unprojected reference run (same profiles), inverting TORAX’s conversion to obtain the signed fluxes:

quantity	result
negative raw heat diffusivities, and those reaching the stop	150 negative raw heat diffusivities at 19 faces; 46 would reach the 1 gB stop, at 31 of 40 states, the first at state 1C-240
of those, on faces the projected reference would serve	26 would be served, the first at state 4 (faces 11 and 12, ion, −8.0 and −33.8 gB); near the axis the projected magnitude reaches 6020 gBC-241
candidate against the guarded historical reference, shared TGLF faces	T_e 32.0%, T_i 41.5% on the 14 faces where both serve TGLF, against the 15% limitC-242

The stop applies to every projection, served or not, so on this trajectory it fires at state 1; served faces alone would stop it at state 4. Projection would also change which faces are served: 840 of the 1040 face-states against 717 historically. Limits: the fluxes are inferred, not direct TGLF outputs; a projected run diverges from the saved trajectory after its first served projection, so the screen is not a replay; the edge faces 0 and 25 have no interior inversion. The last row compares with the guarded TGLF/fallback hybrid and is descriptive, not a gate result.

MAST-U remediation diagnosis

The owner prioritizes the failed MAST-U criterion (OQ-25). Matched final-state probes show substantial flux error: all 17 in-domain final-state probes succeed; on 12 served faces with reference flux above 1 gB, median relative errors are 41.17% Q_e and 74.27% Q_i; an unconstrained v3 control gives 38.05/71.88%C-181. The existing unconstrained v3 model also misses those feedback states. That control is diagnostic and does not meet the owner’s monotonicity contract; pointwise scores are not a coupled comparison.

The accepted-state replay reproduces the failed saved trajectory: all saved temperature, density and psi values are reproduced exactly; four final inner faces exceed the existing ion-diffusivity guard bound; 44.81% of accepted-state face diagnostics reject the surrogateC-182. Four final inner faces lie in the model’s box but exceed the ion-diffusivity guard bound. Captured masks cover accepted states, not the solver’s intermediate evaluations. The isolated inner served face has zero final heat flux in both model and TGLF even though its temperature differs. No face is removed from the acceptance comparison.

The approved refresh collected feedback-state labels on training equilibria only, with both test equilibria excluded. It retains full solver inputs and applies the approved-region filter. The local result review checks the finished artifacts: eight local checks pass for approved allocation/time, hashes and lineage, full-input alignment, case budget, unique coordinates, training-only equilibria, source model and finite successful labelsC-183. It compares each label input row with the selected case and the source trajectory’s accepted-state solver arrays, and binds lineage by hash. These checks establish collection integrity; they do not establish held-out accuracy or a successful coupled remedy. The owner approved artifact synchronization in OQ-28. We checked remote privacy settings and downloaded every uploaded record by artifact identifier: all 26 uploaded artifact records covering 18 distinct files match both remote SHA-256 metadata and downloaded bytes; the folder and private visibility match the approved request, and the offline payload queue is emptyC-184. Duplicate provenance sidecars are retained as distinct records; name-based retrieval is ambiguous for those duplicates. Downloads by identifier verify every record without changing the remote artifacts. Retraining and an improved closed-loop result remain pending. No new certificate or domain is deployed, and the 15% tolerance is unchanged.

Remaining acceptance work

Formal certificates, conformal coverage, the EC coupled reference check, certificate-bound guards, CI proof reruns and the human certification review remain pending. Pedestal has no labelled split for conformal calibration and no local full-EPED physics reference. The owner prioritizes diagnosing and remediating the MAST-U closed-loop failure first (OQ-25).

Candidate replay preparation

Entry 48 records R6 tooling. The runner supports an explicit immutable candidate directory while preserving default model selection. New trajectories record the full scenario configuration, source runner, model and metadata, scenario plan and equilibrium provenance. Preparation binds a source snapshot and checks every external input digest and environment version before execution.

Reference reuse reconstructs the historical scenario from its checksum-bound runner and clean source revision. Physics/core/dataset modules and the scenario plan are byte-identical to that revision. Solver, fallback, wrapper post-processing and guard settings match recorded metadata; the candidate differs in its model path. Its previously audited box stays fixed. Historical metadata lacks the run index, but its bound runner selects the first scenario explicitly. External dependency bytes and a full resolved configuration were not recorded historically; the audit states that limitation and checks pinned/current versions instead of supplying retrospective hashes. Actual post-run configuration, grids, time points, provenance and finite convergence remain required.

The formal comparison uses every candidate-served face, interpolating both profiles onto those coordinates and normalizing RMS difference by the candidate temperature mean. The report retains original served-mask counts, overlap and faces added/removed. A separate fixed-baseline-mask diagnostic evaluates the candidate temperatures on the old faces; it never replaces the formal mask. Whole-profile and both-adjacent-faces cell errors are retained. An isolated served face remains eligible for the formal metric even when the supplementary cell metric is unavailable. Existing comparison defaults are preserved.

Accepted-state history captures generic guard features and raw coefficients before post-processing. Rejection diagnostics count model-domain violations, generic feature finiteness/box failures, nonfinite coefficients, negative diffusivities, excessive diffusivity and convection. Predicate counts overlap, so a separate priority partition provides counts that sum to the number of rejected face states. Candidate diagnostics must reproduce the saved raw predicate exactly. The historical replay lacks generic features; its unavailable predicate evidence stays explicit. These rates describe accepted states, not intermediate transport calls, and no fallback acceptance threshold is chosen.

40 focused checks pass in normal and Tier A modes; the two-step training-only candidate smoke is finite and reconstructs the raw accepted-state guard predicate exactlyC-188 checks configuration/mask isolation, raw guard accounting, immutable package/input rejection and historical runner compatibility. A bounded two-step smoke uses a training equilibrium only and validates source-package execution, finite profiles and raw guard reconstruction. Saved baseline artifacts also reproduce the existing comparison exactly through the new report. No held-out candidate result or formal certificate is claimed.

Candidate replay result

Entry 49 records the consumed owner-approved attempt. The bounded solver run completes finite and converged; actual scenario settings, time/radial grids and checksum-bound inputs match preparation. The comparison rejects reference coverage (the single approved replay finishes in 65 seconds within its 240-second bound, with 40 finite converged steps and 146 passing integrity checks; comparison exits with a reference-coverage failure at candidate-served face 4, normalized radius 0.16C-189). The saved physics trajectory used fallback at a candidate-served face. A formal temperature pass/fail cannot be computed against that reference under the existing contract. Its original success report is absent; a separate provenance-bound, read-only saved-output audit records the failure without executing another solver.

Mask comparison retains every candidate face, added/removed faces and overlap. Descriptive distances to the saved hybrid physics/fallback trajectory use the same RMS normalization and are explicitly ineligible for acceptance. The fixed-baseline-mask comparison remains supplementary. All values and the electron regression remain visible: candidate/baseline serve 15/13 faces with 11 overlapping; fixed-baseline-mask candidate T_e/T_i errors are 42.1252%/48.1182%, versus baseline 35.3331%/49.1458%; candidate whole-profile errors are 29.7365%/41.8856%, and own-mask descriptive distances to the hybrid reference are 29.8865%/40.0063%C-190. No unfavorable face is removed and no criterion is replaced by a whole-profile metric.

Accepted-state raw predicate reconstruction remains exact. Counts distinguish overlapping predicates from an exclusive partition: candidate rejects 415/1040 accepted-state face records (39.9038%), versus baseline 466/1040 (44.8077%); exclusive candidate reasons are 341 model-box exits, 50 excessive diffusivities and 24 excessive convection values, with exact raw guard reconstructionC-191. Model-domain exits produce nonfinite raw surrogate coefficients on rejected faces; no accepted coefficient is nonfinite. Historical generic-feature evidence is absent. These are accepted-state face records rather than intermediate transport-call counts; V10 sets no acceptance threshold yet.

The historical reference contains no raw guard reasons, so its rejection cause cannot be reconstructed from its saved arrays. Diagnose reference admissibility before proposing new reference compute; rerunning an identical scenario does not ensure coverage. A separate single sampling experiment is proposed using training-only evidence, with unchanged original holdouts and physics. It needs a frozen implementation, checks, smoke and concrete resource review before fitting. Neither that proposal nor the consumed replay approves new compute, synchronization or model/guard replacement. K-030 stays open; no formal proof is supplied.

Reference diagnostic preparation

The saved reference retains its final mask and finite profiles but lacks full solver inputs, raw coefficients and accepted-state reasons. Its log confirms settings and convergence; it does not distinguish an input-policy failure from a nonfinite, negative or excessive transport coefficient at the uncovered face. No cause is inferred.

The prepared diagnostic preserves the scenario, physics sources, solver, guard and fallback. Each accepted state supplies full prepared inputs, worker-input validity, raw reference/fallback coefficients, generic features and the exact guard mask. Post-processing remains unchanged. Reporting retains all faces and both overlapping predicates and an exclusive guard partition. Input-policy invalidity is recorded separately; there is no surrogate model box on the TGLF reference. The last diagnostic supplies the final mask without an additional duplicate reference evaluation.

32 focused checks pass in each mode; a two-step synthetic training-equilibrium smoke is finite and reconstructs the raw guard exactly; all 77 source modules pass typing, and lint/format plus batch syntax passC-192 checks input conversion, mask reconstruction, immutable source/input rejection, allocation refusal and failed-run artifact retention. A bounded synthetic training-equilibrium smoke exercises host stepping and the real input converter while forbidding physical TGLF calls. It also checks canonical paths through source-package symlinks and the full resolved configuration. This is tooling evidence, not new physical labels, TGLF cost or temperature acceptance.

The source package freezes original inputs, candidate trajectory and dependency records. Numerical/input-stack distributions and the compiled TGLF extension/link closure are byte-bound; other installed distributions are version-bound. Historical missing dependency bytes remain explicit. A dedicated single diagnostic job, resource estimate from historical accounting and timeout limits were prepared for OQ-31. That preparation is historical; the approved, consumed diagnostic is recorded below. Failure retains partial outputs and failed offline tracking; uploads require later review.

If the diagnostic retains the uncovered face, it remains ineligible for the formal temperature criterion. Review the cause and any physically justified remedy before a new acceptance claim. The separate sampling experiment remains a proposal. Entry 50 is the narrative account. Current model/guard and K-030 remain.

Reference diagnostic result

The owner-approved diagnostic is consumed. the diagnostic completes in 517 seconds within its 30-minute bound, with 40 finite converged steps, exact historical temperature/density/poloidal-flux-profile and final-mask equality, and 171 passing saved-output integrity checksC-193 records its bounded completion and exact saved-profile/final-mask reproduction. The accepted-state history retains prepared inputs, raw transport and fallback coefficients, generic features and guards. Source/input/dependency and full resolved configuration bindings match the reviewed package; historical missing external dependency bytes stay missing.

final face 4 at normalized radius 0.16 has valid inputs but raw electron heat diffusivity -0.02792124888 m²/s; negative heat diffusivity rejects that face at 8 of 40 accepted states; reference rejection is 323/1040 accepted-state face records (31.0577%)C-194 explains the uncovered face. The prepared inputs pass the worker policy. Negative raw heat diffusivity fails the existing guard before diffusivity post-processing. The final rejection is electron heat diffusivity; earlier rejected states include ion heat diffusivity. No face or coefficient is removed, clipped or admitted to change reference coverage. Every worker-input and raw guard decision is reconstructed exactly. Accepted-state rejection reasons retain overlapping counts and an exclusive partition; they are not intermediate solver-call accounting or a fallback acceptance gate.

The read-only audit uses the same diagnostic-report logic and checks artifact integrity, not independent physics validity. Exact historical array equality is checked separately. Completed offline local artifact copies match by checksum; synchronization still needs payload review. Entry 51 is the narrative account.

The saved raw coefficients follow the reference’s flux-to-transport conversion; direct heat-flux and mode-resolved outputs were not retained. Signed transport’s physical or numerical origin and any flux-preserving reference treatment require physics review (OQ-32). Another identical run does not make the reference admissible. Formal candidate temperature acceptance remains not evaluable, K-030 stays open and the current model/guard remain selected. The separate sampling proposal has no frozen fitting request.

Signed heat conversion review

The saved-state review reconstructs face temperatures and radial derivatives with the pinned transport solver’s cell representation and bound magnetic geometry. Source checks cover the recorded conversion, geometry and gradient files. No simulation or transport model is prepared; physical solver calls are forbidden. Every state of the investigated face is retained.

For each heat channel the converter uses

[ P_s=Q_s^{gB}Q_{GB},V’/_b, s=-P_s/(n_s{_n}T_s,g_1/V’+), ]

with temperature in joules and the fixed numerical denominator correction. Inverting this equation gives an inferred heat flux, which is converted back through the native implementation. 33 focused checks pass in each mode, including 14 new sign/units/history tests; all 80 native heat-converter round trips meet the mixed 1e-12 parity criterion (maximum absolute difference 8.88e-16 m²/s), 32 numerical source files match the diagnostic bindings, and all 78 source modules pass typingC-196 records those numerical checks and synthetic tests. A round trip checks algebra and units; it cannot independently validate the originating solver flux.

the final electron heat flux is inferred as -0.001689376033 gB; all 9 negative channel records at 8 accepted states have outward-decreasing temperature and no denominator-epsilon sign reversal, with maximum epsilon ratio 1.03e-11; all negative magnitudes are below 1 gBC-195 narrows the sign diagnosis. Temperatures decrease outward in all negative heat-channel records, and the denominator correction changes none of their signs. The saved coefficients therefore imply inward signed heat flux in this representation. Their magnitudes are below the offline accuracy gate’s reference-flux floor; neither that gate nor their small size establishes physical validity or a numerical-error explanation. The inferred ion channel is the reference worker’s sum over main and impurity ions, whereas the surrogate learns main-ion heat flux. Separate species contributions remain unobserved.

The current raw guard rejects negative diffusivity before post-processing. Moving a positive floor before that rejection changes reference physics and coverage. A signed-flux-preserving closure would require an explicit stable representation and compatible surrogate contract; it cannot be inferred from one effective coefficient. The current in-memory interface does not expose mode spectra, so richer collection requires another prepared output route.

This is an algebraic/source review, not an adopted physical remedy. OQ-32 now selects retaining the current nonnegative contract while investigating. Formal candidate acceptance remains not evaluable, and K-030 stays open. Current model/guard, every face, splits and tolerances are preserved. Entry 52 is the narrative account.

Owner disposition and licence

The owner selected retaining the existing positive-flux approximation, physical contract and raw guard (OQ-32). Richer direct-flux and supported mode evidence requires a prepared diagnostic output route, validated tooling and a concrete execution review. The existing inferred-flux and conversion evidence remains qualified as in C-195/C-196; this decision supplies no new physics measurement and makes no rejected face admissible.

OQ-17 selects MIT for original toolkit code/documentation. The root licence has copyright 2026 Vignesh Gopakumar; package metadata reads the licence file. Local source and wheel builds contain that text and declare the licence file. The wheel retains the existing EPEDNN licence and notice byte-for-byte. These packaging checks do not replace dependency/data redistribution reviews or authorize a public release. Runtime source, tests and model selection are unchanged; the retained test statistics remain historical execution evidence.

Direct heat diagnostic route

An original native driver links the byte-bound TGLF library, reads the complete generated input and executes one local-state solve. Full-precision text retains particle and heat flux by species, low-k heat totals, the native ky grid and weights, growth/frequency pairs, and saturated and quasilinear heat spectra by species, field, ky and mode. An independent synthetic branch fills those arrays without reading an equilibrium or calling the solver. The strict reader rejects missing, extra, nonfinite or dimensionally inconsistent records.

The paired route runs the pinned in-memory wrapper in a fresh process with the same complete defaults, global settings and prepared local inputs. Input precedence matches the reference worker. Native shape parameter names omit the wrapper’s local suffix; mapping them preserves register values and the native generated-file audit checks all settings. No parser default silently replaces a declared value.

For the declared logarithmic ky grid, each interval uses D = log(k1/k0)/(k1-k0), w1 = k1*(1-k0*D) and w0 = k0*(k1*D-1), with first weights zero and the first ky. The contribution is w0*previous_spectrum + w1*current_spectrum. Sum all fields, modes and intervals for total heat; native low-k heat retains phi and perpendicular magnetic fields through ky at most one. Keep all signed contributions and compare totals at mixed relative/absolute tolerance 1e-12 in gyro-Bohm units.

Separate comparisons report native versus paired species fluxes, and paired electron/total-ion flux versus the saved inverse conversion. Any disagreement is retained as diagnostic evidence. The native sheared double-pass eigenvalues may retain unsheared first-pass values; growth/frequency pairs alone neither label a mode physically nor prove numerical convergence. Solver status and finite output checks supply only the supported numerical diagnostics.

55 focused checks pass in each mode, including 22 direct-output and settings checks; all 79 source modules pass typing; the compiled synthetic writer preserves signed species heat and passes total/low-k spectral parity without calling TGLFC-197 records preparation checks. This does not establish direct physical flux parity, reference admissibility or coupled acceptance. OQ-33’s permission for runs shorter than six hours leaves the selected model/guard, physical contract, training isolation and owner physics decisions in force.

Diagnostic wrapper status fix

The first rich diagnostic failed in paired reporting after its first solve: the compiled wrapper exposes integrated flux registers but not the Fortran interface’s error-status register. Source availability is insufficient evidence of Python-interface availability. The consumed attempt retains partial native output, failed logs, executed-call count and final scheduler accounting.

Paired reporting now records whether status is exposed, preserves absent status as unavailable, validates finite fluxes and retains any reported failure status. Native status remains available through the driver. This checks software/output integrity; unavailable convergence evidence is not replaced by a zero status. 25 diagnostic checks pass in each mode, including unavailable status, exposed failure status and nonfinite output; 33 unchanged focused checks are retained for 58 focused recorded passes per modeC-198 binds the synthetic worker regressions. A new package is frozen after the correction, with a separate summary and retained test-report directory; consumed request evidence is never overwritten. ## Signed reference literature review {#signed-reference-literature-review}

The complete local-state collection is retained despite a subsequent tracking failure (648 integrity checks pass on the complete 15-state collection; all affected signed states agree between backends, but four control states fail the existing parity criterion; original terminal tracking failure is preserved and archive recovery calls no solverC-199). The offline tracker copied repeated basenames; archival recovery instead preserves relative case paths in one checksum-bound bundle. Recovery does not call the solver or alter original accounting.

The owner delegates approval of the recommended reference method (OQ-34). The target is signed, species-resolved TGLF with fixed turbulence settings and matched geometry, normalization and transport equations. The present guarded hybrid trajectory remains a regression baseline with unresolved coverage. Numerical reproducibility, physical validation and coupled acceptance are distinct.

GACODE output definitions distinguish species energy weights, eigenvalues and integrated spectra. Staebler et al. (2024), §5.2 motivates checking anomalous reduced-model cases before higher-fidelity gyrokinetic study. Snoep et al. (2025) demonstrates matched spectral and heat-flux verification. Lestz et al. (2025) shows spherical-tokamak predictions depend on turbulence and transport treatment. These sources support the verification method, not this case’s physical validity.

Repeatability tooling retains two fresh-process results per selected state and backend, each compared with its consumed output at the existing mixed 1e-12 criterion (31 synthetic diagnostic tests pass in each mode, including archive identity and repeatability completeness/discrepancy checks; 33 unchanged focused records are retained, giving 64 focused recorded passes per modeC-200). Missing identities or nonfinite values invalidate the collection. No averaging, favorable-backend selection, negative-flux clipping or physical mode assignment is performed. A flux-preserving conservative stable energy closure remains to be reviewed; a negative effective turbulent diffusivity does not by itself justify negative total diffusion. ## Reference repeatability {#reference-repeatability}

The bounded fresh-process diagnostic completes and its saved-output audit passes (521 saved-output checks pass; every within-backend fresh-process repeat is exactly equal and agrees with its consumed output, while all four cross-backend discrepancies persist; native accounting completes within the reviewed bound and the offline archive copy matches its checksumC-201). For each selected state, native and wrapper backends receive two unchanged-input calls. Report each species vector separately; compare the two vectors within a backend and compare each with that backend’s consumed result. Retain cross-backend comparisons separately at the existing mixed 1e-12 criterion.

Within-backend vectors repeat exactly; the prior cross-backend differences persist. Repeatability cannot establish numerical convergence or physical validity. The historical pinned wrapper remains the reproduction anchor, while the native output route supplies additional diagnostics. A read-only assignment audit finds no observable input-register precision loss. The cause of backend differences remains unresolved; no particular compilation or physical mechanism is asserted.

The next reference review should quantify basis/quadrature/wavenumber convergence with predeclared refinements and unchanged baseline controls. Any stable signed energy closure must retain the reviewed flux, conserve energy and demonstrate time/grid convergence. The served surrogate contract, raw guard and temperature threshold remain fixed. K-030 and M4 stay open.

Bounded reference refinement

The synthetic refinement and evidence checks pass (40 focused synthetic checks pass in each mode after the input-path correction, covering signed channels, refinement identities, baseline drift, incomplete evidence and existing diagnostic output handlingC-202). Retain original settings, then vary parallel basis, Gauss–Hermite quadrature and high-wavenumber resolution separately and together. Both minimum and maximum basis settings vary, affecting width optimization and the final eigenvalue solve. Their effects are not isolated by that ladder. Pinned KYGRID_MODEL=4 leaves its low-wavenumber nodes fixed while NKY refines its logarithmic high-wavenumber part.

For each backend and species, report all fluxes, observed minimum/maximum, successive differences and sign changes. Form the ion sum before taking these statistics. Relative last-step differences divide by the larger absolute flux at the two levels, with zero/zero reported as zero. No flux floor, averaging, Richardson extrapolation or new acceptance threshold is introduced. Backend parity at the existing mixed tolerance remains separate from physical convergence.

The first execution failed before solver calls on relative historical evidence paths after a working-directory change. The path fix and relocated preflight preserve source/input bindings. A separate quota-failed preparation is retained; OQ-35 approves alternate shared-work storage for this diagnostic only. K-030, reference admissibility and coupled acceptance remain open pending measurements.

Reference refinement result

The complete bounded collection passes its saved-output audit (2076 integrity checks pass on the complete bounded study; baseline reproduction, signed species outputs, spectral accounting, native completion and the local archive copy are verified, while electron-flux signs change across refinement levels and finest-level backend differences remainC-203), but the reference remains numerically unconverged. Signed electron heat changes sign across levels at every selected state in both backends. The joint minimum-/maximum-basis ladder has substantially greater sensitivity than the separate quadrature and high-ky ladders. Since minimum basis sets the width-search calculation and maximum basis sets the final solve, the current evidence cannot assign the effect to one component. Finest-level backend differences persist. No particular compiler or physical instability is identified.

Next separate those two basis roles and retain width/growth diagnostics before extending the refinement budget. Low-ky, width-search resolution and mode-count limits remain explicit. A stable conservative signed-energy closure remains a later conditional review, not a consequence of seeing negative values at the finest tested resolution. Current model/guard, the temperature criterion and K-030 remain unchanged; no new coupled acceptance is evaluated.

The archive is checksum-matched in the authoritative local tracking record. Simvue’s mirror was unavailable; neither a remote record nor an upload is claimed.

Separate basis roles

The factorial diagnostic crosses width-search basis and final-solve basis while holding other saved settings fixed. Its synthetic reporting checks pass (54 focused synthetic checks pass in each mode, including separated basis effects, interactions, signed channels, incomplete evidence and consumed-control drift; 553 unchanged recorded checks are retained separatelyC-204). Report changes along each fixed-other-basis axis and the cross-difference relative to the original minimum/maximum setting; retain signs, species channels, total-ion sums and both backends. Prior diagonal cells serve as reproduction controls, not convergence targets.

The native output driver reads selected width, saved search growth and retained final-mode spectra from the unchanged linked library. The protocol requires zero shear and a fresh width search: the double-pass path could overwrite a register with a different meaning. The retained width can revert to its input value if the final solve finds no unstable mode. Mode ranks are not tracked physical branches. The wrapper supplies fluxes only. Freeze and verify the package before the bounded allocation, then reconstruct its saved outputs independently.

Basis-role results

The completed grid passes its saved-output audit and reproduces all consumed controls (2139 integrity checks pass on the complete 54-pair basis grid and all 36 consumed-control comparisons reproduce the preceding study; electron flux changes sign at every state, steps reach 4.28 gB along the final basis and 4.11 gB along the search basis, and at the largest final basis the flux is a residual of order 1e-3 gBC-205). Both roles change the flux: steps along the final-solve basis are typically larger, but single steps along the search basis also exceed 4 gB, and cross-differences reach 3.96 gB. Search growth is identical across final-basis settings, and every width change along the final basis is the stable-solve fallback to the input width. At the largest final basis, low-ky flux collapses and the remaining signed flux is of order 1e-3 gB; at the middle final basis with larger search basis, high-ky roots with growth rates of 2-4 carry much of the flux. Up to half of unstable cells select the upper width bound. These are register observations; they identify no physical branch, cause or correct setting.

Extension results

The extension diagnostic passes its audit and reproduces its controls (3029 integrity checks pass on the complete 78-pair extension and all 36 control comparisons reproduce job 2687308; NBASIS_MAX 16 still moves electron flux by up to 0.48 gB per step, and widening the width search from 1.65 to 3.3 changes it from about 1e-3 gB to as much as 181 gBC-206). Raising the final basis from 10 to 16 does not settle the electron flux, and high-ky electron-direction roots appear and vanish along the ladder. Raising the width search’s upper bound from 1.65 to 2.3 and 3.3 changes the flux by up to five orders of magnitude, almost entirely at ky≤1; the default bound is selected often, and the search optimum becomes interior only at 3.3 for the standard basis. These are observations of the pinned solver, not error bounds or causes. The standard settings remain the training-label convention (K-032).

Projected-reference stop review

OQ-38 selects the standard-settings convention and permits projecting finite negative heat diffusivities to zero in the reference only. The consumed trajectory stopped at the approved projection limit (the projected-reference job failed after 108 s when the log reported 3.93119 gB against the 1 gB stop limit; no completed reference was savedC-217). The saved exception reports a magnitude but no triggering face, state or channel. This supplies no completed reference and cannot close K-030; the convention does not lift the numerical sensitivity in K-032. OQ-42 then limited the MAST-U scope (MAST-U scope).

The original host runner accumulated projection history in memory and raised on the limit before saving it. Existing tests checked that it stopped and wrote no successful trajectory, so they missed the lost evidence. The corrected runner writes a bound projection log before enforcing the limit and saves a separate raw diagnostic snapshot on failure. Regression tests check those bytes and their provenance after the actual loop raises, with physical solver calls forbidden.

Only finite negative heat coefficients are zeroed. Both infinities and NaN remain invalid; a numerical maximum alone would incorrectly map negative infinity to zero. The saved-output audit requires full guard features and exact boolean-mask dimensions. Future acceptance also checks parent hashes and the complete frozen scenario, so individually valid sidecars cannot hide substituted inputs. These changes do not modify the selected surrogate or production guard settings.

The original failed package and missing information remain recorded. No repeated reference run or recovered face identity is claimed. Entry 66 records the review.

Transport monotonicity

The V4 result is all 20 members of each ensemble pass both heat-flux monotonicity properties, with derivative lower bound zero over the full training boxC-247. Narrative entry 74 accompanies this technical account. The result proves an imposed network property, with the K-025 physical-model departure caveat retained.

For one constrained head, write its derivative as

\[ \frac{\partial Q}{\partial g} = \frac{s_y}{s_x} W_{out} D_L W_L \cdots D_0 w_g. \]

The gradient coordinate is excluded from the free trunk and from its own head’s free input vector. The effective constrained weights are absolute values of saved parameters; all normalization scales are positive. For ELU, the derivative is \(\exp(\min(z,0))\); for reflected ELU it is \(\exp(\min(-z,0))\); for the saturated mix it is \(\exp(-\max(|z|-1,0))\). Every derivative lies in \([0,1]\).

The structural route checks the saved routing, finite parameters, scales and supported transforms. The second route exports the derivative product itself and uses auto_LiRPA interval bound propagation over independent diagonal entries in \([0,1]\). This enlarged slope domain contains the image of the entire raw-input box; no box shrinking or input split is required. The result is a non-negative derivative before the output ReLU. The positive affine maps, ReLU, inverse signed-log transform and mean preserve monotonicity through serving.

Each export and derivative graph is checked against JAX before the corresponding proof, on random-box and original held-out points, under OQ-26. These numerical comparisons validate the implementation path; the domain-wide result comes from the structural and interval arguments. The certificates cover real-valued functions represented by the saved parameters, not directed-rounding guarantees for every floating-point execution.

Certificates retain individual member/pair bounds, model and box hashes, verifier versions and source digests. V4 is complete for the two baseline transport ensembles. Physical reference admissibility, output bounds, conformal calibration, production guard binding, CI re-proofs and the final certification review remain separate obligations.

Output bounds

The first bounded run is audited: EC all five EC members have finite CROWN bounds for both launcher families; current and width bounds remain very looseC-262; pedestal all nine pedestal pressure and half-width pairs have finite bounds over the recorded ITER trajectory box, with the widening and domain clipping statedC-263. Transport remains unresolved (all twenty members of each transport ensemble have finite training-space bounds that overflow the inverse signed-log transform; no finite physical guard domain is certifiedC-264). V5 is not complete and these bounds are not installed in production guards. Narrative entry 78 accompanies this record.

V5 now has an executable CROWN calculation and complete input splitting. The verifier first checks each proof export against JAX on random box points and the original held-out inputs. Transport’s input logarithms map interval endpoints monotonically. Its signed-log inverse is applied only after bounding the training-space output. EC fixes the launcher indicator to one family at a time while retaining every other stored input range, then applies the serving clamps to each member’s interval.

The proof graph expresses ELU as

\[\operatorname{ELU}(x)=\operatorname{ReLU}(x) +\exp(-\operatorname{ReLU}(-x))-1.\]

The saturated monotone-head activation uses the equivalent expression

\[\operatorname{clip}(x,-1,1) +\exp(-\operatorname{ReLU}(-x-1)) -\exp(-\operatorname{ReLU}(x-1)).\]

These identities avoid unsupported export operators. They preserve the real-valued function, but the separate relaxations can be loose; passing parity does not guarantee useful bounds. The retained certificate names the float64 calculation and does not claim directed-rounding verification of IEEE execution.

Each split bisects the largest side relative to the original box. A parent is replaced only after both children have bounds. Child intervals are intersected with their parent, and the final interval is the minimum lower and maximum upper bound across all retained leaves. The leaf and time budgets are explicit. The time budget is checked between bound calls; the execution wrapper supplies the hard process limit. Sampled extrema measure the interval’s tightness and must lie inside it; samples never supply the proof.

For the pedestal, the diagnostic now saves the upstream input vector at every retained output state, its feature names and model hash. The proof box encloses those vectors, widened by a declared fraction of the upstream range on each axis. Any clipping of that margin at the upstream domain is recorded; a visited point outside the upstream domain fails. The upstream box alone cannot replace a missing trajectory. CROWN bounds the neural residual; interval composition adds the power law, squares each solution and multiplies each pressure by the positive density interval. All pressure and half-width solutions remain explicit, including the GH solution used by TORAX.

Reports bind the model, property, boxes, datasets, producing source and verifier library. A nonfinite physical interval is recorded as unknown. Such a row supplies no guard domain; V10 integration requires usable certified bounds and the owner’s fallback-rate threshold.

Optimized output bounds

The runner also supports --method alpha-CROWN, with explicit optimizer iteration and soft time budgets. Ordinary CROWN remains the default. On every sub-box, the optimized route computes ordinary CROWN, interval propagation and alpha-CROWN, then intersects their output intervals. Thus it cannot loosen the same sub-box’s baseline bound, and interval propagation retains structural ranges such as nonnegative heat-flux outputs. Invalid or nonfinite optimizer results fail explicitly.

The optimizer budget applies separately to lower and upper bound calculations and is checked between iterations. Graph setup and an in-progress iteration can exceed it; a separate process timeout supplies the hard limit. Certificates and their provenance record the selected method, iteration cap and soft time budget. Arithmetic remains float64 throughout. A physical-transform overflow now identifies inverse signed-log and the largest training-bound magnitude in the retained failure reason.

The retained follow-up uses the original complete transport boxes and weights. Its settings are three optimizer iterations, a five-second soft budget per bound side and one leaf per member; both twenty-member runs finished within the nine-minute hard process limitC-267. The widths relative to the earlier run are median width 0.164 of the earlier bound, range 0.082–0.605 across member outputs; all twenty physical member results remain unknownC-265 for ITER and median width 0.114 of the earlier bound, range 0.060–0.220 across member outputs; all twenty physical member results remain unknownC-266 for MAST-U. This compares one-leaf optimized bounds with four-leaf ordinary CROWN bounds; it is not an experiment that holds the partition budget fixed. Every physical member result remains unknown. No production guard domain follows from this experiment.

For intervals \([l_C,u_C]\), \([l_I,u_I]\) and \([l_A,u_A]\) enclosing the same output, the returned interval is

\[[\max(l_C,l_I,l_A),\;\min(u_C,u_I,u_A)].\]

This cannot loosen the ordinary CROWN interval on that same sub-box. Nonfinite or inconsistent intervals are rejected. The retained audit checks model and property identity against the earlier run, frozen source digests, complete input coverage, all member outcomes and the physical-transform overflow reasons. This audit shares the toolkit’s provenance machinery; it does not supply independent verification of auto_LiRPA or directed-rounding guarantees.

The implementation is retained in the experiment’s frozen source snapshot and was integrated in the subsequent proof-tool commit after focused validation. Narrative entry 79 accompanies this account.

Conformal calibration

V7 is complete for the three labelled surrogates (90% intervals calibrated on the v1 validation split cover 0.887–0.907 on the v1 test and v2-random splits (6 outputs, ITER and MAST-U); 9 of 12 lie in the 0.893–0.907 range expected for exchangeable data, the other three miss it by at most 0.006C-256, the same intervals cover 0.996–1.000 of the v3 test states; there the half-width that would give 90% is 3.3–5.5 times smaller in signed-log units (ITER Q_e 0.48 against 2.21)C-257, 90% intervals calibrated on 190 guard-accepted validation states (4 runs) cover 0.876–0.978 of 548 served test states (8 runs); all six outputs lie within or above the 0.856–0.938 range expected for exchangeable data; per-run coverage 0.78–1.00C-258). Entry 76 is the narrative account.

For each served output, with prediction \(\hat y\) and label \(y\) on \(n\) calibration points, the score is \(s_i = |y_i - \hat y_i|\). The half-width is the \(k\)-th smallest score, with \(k = \lceil (n+1)(1-\alpha) \rceil\) and \(\alpha = 0.1\). The interval is \([\hat y - q, \hat y + q]\). If calibration and test points are exchangeable, the interval covers a new label with probability at least \(1-\alpha\). The probability is marginal, over both the calibration draw and the new point. MAPIE’s prefit SplitConformalRegressor computes \(q\), and the code checks each value against the exact rank.

The prediction is the one each guard serves. - Transport. The prediction is the members’ mean in training space, \(t = \operatorname{sign}(Q)\log(1 + |Q|)\). The score is taken in \(t\), and the physical interval is the inverse transform of \([\hat t - q, \hat t + q]\). The transform is increasing, so coverage is the same in both spaces. A half-width \(q\) spans a factor \(e^{q}\) on \(1 + |Q|\). - EC. The prediction is the bounded per-MW output. Only states that the EC source’s guard would accept count: padded box, finite outputs, and member spreads within the source defaults. Transport counts only points inside its training box.

Calibration uses the split recorded with each model, which also chose each member’s early-stopping epoch. Test coverage is the evidence. For \(m\) test points, the number covered under exchangeability is beta-binomial with parameters \((m, k, n+1-k)\). Its central 90% range, which includes both random draws, is stored beside each coverage. Before calibrating, the code re-scores every split and must match the model’s stored RMSE to \(10^{-4}\); the match was exact.

The results, stored per surrogate: - Transport, data drawn like the calibration split. Coverage is close to 0.9. - Transport, held-out TORAX trajectory states. Coverage is 0.996–1.000. The half-widths that would give 90% there are 3.3–5.5 times smaller. Whether to add a loop-state calibration for M5 awaits an owner decision. - Transport, by flux size. The score is uniform in \(t\), so coverage is lower where \(|Q| > 1\) gB (0.86–0.90 on v1 test) and higher below it. - EC. Pooled coverage of the 548 served states from eight held-out runs is 0.876–0.978. Per run it ranges from 0.78 to 1.00. Within a run, states are correlated. - Pedestal. EPEDNN has no labelled data here, so it has no interval.

Records bind the model and manifest hashes through provenance sidecars. Readers obtain them through load_record, which refuses a record whose model hash differs.

Loop-state calibration (OQ-44)

The owner chose a second transport calibration on the states the coupled runs visit, for M5 (calibrated on half of the held-out v3 trajectory runs, the 90% half-widths are 0.21–0.32 of the V7 values; the intervals span a factor 1.8–3.3 on 1 + abs(flux) instead of 9–60C-259, calibrated on 16 held-out runs and tested on the other 16, coverage is 0.870–0.894; the reverse direction gives 0.905–0.924; single runs 0.75–0.97C-260, calibrated on 4 held-out runs, the intervals cover 0.936–0.966 of the other 4; calibrated the other way they cover 0.711–0.818; not reliable for a new ITER runC-261). Entry 77 is the narrative account. The V7 records above remain the M4 deliverable.

The held-out v3 test runs are whole TORAX trajectories: eight for ITER and 32 for MAST-U. The split rule was committed before any residual on these states was computed: - group the runs by scenario family (ITER) or equilibrium (MAST-U); - permute each group’s runs with a fixed seed; - deal the runs alternately to half A (calibration) and half B (report); - drop states shared by runs in both halves (common start-up states).

The method is otherwise the V7 one. The reverse direction, calibrating on B and reporting on A, tests whether runs are exchangeable.

The half-widths fall to 0.21–0.32 of the box-wide values. For MAST-U, coverage of the other half is 0.870–0.894, and 0.905–0.924 in reverse; single runs range from 0.75 to 0.97. For ITER, coverage of B is 0.936–0.966, but only 0.711–0.818 in reverse. The marginal guarantee assumes that calibration and test points are exchangeable. With four runs per half and systematic differences between runs, that assumption fails for ITER. A calibration that treats runs as the unit needs more held-out trajectories than the eight available.

Direct ELU pilot

A separate proof graph replaces the ELU decomposition with a direct convex relaxation. For alpha=1, let \(f(x)=x\) for \(x\ge0\) and \(f(x)=e^x-1\) otherwise. On a finite interval \([l,u]\), the tangent at \(t\) gives \(f(x)\ge f(t)+f'(t)(x-t)\), and convexity gives \(f(x)\le f(l)+(f(u)-f(l))(x-l)/(u-l)\). Point intervals use the local derivative; positive intervals are exactly linear. The fixed tangent uses the interval midpoint clipped to \([-1,0]\), with exact handling for point and positive intervals. This choice is valid but does not optimize tightness.

The saturated head has the equivalent expression \(f(1-\operatorname{ReLU}(-s))-f(1-\operatorname{ReLU}(s))\). Each term is in \([-1,1]\), so the expression retains the structural range \([-2,2]\) without subtracting unbounded linear terms. Input preprocessing, normalization, weights, heat-output ReLU and inverse signed-log remain those of the saved model. The direct-ELU operator is used only by the separate experimental proof runner.

Fresh JAX parity on random-box and original held-out points precedes each proof, including the existing physical-export check. CROWN is intersected with interval propagation. The focused checks are 40 focused checks pass in both normal and Tier A modes; lint, formatting and typing passC-269. The pilot outcome is member 0 of each ensemble remains unknown; both processes complete in about 23 seconds, with physical inverse-transform overflow and looser intervals than the earlier optimized runC-268: both selected members remain unknown, and the unoptimized bounds are looser than the previous optimized calculation. The other members were not attempted. No physical counterexample or new guard domain follows.

The audit binds saved source, model, property, full-box intervals and process outcomes. Arithmetic has the same float64 real-network scope as the earlier V5 calculations. Improve intermediate intervals and tangent selection before another frozen pilot; a larger run of the current method is not justified by these results.

Optimized direct ELU and intermediate diagnostics

The direct-ELU lower relaxation can be parameterized by slope rather than tangent location. For \(a\in[0,1]\),

\[f(x)\ge ax+a-1-a\log a.\]

For \(a>0\) this is the tangent at \(\log a\); at \(a=0\) its continuous limit is the constant \(-1\). This includes strongly saturated lower bounds that the earlier fixed tangent, clipped to \([-1,0]\), could not select. Optimizer parameters are clipped to \([0,1]\) separately per objective and bound side. Positive-only and point intervals retain their exact affine expression. The upper secant and the saved network remain unchanged. A finite logarithm floor handles the zero-slope limit with a conservative intercept and finite gradients.

The runner computes CROWN and interval propagation first, then alpha-CROWN, and intersects all three results. It saves each interval separately so the effect of optimization can be assessed on the same graph and domain. It also records the minimum lower endpoint, maximum upper endpoint, largest neuron width and sign-region counts for each ELU input in the baseline CROWN pass. Completed diagnostics remain available if subsequent optimization fails.

The new frozen pilot uses member 0 of each baseline ensemble, a single leaf and twelve optimizer iterations with a ten-second soft budget per bound side. Each process finishes in about 45 seconds. Its outcome is both selected members remain unknown despite interval-width reductions of about 30–275 times against the same-graph fixed-tangent baseline; physical inverse-transform overflow persistsC-272; its validation is 50 focused checks pass normally and with Tier B disabled; repository lint, formatting and typing of all 91 source modules passC-273. The training-space interval widths are 0.00364–0.02586 of the same-process unoptimized widths for ITER and 0.00549–0.03332 for MAST-U. No finite physical enclosure results.

There are 39 direct-ELU nodes in each graph. Baseline activation-input widths reach \(1.1014\times10^{10}\) for ITER and \(1.1079\times10^9\) for MAST-U. These intervals describe a relaxation and need not be reachable model activations. The retained source/model/property hashes and saved-output audit preserve the comparison. Next tighten intermediate intervals, using analytic activation ranges while retaining complete input coverage, before another member-level pilot. The present result does not justify an ensemble expansion or a guard output domain. V5 and K-033 remain open.

Intermediate range pilot

The next proof setting enables the verifier’s intersection of intermediate CROWN and interval-propagation bounds. Direct ELU activation intervals are obtained from monotonicity once the preactivation interval is bounded. The setting is explicit and opt-in; prior calculations keep their defaults.

The two-member full-box pilot gives both selected transport members remain physically unknown; largest baseline activation widths fall to 0.246 and 0.449 of the preceding pilot, but inverse signed-log overflow persistsC-274. Largest baseline activation-input widths fall to 0.2456 of the preceding ITER width and 0.4491 for MAST-U. The physical inverse still overflows. Final optimized intervals are not uniformly tighter: the soft optimization time limits stop iterations at different points. Neither a finite physical bound nor a full ensemble certificate follows, and the other members were not attempted.

EC local robustness and recorded states

The EC robustness property applies to the served ensemble heating centre. If \(g_i(x)\) is member \(i\)’s raw output in physical units, the source returns

\[c(x)=\operatorname{clip}\left(\frac{1}{M}\sum_i g_i(x)_2,0,1\right).\]

The proof graph sums raw member centres and divides by the member count. This preserves the batch axis for the verifier. A monotone clamp is applied to the final raw enclosure. Clamping each member first would change the response. Fresh parity against JAX is checked on recorded states and original held-out inputs before any local bound can be issued.

The exact input matrix is recorded from TORAX’s accepted output states using the source’s own interpolation: electron temperature, density and effective charge at the reference tabular radii, then the launcher flag and launch coordinates. Saved face profiles allow an independent reconstruction. Model and metadata hashes, complete input and resolved configurations, times, numerical outputs and raw guard decisions accompany the trace. The result is 30 upper-launcher states (29 served) and 27 equatorial-launcher states (16 served) retain exact features, profiles, outputs, model identity, configurations and guard decisionsC-275. This is state recording, not a new physical reference pass.

At a state \(x\), continuous coordinates receive half-width \(\delta_j=0.01(u_j-l_j)\) from the full stored training ranges; the launcher flag has zero half-width. The full local box is \([x-\delta,x+\delta]\). The property requires it to lie inside \([l,u]\); boundary sides are not clipped. Only an eligible box can be certified against \(|c(z)-c(x)|\le0.05\) throughout the box. A true evaluated violating point can falsify the property. An enclosure that extends past the tolerance is unknown unless such a point is found.

Every recorded box is out of domain (all 57 complete EC local boxes are out of domain, including all 45 served states; zero robustness proofs or model counterexamples are claimedC-276). Effective charge lies near the lower 1.6 boundary and its symmetric perturbation extends to about 1.596. Upper and equatorial launcher positions occupy opposite training R/Z edges; perturbing either position symmetrically crosses a boundary at every state. Some late equatorial temperature profiles are outside the trained range as well. The state guard can serve a point at an edge without certifying a neighbourhood. No CROWN state-bound calculation is needed for these exclusions.

K-034 records this limitation. Under OQ-45 the owner selected retaining the strict result as a limitation, with no clipped box or changed perturbation scope. No property or tolerance has changed. The deterministic later reference selection is twenty output states per launcher are selected at evenly spaced indices for the later GENRAY comparison; no reference solver execution or accuracy resultC-278: equally spaced state indices including both endpoints, independent of guard outcome or surrogate error. Equilibrium, profile conversion, launch settings, executable and resource bounds still need a concrete GENRAY package.

The first frozen package omitted dataset provenance sidecars. Its proof stages failed during loading; the successful EC recordings were retained and reused. A corrected package binds those sidecars and exercises all actual relocated loaders before proof execution. Independent audits check the saved bounds, feature reconstruction, inference outputs, raw guard masks, complete local boxes, boundary reasons, process results and reference selection. Focused validation is 70 focused checks pass normally and with Tier B disabled; lint, formatting and typing of all 92 source modules passC-277; it does not claim a fresh full-suite run.

EC–GENRAY reference comparison

The EC reference package is forty decks bound to the unchanged selection, exact model and traces, frozen source, equilibrium, executable and runtime; eight workers with a thirty-minute hard limitC-279. The implementation lives in tkit.verify.ec_reference; entry 84 is the narrative account. State selection is inherited without alteration from the evenly spaced indices in the retained traces. The preparer checks model and metadata hashes, feature names and dimensions, and exact state, time, launch and guard identities. It independently reconstructs each input from the saved face profiles at the reference tabular radii. The recorded feature vector supplies the deck: temperature converts from electron-volts to kilo-electron-volts and density to the reference tabular units. Launcher positions and angles keep their original convention.

The request binds rendered decks, all toolkit source, the reference template and equilibrium, executable, resolved shared-library bytes and Python version. The batch process imports the frozen source explicitly. Preflight rechecks those identities from the actual execution path. Exclusive evidence paths and a request-level consumed marker prevent accidental reruns, including attempts with different output paths. Each case has a hard timeout and retains the actual deck, native output, logs, status and checksums. An audit reconstructs the comparison from these bytes without rerunning the reference solver.

The reference absorbed power is the sum of Landau and collisional electron heating. The existing current label and sign convention are retained: multiply the native total current by the sign of the equilibrium plasma-current and magnetic-field product, so co-current is positive. Native totals are normalized by the actual injected power to the model’s reference injection. Compare with the physically bounded ensemble outputs recorded before guard selection.

For prediction \(p\) and reference \(r\), the per-case error is \(|p-r|/|r|\), checked against the unchanged tolerance in C-279. No flux or current denominator floor is introduced. An exactly zero reference passes only with an exactly zero prediction; the remaining zero-reference errors are undefined and fail. The report retains every case and its power and current error. It reports both all-selected and served-only conjunctions; any missing or failed reference makes the overall comparison incomplete. Rejected-state predictions are diagnostic and cannot establish accuracy of the source actually used by TORAX.

K-028 still applies: the reference uses the existing fixed equilibrium, rather than a sequence matched to the evolving TORAX geometry. Agreement in this comparison would test the retained surrogate/reference convention on loop states; it would not establish a reference-coupled trajectory or certify M4. OQ-42 and the measured EC local-domain limitation remain unchanged. Focused validation is 40 affected tests pass normally and with Tier B disabled; repository lint, formatting, typing of 93 modules and batch syntax passC-280.

The completed run and independent saved-output audit give 40/40 cases pass the unchanged 10% power and signed-current limits, including 31/31 served states; maximum current error 9.606% EL and 7.393% UL, maximum power error 0.07483% EL and 0.02599% ULC-281. Every preselected case has a successful reference and meets both criteria, including the subset served by the actual guard. The independent audit reloads the frozen model, recomputes its predictions and reconstructs guard decisions before comparing native-total algebra against the report. Rejected predictions remain separately identified. This completes the sampled V9 comparison under the existing reference convention; it does not lift K-028 or the EC local-box limitation, and the M4 certification review remains pending.

Verified artifacts in the guards

V10 loads each verified model through its digest-checked manifest. The explicit box must match the loader’s feature order and previous domain. File IO occurs on the host before tracing; only arrays enter the compiled guard. Available output certificates hold a separate input box and output interval per family. The predicate applies only when an input lies inside an exact certified input box, with inclusive endpoints. Outside every proof box, it adds no certificate-based rejection; the ordinary input and physical-output checks still apply.

The ordinary EC numerical guard margin cannot enlarge a proof box. Removing that expansion from the inherited draft leaves none of the retained EC states inside its exact proof boxes; the pedestal trajectory is covered (all four verified input boxes match the previous loaders; 48 of 48 retained pedestal states keep identical predictions and decisions; none of the 57 EC states is inside the exact proof boxes, so no EC certificate-based output check applies thereC-284). Transport has no finite output certificate under OQ-46. OQ-50 adopts the fallback-rate thresholds as report-only alerts. Accepted-state rejection is not internal solver usage.

Hybrid-only calibration for M5

OQ-48 keeps the model, splits, V7 and the failed pooled record fixed. It restricts calibration to served states of the new hybrid runs and reporting to the older hybrid test runs. A shared state belongs to the family only when every owner run belongs to it. Absolute residuals in signed-log space use the same finite-sample split-conformal rank. A separate frozen reverse audit calibrates on the older hybrid test states and reports on the new ones. Every output must reach the existing pooled reading bar in both directions (hybrid calibration covers 0.914/0.915/0.904 of the older hybrid test states; the reverse audit covers 0.887/0.869/0.900; all exceed the fixed 0.85 pooled barC-285).

Leaving each new run out reports the run-to-run coverage spread; pooled success does not imply a run-level or simultaneous guarantee. M5 uses one coherent uniform discrepancy factor multiplying these marginal half-widths, an explicit prior assumption rather than a distribution inferred from conformal coverage. Its separate Bayesian audit uses one mean residual vector per run, the full empirical channel covariance and a uniform scalar prior. Conditional Metropolis moments are compared with the exact truncated-normal posterior (four Metropolis chains give transport-error factor mean -0.01978, standard deviation 0.01992 and split R-hat 1.00266; exact conditional moments are -0.02033 and 0.01984C-288). The other physical priors are not calibrated.

Portable pipeline boundaries

V5 reports and provenance sidecars are packaged byte-for-byte. Model/manifest/box binding remains checked at load time, including when a wheel loads an external verified model directory (installed-wheel EC and pedestal loaders retain their output certificates with externally copied verified directories; unresolved transport bounds remain explicitly K-033C-289). An existing malformed manifest fails closed rather than dropping certificate checks. The fallback monitor applies identical validation to explicit API thresholds and YAML configuration, so nonfinite values cannot be reported as within threshold.

The M5 selector derives its decision from primary and reverse coverage, checks the unchanged reading bar for every channel and binds all evidence to the exact model and manifest. Scientific failure selects the unchanged V7 fallback; missing or altered evidence raises an error. The completed study’s widths remain identical (all three selected hybrid half-widths are unchanged; both-direction coverage and exact model/manifest/evidence bindings are rechecked before a future runC-290). These are execution-integrity checks, not additional physics certificates.

Complete-box partition pilot

The follow-up partitions each original transport box into a complete binary cover. Each leaf uses the existing analytic LP support bands, independently finite variable boxes and stationarity-corrected inequality duals. Unknown or timed-out optimization retains the independently valid inherited enclosure; a primal objective is never accepted as a bound. The union must cover every original input, and aggregation must retain every leaf.

The independent audit reconstructs the cover, source and model bindings, fresh exported predictions, original held-out physical predictions and JAX predictions at sampled extrema. Both physical enclosures remain unresolved (both member-zero pilots retain overflowing physical enclosures despite complete input-box coverage; no sampled overflow witness was found, and all forty transport V5 results remain unresolvedC-293). No sampled overflow witness was found. This does not establish a domain-wide finite enclosure or show the real-valued network is infinite. The calculation uses float64 without directed IEEE rounding guarantees.

Retained solver counters motivate a separate scheduling diagnosis: final output objectives can be skipped after intermediate work consumes a shared clock. A new method must reserve final-objective time, retain corrected duals for independent replay and undergo review before execution. The unchanged all-member gate still requires both pilot members to pass before expansion. K-033, dependent transport V6, EC local-domain exclusions and the human certification gate remain open.

Reserved final-objective result

The bounded follow-up gives each intermediate activation a separate clock and reserves a final clock after every output head contributes constraints. Deterministic activation ordering permits cross-process replay. Incremental artifacts retain sparse constraints, finite variable boxes, affine forms, signed objectives, usable inequality duals and explicit interval fallback for every skipped or unusable objective. The independent auditor reconstructs the original graph and activation constraints, then replays stationarity corrections rather than trusting solver objectives or producer summaries.

All final objectives run, but the independently audited physical enclosures remain nonfinite (both full-box pilots retain nonfinite physical enclosures after all final objectives run; independent graph, constraint and corrected-dual replay passes, with no finite physical candidateC-297). Intersecting with the inherited enclosure preserves its endpoints exactly. Large relaxation terms dominate the small residual corrections; final-objective starvation alone does not explain the remaining looseness. Neither an identical retry nor an ensemble sweep follows from this result. The full-box property, stored models, guards and human acceptance gate remain unchanged.

Transport retraining for bounded verification (OQ-46 (b))

The retraining was declared before any training: candidates, targets, evaluator and selection rule (reviews/m4-transport-retrain-v1/README.md). There were four variants per machine, each an ensemble of 20 members, using the monotone signed-log recipe of the current models. Only the network size and an input-Jacobian penalty changed. The variants were a width-64 trunk with one residual block of two layers, or a single width-128 layer, each with penalty 0 or 1e-2.

• Penalty. Weight times the mean squared Frobenius norm of the member’s input Jacobian, in normalised units, on the first 256 rows of each batch. It is in the training loss only. Validation and early stopping use the data loss.
• Targets.
  • 1. median relative error ≤ 0.30 on Q_e and Q_i on the v3 test split;
  • (2a) every per-face operating box bounded for all members;
  • (2b) every in-domain V6 box bounded for all members;
  • 3. gradient sensitivity, reported only.
• What “bounded” means. The training-space bound converts to a finite physical bound through the served inverse signed-log.
• Evaluator. CROWN on the direct ELU graph, then the default graph, then input splitting. It is fail-fast: after the first failed (box, member), the remaining boxes are bounded for member 0 only, without splitting, and those results are for information only.

Round 1 found that the penalty is what makes V6 boxes boundable, and that it costs MAST-U accuracy (none of 8 retrained candidates passes; with Jacobian penalty 1e-2 every in-domain V6 box is bounded, and without it the first V6 box failsC-320). Round 2 raised the per-split time budget, after round 1 had been seen, and tried two smaller MAST-U penalties. It failed again (12 of 20 ITER members bound every operating face; MAST-U Q_i error 0.345 and 0.370 against a 0.30 targetC-321). Its splits reached the 4096-leaf limit and gained about 1%. The partition halves the longest relative side of each leaf in turn, which is too slow to shrink any one leaf in 17 dimensions. A post-hoc sampling diagnostic showed the bounds were loose, not the networks (sampled outputs from -4.2 to 8.1 against CROWN bounds from -665 to 733C-322).

Round 3: verifier change for ITER

MAST-U stopped at round 2 by owner decision, because no MAST-U model meets the accuracy target. For ITER, round 3 adds two steps to the evaluator, used only when CROWN on the whole box fails. The steps were declared before any failing case was bounded (round3/README.md).

1. alpha-CROWN on the whole box: 100 iterations, at most 120 s, intersected with CROWN and interval bounds.
2. Targeted splitting (bounds.bound_partition_targeted).
   • The leaf with the largest |bound|, among those not yet finite, is halved next.
   • The split axis maximises box width × |central-difference gradient| at the leaf centre, for that leaf’s worst output.
   • Leaves use CROWN and are intersected with their parent.
   • Splitting stops when every leaf is finite, or at 4096 leaves or 3600 s.

All 20 members bound all 38 faces (all 20 members on all 38 operating faces: 727 bounded directly, 17 by alpha-CROWN, 16 by targeted splitting of 3 to 161 leavesC-323). The bounds are finite but very wide (median largest bound 148 and maximum 709.6 in signed-log units, against an overflow limit of 709.78C-324): the targeted split stops as soon as every leaf is finite, so split cases end just under the overflow limit. The result shows that the bare network cannot overflow on any operating box. It does not give a useful flux range; the envelope bounds of OQ-46 (a) do that for the served output. The candidate is less accurate than v1 (median error 0.178 and 0.169 for Q_e and Q_i, against 0.072 and 0.108 for v1C-325). It is now packaged as version 2 with separate property, envelope, calibration and integrity records. CI checks both versions; M5 keeps version 1.

The fresh package audit binds exact operating boxes and selected local-state centres to source, model and data hashes. Its actual local-robustness rule compares the served ensemble’s interval against the centre prediction: each heat-flux change must stay within 10% of the certified full-training-box served range when raw inputs vary by 1% of their training range. 12 states proved, three unknown and five outside domain under the actual local-robustness toleranceC-326. Finite bounds alone do not satisfy this tolerance. Unknown cases are inconclusive enclosures, not observed violations, and the package does not claim full V6. Heavy bounds and dataset calibration are retained evidence rather than rerun in quick CI. Packaging itself does not confer owner certification. OQ-52 separately records the owner’s certification within the stated limits; unknown and outside-domain cases remain unproved.