Shared α-CROWN Transfer Lemmas

Common definitions and local proof lemmas for the graph-dialect α-CROWN and α/β-CROWN transfer rules over ℝ. These facts connect affine bounds, IBP boxes, ReLU relaxations, dimension casts, and pointwise graph semantics.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.FlatBox.ext' {α : Type} [TorchLean.Storage α] [Context α] {B1 B2 : FlatBox α} (hDim : B1.dim = B2.dim) (hLo : B1.lo ≍ B2.lo) (hHi : B1.hi ≍ B2.hi) : B1 = B2

Extensionality for FlatBox: equal dimension and heterogeneously equal endpoints.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.FlatBox.ext'_iff {α : Type} [TorchLean.Storage α] [Context α] {B1 B2 : FlatBox α} : B1 = B2 ↔ B1.dim = B2.dim ∧ B1.lo ≍ B2.lo ∧ B1.hi ≍ B2.hi

Helper assumptions

def NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.InputsMatch (inputs : Std.HashMap ℕ CertSoundness.Val) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) : Prop

The designated input entry in inputs matches the concrete point x (up to a castDimScalar).

def NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.IBPEnclosesVals (ibp : Array (Option (FlatBox ℝ))) (vals : Array (Option CertSoundness.Val)) : Prop

Pointwise: whenever both arrays contain entries at id, the IBP box encloses the semantic value.

def NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.AlphaOK (alpha : Array (Option (FlatTensor ℝ))) : Prop

Well-formedness condition for α vectors: each component lies in [0,1].

Theorems.Semantics.encloses ↔ componentwise inequalities (via getScalar)

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.encloses_iff_getScalar {n : ℕ} (lo hi x : TorchLean.Tensor ℝ [n]) : Theorems.Semantics.encloses { dim := n, lo := lo, hi := hi } x ↔ ∀ (i : Fin n), lo.getScalar i ≤ x.getScalar i ∧ x.getScalar i ≤ hi.getScalar i

Small tensor algebra helpers

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.add_spec_full_zero_right {n : ℕ} (t : TorchLean.Tensor ℝ [n]) : t.addSpec (TorchLean.Tensor.full (Spec.Shape.dim n Spec.Shape.scalar) 0) = t

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.linear_spec_bias_zero_eq_matvec {m n : ℕ} (W : TorchLean.Tensor ℝ [m, n]) (x : TorchLean.Tensor ℝ [n]) : Spec.linearSpec { weights := W, bias := TorchLean.Tensor.full (Spec.Shape.dim m Spec.Shape.scalar) 0 } x = Spec.matVecMulSpec W x

A linear layer with zero bias is a plain matrix-vector product.

The certificate builders emit zero biases for the layers that have none, so without this the transfer proofs would carry a + 0 through every step.

Small cast lemmas (avoid cases on equalities mentioning record fields)

castDimScalar_trans comes from CertSoundness (opened above) and castDimScalar_self from the engine module where the cast is defined; this file already depends on both for the rest of the interval lemmas. Each of them was stated a second time here, word for word, before this note replaced them.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.castDimScalar_proof_irrel {n n' : ℕ} (h₁ h₂ : n = n') (t : TorchLean.Tensor ℝ [n]) : castDimScalar h₁ t = castDimScalar h₂ t

