Realized. gumStdUnc folds the \kappa_2 contributions. Stage 0 supplied the c_i explicitly; Stage 1 now sources them from the autograd carrier (one reverse pass over the write-once model at the input means), leaving this fold unchanged — the Degenhardt example checks the two agree, both giving u_c = 1.662.

Realized. willinkCombine combines \kappa_2 and \kappa_4; willinkK95/willinkK99 are the rational Pearson-percentile fits (Willink eqs. 6/7); willinkHalfWidth99 composes them.

Realized. Mcm.run over the Float carrier, drawing each input through its invCDF. Efficiency is not its job — fidelity is.

Realized (Stage 1, Sensitivity.gradient; retargeted in Stage 3.5). The model kernel — the same source run at Float for Monte Carlo — is interpreted at TorchLean's reverse-mode TapeBuilder carrier; each input enters as a differentiable leaf, and one total dense reverse pass (Tape.backwardDenseFrom, seeded 1 at the scalar output) reads every c_i, with no model rewrite. Since Stage 3.5 this is the very entry point TorchLean's soundness theorem backwardDenseFrom_lowerGraphToTape_adjoint_fderiv characterizes: on a compiled graph at the ℝ carrier its input-prefix output is the adjoint of the Fréchet derivative of the forward evaluation (the eager-tape provenance — narrowed at Stage 3.6 to a closure-provenance question, see the direct-simulation theorem below — and the Float-vs-ℝ deviation remain the two documented gaps). On the Degenhardt fictive model the bridge returns (c_1, c_2, c_3) = (5, 5, 2.25) and reproduces the GUM u_c = 1.662 exactly (the DegenhardtSensitivity example). The op class is exp/log/sqrt with arithmetic; trigonometric models await tape VJP nodes.

Realized (PRSim.direct_PR_soundness_compiled, with backwardDenseFrom_ok for the totality half and forwardSim_lowerGraphToTape inhabiting the simulation relation; Experiments/PRSimulation.lean, sorry-free). The endpoint is the input-prefix projection of the Stage-3.5 theorem transported to the runtime array by two erasure lemmas (block-reads invert context flattening; Array.extract is the erased typed prefix) — no reverse-pass fold argument is re-derived, so the adjoint mathematics enters exactly once, through the Stage-3.5 bridge. The totality half threads the "every slot carries its node's shape" invariant through the accumulation fold, value-free; the shape-totality hypothesis is honest and necessary, since a value-correct tape with an erroring closure refutes the unconditioned claim — the closure-provenance identification for the eager path is the next theorem. The AutogradDirectSim example instantiates everything concretely and pins the axiom profiles to the classical trio.

Realized (PRSim.direct_PR_soundness_eager, via backwardDenseFrom_eager_eq_compiled; Experiments/EagerProvenance.lean, sorry-free). EagerBuilds is the provenance relation — its base tape is the compiled tape of the empty graph, definitionally — and the identification is pure accounting, never a re-derived fold: the compiled node's dense contribution list is folded by the upstream accumulation bridge, the eager node's sparse two-element list by a new single-slot lemma (one accumulation call is a one-hot context addition), and the two context updates coincide by flatten-injectivity through the vectorization homomorphisms — the eager closure's stored product-rule payloads are exactly the ofVec-authored node's Hadamard vjp blocks. Push-invariance lemmas restrict the extended tape's loop to its prefix, so the structural induction consumes its hypothesis directly. Honest residuals: ops beyond add/mul (one more crank of the same machine per op), the TapeM state-monad sugar (a one-line wrapper per op), and the Float-vs-ℝ deviation — the workstream's own Adequacy claim. The AutogradDirectSim example witnesses EagerBuilds for the concrete product tape and pins the classical-trio axiom profile.

Realized over ℝ: willinkCumulants_cons, with the Cumulants AddCommMonoid instance (the combine/empty monoid laws) providing the associativity/commutativity/unit that make the independent fold well-defined.

Realized over ℝ (theorem T2 of UNCERTAINTY.md, gum_eq_willink_of_normal; #print axioms shows it sorry-free — no sorryAx). Two parts: willinkCumulants_kappa2 — the variance fold is literally the GUM one — and the shape collapse w_i = 0 \Rightarrow \gamma_Y = 0 \Rightarrow k_p is the standard-normal percentile, so the half-widths coincide. Establishes the top edge of the ladder; the lower edge — that Willink is the fourth-cumulant truncation of the linearized SSPRC, because convolution adds cumulants — is theorem T3 below.