Exact CROWN output-query checks

Recompute affine bounds for dense/ReLU networks and prove strict or non-strict output inequalities over an input box. The arithmetic is rational; the conclusion uses TorchLean's existing real module semantics. Every transfer and final query check is proved here, with no external soundness premise.

def NN.Verification.Cert.CROWNQuery.checkUpper {n m : ℕ} (strict : Bool) (upper : MLTheory.CROWN.AffineVec ℚ n m) (input : MLTheory.CROWN.Box ℚ [n]) : Bool

Check all upper endpoints against zero, using strict inequalities when requested.

theorem NN.Verification.Cert.CROWNQuery.affine_interval_encloses {n m : ℕ} (a : MLTheory.CROWN.AffineVec ℚ n m) (input : MLTheory.CROWN.Box ℚ [n]) (x : TorchLean.Tensor ℝ [n]) (hx : MLTheory.CROWN.Graph.Theorems.Semantics.encloses { dim := n, lo := RationalReflection.realTensor input.lo, hi := RationalReflection.realTensor input.hi } x) (i : Fin m) : (RationalReflection.realTensor (MLTheory.CROWN.IBP.linear a.A input { lo := a.c, hi := a.c }).lo).getScalar i ≤ (MLTheory.CROWN.Graph.CrownCertSoundness.affineEvalAt (RationalReflection.realAffine a) x).getScalar i ∧ (MLTheory.CROWN.Graph.CrownCertSoundness.affineEvalAt (RationalReflection.realAffine a) x).getScalar i ≤ (RationalReflection.realTensor (MLTheory.CROWN.IBP.linear a.A input { lo := a.c, hi := a.c }).hi).getScalar i

Interval bounds of an exact affine form over the input box enclose its real evaluation.

theorem NN.Verification.Cert.CROWNQuery.checkUpper_sound {n m : ℕ} (strict : Bool) (upper : MLTheory.CROWN.AffineVec ℚ n m) (input : MLTheory.CROWN.Box ℚ [n]) (h : checkUpper strict upper input = true) (x : TorchLean.Tensor ℝ [n]) (hx : MLTheory.CROWN.Graph.Theorems.Semantics.encloses { dim := n, lo := RationalReflection.realTensor input.lo, hi := RationalReflection.realTensor input.hi } x) (i : Fin m) : if strict = true then (MLTheory.CROWN.Graph.CrownCertSoundness.affineEvalAt (RationalReflection.realAffine upper) x).getScalar i < 0 else (MLTheory.CROWN.Graph.CrownCertSoundness.affineEvalAt (RationalReflection.realAffine upper) x).getScalar i ≤ 0

Every accepted upper form is below zero throughout the real input box.

structure NN.Verification.Cert.CROWNQuery.Bounds (n m : ℕ) : Type

Affine bounds with their input and output dimensions checked by Lean.

• lo : MLTheory.CROWN.AffineVec ℚ n m
• hi : MLTheory.CROWN.AffineVec ℚ n m

def NN.Verification.Cert.CROWNQuery.Bounds.flat {n m : ℕ} (b : Bounds n m) : MLTheory.CROWN.Graph.FlatAffineBounds ℚ

Forget the static dimensions to reuse the dimension-carrying CROWN transfer functions.

def NN.Verification.Cert.CROWNQuery.Bounds.Encloses {n m : ℕ} (b : Bounds n m) (x : TorchLean.Tensor ℝ [n]) (y : TorchLean.Tensor ℝ [m]) : Prop

The bounds enclose a value at a particular real input.

def NN.Verification.Cert.CROWNQuery.Bounds.identity (n : ℕ) : Bounds n n

The identity affine bounds at the network input.

def NN.Verification.Cert.CROWNQuery.Bounds.linear {n m k : ℕ} (b : Bounds n m) (w : TorchLean.Tensor ℚ [k, m]) (bias : TorchLean.Tensor ℚ [k]) : Bounds n k

Push affine bounds through an exact linear layer with the sign-split CROWN transfer.

def NN.Verification.Cert.CROWNQuery.Bounds.interval {n m : ℕ} (b : Bounds n m) (input : MLTheory.CROWN.Box ℚ [n]) : MLTheory.CROWN.Box ℚ [m]

Bound each affine form over the original input box.

def NN.Verification.Cert.CROWNQuery.Bounds.relu {n m : ℕ} (b : Bounds n m) (input : MLTheory.CROWN.Box ℚ [n]) (alpha : TorchLean.Tensor ℚ [m]) : Bounds n m

Push affine bounds through ReLU using the α lower and triangle upper relaxations.

theorem NN.Verification.Cert.CROWNQuery.Bounds.identity_encloses {n : ℕ} (x : TorchLean.Tensor ℝ [n]) : (identity n).Encloses x x

theorem NN.Verification.Cert.CROWNQuery.Bounds.linear_encloses {n m k : ℕ} (b : Bounds n m) (w : TorchLean.Tensor ℚ [k, m]) (bias : TorchLean.Tensor ℚ [k]) (x : TorchLean.Tensor ℝ [n]) (y : TorchLean.Tensor ℝ [m]) (h : b.Encloses x y) : (b.linear w bias).Encloses x ((Spec.matVecMulSpec (RationalReflection.realTensor w) y).addSpec (RationalReflection.realTensor bias))

