α-CROWN Transfer: IBP Fallback #
The cases of alphaCrown_transfer_sound for operators outside the affine-transfer subset. The
step can only succeed through the constant enclosure derived from the IBP box at the same node,
which is sound because IBPEnclosesVals says that box encloses the semantic value.
theorem
NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.fallback_sound
{ibp : Array (Option (FlatBox ℝ))}
{vals : Array (Option CertSoundness.Val)}
{ctx : AffineCtx}
{x : TorchLean.Tensor ℝ [ctx.inputDim]}
{id : ℕ}
{B0 : FlatBox ℝ}
{b : FlatAffineBounds ℝ}
{v : CertSoundness.Val}
(hib : ibp[id]! = some B0)
(hb : Cert.boundsConst ctx.inputDim B0.dim B0.lo B0.hi = b)
(hv : vals[id]! = some v)
(hlt : id < vals.size)
(hibp : IBPEnclosesVals ibp vals)
:
CrownCertSoundness.EnclosesAtInput ctx x b v
The IBP fallback: if the step returned the constant enclosure of the IBP box B0 stored at
id, that enclosure is sound because IBPEnclosesVals says B0 encloses the semantic value at
id. The dispatch in alphaCrown_transfer_sound obtains hib and hb by splitting the unfolded
step equation, with or without the crownNodeSemanticsSupported guard.