Numerical certificate policy guards

Every fixed-left range transfer (matrix product, whole and axis sums and means, average pooling, mean squared error, and LayerNorm) succeeds only after the reduction guard accepts the node, and the guard reads the numerical policy of a selected capsule. The lookup takes the first kernel with a matching node id. AcceptedGraphKernelPlan does not require ids to be distinct, so the reduction guard does not consult a later kernel with the same id. Each capsule still passes the accepted plan's policy and evidence gate. The statements establish the consumer's policy gate, not numerical correctness of a native implementation.

theorem Proofs.RuntimeApprox.NumericalCertificate.requireFixedLeftReduction_eq_ok_iff (plan : NN.Backend.AcceptedGraphKernelPlan) (node : NN.IR.Node) : requireFixedLeftReduction plan node = Except.ok () ↔ ∃ (policy : NN.Backend.NumericalPolicy), nodeNumericalPolicy plan node.id = some policy ∧ policy.reduction = NN.Backend.ReductionPolicy.fixedLeft

The reduction guard succeeds exactly when the selected node policy declares fixedLeft.

theorem Proofs.RuntimeApprox.NumericalCertificate.requireFixedLeftReduction_selected_capsule {plan : NN.Backend.AcceptedGraphKernelPlan} {node : NN.IR.Node} (hguard : requireFixedLeftReduction plan node = Except.ok ()) : ∃ (kernel : NN.Backend.IR.PlannedNodeKernel), Array.find? (fun (kernel : NN.Backend.IR.PlannedNodeKernel) => kernel.nodeId == node.id) plan.graphPlan.kernels = some kernel ∧ kernel.nodeId = node.id ∧ kernel.capsule.numericalPolicy.reduction = NN.Backend.ReductionPolicy.fixedLeft ∧ NN.Backend.PlannedKernel.acceptable plan.policy { op := kernel.op, capsule := kernel.capsule } = true

A successful reduction guard uses the actual first matching capsule, with its fixed-left declaration and its complete accepted-plan policy and evidence gate.

theorem Proofs.RuntimeApprox.NumericalCertificate.requireFixedLeftReduction_of_bind_ok {β : Type} {plan : NN.Backend.AcceptedGraphKernelPlan} {node : NN.IR.Node} {rest : Unit → Except String β} {result : β} (h : requireFixedLeftReduction plan node >>= rest = Except.ok result) : requireFixedLeftReduction plan node = Except.ok ()

A computation that starts with the fixed-left guard succeeds only if the guard succeeds.

theorem Proofs.RuntimeApprox.NumericalCertificate.matmulContract_derive_requires_fixedLeft {context : NumericalRangeContext} {node : NN.IR.Node} {result : RangeTransferResult} (hderive : matmulContract.derive context node = Except.ok result) : requireFixedLeftReduction context.plan node = Except.ok ()

A successful matrix-product range transfer must have passed the fixed-left policy guard.

theorem Proofs.RuntimeApprox.NumericalCertificate.sumContract_derive_requires_fixedLeft {context : NumericalRangeContext} {node : NN.IR.Node} {result : RangeTransferResult} (hderive : sumContract.derive context node = Except.ok result) : requireFixedLeftReduction context.plan node = Except.ok ()

A successful whole-tensor sum transfer must have passed the fixed-left policy guard.

theorem Proofs.RuntimeApprox.NumericalCertificate.mseContract_derive_requires_fixedLeft {context : NumericalRangeContext} {node : NN.IR.Node} {result : RangeTransferResult} (hderive : mseContract.derive context node = Except.ok result) : requireFixedLeftReduction context.plan node = Except.ok ()

A successful mean-squared-error transfer must have passed the fixed-left policy guard.

theorem Proofs.RuntimeApprox.NumericalCertificate.averagePoolContract_derive_requires_fixedLeft (padded : Bool) {context : NumericalRangeContext} {node : NN.IR.Node} {result : RangeTransferResult} (hderive : (averagePoolContract padded).derive context node = Except.ok result) : requireFixedLeftReduction context.plan node = Except.ok ()

A successful average-pooling transfer must have passed the fixed-left policy guard.

theorem Proofs.RuntimeApprox.NumericalCertificate.axisReductionContract_derive_requires_fixedLeft (mean : Bool) {context : NumericalRangeContext} {node : NN.IR.Node} {result : RangeTransferResult} (hderive : (axisReductionContract mean).derive context node = Except.ok result) : requireFixedLeftReduction context.plan node = Except.ok ()

A successful axis sum or mean transfer must have passed the fixed-left policy guard.

theorem Proofs.RuntimeApprox.NumericalCertificate.layerNormContract_derive_requires_fixedLeft {context : NumericalRangeContext} {node : NN.IR.Node} {result : RangeTransferResult} (hderive : layerNormContract.derive context node = Except.ok result) : requireFixedLeftReduction context.plan node = Except.ok ()

A successful LayerNorm transfer must have passed the fixed-left policy guard.

theorem Proofs.RuntimeApprox.NumericalCertificate.matmulContract_derive_selected_capsule {context : NumericalRangeContext} {node : NN.IR.Node} {result : RangeTransferResult} (hderive : matmulContract.derive context node = Except.ok result) : ∃ (kernel : NN.Backend.IR.PlannedNodeKernel), Array.find? (fun (kernel : NN.Backend.IR.PlannedNodeKernel) => kernel.nodeId == node.id) context.plan.graphPlan.kernels = some kernel ∧ kernel.nodeId = node.id ∧ kernel.capsule.numericalPolicy.reduction = NN.Backend.ReductionPolicy.fixedLeft ∧ NN.Backend.PlannedKernel.acceptable context.plan.policy { op := kernel.op, capsule := kernel.capsule } = true

The matrix-product range consumer inherits the selected capsule's accepted fixed-left policy.