Margin positivity ⇒ L∞ certificate. If for every wrong class the margin f · y − f · j is strictly positive at every point of the box x ∓ ε, then y is the strict argmax under every perturbation with |δ i| ≤ ε coordinatewise.

The peer of certified_of_boxSound one rung lower: it says nothing about HOW the margin was bounded, so a CROWN bound and a margin-direct interval bound discharge it the same way. Bounding the margin rather than the two logits separately is itself a tightening — it keeps the correlation between f · y and f · j that a box separation throws away.

Lower envelope. α · z ≤ relu z for ANY α ∈ [0,1], with no reference to [l,u] at all. Soundness is therefore insensitive to the choice of α: optimizing it (α-CROWN) is a tightness question, never a correctness one, and a rounded α needs no re-verification.

Upper envelope. On [l, u] with l ≤ 0, any nonneg s at or above the chord slope dominates relu. The chord condition is stated as u ≤ s * (u - l) rather than s = u / (u - l), which is what lets a generator ROUND s up to a /2^k grid and still discharge it by norm_num — the rational-size lever (see the header).

Proof: g z = s·(z−l) − relu z is affine on [0,u] with g 0 = −s·l ≥ 0 and g u = s·(u−l) − u ≥ 0, hence nonneg between; below 0 it is trivial.

A neuron that is dead on the whole box (u ≤ 0) contributes exactly 0 — both envelopes are exact and the coefficient vanishes.

A neuron that is active on the whole box (0 ≤ l) is EXACT: relu z = z, so it passes its margin coefficient through unrelaxed. This is where CROWN keeps everything IBP would have widened.

Unstable neuron, POSITIVE margin coefficient: take the lower envelope, whose slope α is unconstrained in [0,1].

Unstable neuron, NEGATIVE margin coefficient: multiplying by v ≤ 0 flips the inequality, so the upper envelope is what lower-bounds the contribution. This is the only branch that carries a constant, and the only one whose slope must be verified against the chord.

Transport a ReluLB along equalities of its coefficient and constant — the join between the engine's branch-selected form and the generator's emitted literals.

All four branches in one lemma, uniform in v. The chord condition is required only where it is used — on a genuinely unstable neuron — so a stable neuron discharges it vacuously and may carry s = 0.

This is what keeps a generated instance affordable: the relaxation is proved once per NEURON (16 facts), not once per (class, neuron) pair (144), because nothing here depends on which wrong class is being separated.

Back-substitution is exact: relaxing in pre-activation space and then substituting z = W1 x' is the same linear function of x' as the CROWN row applied directly.

Concretization, once. On the uniform box x ∓ ε a linear functional bottoms out at ⟨A, x₀⟩ − ε‖A‖₁. This is denseLo_uniform read at the one-row matrix A — reused, not re-derived. ONE ℓ1 norm per (image, class), where IBP pays one per (image, neuron).

The two-layer net, evaluated one logit at a time — denseE/reluE peeled exactly once, so the inner denseE W1 x' stays folded (unfolding it would put a 784-term sum under every max).

The margin bound. Summing the per-neuron relaxations gives a linear lower bound on f · y − f · j in pre-activation space. z is abstract here: the bound is a statement about the relaxation, not about the net.

CROWN-IBP L∞ certificate for dense ∘ relu ∘ dense.

For each wrong class j, the generator supplies relaxation coefficients a j and constants cc j for the margin row W2 y · − W2 j ·, discharged against the IBP pre-activation box by the reluLB_* instances; the certificate fires when the ONE concretized linear bound is positive:

⟨A, x₀⟩ − ε‖A‖₁ + Σ cc  >  0,    A = crownRow (a j) W1.

Note the box in hrelax is literally denseLo W1 … / denseHi W1 … — the interval box IntervalBound.lean proves — not a float recomputation. That is forced by the statement, which is the point: CROWN-IBP is sound only if the [l,u] you relax against are the ones that actually hold on the box the certificate quantifies over.

The combined row, entry by entry, is a plain dotZ of the coefficients against the rows' i-th column.

The CROWN row, in one kernel-checkable object. With coefficients aₜ = csₜ / dc and weights W1ₜᵢ = rowsₜᵢ / dw, the ℝ-level crownRow is the integer combZ over dc·dw.

‖A‖₁ from one absSumZ … := by decide +kernel fact. One ℓ1 norm per (image, class), where IBP pays one per (image, neuron) — and the 784 entries of A are never emitted, only folded.