Graph IBP Certificate Soundness

The induction theorem: local IBP certificate consistency plus local semantic consistency implies that every certified node box encloses the corresponding semantic value.

The per-operator cases live under GraphCertSoundness/Main/; this file states the graph-level assumptions, dispatches on the node kind, and runs the strong induction over node ids.

Main theorem: local IBP certificate implies semantic enclosure (supported subset)

We use strong induction on node id, assuming a topological order: every parent id is strictly smaller than the node id.

def NN.MLTheory.CROWN.Graph.CertSoundness.TopoSorted (g : Graph) : Prop

Topological order assumption: all parent ids are strictly smaller than the node id.

def NN.MLTheory.CROWN.Graph.CertSoundness.Supported (g : Graph) : Prop

A graph is supported by this soundness theorem if every node kind is in our supported subset.

def NN.MLTheory.CROWN.Graph.CertSoundness.InputsEnclosed (g : Graph) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ Val) : Prop

Inputs are well-formed if every .input node has a value, and that value is enclosed by its input box from ParamStore.inputBoxes.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.parent_lt_array_size {β : Type} {g : Graph} (entries : Array β) (hSize : entries.size = g.nodes.size) (htopo : TopoSorted g) {id parent : ℕ} (hid : id < g.nodes.size) (hparent : parent ∈ g.nodes[id]!.parents) : parent < entries.size

A topologically earlier parent fits every node-indexed array with graph-sized storage.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.parents_enclosed_of_ih {g : Graph} {cert : Array (Option (FlatBox ℝ))} {vals : Array (Option Val)} {k : ℕ} (htopo : TopoSorted g) (hk : k < g.nodes.size) (ih : ∀ p < k, p < g.nodes.size → ∀ (B : FlatBox ℝ) (v : Val), cert[p]! = some B → vals[p]! = some v → EnclosesBox B v) : ParentsEnclosed g.nodes cert vals k

The induction hypothesis for all earlier nodes yields ParentsEnclosed at node k, because TopoSorted places every parent strictly before k.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.node_encloses_of_parents {g : Graph} {ps : ParamStore ℝ} {cert : Array (Option (FlatBox ℝ))} {inputs : Std.HashMap ℕ Val} {vals : Array (Option Val)} {k : ℕ} {B : FlatBox ℝ} {v : Val} (hsupp : Supported g) (hinputs : InputsEnclosed g ps inputs) (hk : k < g.nodes.size) (hcertStep : certStepNode? g.nodes ps cert k = some B) (hvalStep : evalNode? g.nodes ps inputs vals k = some v) (hpe : ParentsEnclosed g.nodes cert vals k) : EnclosesBox B v

One step of the induction: a supported node whose parents are enclosed is itself enclosed. This is the dispatch over operator kinds; each arm is a lemma under Main/.

The enclosure theorem

Assumptions:

• TopoSorted g: induction works (parents are earlier).
• Supported g: every node kind is handled by the proof.
• CertLocalOK g ps cert: the certificate is locally consistent with the IBP step.
• InputsEnclosed g ps inputs: semantic inputs are inside the certified input boxes.
• SemLocalOK g ps inputs vals: vals is a locally-consistent semantic interpretation.

Conclusion:

• For every node id, if the semantics produces a value v and the certificate has a box B, then B encloses v.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.cert_encloses_semantics_of_some (g : Graph) (ps : ParamStore ℝ) (cert : Array (Option (FlatBox ℝ))) (inputs : Std.HashMap ℕ Val) (vals : Array (Option Val)) (htopo : TopoSorted g) (hsupp : Supported g) (hcert : CertLocalOK g ps cert) (hsem : SemLocalOK g ps inputs vals) (hinputs : InputsEnclosed g ps inputs) (id : ℕ) : id < g.nodes.size → ∀ (B : FlatBox ℝ) (v : Val), cert[id]! = some B → vals[id]! = some v → EnclosesBox B v

Enclosure for every node where both the certificate box and the semantic value are present.

This is the non-vacuous companion of cert_encloses_semantics: it quantifies over the box and value explicitly instead of matching on cert[id]! and vals[id]!. The strong induction runs here, since this shape is the one the operator lemmas need for their parents.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.cert_encloses_semantics (g : Graph) (ps : ParamStore ℝ) (cert : Array (Option (FlatBox ℝ))) (inputs : Std.HashMap ℕ Val) (vals : Array (Option Val)) (htopo : TopoSorted g) (hsupp : Supported g) (hcert : CertLocalOK g ps cert) (hsem : SemLocalOK g ps inputs vals) (hinputs : InputsEnclosed g ps inputs) (id : ℕ) : id < g.nodes.size → match cert[id]!, vals[id]! with | some B, some v => EnclosesBox B v | x, x_1 => True

Enclosure of every certified node box around the corresponding semantic value.

The conclusion matches on cert[id]! and vals[id]! and is trivially true when either entry is missing. This shape is kept because downstream files instantiate it directly with the runtime arrays produced by runIBP? and the evaluator, where presence of an entry is not known up front. See cert_encloses_semantics_of_some for the explicitly quantified form.