Shared definitions for the graph CROWN engine.

This file contains the rank-one tensor representation, parameter stores, interval boxes, shape permutation helpers, and tensor casts used by the IBP, derivative, affine, CROWN, and backward objective passes.

structure NN.MLTheory.CROWN.Graph.FlatTensor (α : Type) [TorchLean.Storage α] [Context α] : Type

An existentially sized rank-one tensor used by the flat LiRPA engine.

Graph nodes carry dimensions discovered while lowering, so the dimension cannot always appear in the surrounding static type. The field n is the hidden tensor dimension, not duplicate runtime storage.

• n : ℕ

  Number of scalar entries.

• v : TorchLean.Tensor α [self.n]

  Rank-one tensor payload (shape .dim n .scalar).

structure NN.MLTheory.CROWN.Graph.ConcatLayout : Type

Geometry shared by all concat transfers, preserving parent occurrences in list order.

• leading : Spec.Shape

  Dimensions before the selected axis.

• trailing : Spec.Shape

  Dimensions after the selected axis.

• lengths : List ℕ

  Selected-axis length of each parent occurrence, including zero lengths.

def NN.MLTheory.CROWN.Graph.ConcatLayout.parentShape (layout : ConcatLayout) (parent : Fin layout.lengths.length) : Spec.Shape

Shape of one parent occurrence.

def NN.MLTheory.CROWN.Graph.ConcatLayout.outputShape (layout : ConcatLayout) : Spec.Shape

Shape of the concatenated output.

def NN.MLTheory.CROWN.Graph.ConcatLayout.flatEquiv (layout : ConcatLayout) : (parent : Fin layout.lengths.length) × Fin (layout.parentShape parent).size ≃ Fin layout.outputShape.size

Bijection between parent scalar coordinates and concatenated scalar coordinates.

def NN.MLTheory.CROWN.Graph.ConcatLayout.concat {α : Type} [TorchLean.Storage α] (layout : ConcatLayout) (values : (parent : Fin layout.lengths.length) → TorchLean.Tensor α [(layout.parentShape parent).size]) : TorchLean.Tensor α [layout.outputShape.size]

Read every output from its unique parent coordinate, without scalar arithmetic.

def NN.MLTheory.CROWN.Graph.ConcatLayout.split {α : Type} [TorchLean.Storage α] (layout : ConcatLayout) (value : TorchLean.Tensor α [layout.outputShape.size]) (parent : Fin layout.lengths.length) : TorchLean.Tensor α [(layout.parentShape parent).size]

Pull output coefficients back to one parent occurrence using the same coordinate bijection.

def NN.MLTheory.CROWN.Graph.concatLayout? (axis : ℕ) (parentShapes : Array Spec.Shape) (outputShape : Spec.Shape) : Option ConcatLayout

Validate concat geometry against the IR contract and its declared output shape.

def NN.MLTheory.CROWN.Graph.concatNodeLayout? (nodes : Array Node) (node : Node) (axis : ℕ) : Option ConcatLayout

Validate and collect every concat parent; missing ids are rejected before reading payloads.

def NN.MLTheory.CROWN.Graph.concatFlatValues? {α : Type} [TorchLean.Storage α] [Context α] (layout : ConcatLayout) (values : Array (FlatTensor α)) : Option (FlatTensor α)

Concatenate flat values after checking every parent payload length.

def NN.MLTheory.CROWN.Graph.concatFlatBoxes? {α : Type} [TorchLean.Storage α] [Context α] (layout : ConcatLayout) (boxes : Array (FlatBox α)) : Option (FlatBox α)

Concatenate interval endpoints through the value coordinate map, without rounding.

def NN.MLTheory.CROWN.Graph.concatNodeBoxes? {α : Type} [TorchLean.Storage α] [Context α] (nodes : Array Node) (boxes : Array (Option (FlatBox α))) (node : Node) (axis : ℕ) : Option (FlatBox α)

Shared concat rule for value, first-derivative and mixed-second-derivative interval passes.

structure NN.MLTheory.CROWN.Graph.LinParams (α : Type) [TorchLean.Storage α] [Context α] : Type

Parameters for a linear layer y = W*x + b in flattened form.

m is the output dimension and n is the input dimension.

