Pack param shape descriptors: [nParams, rank0, d0..., rank1, d1..., ...] as int32 LE.

Pack a single shape: [rank, d0, d1, ...] as int32 LE (for x input).

Chapter-5 real ResNet-34 params (IMAGENETTE 3×224×224 — paper-native ImageNet resolution): 7×7 stride-2 stem {W=[64,3,7,7],γ,β} (224→112), then the 16 basic blocks (3 strided downsample {W,γ,β}×2 + proj{W,γ,β}; 13 identity {W,γ,β}×2) at channels 64/128/256/512 (spatial 56/28/14/7), then dense {W,b}. Per-channel BN ⇒ γ/β are rank-1 [c] (not rank-0 scalars). 110 params (no conv biases: every conv is BN-followed). The (dims, initKind) order MUST match the @resnet34_<variant>_train_step and @resnet34_fwd signatures, rendered by Proofs/Codegen/ResNet34RenderB.lean. initKind: 0 = random weight (mkParam: conv He fan-out, dense Glorot), 1 = ones (γ), 2 = zeros (β / bias).

(dims, initKind) for every param, in func-arg order.

Chapter-6 MobileNetV2 params (IMAGENETTE 3×224×224 — paper-native ImageNet resolution, full-paper downsampling [t,c,n,s]): stem {W,γ,β} (3×3 stride-2 conv 3→32), then 17 inverted-residual blocks — each expand 1×1 {W,γ,β}, depthwise 3×3 {W,γ,β} (a [mid,1,3,3] kernel, feature_group_count = mid; stride-2 for the downsampling blocks), project 1×1 {W,γ,β} — then the head 1×1 conv {W,γ,β} (320→1280, the MNv2 "features" layer: conv→BN→relu6 before GAP, so the pooled tensor isn't the constant β of an instance-normed BN) and dense {W,b}.

158 params (no conv biases: every conv here is BN-followed and BN removes a bias). At K = 1000 the count is 3,504,872, the JAX reference's. Per-channel BN ⇒ γ/β are rank-1 [c]. Spatial 224→112(stem)→56→28→14→7 — the MobileNetV2 /32 flow. The (dims, initKind) order MUST match @mobilenetv2_adam_train_step's signature (and @mobilenetv2_fwd's) — both rendered from the same Proofs.StableHLO.mnv2FwdChainB traversal. Strides live only in the renderers (no param-shape effect). initKind: 0 = random weight (mkParam: conv He fan-out, dense Glorot), 1 = ones (γ), 2 = zeros.

(ic, mid, oc) per block — MUST match tests/TestMobilenetV2*.lean blocks. Full paper net (17).

(dims, initKind) for every param, in func-arg order.

Chapter-7 EfficientNet-B0 params (Imagenette 3×224×224 — the [t,c,n,s,k] config, all-swish + batch norm): stem {W,γ,β} (3×3 stride-2 conv 3→32), then 16 MBConv layers across 7 stages (channels [16,24,40,80,112,192,320], kernels [3,3,5,3,5,5,3], expand [1,6,6,6,6,6,6] — the MBConv1 stage-1 blocks have NO expand conv) — each (when expanded) expand 1×1 {W,γ,β}, depthwise k×k {W,γ,β} ([mid,1,k,k], feature_group_count = mid), squeeze-excite {Ws₁[mid,r],bs₁[r], Ws₂[r,mid],bs₂[mid]} (r = ic/4), project 1×1 {W,γ,β} — then head 1×1 conv {W,γ,β} (320→1280) and dense {W,b}. Batch-norm γ/β rank-1 [c]. 213 params (the 49 BN-followed convs carry no bias; at K = 1000 this is 5,288,548 — the JAX reference's own count). SE's two biases stay: those 1×1 convs are followed by the sigmoid gate, not by BN, so nothing absorbs them and the reference carries them. Spatial 224→112→56→28→14→7 (stride-2 stem, 4 strided stages). The (dims, initKind) order MUST match @efficientnet_train_step's signature, rendered by Proofs/Codegen/EfficientNetRender/Basic.lean. initKind: 0 = random weight (mkParam: conv He fan-out, dense Glorot), 1 = ones (γ), 2 = zeros (β / bias), 7 = SE FC (var 2/out under seFanOutInit, the reference's 1×1-conv fan-out; else Glorot).

(dims, initKind) for every param, in func-arg order — generated from the B0 stage spec exactly as tests/TestEfficientNet*.lean blocks (stem out 32, prev threading).

Chapter-8 ConvNeXt-T params (IMAGENETTE 3×224×224 — paper-native resolution): 4×4/s4 patchify stem {W=[96,3,4,4],b} (224→56), then [3,3,9,3] blocks @ [96,192, 384,768] (spatial 56/28/14/7) with 3 between-stage LN+2×2/s2 downsamples, then head GAP → LN(768) → dense {W,b}. The patchify stem carries a channel LN {γ,β} [96]. ConvNeXt block (9 params): depthwise 7×7 {W=[c,1,7,7],b} → channel LN (per-channel γ/β [c]) → 1×1 expand {W=[4c,c,1,1],b} → GELU → 1×1 project {W=[c,4c,1,1],b} → layerScale (per-channel γ=[c]). Each downsample (4 params): channel LN {γ,β} [c] + 2×2 conv {W=[2c,c,2,2],b}. 182 params. The (dims, initKind) order MUST match @convnext_train_step's signature, rendered by Proofs/Codegen/ConvNeXtRender.lean. initKind: 0 = random weight (mkParam; σ = 0.02 under its ConvNeXt flag), 1 = ones (LN γ), 2 = zeros (LN β / bias), 3 = 1e-6 (layerScale γ, the paper's init).

(dims, initKind) for every param, in func-arg order.

The head is GAP → LN(768) → dense, as in both the paper (self.norm(x.mean([-2,-1])), nn.LayerNorm(dims[-1], eps=1e-6)) and timm (NormMlpClassifierHead). 182 param tensors; the floats are 27,827,818 at K = 10, i.e. 28,589,128 at K = 1000 — timm's count. Without the head LN the count would be short by exactly 2×768 = 1,536, so a near-matching count is not evidence of the right architecture.

Chapter-9 ViT-Tiny params (IMAGENETTE 3×224×224, patch-16): a 16×16/s16 conv patch embed {W=[192,3,16,16],b} (224→14×14=196 patches), a learned CLS token [192] (1D, matching the proof-tied render) + positional embed [197,192], then 12 pre-norm transformer blocks (dim 192, 3 heads, MLP 768), final LayerNorm γ/β, CLS-slice dense head {W=[192,10],b}. LayerNorm γ/β are per-channel [192] (normalize ∘ per-channel affine, as in Proofs.vitForwardKV). Each block (16 params): LN1 γ/β, Wq/bq/Wk/bk/Wv/bv/Wo/bo [192,192]/[192], LN2 γ/β, MLP Wfc1[192,768]/bfc1/Wfc2[768,192]/bfc2. 4+12·16+4 = 200 params. The (dims,initKind) order MUST match @vit_train_step/@vit_fwd, whose parameter list is Proofs.StableHLO.vitParamSig (Proofs/Codegen/ViTRender.lean). initKind: 0 = random weight (mkParam: conv He fan-out, dense Glorot, or timm's σ = 0.02 under its ViT flag), 1 = ones (LN γ), 2 = zeros (LN β / bias), 5 = embedding (CLS / pos: σ = 0.02 under the ViT flag, zeros without it), 8 = the patch-embed bias (PyTorch's Conv2d default U(±1/√768) under patchEmbedBiasTorch, zeros without it — VLayer.patchEmbed).

(dims, initKind) for every param, in @vit_train_step func-arg order.