Phased α-CROWN step function: case inversion

Lemmas that read off what stepPhased computed at a node.

Away from ReLU nodes that carry phases, stepPhased is stepAlpha. On a ReLU node with phases, the step succeeds only when the unary parent has a certificate entry and an IBP box of the same output dimension, and phaseRelaxVec? accepts the phases against that box. The inversion lemma stepPhased_relu_phase_inv exposes exactly those ingredients, together with the range of the α vector actually used (explicit or default).

Reduction to α-CROWN

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.stepPhased_eq_stepAlpha (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (alpha : Array (Option (FlatTensor ℝ))) (phases : Array (Option (Array ℤ))) (cert : Array (Option (FlatAffineBounds ℝ))) (ctx : AffineCtx) (id : ℕ) (hnoPhases : g.nodes[id]!.kind = IR.OpKind.relu → Cert.getPhases? phases id = none) : stepPhased g ps ibp alpha phases ctx cert id = stepAlpha g ps ibp alpha ctx cert id

stepPhased is stepAlpha at every node that is not a ReLU carrying phases.

The hypothesis is phrased as an implication so that a single lemma covers both the non-ReLU kinds and ReLU nodes with no phases.

Inversion of the phased ReLU branch

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.stepPhased_relu_phase_inv (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (alpha : Array (Option (FlatTensor ℝ))) (phases : Array (Option (Array ℤ))) (cert : Array (Option (FlatAffineBounds ℝ))) (ctx : AffineCtx) (id : ℕ) (b : FlatAffineBounds ℝ) (nodePhases : Array ℤ) (p1 : ℕ) (halpha : AlphaOK alpha) (hk : g.nodes[id]!.kind = IR.OpKind.relu) (hphases : Cert.getPhases? phases id = some nodePhases) (hps : IR.unaryParent? g.nodes[id]!.parents = some p1) (hs : stepPhased g ps ibp alpha phases ctx cert id = some b) : ∃ (xin : FlatAffineBounds ℝ) (preB : FlatBox ℝ) (hout : xin.outDim = preB.dim) (αt : TorchLean.Tensor ℝ [preB.dim]) (relaxLo : TorchLean.Tensor (Runtime.Ops.ReLURelax ℝ) [preB.dim]) (relaxHi : TorchLean.Tensor (Runtime.Ops.ReLURelax ℝ) [preB.dim]), Cert.getAff? cert p1 = some xin ∧ ibp[p1]! = some preB ∧ (∀ (i : Fin preB.dim), 0 ≤ αt.getScalar i ∧ αt.getScalar i ≤ 1) ∧ Cert.phaseRelaxVec? preB.lo preB.hi αt nodePhases = some (relaxLo, relaxHi) ∧ b = { inDim := xin.inDim, outDim := preB.dim, loAff := Runtime.Ops.ReLU.propagateAffine relaxLo (castAffineOut hout xin.loAff), hiAff := Runtime.Ops.ReLU.propagateAffine relaxHi (castAffineOut hout xin.hiAff) }

What a successful phased step on a ReLU node with phases must have computed.

The parent p1 has a certificate entry xin and an IBP box preB of matching output dimension, phaseRelaxVec? accepted nodePhases against preB for some α vector αt with entries in [0, 1] (the explicit one, cast to preB.dim, or the default one), and the produced bounds are the phase relaxations propagated through the parent's affine bounds.