castDimScalar is proof-irrelevant in its equality argument.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.getScalar_castDimScalar {n n' : ℕ} (h : n = n') (t : TorchLean.Tensor ℝ [n]) (i : Fin n') : (castDimScalar h t).getScalar i = t.getScalar (Fin.cast ⋯ i)

getScalar commutes with castDimScalar (up to Fin.cast).

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.relu_spec_castDimScalar {n n' : ℕ} (h : n = n') (t : TorchLean.Tensor ℝ [n]) : castDimScalar h (Activation.reluSpec t) = Activation.reluSpec (castDimScalar h t)

Activation.reluSpec commutes with castDimScalar.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.mat_vec_mul_full_one_castDimScalar {n n' : ℕ} (h : n = n') (v : TorchLean.Tensor ℝ [n]) : Spec.matVecMulSpec (TorchLean.Tensor.full (Spec.Shape.dim 1 (Spec.Shape.dim n Spec.Shape.scalar)) 1) v = Spec.matVecMulSpec (TorchLean.Tensor.full (Spec.Shape.dim 1 (Spec.Shape.dim n' Spec.Shape.scalar)) 1) (castDimScalar h v)

A small matVecMulSpec cast lemma used for single-row “sum” encodings.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.affineEvalAt_castAffineOut {inDim outDim outDim' : ℕ} (h : outDim = outDim') (aff : AffineVec ℝ inDim outDim) (x : TorchLean.Tensor ℝ [inDim]) : CrownCertSoundness.affineEvalAt (castAffineOut h aff) x = castDimScalar h (CrownCertSoundness.affineEvalAt aff x)

affineEvalAt commutes with casting the output dimension of an affine form.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.boundsEvalAt_castAffineOut (xin : FlatAffineBounds ℝ) {outDim' : ℕ} (h : xin.outDim = outDim') (x : TorchLean.Tensor ℝ [xin.inDim]) : CrownCertSoundness.boundsEvalAt { inDim := xin.inDim, outDim := outDim', loAff := castAffineOut h xin.loAff, hiAff := castAffineOut h xin.hiAff } x = { dim := outDim', lo := castDimScalar h (CrownCertSoundness.boundsEvalAt xin x).lo, hi := castDimScalar h (CrownCertSoundness.boundsEvalAt xin x).hi }

boundsEvalAt commutes with casting the output dimension of affine bounds.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.sem_encloses_castDim {B : FlatBox ℝ} {n' : ℕ} (h : B.dim = n') (x : TorchLean.Tensor ℝ [B.dim]) : Theorems.Semantics.encloses B x → Theorems.Semantics.encloses { dim := n', lo := castDimScalar h B.lo, hi := castDimScalar h B.hi } (castDimScalar h x)

Semantics.encloses is preserved under casting a box and point to an equal dimension.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.sem_encloses_of_eq {B1 B2 : FlatBox ℝ} (h : B1 = B2) (x : TorchLean.Tensor ℝ [B1.dim]) : Theorems.Semantics.encloses B1 x → Theorems.Semantics.encloses B2 (castDimScalar ⋯ x)

Semantics.encloses respects definitional equality of boxes.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.sem_encloses_value_eq {B : FlatBox ℝ} {x y : TorchLean.Tensor ℝ [B.dim]} (hxy : x = y) : Theorems.Semantics.encloses B x → Theorems.Semantics.encloses B y

Semantics.encloses respects definitional equality of values.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.enclosesAtInput_castOut (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (xin : FlatAffineBounds ℝ) (vp : FlatTensor ℝ) {outDim' : ℕ} (hout : xin.outDim = outDim') (hvout : vp.n = outDim') : CrownCertSoundness.EnclosesAtInput ctx x xin vp → CrownCertSoundness.EnclosesAtInput ctx x { inDim := xin.inDim, outDim := outDim', loAff := castAffineOut hout xin.loAff, hiAff := castAffineOut hout xin.hiAff } { n := outDim', v := castDimScalar hvout vp.v }

EnclosesAtInput is preserved under casting the output dimension of bounds and value payloads.

Matrix sign-splitting bound (pointwise, over ℝ)

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.get2_mat_pos {m n : ℕ} (W : TorchLean.Tensor ℝ [m, n]) (i : Fin m) (j : Fin n) : Spec.get2 (IBP.matPos W) i j = if Spec.get2 W i j > 0 then Spec.get2 W i j else 0

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.get2_mat_neg {m n : ℕ} (W : TorchLean.Tensor ℝ [m, n]) (i : Fin m) (j : Fin n) : Spec.get2 (IBP.matNeg W) i j = if Spec.get2 W i j > 0 then 0 else Spec.get2 W i j

Entries of the negative part of a matrix: the entry where it is not positive, else zero.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.signSplit_term_upper (w l u x : ℝ) (hlx : l ≤ x) (hxu : x ≤ u) : w * x ≤ (if 0 < w then w else 0) * u + (if 0 < w then 0 else w) * l

One term of the interval upper bound: w * x is at most w⁺ * u + w⁻ * l.

This is the whole idea of sign splitting. A positive weight is maximized at the upper endpoint and a negative one at the lower endpoint, so pairing each sign with the right endpoint is what makes the matrix version below a coordinatewise consequence.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.signSplit_term_lower (w l u x : ℝ) (hlx : l ≤ x) (hxu : x ≤ u) : (if 0 < w then w else 0) * l + (if 0 < w then 0 else w) * u ≤ w * x

The lower-bound companion: w⁺ * l + w⁻ * u is at most w * x.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.encloses_linear_signSplit {m n : ℕ} (W : TorchLean.Tensor ℝ [m, n]) (b : TorchLean.Tensor ℝ [m]) (lo hi x : TorchLean.Tensor ℝ [n]) (hx : Theorems.Semantics.encloses { dim := n, lo := lo, hi := hi } x) : Theorems.Semantics.encloses { dim := m, lo := ((Spec.matVecMulSpec (IBP.matPos W) lo).addSpec (Spec.matVecMulSpec (IBP.matNeg W) hi)).addSpec b, hi := ((Spec.matVecMulSpec (IBP.matPos W) hi).addSpec (Spec.matVecMulSpec (IBP.matNeg W) lo)).addSpec b } ((Spec.matVecMulSpec W x).addSpec b)

Interval bound propagation through an affine layer is sound.

The positive and negative parts of W are applied to opposite endpoints, so the resulting box encloses W x + b for every x in the input box. This is plain IBP; α-CROWN uses it for the intermediate boxes that its ReLU relaxations are built from.

ReLU relaxations used by α-CROWN

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.relu_relax_scalar_upper_real_runtime (l u x : ℝ) (hlx : l ≤ x) (hxu : x ≤ u) : have rp := Runtime.Ops.ReLU.relaxScalar l u; Activation.Math.reluSpec x ≤ rp.slope * x + rp.bias

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.relax_scalar_slope_nonneg (l u : ℝ) : 0 ≤ (Runtime.Ops.ReLU.relaxScalar l u).slope

The upper ReLU relaxation has nonnegative slope, in all three phase branches.

Monotonicity of the relaxation is what lets the transfer proofs multiply an inequality by the slope without flipping it, so this small fact is used pervasively downstream.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaRelaxLowerScalar_slope_nonneg (l u a : ℝ) (ha0 : 0 ≤ a) : 0 ≤ (Cert.alphaRelaxLowerScalar l u a).slope

The α-parameterized lower relaxation also has nonnegative slope, for any α ≥ 0.

ReLU relaxations used by α/β-CROWN (β phase constraints)

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.phaseConsistentScalar?_inactive {l u : ℝ} : Cert.phaseConsistentScalar? l u Cert.ReLUPhase.inactive = some () → u ≤ 0

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.phaseConsistentScalar?_active {l u : ℝ} : Cert.phaseConsistentScalar? l u Cert.ReLUPhase.active = some () → 0 ≤ l

Accepting an active phase constraint forces 0 ≤ l, so the neuron really is unambiguously on.

This is how the β-CROWN branch decisions are validated: the checker refuses a phase assignment that the interval bounds do not already support, rather than trusting the search that proposed it.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.phaseRelaxUpperScalar_slope_nonneg (l u : ℝ) (ph : Cert.ReLUPhase) : 0 ≤ (Cert.phaseRelaxUpperScalar l u ph).slope

Nonnegative slope for the upper relaxation under any phase constraint.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.phaseRelaxLowerScalar_slope_nonneg (l u a : ℝ) (ph : Cert.ReLUPhase) (ha0 : 0 ≤ a) : 0 ≤ (Cert.phaseRelaxLowerScalar l u a ph).slope

Nonnegative slope for the lower relaxation under any phase constraint and α ≥ 0.

ReLU transfer helpers (getScalar-level)

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.defaultAlphaVec_range {n : ℕ} (lo hi : TorchLean.Tensor ℝ [n]) (i : Fin n) : 0 ≤ (Cert.defaultAlphaVec lo hi).getScalar i ∧ (Cert.defaultAlphaVec lo hi).getScalar i ≤ 1

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.getScalar_relu_spec {n : ℕ} (t : TorchLean.Tensor ℝ [n]) (i : Fin n) : (Activation.reluSpec t).getScalar i = Activation.Math.reluSpec (t.getScalar i)

The vector ReLU is the scalar ReLU coordinatewise.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.getScalar_runtime_relu_relax_vector {n : ℕ} (lo hi : TorchLean.Tensor ℝ [n]) (i : Fin n) : (Runtime.Ops.ReLU.relaxVector lo hi).getScalar i = Runtime.Ops.ReLU.relaxScalar (lo.getScalar i) (hi.getScalar i)

The vector relaxation is the scalar relaxation coordinatewise, which is what turns the scalar soundness lemmas above into statements about whole layers.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.getScalar_alphaRelaxLowerVec {n : ℕ} (lo hi αv : TorchLean.Tensor ℝ [n]) (i : Fin n) : (Cert.alphaRelaxLowerVec lo hi αv).getScalar i = Cert.alphaRelaxLowerScalar (lo.getScalar i) (hi.getScalar i) (αv.getScalar i)

Same coordinatewise reading for the α-parameterized lower relaxation.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.getScalar_affineEvalAt_relu_propagate_affine {inDim hidDim : ℕ} (relax : TorchLean.Tensor (Runtime.Ops.ReLURelax ℝ) [hidDim]) (aff : AffineVec ℝ inDim hidDim) (x : TorchLean.Tensor ℝ [inDim]) (i : Fin hidDim) : (CrownCertSoundness.affineEvalAt (Runtime.Ops.ReLU.propagateAffine relax aff) x).getScalar i = have rp := relax.getScalar i; rp.slope * (CrownCertSoundness.affineEvalAt aff x).getScalar i + rp.bias

Propagating an affine form through a ReLU relaxation acts coordinatewise as slope * value + bias.

The implementation scales the whole matrix and shifts the whole constant, so this lemma is the bridge from that global operation to the per-neuron reasoning the soundness proof needs.

β phase vectors (AlphaBetaCROWN.phaseRelaxVec?) are executable, so to reason about them we extract their per-index consequences from the fact they returned some ....

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.List.all_eq_true_of_mem {α : Type} (p : α → Bool) (xs : List α) : xs.all p = true → ∀ x ∈ xs, p x = true

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.phaseRelaxVec?_some_getScalar {n : ℕ} (lo hi αv : TorchLean.Tensor ℝ [n]) (phases : Array ℤ) (relaxLo relaxHi : TorchLean.Tensor (Runtime.Ops.ReLURelax ℝ) [n]) (h : Cert.phaseRelaxVec? lo hi αv phases = some (relaxLo, relaxHi)) : phases.size = n ∧ ∀ (i : Fin n), ∃ (ph : Cert.ReLUPhase), Cert.phaseConsistentScalar? (lo.getScalar i) (hi.getScalar i) ph = some () ∧ relaxHi.getScalar i = Cert.phaseRelaxUpperScalar (lo.getScalar i) (hi.getScalar i) ph ∧ relaxLo.getScalar i = Cert.phaseRelaxLowerScalar (lo.getScalar i) (hi.getScalar i) (αv.getScalar i) ph

Unpack a successful phaseRelaxVec?: the phase array has the right length, and every coordinate carries a phase that is consistent with its interval and whose two relaxations are the scalar ones.

The checker returns only the relaxations, so this is the lemma that recovers the phase witnesses the soundness argument has to case on.

Evaluating linearBoundsFromAffine at a point

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.get2_add_spec {m n : ℕ} (A B : TorchLean.Tensor ℝ [m, n]) (i : Fin m) (j : Fin n) : Spec.get2 (A.addSpec B) i j = Spec.get2 A i j + Spec.get2 B i j

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.mat_vec_add_matrix {m n : ℕ} (A B : TorchLean.Tensor ℝ [m, n]) (x : TorchLean.Tensor ℝ [n]) : Spec.matVecMulSpec (A.addSpec B) x = (Spec.matVecMulSpec A x).addSpec (Spec.matVecMulSpec B x)

Matrix-vector multiplication is additive in the matrix.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.mat_vec_mul_spec_full_zero {m n : ℕ} (x : TorchLean.Tensor ℝ [n]) : Spec.matVecMulSpec (TorchLean.Tensor.full (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)) 0) x = TorchLean.Tensor.full (Spec.Shape.dim m Spec.Shape.scalar) 0

The zero matrix sends every vector to zero, which is what makes constant bounds constant.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.mat_vec_mul_spec_aff_identity {n : ℕ} (x : TorchLean.Tensor ℝ [n]) : Spec.matVecMulSpec (Cert.affIdentity n).A x = x

The identity affine certificate acts as the identity on inputs.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.boundsEvalAt_bounds_identity {n : ℕ} (x : TorchLean.Tensor ℝ [n]) : CrownCertSoundness.boundsEvalAt (Cert.boundsIdentity n) x = { dim := n, lo := x, hi := x }

The identity bounds certificate evaluates to the degenerate box [x, x].

This is the base case of every certificate chain: the input is bounded by itself exactly.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.boundsEvalAt_bounds_const {inDim outDim : ℕ} (lo hi : TorchLean.Tensor ℝ [outDim]) (x : TorchLean.Tensor ℝ [inDim]) : CrownCertSoundness.boundsEvalAt (Cert.boundsConst inDim outDim lo hi) x = { dim := outDim, lo := lo, hi := hi }

A constant bounds certificate evaluates to its own endpoints, ignoring the input.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.add_spec_left_comm {s : Spec.Shape} (a b c : TorchLean.Tensor ℝ s) : a.addSpec (b.addSpec c) = b.addSpec (a.addSpec c)

Left commutativity of tensor addition, derived from associativity and commutativity.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.add_spec_pair_distrib {s : Spec.Shape} (a b c d : TorchLean.Tensor ℝ s) : (a.addSpec b).addSpec (c.addSpec d) = (a.addSpec c).addSpec (b.addSpec d)

Regroup (a + b) + (c + d) as (a + c) + (b + d).

Certificate composition produces sums in the order the layers were visited, while the goal groups them by which affine form they came from; this is the reassociation that reconciles the two.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.affineEvalAt_linear_pair {inDim n m : ℕ} (W₁ W₂ : TorchLean.Tensor ℝ [m, n]) (aff₁ aff₂ : AffineVec ℝ inDim n) (b : TorchLean.Tensor ℝ [m]) (x : TorchLean.Tensor ℝ [inDim]) : CrownCertSoundness.affineEvalAt { A := (Spec.matMulSpec W₁ aff₁.A).addSpec (Spec.matMulSpec W₂ aff₂.A), c := ((Spec.matVecMulSpec W₁ aff₁.c).addSpec (Spec.matVecMulSpec W₂ aff₂.c)).addSpec b } x = ((Spec.matVecMulSpec W₁ (CrownCertSoundness.affineEvalAt aff₁ x)).addSpec (Spec.matVecMulSpec W₂ (CrownCertSoundness.affineEvalAt aff₂ x))).addSpec b

Evaluating the composition of a linear layer with two incoming affine forms distributes over the pair: matrices compose, constants are pushed through, and the bias is added once at the end.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.boundsEvalAt_linear_bounds_from_affine {n m : ℕ} (W : TorchLean.Tensor ℝ [m, n]) (b : TorchLean.Tensor ℝ [m]) (xB : FlatAffineBounds ℝ) (hout : xB.outDim = n) (x : TorchLean.Tensor ℝ [xB.inDim]) : CrownCertSoundness.boundsEvalAt (Cert.linearBoundsFromAffine W b xB hout ⋯) x = { dim := m, lo := have l := CrownCertSoundness.affineEvalAt (castAffineOut hout xB.loAff) x; have u := CrownCertSoundness.affineEvalAt (castAffineOut hout xB.hiAff) x; ((Spec.matVecMulSpec (IBP.matPos W) l).addSpec (Spec.matVecMulSpec (IBP.matNeg W) u)).addSpec b, hi := have l := CrownCertSoundness.affineEvalAt (castAffineOut hout xB.loAff) x; have u := CrownCertSoundness.affineEvalAt (castAffineOut hout xB.hiAff) x; ((Spec.matVecMulSpec (IBP.matPos W) u).addSpec (Spec.matVecMulSpec (IBP.matNeg W) l)).addSpec b }

Evaluating the bounds certificate that a linear layer builds from an incoming affine bound gives exactly the sign-split box of the evaluated endpoints.

This is the lemma that connects the certificate the checker writes down to the interval arithmetic that encloses_linear_signSplit proves sound, and it carries the output-dimension cast that the graph dialect needs because layer widths are only equal up to a proof.

Step wrapper

noncomputable def NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.stepAlpha (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (alpha : Array (Option (FlatTensor ℝ))) (ctx : AffineCtx) : Array (Option (FlatAffineBounds ℝ)) → ℕ → Option (FlatAffineBounds ℝ)

Wrapper around alphaCrownStepNode? in the CrownTransferSound “step function” shape.

noncomputable def NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.stepAlphaBeta (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (alpha : Array (Option (FlatTensor ℝ))) (beta : Array (Option (Array ℤ))) (ctx : AffineCtx) : Array (Option (FlatAffineBounds ℝ)) → ℕ → Option (FlatAffineBounds ℝ)

Wrapper around alphaBetaCrownStepNode? in the CrownTransferSound “step function” shape.