• m : ℕ

  Output dimension.

• n : ℕ

  Input dimension.

• w : TorchLean.Tensor α [self.m, self.n]

  Weight matrix W (shape m × n).

• b : TorchLean.Tensor α [self.m]

  Bias tensor b (shape m).

structure NN.MLTheory.CROWN.Graph.MatParams (α : Type) [TorchLean.Storage α] [Context α] : Type

Matrix parameters for bias-free matmul: y = W x.

• m : ℕ

  Output dimension.

• n : ℕ

  Input dimension.

• w : TorchLean.Tensor α [self.m, self.n]

  Weight matrix W (shape m × n).

def NN.MLTheory.CROWN.Graph.axisCoordinateOfFlat (shape : Spec.Shape) (axis idx : ℕ) : ℕ

Coordinate on axis corresponding to a row-major flat index.

def NN.MLTheory.CROWN.Graph.batchNormEvalScale {α : Type} [TorchLean.Storage α] [Context α] (config : IR.BatchNormEvalParams α) (ci : Fin config.c) : α

Eval BatchNorm scale for one channel.

def NN.MLTheory.CROWN.Graph.batchNormEvalBias {α : Type} [TorchLean.Storage α] [Context α] (config : IR.BatchNormEvalParams α) (ci : Fin config.c) : α

Eval-mode BatchNorm bias after folding one channel's running statistics into an affine map.

def NN.MLTheory.CROWN.Graph.batchNormEvalLinear? {α : Type} [TorchLean.Storage α] [Context α] (parentShape : Spec.Shape) (channelAxis : ℕ) (config : IR.BatchNormEvalParams α) : Option (LinParams α)

Build the exact diagonal affine form for eval-mode BatchNorm on an arbitrary channel axis.

The graph records the channel axis while the payload stores one scale and bias per channel. A malformed axis or mismatched channel extent has no verifier transfer rule.

structure NN.MLTheory.CROWN.Graph.ParamStore (α : Type) [TorchLean.Storage α] [Context α] : Type

Parameters keyed by node id (weights, biases, constants, and seeded input boxes).

This is kept compact: it is the graph interpreter used to run IBP/CROWN on a pure Graph without pulling in a heavyweight runtime.

• inputBoxes : Std.HashMap ℕ (FlatBox α)

  Seed boxes for designated input nodes (id -> FlatBox).

• constVals : Std.HashMap ℕ (FlatTensor α)

  Constants (id -> FlatTensor).

• linearWB : Std.HashMap ℕ (LinParams α)

  Linear layer params (id -> (W,b)).

• matmulW : Std.HashMap ℕ (MatParams α)

  Matmul params (id -> W) for bias-free multiplication.

• convCfg : Std.HashMap ℕ (IR.ConvParams α)

  Convolution specs (id -> convolution configuration).

• batchNormEval : Std.HashMap ℕ (IR.BatchNormEvalParams α)

  Eval-mode BatchNorm parameters (id -> gamma/beta/running stats).

• layerNorm : Std.HashMap ℕ (IR.LayerNormParams α)

  Affine LayerNorm parameters keyed by node id.

  Trailing-shape value bounds use the stored scale, bias, and epsilon. An absent payload selects unit scale, zero bias, and default epsilon. The derivative transfers use the same stored parameters and reject incompatible payload shapes.

def NN.MLTheory.CROWN.Graph.ParamStore.seedInputBox {α : Type} [TorchLean.Storage α] [Context α] (ps : ParamStore α) (inputId : ℕ) (xB : FlatBox α) : ParamStore α

Insert an input interval box for a graph node.

def NN.MLTheory.CROWN.Graph.ParamStore.seedLInfBall {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] {s : Spec.Shape} (ps : ParamStore α) (inputId : ℕ) (center : TorchLean.Tensor α s) (eps : α) : ParamStore α

Seed a graph input with a uniform ℓ∞ box around a shaped tensor.

def NN.MLTheory.CROWN.Graph.planConvTransfer? {α : Type} [TorchLean.Storage α] (configuration : IR.ConvConfig) (parameters : IR.ConvParams α) (parentShape outShape : Spec.Shape) : Option Spec.Shape

Validate convolution geometry and return its leading batch shape.

