The flattened slab is the Mat row — the form every per-example op consumes.

Adding a batch-uniform vector shifts every example's slab the same way — the shape a zeroed residual body contributes, and the reason it is transparent to the example difference.

batchMap acts slab by slab.

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).

⭐ The one arithmetic fact: ((c,i),j) and (c,(i,j)) are the same offset, so the mul_assoc cast that defines bnBatchLA sends the network cell to the bnBatchTensor4 cell. finProdFinEquiv is row-major, so both sides are j + w·i + h·w·c + oc·h·w·n.

The row, read at (n, (i, j)), is the cell (n, c, i, j).

⭐⭐ The bridge: a cell of a bnBatchLA output is the scalar bnForward of that cell's channel row, at that cell's position in the row. Everything else in this file is BN algebra on one row.

⭐ The workhorse. A property of every cell of a bnBatchLA output, reduced to the scalar bnForward on each channel's row — no index decomposition at the call site. Every clause of the shape "this BN output is off the kink / inside a window" goes through here.

BN acts on coordinate differences by γ·istd — the exact identity that propagates the carrier undamped through every BN, and the reason no BN-variance derivative is ever taken: the difference is γ · (difference) · istd with istd evaluated at the same activation.

The two-sided BN margin |bn − β| ≤ |γ|·√n, with no mean/variance computation (bnXhat_sq_le). bnForward_lb's symmetric form; what makes a large β keep a relu off its kink at every input, so the structural net needs no eventually-argument for its relus.

√n < β from n < β² — the margin check at each of the witness's BN widths.

A constant activation has a constant row.

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

The batched margin: with γ, β channel-constant, every cell is within |g|√(N·h·w) of b.

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.

Batch BN is injective within one example and channel (γ_c ≠ 0): it is the strictly monotone affine map γ_c·istd_c·(· − μ_c) + β_c there. The stem pool's no-tie discharge — equal pooled cells force equal pre-BN cells, and the witness's ramp is positionally injective.

The centre-tap conv value: b o + s · (input channel 0 at the same position), at every output channel. ⚠ c₀ is passed in (rather than built from 0 < ic) so that the carrier's channel index is the same term at every use site — ring needs those istds to be one atom.

The flat centre-tap conv, in cell coordinates.

Decimation reads position (2i, 2j), channel for channel (the generic peer of the retired 2-channel decimate_unflatten).

The strided centre-tap conv: b o + s · (input channel 0 at the even position).

The batched centre-tap conv, in cell coordinates — the carrier's conv step at stride 1 (ResNet-50's stage-1 projection is the one site that needs it).

The batched strided centre-tap conv, in cell coordinates — the carrier's conv step.

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).

Odd decimation reads position (2i+1, 2j+1), channel for channel — the peer of decimate_unflatten.

The strided XLA-SAME centre-tap conv: b o + s · (input channel 0 at the ODD position). flatConvStride2Xla is decimateOddFlat ∘ flatConv, so this is flatConvStride2_ctK with decimateOdd_unflatten in place of decimate_unflatten.

The batched strided XLA-SAME centre-tap conv, in cell coordinates — MobileNetV2's stem.

The centre-tap depthwise value: b ch + s · (the same channel at the same position).

The flat centre-tap depthwise, in cell coordinates.

The batched centre-tap depthwise — the carrier's depthwise step at stride 1.

The strided XLA-SAME centre-tap depthwise, at the odd position.

The batched strided XLA-SAME centre-tap depthwise — MobileNetV2's four downsampling blocks.

A zeroed depthwise (zero kernel, zero bias) sends everything to the constant 0 — the residual bodies of an inverted-residual net. ⛔ No strided peer is needed: a net's strided blocks change channels, so they are on the carrier and never carry a zeroed kernel.

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.

⭐ The 3×3/s2 pool shifts with a uniform offset. If one slab's channel is another's plus the constant δ, so are their pooled values — max of a uniformly shifted family (Finset.apply_sup'_eq_sup'_comp at (· + δ)). No argmax or eventually-argument: this holds at every point of the ray, which is what lets the carrier cross the only real kink in the net.

The pool keeps a nonnegative slab nonnegative (it selects a window cell).

GAP of a uniformly shifted channel is shifted by the same constant.

relu is continuous everywhere — it is max · 0; only its derivative has a kink.

A residual branch is continuous when its body is.

A projected residual is continuous when both branches are.

bnIstd is continuous in the activation (ε > 0).

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

maxPool3s2Flat is continuous (a sup' of coordinates).

batchMap of a continuous per-example op is continuous.

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 strided XLA-SAME peer of EDiff_dw. The carrier is spatially uniform, so decimation — whichever phase it keeps — is transparent to it.

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

W·a + b determines a and b when b < W (division with remainder).

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

⭐ The pre-BN stem activation is positionally injective within each example and channel: the centre tap decimates the ramp, and example 0's uniform +t shifts every position alike.

⭐ 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.