α/β-CROWN Graph Transfer Soundness #
Pointwise soundness theorem for the β-extended graph transfer rule.
The proof is a dispatch over two cases. Every node that is not a ReLU carrying a β vector is
handled by alphaCrown_transfer_sound, since stepAlphaBeta agrees with stepAlpha there
(stepAlphaBeta_eq_stepAlpha). A ReLU node with a β vector is handled by inverting the step
(stepAlphaBeta_relu_beta_inv), reading off the parent's value from the semantics, and applying
the pointwise β-phase ReLU lemma enclosesAtInput_relu_beta.
Semantic glue #
The parent hypothesis of CrownTransferSound, specialised to a parent whose certificate entry and
semantic value are both present.
A ReLU node's semantic value is relu of its unary parent's value.
The IBP box of a parent node encloses that parent's semantic value.
Per-case soundness #
Soundness of stepAlphaBeta at every node handled by the α-CROWN rule: all non-ReLU kinds, and
ReLU nodes with no β entry. The step is literally stepAlpha there, so this is
alphaCrown_transfer_sound read at one node.
Soundness of stepAlphaBeta at a ReLU node carrying a β vector.
The step inversion supplies the parent's certificate entry, its IBP box, the α vector used, and
the accepted phase relaxations; the semantics supplies the parent's value;
enclosesAtInput_relu_beta does the rest.
Main transfer theorem #
Pointwise soundness of the graph-dialect α/β-CROWN transfer rule.
This is the β-extended analog of alphaCrown_transfer_sound. The step function additionally
receives a beta array of per-ReLU phase constraints (active, inactive, unstable). At a ReLU node
with a β vector, phaseRelaxVec? checks each phase against the IBP pre-activation interval via
phaseConsistentScalar? (inactive needs u ≤ 0, active needs 0 ≤ l) and, if every phase
passes, uses the phase's exact affine rule for that unit; an inconsistent phase rejects the step
rather than falling back to another relaxation. All other nodes use the α-CROWN rule.
What the β relaxation contributes here, and what it does not. Because a phase is accepted only
when the IBP interval already implies it, a β vector can never certify a sign that the supplied
ibp box does not fix on its own; for such stable units the phase rule coincides with the
standard relaxation. The theorem therefore establishes two things about β: the exact rules are
sound whenever the consistency check passes, and inconsistent phase vectors are rejected. It does
not model branch-and-bound split constraints. A split that tightens beyond IBP would have to be
reflected in a tighter ibp argument, which this theorem takes as given through
IBPEnclosesVals.
The theorem states that this concrete step function satisfies CrownTransferSound, and thus can
be used as the trusted checker semantics in crown_checker_encloses_semantics.
A locally replayed α/β-CROWN certificate encloses every corresponding graph value.
This is the user-facing composition of alphaBetaCrown_transfer_sound with the generic graph
certificate checker. The certificate producer remains untrusted: hcert requires its entries to
agree node-by-node with TorchLean's α/β transfer function.