Lowered Forward Evaluation: Prefix Preservation

Lowering a forward let-chain only appends IR nodes and only inserts payload at fresh node ids. These lemmas record that every node and payload entry below the starting graph size is unchanged by lowering the rest of the chain.

theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_ps_constVals_get?_lt {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (g : ForwardLetChain α paramShapes inShape ss out) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) {k : ℕ} (hk : k < c.graph.nodes.size) : (lowerForwardLetChain g params c).ps.constVals.get? k = c.ps.constVals.get? k

Lowering a let-chain does not change ps.constVals entries for keys < c.graph.nodes.size. Lowering only inserts payload at the fresh node id, so older keys are unchanged.

theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_ps_linearWB_get?_lt {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (g : ForwardLetChain α paramShapes inShape ss out) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) {k : ℕ} (hk : k < c.graph.nodes.size) : (lowerForwardLetChain g params c).ps.linearWB.get? k = c.ps.linearWB.get? k

Lowering a let-chain does not change ps.linearWB entries for keys < c.graph.nodes.size. Lowering only inserts linear payload at the fresh node id, so older keys are unchanged.

theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_ps_convCfg_get?_lt {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (g : ForwardLetChain α paramShapes inShape ss out) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) {k : ℕ} (hk : k < c.graph.nodes.size) : (lowerForwardLetChain g params c).ps.convCfg.get? k = c.ps.convCfg.get? k

Lowering a let-chain does not change ps.convCfg entries for keys < c.graph.nodes.size. Lowering only inserts convolution payloads at fresh node ids, so older keys are unchanged.

theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_ps_batchNormEval_get?_lt {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (g : ForwardLetChain α paramShapes inShape ss out) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) {k : ℕ} (hk : k < c.graph.nodes.size) : (lowerForwardLetChain g params c).ps.batchNormEval.get? k = c.ps.batchNormEval.get? k

Lowering a let-chain does not change ps.batchNormEval entries for keys below the starting graph size. Eval-mode BatchNorm payloads enter through the broader IR/import bridge, not through this proved first-order fragment.

theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_ps_layerNorm_get?_lt {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (g : ForwardLetChain α paramShapes inShape ss out) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) {k : ℕ} (hk : k < c.graph.nodes.size) : (lowerForwardLetChain g params c).ps.layerNorm.get? k = c.ps.layerNorm.get? k

Lowering a let-chain preserves LayerNorm payloads below the starting graph size.

A payload-free LayerNorm step erases only its own fresh id, preventing stale future entries from changing the source fragment's unit-affine semantics.

theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_getNode_lt {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (g : ForwardLetChain α paramShapes inShape ss out) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) {i : ℕ} (hi : i < c.graph.nodes.size) : (lowerForwardLetChain g params c).graph.getNode i = c.graph.getNode i

lowerForwardLetChain does not change existing nodes at indices < c.graph.nodes.size. Lowering only appends nodes, so getNode agrees on the prefix.

theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_nodesSize_le {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (g : ForwardLetChain α paramShapes inShape ss out) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) : c.graph.nodes.size ≤ (lowerForwardLetChain g params c).graph.nodes.size

lowerForwardLetChain is monotone in graph.nodes.size (it only appends nodes).