MLP Deterministic Initialization

GraphSpec chains (Chain + >>>) have a typed parameter ABI: each model comes with an explicit type-level list ps : List Shape describing the shapes and the order of its parameter tensors.

For execution/training examples, we often want deterministic (but nontrivial) initialization rather than “all zeros”. GraphSpec supports that by letting primitives optionally provide a TorchLean Layer (via Primitive.toLayerM?), whose initState uses occurrence-indexed seeds.

This file proves one concrete bridge theorem: for the 2-layer MLP Models.mlp, the deterministic initialization obtained from GraphSpec is exactly the same typed parameter list you would get by initializing the two TorchLean Linear layers directly with the expected occurrence-indexed seeds.

That matters because GraphSpec models expose parameters by a typed ABI, not by mutable module fields. This theorem checks that the ABI order used by GraphSpec initialization agrees with the runtime layer order used by TorchLean.

theorem NN.GraphSpec.Models.mlp_detInitParams_eq_torchlean_linear_inits (inputWidth hiddenWidth outputWidth : ℕ) : LowerToDAG.Chain.detInitParams? (mlp inputWidth hiddenWidth outputWidth) = Except.ok ((Runtime.Autograd.Model.Layers.linear inputWidth hiddenWidth).initState.append (Runtime.Autograd.Model.Layers.linear hiddenWidth outputWidth 1).initState)

Deterministic init for Models.mlp is exactly the concatenation of the two TorchLean Linear initializers.

Seed discipline:

• the first linear weight uses occurrence index 0,
• the second linear weight uses occurrence index 1,
• both biases are initialized exactly to zero.