Realized (Stage 3, Adequacy) over the Float carrier. Addition runs a swamping check (the smaller-magnitude operand's uncertainty against half the sum's ulp), subtraction a cancellation check (relative uncertainty reaching 100%); the NumCarrier instance closes with these plus the arithmetic and MathCarrier fields, so the same kernel the earlier rungs evaluate runs here to emit the report. The AdequacySwamping example flags a large-accumulator model and certifies its small-accumulator variant clean — one WO1 kernel, checked for free.

Realized over ℝ (Adequacy.Absorption.absorb, with resolve the converse): on the uniform grid u·ℤ, round_u(x+y) = u·round((x+y)/u), and |y| < u/2 places (x+y)/u within a half-integer of x/u, so it rounds to x/u. The binary32 realization is TorchLean's neuralRound nearest-point optimality and neuralUlp (Adequacy.Fp32Grounding). Sorry-free.

Realized over ℝ (Adequacy.Sterbenz32.flx_sterbenz), the real-number analogue of TorchLean's neural_generic_format_FLX_sterbenz: align both operands to the smaller exponent, and the factor-of-two condition bounds the difference's mantissa below 2^p. sub_exact_on_grid gives the grid form (the difference rounds to itself). Sorry-free. Stage 3.2 carries this to the FLT/fexp32 format binary32 actually uses (gradual underflow) — the genuine grounding is thm_uq_sterbenz_fp32.

Realized over ℝ/FP32 (Stage 3.2, Adequacy.Fp32Grounding.round32_sterbenz_exact / sub32_exact_of_sterbenz), grounded in the TorchLean PR's neural_generic_format_FLT_sterbenz. That FLT Sterbenz lemma splits on the underflow boundary β^(prec+emin): on the subnormal side the fixed emin grid subtracts exactly (FLT_to_FIX → FIX_sub → FIX_to_FLT), on the normal side it transports through the unbounded FLX family (FLT_to_FLX → FLX_sterbenz → FLX_to_FLT_of_normal). Composing it with neural_round_preserves_generic (rounding is the identity on representable reals) gives \mathrm{round}_{32}(u - v) = u - v, so the per-op sub32_within_half_ulp half-ulp bound collapses to zero in the Sterbenz regime. Sorry-free ([propext, Classical.choice, Quot.sound]), exercised by the AdequacySterbenz32 example.

Realized over ℝ (Adequacy.Soundness.verdict_sound): the forward direction is A1 absorb, the reverse is the contrapositive of resolve, giving the biconditional unc < ½ ulp ↔ fl(s + unc) = s for a representable accumulator and an uncertainty within one ulp. The AdequacyLadder example applies it to concrete values with a sorry-free axiom profile. This is the per-site soundness that grounds the runtime carrier.

Realized over ℝ/FP32 (Stage 3.1, Adequacy.DagBound). The forward-error accumulation dag_fp32_error_bound composes the per-operation half-ulp bounds (Adequacy.Fp32Grounding.{add32,sub32,mul32,div32}_within_half_ulp, the genuine FP32.{add,sub,mul,div}_abs_error) with the triangle inequality and the first-order propagation of operand errors along the DAG; applying it at both inputs and one more triangle step gives the box-faithfulness bound dag_fp32_box_faithful, and dag_fp32_box_exact_of_flagFree is the flag-free equality. The linear nodes +/− pass operand error through with coefficient one; the nonlinear ×/÷ carry the GUM magnitude factors (|b|, 1/|b|, |a|/|b|²), a div node's bound holding on the nonzero-denominator side condition Regular (vacuous on ÷-free DAGs). Sorry-free (#print axioms → [propext, Classical.choice, Quot.sound]), instantiated on concrete +/−/×/÷ DAGs in the AdequacyDag example (the executable-carrier bridge is built, Stage 3.3).

Realized as ExactRepresentable and flagFree_iff_exactRepresentable (Stage 3.8, Adequacy.DagBound). Both directions of the induction need the operand condition first, which is what identifies the two readings of a node's operands; the node step is then Fp32Grounding.round32_eq_self_iff, that round32 fixes exactly the representable reals. That characterization is also what makes the relocated condition minimal for this conclusion: nothing weaker on a node's exact value keeps that node from rounding.

The consequence worth stating is that the flag-free theorems are now about an inhabited regime. AdequacyDag discharges ExactRepresentable on a doubling chain at two input assignments and derives the box equality with no hypothesis left standing — where mix_box_exact and prod_box_exact assume flag-freedom and nothing supplies it.

What is not done is the weaker regime the residual list still carries: a no-absorption condition would allow rounding and ask only that a tracked contribution survive it, which makes equality of the variations false and so requires a different conclusion — a resolution statement lifting A1's converse resolve along the DAG, as dag_fp32_error_bound lifts the half-ulp bound.

Realized in Adequacy.RefinementBridge. The identification is definitional — the refinement rounds by the format's own rounding — so the induction does nothing but apply, at each node, that rounding fixes exactly the representable reals.