theorem NN.Verification.Cert.CROWNQuery.Bounds.interval_encloses {n m : ℕ} (b : Bounds n m) (input : MLTheory.CROWN.Box ℚ [n]) (x : TorchLean.Tensor ℝ [n]) (y : TorchLean.Tensor ℝ [m]) (hx : MLTheory.CROWN.Graph.Theorems.Semantics.encloses { dim := n, lo := RationalReflection.realTensor input.lo, hi := RationalReflection.realTensor input.hi } x) (hy : b.Encloses x y) (i : Fin m) : (RationalReflection.realTensor (b.interval input).lo).getScalar i ≤ y.getScalar i ∧ y.getScalar i ≤ (RationalReflection.realTensor (b.interval input).hi).getScalar i

def NN.Verification.Cert.CROWNQuery.checkAlpha {m : ℕ} (alpha : TorchLean.Tensor ℚ [m]) : Bool

Every proposed ReLU lower slope lies in [0, 1], as the relaxation soundness requires.

theorem NN.Verification.Cert.CROWNQuery.checkAlpha_sound {m : ℕ} (alpha : TorchLean.Tensor ℚ [m]) (h : checkAlpha alpha = true) (i : Fin m) : 0 ≤ (RationalReflection.realTensor alpha).getScalar i ∧ (RationalReflection.realTensor alpha).getScalar i ≤ 1

theorem NN.Verification.Cert.CROWNQuery.Bounds.relu_encloses {n m : ℕ} (b : Bounds n m) (input : MLTheory.CROWN.Box ℚ [n]) (alpha : TorchLean.Tensor ℚ [m]) (ha : checkAlpha alpha = true) (x : TorchLean.Tensor ℝ [n]) (y : TorchLean.Tensor ℝ [m]) (hx : MLTheory.CROWN.Graph.Theorems.Semantics.encloses { dim := n, lo := RationalReflection.realTensor input.lo, hi := RationalReflection.realTensor input.hi } x) (hy : b.Encloses x y) : (b.relu input alpha).Encloses x (Activation.reluSpec y)

inductive NN.Verification.Cert.CROWNQuery.Network : ℕ → ℕ → Type

Dense/ReLU networks with a proposed lower-relaxation slope at each ReLU.

• linear {n m : ℕ} (layer : Spec.LinearSpec ℚ n m) : Network n m
• relu {n : ℕ} (alpha : TorchLean.Tensor ℚ [n]) : Network n n
• comp {n m k : ℕ} : Network n m → Network m k → Network n k

noncomputable def NN.Verification.Cert.CROWNQuery.Network.model {n m : ℕ} : Network n m → Spec.Module.Chain ℝ [n] [m]

Use the same linear and activation modules as ordinary TorchLean models.

def NN.Verification.Cert.CROWNQuery.Network.propagate {n m k : ℕ} (net : Network m k) (b : Bounds n m) (input : MLTheory.CROWN.Box ℚ [n]) : Option (Bounds n k)

Recompute affine bounds with existing CROWN transfers and exact rational arithmetic.

theorem NN.Verification.Cert.CROWNQuery.Network.propagate_sound {n m k : ℕ} (net : Network m k) (b : Bounds n m) (input : MLTheory.CROWN.Box ℚ [n]) (out : Bounds n k) (h : net.propagate b input = some out) (x : TorchLean.Tensor ℝ [n]) (y : TorchLean.Tensor ℝ [m]) (hx : MLTheory.CROWN.Graph.Theorems.Semantics.encloses { dim := n, lo := RationalReflection.realTensor input.lo, hi := RationalReflection.realTensor input.hi } x) (hy : b.Encloses x y) : out.Encloses x (net.model.forward y)

Replayed bounds enclose the whole network, not just individual certificate entries.

structure NN.Verification.Cert.CROWNQuery.Query (n m : ℕ) : Type

A conjunction of affine output inequalities, interpreted as weights * output + bias.

• network : Network n m
• input : MLTheory.CROWN.Box ℚ [n]
• numConstraints : ℕ
• inequalities : Spec.LinearSpec ℚ m self.numConstraints
• strict : Bool

def NN.Verification.Cert.CROWNQuery.boxOrdered {n : ℕ} (input : MLTheory.CROWN.Box ℚ [n]) : Bool

Every lower endpoint is at most its upper endpoint; a reversed box has no real members.

def NN.Verification.Cert.CROWNQuery.Query.wellFormed {n m : ℕ} (q : Query n m) : Bool

Reject reversed boxes and empty input, output, or query dimensions.

def NN.Verification.Cert.CROWNQuery.Query.check {n m : ℕ} (q : Query n m) : Bool

An executable safety check; no externally supplied affine bounds are trusted.

def NN.Verification.Cert.CROWNQuery.Query.Safe {n m : ℕ} (q : Query n m) : Prop

Every real input in the decoded box satisfies every decoded output inequality.

theorem NN.Verification.Cert.CROWNQuery.Query.check_sound {n m : ℕ} (q : Query n m) (h : q.check = true) : q.Safe

Acceptance implies query-level soundness with no unproved transfer or coverage premise.