Scalar soundness for phased ReLU relaxations (over ℝ)

This file proves the operator-level soundness facts used by phased α-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.phaseConsistent_inactive_of_some (l u : ℝ) (h : Cert.phaseConsistentScalar? l u Cert.ReLUPhase.inactive = some ()) : u ≤ 0

An accepted inactive phase has nonpositive upper endpoint.

theorem NN.MLTheory.CROWN.Proofs.phaseConsistent_active_of_some (l u : ℝ) (h : Cert.phaseConsistentScalar? l u Cert.ReLUPhase.active = some ()) : 0 ≤ l

An accepted active phase has nonnegative lower endpoint.

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

The phase-aware upper relaxation is sound for any phase the interval bounds actually admit.

The consistency hypothesis is what makes this true: on a claimed-inactive neuron the relaxation is the constant zero line, which only dominates relu because u ≤ 0 was checked first.

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

The phase-aware lower relaxation is sound, for every slope a ∈ [0, 1].

The free a is the α of α-CROWN: on an unstable neuron any slope in the unit interval gives a valid lower line, and the search is allowed to pick whichever one tightens the final bound.