The reason to keep both routes rather than consolidate is that their side conditions are about different things. The division law is unconditional at the specification rung only because \mathbb{R} totalizes division by zero, which is why the executable rung instead carries the divisor's nonzero decoded mantissa — a question of definedness. The adequacy DAG's regularity condition is unrelated to that: the per-operation bound for division has no hypothesis at all, and regularity guards the propagation factors — a question of magnitude. Merging them would conflate the two, and the weighted mean is where that would cost something: at its single division node the two rungs' licenses are independent in both directions.

Realized over ℝ/IEEE32Exec (Stage 3.3, Adequacy.ExecBridge), grounded in TorchLean's IEEE32Exec.ulpExp? + bpow_eq_ulp_of_ulpExp?_eq_some (an executable ULP answer equals ulp₃₂; the query answers on exactly the finite fragment) and round_add_eq_left_of_absorbs (a 3-line corollary of the toReal_add_eq_round_of_isFinite op-level refinement, since FloatLib's Model.roundAt binary32 is round₃₂). exec_verdict_sound composes them: when absorbs s δ fires, round₃₂(\mathrm{toReal}\,s + \mathrm{toReal}\,δ) = \mathrm{toReal}\,s. Sorry-free ([propext, Classical.choice, Quot.sound]); the executable side is run (#guard) at 2^{25} and 10^8 in the AdequacyExecBridge example, which also confirms the axiom profile. The host-Float Adequacy carrier stays the fast, unverified mirror.

Realized (Stage 3.4, Adequacy.Significance.analyzeQ over Uncertainty.Budget). The three budget roles get kinds (stdUncQ, sensitivityQ, contributionQ gated by ProductKind kₛ kᵢ kₒ, combinedQ); the model stays carrier-raw, so no kinded autograd is needed — the kinds are the caller-declared overlay on the budget. On the Degenhardt descriptors the coupling reproduces (c_i) = (5, 5, 2.25), the kinded contributions (c_i u_i) = (1.0, 1.30, 0.28) at \mathrm{ measurandY}, and their quadrature reproduces the GUM combined uncertainty u_c = 1.662359 exactly; #check_failure probes make the conflations (sensitivity↔uncertainty, heterogeneous quadrature, field swap) type errors. A 10^8-accumulator swamps a contribution (< \tfrac12\,\mathrm{ulp}_{32}(10^8) = 4); the flag's soundness is the A3 verdict, and contribution_absorbed_at_scale applies it at the contribution scale, sorry-free. (ProductKind.ofRatio is liberal, so the gate enforces the GUM shape and forbids un-sanctioned mixing while the author asserts k_s = k_o/k_i.) The budget is carrier-generic (Uncertainty.Budget over [NumCarrier R]) — the second axis, orthogonal to the kind: the same combinedQ runs at ℝ (to prove laws), at Float (to run), and at the adequacy carrier, where its quadrature \sqrt{\sum u_i^2} adequacy-checks itself (the example flags a 10^{-3} contribution swamped beside a 10^8 one).

Realized (Stage 3.4 extension, residual 2; Uncertainty.BudgetDag, Mathlib/Torch-free, carrier-generic over [NumCarrier R]). The transposed witness is QuotientKind.toProductKind (QuantityClassification); the value component rides along unperturbed (propagateQ_value_eq_valueQ). Deliberately no add/sub nodes — the homogeneous linear case is already the flat kinded budget fed by autograd sensitivities, so tree +/− would be a second authoring of the same quadrature. Exercised on the block-density model \rho = m/((l\cdot w)\cdot h) (UncertaintyExamples.BudgetDagDensity): five distinct kinds through one budget — untypeable under the significance wiring's single shared input kind — with #guards reproducing \rho = 2500, the per-leaf contributions (1.0, 2.5, 5.0, 25.0), and u_c = \sqrt{657.25} \approx 25.637, and #check_failure probes making the operand swap, the heterogeneous quadrature, and the kind-misplaced leaf type errors.

Realized over ℝ (Uncertainty.BudgetExpr.propagateQ_unc_eq_combinedQ, in BudgetDagLaws), under a NonnegUncs hypothesis (nonnegativity of every leaf uncertainty — statable only at the ordered proof carrier, the core NumCarrier being deliberately branchless). Structural induction: Quantity.ext reduces each node to a magnitude identity in the sumSq sum-of-squares vocabulary (sumSq_append, the scaled families sumSq_map_mul_left/_right/_div), each child radicand re-expressed as \sqrt{S}\cdot \sqrt{S} (Real.mul_self_sqrt) and closed by ring. No divisor-nonzero hypotheses — division is ℝ's totalized x/0 = 0 and both sides degenerate identically. Sorry-free (#print axioms → [propext, Classical.choice, Quot.sound], pinned in BudgetDagDensity). Two textbook relative-uncertainty corollaries (mul_leaf_relative_quadrature, div_leaf_relative_quadrature) give (u_y/|y|)^2 = (u_a/|a|)^2 + (u_b/|b|)^2 for single nodes, there needing the nonzero-value hypotheses relative uncertainty divides by.