The canonical IR contract checks channels, groups, dilation, stride, padding and spatial rank. The payload and declared output must agree with the same geometry before any CROWN transfer runs.

def NN.MLTheory.CROWN.Graph.crownNodeSemanticsSupported {α : Type} [TorchLean.Storage α] [Context α] (nodes : Array Node) (ps : ParamStore α) (id : ℕ) : Bool

Check the graph-level semantic restrictions imposed by the current CROWN engine.

Convolution payloads must match the declared geometry; LayerNorm payloads must match the entire normalized suffix. Custom computations are unsupported without verification transfer rules. This predicate checks the common shape contract; individual transfers also check their arithmetic and derivative requirements.

def NN.MLTheory.CROWN.Graph.crownGraphSemanticsSupported {α : Type} [TorchLean.Storage α] [Context α] (g : Graph) (ps : ParamStore α) : Bool

Whether every node in a graph is interpreted exactly by the current CROWN engine.

def NN.MLTheory.CROWN.Graph.outputBox? {α : Type} [TorchLean.Storage α] [Context α] (boxes : Array (Option (FlatBox α))) (outId : ℕ) : Except String (FlatBox α)

Read a node's interval box from an IBP-style result array.

@[instance_reducible]

instance NN.MLTheory.CROWN.Graph.instInhabitedFlatBox {α : Type} [TorchLean.Storage α] [Context α] : Inhabited (FlatBox α)

Default inhabitant for FlatBox (a 0-dimensional box at 0).

