α-CROWN Transfer: Linear Nodes

The .linear, .matmul, and .sum cases of alphaCrown_transfer_sound. All three are instances of the sign-splitting rule propagateLinearBounds, proved once in enclosesAtInput_propagateLinearBounds and instantiated with the node's weights (all-ones row for .sum) and bias (zero for .matmul and .sum).

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.enclosesAtInput_propagateLinearBounds {ctx : AffineCtx} {x : TorchLean.Tensor ℝ [ctx.inputDim]} {xin : FlatAffineBounds ℝ} {vp : CertSoundness.Val} {n m : ℕ} (W : TorchLean.Tensor ℝ [m, n]) (bv : TorchLean.Tensor ℝ [m]) (hout : xin.outDim = n) (hvIn : vp.n = n) (hpar : CrownCertSoundness.EnclosesAtInput ctx x xin vp) : CrownCertSoundness.EnclosesAtInput ctx x (propagateLinearBounds W bv xin hout) { n := m, v := Spec.linearSpec { weights := W, bias := bv } (castDimScalar hvIn vp.v) }

Sign-splitting transfer through y = W x + bv: if the affine bounds xin enclose the parent value vp at x, then propagateLinearBounds W bv xin hout encloses W · vp + bv.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.linear_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]} {id : ℕ} {b : FlatAffineBounds ℝ} {v : CertSoundness.Val} (hk : g.nodes[id]!.kind = IR.OpKind.linear) (hs : stepAlpha g ps ibp alpha ctx cert id = some b) (hEvalSome : CertSoundness.evalNode? g.nodes ps inputs vals id = some v) (hpar : ParentsEnclosed g cert vals ctx x id) : CrownCertSoundness.EnclosesAtInput ctx x b v

The .linear case: the step applies the sign-splitting rule to the parent's affine bounds with the node's weights and bias, and the evaluator applies linearSpec to the parent's value.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.matmul_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]} {id : ℕ} {b : FlatAffineBounds ℝ} {v : CertSoundness.Val} (hk : g.nodes[id]!.kind = IR.OpKind.matmul) (hs : stepAlpha g ps ibp alpha ctx cert id = some b) (hEvalSome : CertSoundness.evalNode? g.nodes ps inputs vals id = some v) (hpar : ParentsEnclosed g cert vals ctx x id) : CrownCertSoundness.EnclosesAtInput ctx x b v

The .matmul case: as .linear, with the node's weight matrix and a zero bias.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.sum_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]} {id : ℕ} {b : FlatAffineBounds ℝ} {v : CertSoundness.Val} (hk : g.nodes[id]!.kind = IR.OpKind.sum) (hs : stepAlpha g ps ibp alpha ctx cert id = some b) (hEvalSome : CertSoundness.evalNode? g.nodes ps inputs vals id = some v) (hpar : ParentsEnclosed g cert vals ctx x id) : CrownCertSoundness.EnclosesAtInput ctx x b v

The .sum case: the step treats the sum as the 1 × n linear layer with all-ones weights and zero bias, and the evaluator multiplies the parent's value by the all-ones row.