CrownParamstore

PyTorch → CROWN ParamStore helpers.

This module is not about JSON parsing; it is about what we do after we have already loaded weights into typed Lean tensors.

Why this exists:

• PyTorch “weights” are keyed by module names (state_dict keys).
• TorchLean’s graph backend stores parameters by node id in NN.MLTheory.CROWN.Graph.ParamStore.

So any real bridge needs a small amount of “wiring code” that:

1. chooses a node-id scheme (model-specific),
2. inserts the corresponding (W,b) tensors into the right slots.

These helpers keep NN.Runtime.PyTorch.Import.Core focused on JSON, and so model example loaders can share the same ParamStore-building utilities.

def Import.CROWNParamStore.ofArray {α β : Type} [TorchLean.Storage α] [Context α] (nodeId : ℕ → ℕ) (layers : Array β) (parameter : β → NN.MLTheory.CROWN.Graph.LinParams α) : NN.MLTheory.CROWN.Graph.ParamStore α

Build a graph parameter store from a sequence of layer descriptions.

nodeId assigns graph slots; parameter converts each description to typed weights and bias. Layers are inserted in array order, so the last occurrence of a node id wins.

def Import.CROWNParamStore.map {α β : Type} [TorchLean.Storage α] [Context α] [TorchLean.Storage β] [Context β] (f : α → β) (parameters : NN.MLTheory.CROWN.Graph.LinParams α) : NN.MLTheory.CROWN.Graph.LinParams β

Convert every weight and bias scalar, preserving the linear layer's dimensions.