Scalar ReLU Upper Bound

The CROWN affine upper relaxation bounds ReLU throughout its input interval. The MLP, graph, and phase-aware certificate proofs all use this scalar inequality.

theorem NN.MLTheory.CROWN.Proofs.relu_relax_scalar_upper_real_runtime (l u x : ℝ) (hlx : l ≤ x) (hxu : x ≤ u) : have rp := Runtime.Ops.ReLU.relaxScalar l u; Activation.Math.reluSpec x ≤ rp.slope * x + rp.bias

The CROWN upper chord dominates ReLU on the interval used to construct it.