Scalar soundness for α/β-ReLU relaxations (over ℝ)

This file proves the operator-level soundness facts used by α/β-CROWN at ReLU nodes:

• phaseRelaxUpperScalar is an upper bound on relu for any x ∈ [l,u].
• phaseRelaxLowerScalar is a lower bound on relu for any x ∈ [l,u] (with 0 ≤ α ≤ 1).

The β-phase cases (inactive/active) are exact, and the unstable case reduces to the standard CROWN (upper) and α-CROWN (lower) relaxations.

theorem NN.MLTheory.CROWN.Proofs.phaseRelaxUpperScalar_sound (l u x : ℝ) (hlx : l ≤ x) (hxu : x ≤ u) (ph : Cert.ReLUPhase) (hcons : Cert.phaseConsistentScalar? l u ph = some ()) : have rp := Cert.phaseRelaxUpperScalar l u ph; Activation.Math.reluSpec x ≤ rp.slope * x + rp.bias

theorem NN.MLTheory.CROWN.Proofs.phaseRelaxLowerScalar_sound (l u a x : ℝ) (hlx : l ≤ x) (hxu : x ≤ u) (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (ph : Cert.ReLUPhase) (hcons : Cert.phaseConsistentScalar? l u ph = some ()) : have rp := Cert.phaseRelaxLowerScalar l u a ph; rp.slope * x + rp.bias ≤ Activation.Math.reluSpec x