α-CROWN Graph Transfer Soundness

Pointwise soundness theorem for the graph-dialect alphaCrownStepNode? transfer rule. The proof dispatches on the node kind to the per-operator lemmas in the Alpha subdirectory: leaf nodes (Alpha.Leaf), value-preserving nodes (Alpha.Shape), linear nodes (Alpha.Linear), ReLU (Alpha.ReLU), and the IBP-derived constant fallback (Alpha.Fallback).

Main transfer theorem

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaCrown_transfer_sound (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (alpha : Array (Option (FlatTensor ℝ))) (cert : Array (Option (FlatAffineBounds ℝ))) (inputs : Std.HashMap ℕ CertSoundness.Val) (vals : Array (Option CertSoundness.Val)) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (htopo : CertSoundness.TopoSorted g) (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hinputs : InputsMatch inputs ctx x) (hibp : IBPEnclosesVals ibp vals) (halpha : AlphaOK alpha) : CrownCertSoundness.CrownTransferSound g ps inputs vals ctx x (stepAlpha g ps ibp alpha ctx) cert

Pointwise soundness of the graph-dialect α-CROWN transfer rule.

Fix a graph g, parameters ps, an input point x, and a locally consistent value semantics array vals (that is, vals[id] agrees with evaluating node id from its parents' values).

Assume:

• the designated input node in inputs matches x (InputsMatch),
• the IBP boxes ibp enclose the semantic values in vals (IBPEnclosesVals), and
• the α parameters are well-formed (AlphaOK).

Then the concrete step function alphaCrownStepNode? satisfies the abstract CrownTransferSound requirement: whenever every parent p is enclosed by its certificate entry, the current node id is enclosed by the step-produced certificate entry as well.

This is the key lemma that lets alphaCrownStepNode? plug into the generic end-to-end checker theorem in NN.MLTheory.CROWN.Proofs.GraphCrownCertSoundness.