The batched 3×3/s2 pool, slab by slab.

batchMap at a per-example output that is read as a plain Vec (the head's GAP/dense).

Batch BN keeps equal cells equal within one example and channel: the per-channel affine map reads nothing of a cell but its value. What lets a tie between two stem cells that read identical input patches survive every BN parameter (StemConvTwin in ResNet34ParamGrad).

A constant channel normalizes to β (variance 0, xhat = 0): a zeroed residual body is the constant β₂, whatever γ₂ is. The batched peer of bnForward_const.

Positivity from the margin — |g|√(N·h·w) < b makes the whole BN output strictly positive, at every input. The relu clause of every conv-bn-relu stage in the witness.

The relu6 window from the margin — the two-sided twin of bnBatchLA_pos. With β = b strictly inside (|g|√(N·h·w), 6 − |g|√(N·h·w)) the whole BN output sits strictly inside (0, 6), at every input, so relu6_id_window collapses the stage that follows it. b = 3 centres the window and makes both hypotheses the single check |g|√(N·h·w) < 3.

Both relu6 clauses at once, in the ≠ 0 ∧ ≠ 6 shape every MobileNet smoothness bundle is stated in. Since the bound is input-independent, this discharges a relu6 clause without reading the activation — which is why a relu6 net's whole clause bundle is weight-only.

The carrier step. Two examples of one channel share the channel's mean and istd, so batch BN keeps their difference and multiplies it by γ_c · istd_c. This is what a channel-difference carrier cannot do under per-channel batch BN, and it is why the witness is at N = 2.

A zeroed conv (zero kernel, zero bias) sends everything to the constant 0 — the residual bodies. flatConv_eq_zero lifted across the batch.

A zeroed STRIDED conv sends everything to the constant 0 (decimation of a constant).

Cellwise ⇒ flatwise. A property of every cell (n, c, i, j) holds at every flat index — the bridge from the bcell view back to the ∀ k shape every clause is stated in.

bnRowLA is continuous in the activation — it is a reindex.

1 · √n < 160 whenever n < 25600 — the margin bnBatchLA_pos consumes, at γ = 1, β = 160. Every BN width of a 224×224 ResNet witness clears it (the widest is the stem's 2·112² = 25088).

|1/64|·√n < 3 whenever n < 36864 = (3·64)² — the relu6 margin bnBatchLA_smooth6 consumes, at γ = 1/64, β = 3. It clears both of that lemma's hypotheses at once, β = 3 being the centre of (0, 6). Every relu6 BN width of a 224×224 MobileNetV2 witness fits: the widest is 2·112² = 25088, shared by the stem, b1's depthwise and b2's expand.

The ray is continuous in its parameter.

The ray's carrier: t in channel 0, nothing elsewhere.

A batch-uniform shift (a zeroed residual body) is transparent to the carrier.

Batch BN scales the carrier by γ_c · istd_c — the two examples share the channel's mean and istd, so centring keeps their difference (bnBatchLA_exdiff).

A centre-tap conv copies channel 0's offset to every output channel, and is transparent to the zero padding because only the centre tap is nonzero.

The strided peer of eDiff_conv.

The XLA-SAME strided peer of eDiff_conv — MobileNetV2's stem.

A centre-tap depthwise scales the carrier channel by channel. Unlike eDiff_conv, which collapses δ to the single value s * δ c₀ at every output channel, a depthwise reads only its own channel, so the whole function δ survives, scaled.

The 3×3/s2 pool keeps the carrier, at every t.

The stem BN is strictly positive at every point of the ray (the β = 160 margin).

The stem pool has no tie at the witness: BN is injective within a channel (bnBatchLA_cell_inj) and the pre-BN activation is positionally injective. Stated in the ∀ example, MaxPool3s2Smooth (slab) shape the nets' *PoolSmoothAt unfolds to.

GAP and the dense head deliver the carrier to one class: GAP of a uniformly shifted channel is shifted by the same constant, and a Wd that reads channel c₀ into class j turns the per-channel carrier into δ c₀. Stated on the batchMaps a *HeadB unfolds to, so every net's head instantiates it.

A centre-tap 1×1 (or kH×kW) conv, then its BatchNorm: the carrier is channel c₀'s offset times γ0 · istd, at every output channel.

The strided peer of eDiff_convBn.

A centre-tap depthwise conv, then its BatchNorm: channel by channel, δ ci · γ0 · istd.

The strided peer of eDiff_dwBn.

The XLA-SAME strided peer of eDiff_dwBn.

A zeroed final conv makes a body the constant β₂ — projB at a zero kernel is bnBatchLA of the constant 0, which is β₂ (variance 0). Used for both block kinds.

The projection is strictly positive at every input (the β = 160 margin).

A strided conv-bn-relu stage whose BN is everywhere positive has no relu left.

sealProj, unfolded — bn of the centre-tap strided conv.