JSON acceptance implies output-query safety

crown_query_v1 describes an exact rational dense/ReLU network, an input box, proposed ReLU α values, and affine output inequalities. The checker recomputes affine bounds using existing CROWN transfers. Parameters use integer or fraction strings; numeric JSON literals are rejected.

The theorem concerns the real TorchLean model and query decoded from these bytes. It does not identify this model with an ONNX file or a floating-point deployment. This is a separate format from the binary32 node-replay transcript; β dual variables, cuts, and branch trees are unsupported.

def NN.Verification.CROWNQuery.decodeLayer (n : ℕ) (j : Lean.Json) : Except String ((m : ℕ) × Network n m)

def NN.Verification.CROWNQuery.decodeLayers (n : ℕ) : List Lean.Json → Except String ((m : ℕ) × Network n m)

def NN.Verification.CROWNQuery.decode (j : Lean.Json) : Except String ((n : ℕ) × (m : ℕ) × Query n m)

Decode the model, input domain, and output property from the same document.

def NN.Verification.CROWNQuery.acceptsJson (j : Lean.Json) : Bool

theorem NN.Verification.CROWNQuery.acceptsJson_sound (j : Lean.Json) (h : acceptsJson j = true) : ∃ (n : ℕ) (m : ℕ) (q : Query n m), decode j = Except.ok ⟨n, ⟨m, q⟩⟩ ∧ q.Safe

Every accepted document denotes a model whose outputs satisfy its query throughout its box.

def NN.Verification.CROWNQuery.acceptsText (source : String) : Bool

theorem NN.Verification.CROWNQuery.acceptsText_sound (source : String) (h : acceptsText source = true) : ∃ (j : Lean.Json) (n : ℕ) (m : ℕ) (q : Query n m), Lean.Json.parse source = Except.ok j ∧ decode j = Except.ok ⟨n, ⟨m, q⟩⟩ ∧ q.Safe

Text acceptance implies the universal real output property, without a producer axiom.