Sign-splitting linear bounds (IBP helper)

For a linear layer y = W x + b with input interval x ∈ [lo, hi], we can compute output bounds using the standard sign-splitting trick:

• W⁺ = max(W, 0) (elementwise)
• W⁻ = min(W, 0) (elementwise)

Then:

• y_lo = W⁺·lo + W⁻·hi + b_lo
• y_hi = W⁺·hi + W⁻·lo + b_hi

This is algebraically equivalent to the per-weight min/max rule, but it makes it easy to cache W⁺/W⁻ and matches the common LiRPA/CROWN implementation style.

def NN.MLTheory.CROWN.IBP.linearSignSplit {α : Type} [Context α] {m n : ℕ} (W : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (xB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) (bB : Box α (Spec.Shape.dim m Spec.Shape.scalar)) : Box α (Spec.Shape.dim m Spec.Shape.scalar)

Linear IBP bounds computed via sign-splitting (W⁺/W⁻).