α-CROWN Transfer: Shared Extraction Lemmas

Helper lemmas shared by the per-operator cases of alphaCrown_transfer_sound. They package the parent hypothesis of CrownTransferSound and transport enclosures across output-dimension casts and constant boxes. The safe-lookup inversions for getAff? and getAlpha? live in Common.

def NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.ParentsEnclosed (g : Graph) (cert : Array (Option (FlatAffineBounds ℝ))) (vals : Array (Option CertSoundness.Val)) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (id : ℕ) : Prop

Every parent p of node id whose certificate entry and semantic value are both present is enclosed at the input point x. This is the parent hypothesis of CrownTransferSound with its match unfolded.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.parentsEnclosed_of_match {g : Graph} {cert : Array (Option (FlatAffineBounds ℝ))} {vals : Array (Option CertSoundness.Val)} {ctx : AffineCtx} {x : TorchLean.Tensor ℝ [ctx.inputDim]} {id : ℕ} (hparents : ∀ p ∈ g.nodes[id]!.parents, match cert[p]!, vals[p]! with | some bp, some vp => CrownCertSoundness.EnclosesAtInput ctx x bp vp | x, x_1 => True) : ParentsEnclosed g cert vals ctx x id

The match-shaped parent hypothesis of CrownTransferSound implies ParentsEnclosed.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.parent_encloses_of_unaryParent? {g : Graph} {cert : Array (Option (FlatAffineBounds ℝ))} {vals : Array (Option CertSoundness.Val)} {ctx : AffineCtx} {x : TorchLean.Tensor ℝ [ctx.inputDim]} {id p1 : ℕ} {xin : FlatAffineBounds ℝ} {vp : CertSoundness.Val} (hpar : ParentsEnclosed g cert vals ctx x id) (hps : IR.unaryParent? g.nodes[id]!.parents = some p1) (hxin : Cert.getAff? cert p1 = some xin) (hgv : CertSoundness.getVal? vals p1 = some vp) : CrownCertSoundness.EnclosesAtInput ctx x xin vp

The unique parent of a unary node is enclosed whenever its certificate entry and semantic value are both found by the safe lookups.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.evalNode?_eq_some_of_semLocalOK {g : Graph} {ps : ParamStore ℝ} {inputs : Std.HashMap ℕ CertSoundness.Val} {vals : Array (Option CertSoundness.Val)} {id : ℕ} {v : CertSoundness.Val} (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hid : id < g.nodes.size) (hv : vals[id]! = some v) : CertSoundness.evalNode? g.nodes ps inputs vals id = some v

Under SemLocalOK, a present semantic value at id is the evaluator's output.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.sem_encloses_transport {B1 B2 : FlatBox ℝ} (h : B1 = B2) {x : TorchLean.Tensor ℝ [B1.dim]} {y : TorchLean.Tensor ℝ [B2.dim]} (hxy : x ≍ y) (hx : Theorems.Semantics.encloses B1 x) : Theorems.Semantics.encloses B2 y

Transport an enclosure along an equality of boxes and a heterogeneous equality of values.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.encloses_point_box {n : ℕ} (t : TorchLean.Tensor ℝ [n]) : Theorems.Semantics.encloses { dim := n, lo := t, hi := t } t

A point box encloses its own point.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.enclosesAtInput_boundsConst_of_enclosesBox {ctx : AffineCtx} {x : TorchLean.Tensor ℝ [ctx.inputDim]} {B0 : FlatBox ℝ} {v : CertSoundness.Val} (hEnc : CertSoundness.EnclosesBox B0 v) : CrownCertSoundness.EnclosesAtInput ctx x (boundsConst ctx.inputDim B0.dim B0.lo B0.hi) v

A constant affine enclosure built from a box B0 is sound at every input point whenever B0 encloses the value.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.encloses_castOut_of_enclosesAtInput {ctx : AffineCtx} {x : TorchLean.Tensor ℝ [ctx.inputDim]} {xin : FlatAffineBounds ℝ} {vp : CertSoundness.Val} {n : ℕ} (hout : xin.outDim = n) (hvn : vp.n = n) (hinDim : xin.inDim = ctx.inputDim) (hpar : CrownCertSoundness.EnclosesAtInput ctx x xin vp) : Theorems.Semantics.encloses { dim := n, lo := CrownCertSoundness.affineEvalAt (castAffineOut hout xin.loAff) (castDimScalar ⋯ x), hi := CrownCertSoundness.affineEvalAt (castAffineOut hout xin.hiAff) (castDimScalar ⋯ x) } (castDimScalar hvn vp.v)

Casting the output dimension of enclosing affine bounds yields a box, evaluated at the input point, that encloses the correspondingly cast value. This is the componentwise form of enclosesAtInput_castOut used by the linear and ReLU cases.