Certified label checks

Shared predicates for certified classification from output bounds.

The checker uses one rule: the claimed label's lower bound must be strictly above every other class upper bound. Tensor bounds come from in-memory IBP/CROWN runs. Array bounds come from JSON artifacts.

def NN.Verification.Robustness.TopLabel.strictTopLabelBy {α : Type} [Max α] (n label : ℕ) (lo hi : Fin n → α) (gt : α → α → Bool) : Bool

Strict label certificate over any indexed lower/upper bounds.

def NN.Verification.Robustness.TopLabel.certifiesLabelFromTensorBounds {α : Type} [Context α] {n : ℕ} (lo hi : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (label : ℕ) : Bool

Check a label directly from tensor lower/upper bounds.

def NN.Verification.Robustness.TopLabel.certifiesLabelFromArrayBounds (lo hi : Array Float) (label : ℕ) : Bool

Check a label from JSON-style array lower/upper bounds.