def NN.MLTheory.CROWN.Graph.boxMulElem {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (B1 B2 : FlatBox α) : Option (FlatBox α)

Elementwise product of two FlatBoxes (interval product per component). Requires equal dims.

def NN.MLTheory.CROWN.Graph.toFlatBox {α : Type} [TorchLean.Storage α] [Context α] (n : ℕ) (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : FlatBox α

Convert a dependent Box of shape .dim n .scalar into a FlatBox with dim := n.

def NN.MLTheory.CROWN.Graph.ofFlatBox {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) : Box α (Spec.Shape.dim B.dim Spec.Shape.scalar)

Convert a FlatBox to a dependent Box at shape .dim B.dim .scalar.

def NN.MLTheory.CROWN.Graph.boxAdd {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (B1 B2 : FlatBox α) : FlatBox α

Add two flat interval boxes coordinatewise; dimension mismatches preserve the left box.

def NN.MLTheory.CROWN.Graph.boxSub {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (B1 B2 : FlatBox α) : FlatBox α

Interval subtraction on FlatBox endpoints (sound enclosure).

def NN.MLTheory.CROWN.Graph.boxSum {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (B : FlatBox α) : FlatBox α

Sum all coordinates of a flat box with directed accumulation.

def NN.MLTheory.CROWN.Graph.boxRelu {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) : FlatBox α

Apply ReLU to both endpoints of a FlatBox (monotone activation, so endpoints suffice).

def NN.MLTheory.CROWN.Graph.boxAbs {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (B : FlatBox α) : FlatBox α

Componentwise absolute value bounds using directed negation at negative endpoints.

def NN.MLTheory.CROWN.Graph.boxUnaryEnclosure? {α : Type} [TorchLean.Storage α] [Context α] (enclose : α → α → Option (α × α)) (B : FlatBox α) : Option (FlatBox α)

Apply a scalar interval enclosure coordinatewise to a flat box.

def NN.MLTheory.CROWN.Graph.boxSqrt? {α : Type} [TorchLean.Storage α] [Context α] [NonlinearBoundOps α] (B : FlatBox α) : Option (FlatBox α)

Componentwise square-root bounds using the scalar backend's domain checks.

The supplied real and native-float backends clamp negative lower endpoints to zero and reject wholly negative intervals. A backend may also reject an operation it does not support.

def NN.MLTheory.CROWN.Graph.boxSoftplus? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (B : FlatBox α) : Option (FlatBox α)

Softplus bounds, applied independently at every tensor coordinate.

def NN.MLTheory.CROWN.Graph.boxSafeLog? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (B epsilon : FlatBox α) : Option (FlatBox α)

SafeLog bounds with one shared scalar epsilon interval.

The epsilon parent must contain one scalar. Keeping this check here makes direct graph construction follow the same contract as the typed builder and IR shape inference.

def NN.MLTheory.CROWN.Graph.boxInv? {α : Type} [TorchLean.Storage α] [Context α] [NonlinearBoundOps α] (B : FlatBox α) : Option (FlatBox α)

Componentwise reciprocal bounds, failing when an input coordinate interval crosses zero.

def NN.MLTheory.CROWN.Graph.derivBoxLog? {α : Type} [TorchLean.Storage α] [Context α] [NonlinearBoundOps α] (zB : FlatBox α) : Option (FlatBox α)

Derivative range for log; log' x = 1/x on a strictly positive interval.

def NN.MLTheory.CROWN.Graph.secondDerivBoxLog? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (zB : FlatBox α) : Option (FlatBox α)

Second-derivative range for log; log'' x = -1/x² on a positive interval.

def NN.MLTheory.CROWN.Graph.boxNeg {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) : FlatBox α

Negate an interval box by swapping and negating its endpoints.

def NN.MLTheory.CROWN.Graph.flatAxisPermutation? (sourceShape : Spec.Shape) (perm : Array ℕ) (n : ℕ) : Option (Fin n → Fin n)

Return the flat-coordinate permutation induced by an axis permutation.

perm follows the tensor convention used by Shape.permute?: output axis i is read from input axis perm[i]. The resulting function therefore maps each output flat coordinate to the input flat coordinate from which its value is taken. Invalid permutations and inconsistent dimensions are rejected.

def NN.MLTheory.CROWN.Graph.boxMaxElem {α : Type} [TorchLean.Storage α] [Context α] (B1 B2 : FlatBox α) : FlatBox α

Componentwise max bounds: max(x,y) over interval boxes.

def NN.MLTheory.CROWN.Graph.boxMinElem {α : Type} [TorchLean.Storage α] [Context α] (B1 B2 : FlatBox α) : FlatBox α

Componentwise min bounds: min(x,y) over interval boxes.

def NN.MLTheory.CROWN.Graph.boxSquare {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (B : FlatBox α) : FlatBox α

Componentwise square of an interval box, with downward-rounded lower endpoint squares and upward-rounded upper endpoint squares. The minimum is 0 when the interval crosses 0.

The body is exposed because the proof layer theorem module unfolds this executable rule when proving dimension preservation and pointwise enclosure.

def NN.MLTheory.CROWN.Graph.intervalMul {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (aLo aHi bLo bHi : α) : α × α

Interval multiplication for scalar endpoints: given [aLo,aHi] and [bLo,bHi], return bounds on the product.

def NN.MLTheory.CROWN.Graph.binaryMatmulBox {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (dims : IR.OpContracts.MatmulDims) (left right : FlatBox α) : FlatBox α

Directed contraction with the same scalar indexing and sum order as Graph.matmulFlat.

def NN.MLTheory.CROWN.Graph.ibpBinaryMatmul? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (leftShape rightShape : Spec.Shape) (left right : FlatBox α) : Option (FlatBox α)

Binary matmul with batch broadcasting, vector promotion, and directed endpoint arithmetic.

def NN.MLTheory.CROWN.Graph.ibpUnflatten {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (dim : ℕ) (t : TorchLean.Tensor α [dim]) (h : dim = s.size) : TorchLean.Tensor α s

Reinterpret a flattened tensor as shape s when the element counts agree.

def NN.MLTheory.CROWN.Graph.ibpBroadcastTo {α : Type} [TorchLean.Storage α] [Context α] (s₁ s₂ : Spec.Shape) (Xin : FlatBox α) : Option (FlatBox α)

IBP rule for broadcasting a flattened input box to a target shape.

def NN.MLTheory.CROWN.Graph.ibpReduceSumAxis {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (axis : ℕ) (Xin : FlatBox α) (s : Spec.Shape) : Option (FlatBox α)

Sum one axis with downward lower accumulation and upward upper accumulation.

def NN.MLTheory.CROWN.Graph.ibpSoftmaxRange {α : Type} [TorchLean.Storage α] [Context α] (s : Spec.Shape) (axis dim : ℕ) : FlatBox α

Format-independent softmax enclosure on a flattened tensor.

A singleton row is exactly one. Every coordinate of a longer row lies in [0,1]. This deliberately forgoes a tighter exponential relaxation so executable checking does not assume a directed transcendental implementation that its scalar backend has not supplied.

Hard-masked softmax IBP (last axis)

Blocked coordinates have weight zero. An allowed coordinate lies in [0,1], and it has weight one when it is the only allowed coordinate in its row. These bounds do not evaluate exp or division, so they remain valid for executable endpoint types whose BoundOps instance covers only directed arithmetic. A tighter transfer rule requires separately certified directed bounds for transcendental operations.

def NN.MLTheory.CROWN.Graph.ibpHardMaskedSoftmaxLastTensor {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} : TorchLean.Tensor α s → TorchLean.Tensor α s → TorchLean.Tensor Bool s → TorchLean.Tensor α s × TorchLean.Tensor α s

Conservative interval bounds for hard-masked softmax along the last tensor axis.

LayerNorm interval propagation

Normalization acts independently on each row of the configured trailing shape. Its directed transfer bounds the mean, variance, stabilized denominator, and affine scale and bias.

def NN.MLTheory.CROWN.Graph.ibpLayerNormRange? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (s : Spec.Shape) (dim : ℕ) (axis : ℕ := s.rank - 1) : Option (FlatBox α)

Uniform finite enclosure for normalization over a trailing shape.

For a row of length n, exact LayerNorm without affine scale or bias satisfies |yᵢ| ≤ sqrt n; a singleton row is identically zero. Backends provide the outward-rounded bound through NonlinearBoundOps.layerNormAbsBound. Returning none is preferable to evaluating the normalization with unqualified host division and square root.

def NN.MLTheory.CROWN.Graph.checkedFiniteBounds? {α : Type} [Context α] (bounds : α × α) : Option (α × α)

Validate an interval before using it in a nonlinear transfer. Self-subtraction rejects infinite and NaN IEEE endpoints; finite exact-real endpoints satisfy these checks as well.

def NN.MLTheory.CROWN.Graph.ibpBatchNormEval? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (parentShape : Spec.Shape) (channelAxis : ℕ) (config : IR.BatchNormEvalParams α) (input : FlatBox α) : Option (FlatBox α)

Enclose eval-mode BatchNorm without treating rounded normalization coefficients as exact.

The running statistics are fixed, but their stabilized square root and division still need directed bounds. Coordinates use the denominator interval for their channel.

def NN.MLTheory.CROWN.Graph.directedRowMean? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] {n : ℕ} (bounds : Fin n → α × α) : Option (α × α)

Directed mean bounds for one nonempty row. The denominator encloses the exact row length, including lengths that cannot be represented exactly by the scalar format.

def NN.MLTheory.CROWN.Graph.boxMean? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (B : FlatBox α) : Option (FlatBox α)

Average a nonempty flat box, enclosing both the sum and the exact coordinate count.

def NN.MLTheory.CROWN.Graph.ibpReduceMeanAxis {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (axis : ℕ) (Xin : FlatBox α) (s : Spec.Shape) : Option (FlatBox α)

Average one axis using directed sums and division. The denominator encloses the exact axis length, so a rounded natural-number conversion cannot silently narrow the result.

def NN.MLTheory.CROWN.Graph.directedLayerNormRow? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] {n : ℕ} (lo hi gamma beta : TorchLean.Tensor α [n]) (epsilon : α) : Option (TorchLean.Tensor α [n] × TorchLean.Tensor α [n])

Directed bounds for one LayerNorm row with explicit affine parameters.

The order follows Spec.layerNorm: center the input, center again inside reduceVar, square, average, clamp variance to zero, add epsilon, take a square root, and divide the first centered values directly. Each coordinate is then multiplied by its gamma and shifted by its beta; negative gamma reverses the interval endpoints.

Epsilon must be finite and positive, and the row and affine parameters must be finite. Division and square root use the selected nonlinear backend. Invalid or non-finite intermediate intervals return none. Proofs.LayerNormEnclosure proves enclosure of the real row under the backend's arithmetic laws. Agreement with native arithmetic requires its own numerical correspondence.

def NN.MLTheory.CROWN.Graph.ibpLayerNormPayloadBox? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (s : Spec.Shape) (axis : ℕ) (parameters : IR.LayerNormParams α) (input : FlatBox α) : Option (FlatBox α)

Enclose a LayerNorm payload over the trailing shape starting at axis.

The matrix view and affine suffix are checked by the same helpers used in IR evaluation. Bounds are propagated separately for each row, then flattened back into the graph's storage order. Every payload, including one with default parameter values, uses the directed normalization sequence with its stored affine parameters and epsilon.

def NN.MLTheory.CROWN.Graph.ibpLayerNormBox? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (s : Spec.Shape) (input : FlatBox α) (axis : ℕ := s.rank - 1) : Option (FlatBox α)

Use the backend's uniform LayerNorm range when available; otherwise propagate the supplied input box through the directed normalization sequence over the suffix beginning at axis. Omitting axis selects the final axis.

def NN.MLTheory.CROWN.Graph.castBoxDim {α : Type} [TorchLean.Storage α] {n n' : ℕ} (h : n = n') (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n' Spec.Shape.scalar)

Cast a 1D Box along an equality of dimensions.

def NN.MLTheory.CROWN.Graph.castAffineIn {α : Type} [TorchLean.Storage α] {n n' m : ℕ} (h : n = n') (a : AffineVec α n m) : AffineVec α n' m

Cast the input dimension of an affine map across a proven equality.

def NN.MLTheory.CROWN.Graph.castAffineOut {α : Type} [TorchLean.Storage α] {n m m' : ℕ} (h : m = m') (a : AffineVec α n m) : AffineVec α n m'

Cast the output dimension of an affine map across a proven equality.

@[reducible, inline]

abbrev NN.MLTheory.CROWN.Graph.castDimScalar {α : Type} [TorchLean.Storage α] {n n' : ℕ} (h : n = n') (t : TorchLean.Tensor α [n]) : TorchLean.Tensor α [n']

Cast a dim-scalar tensor across an equality of dimensions.

We keep this as an abbrev so it unfolds aggressively in simp-based soundness proofs.

@[simp]

theorem NN.MLTheory.CROWN.Graph.castDimScalar_self {α : Type} [TorchLean.Storage α] {n : ℕ} (h : n = n) (t : TorchLean.Tensor α [n]) : castDimScalar h t = t

Casting a flat vector tensor along an equality from a dimension to itself changes no data.

def NN.MLTheory.CROWN.Graph.ibpLinearParams {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (p : LinParams α) (Xin : FlatBox α) : Option (FlatBox α)

IBP propagation through explicit linear parameters.

def NN.MLTheory.CROWN.Graph.ibpLinear {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (id : ℕ) (ps : ParamStore α) (Xin : FlatBox α) : Option (FlatBox α)

IBP propagation for a .linear node using ParamStore.linearWB.

def NN.MLTheory.CROWN.Graph.ibpMatmul {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (id : ℕ) (ps : ParamStore α) (Xin : FlatBox α) : Option (FlatBox α)

IBP propagation for a .matmul node (bias-free) using ParamStore.matmulW.

def NN.MLTheory.CROWN.Graph.ibpConvNode {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (configuration : IR.ConvConfig) (parentShape outShape : Spec.Shape) (id : ℕ) (ps : ParamStore α) (Xin : FlatBox α) : Option (FlatBox α)

IBP transfer for a supported convolution node whose parameters are stored in ParamStore.convCfg.

def NN.MLTheory.CROWN.Graph.ibpMonotoneSomeTensor? {α : Type} [TorchLean.Storage α] [Context α] (parentShape outShape : Spec.Shape) (op : Spec.SomeTensor α → Except String (Spec.SomeTensor α)) (input : FlatBox α) : Option (FlatBox α)

Apply a monotone SomeTensor operation independently to both interval endpoints.

def NN.MLTheory.CROWN.Graph.ibpAvgPool? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (config : IR.WindowConfig) (parentShape outShape : Spec.Shape) (input : FlatBox α) : Option (FlatBox α)

Average-pool bounds with directed window sums, counts, and division.

The shared pooling plan validates the spatial suffix and preserves every leading axis. Windows follow the spec's row-major coordinates and padded-cell lookup; padded zeros still contribute to the denominator. Unavailable or nonfinite arithmetic and inconsistent declared shapes return none.