NF Shape Operators

Approximation lemmas for filling, replication, broadcasting, and Boolean masking in the rounded-real NF model. Copied entries retain their error budgets; masked entries are exactly zero. None of these operations introduces arithmetic rounding.

PyTorch correspondence / citations

Related PyTorch shape operations: https://pytorch.org/docs/stable/generated/torch.reshape.html https://pytorch.org/docs/stable/generated/torch.Tensor.view.html https://pytorch.org/docs/stable/generated/torch.permute.html

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_full_const {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {cS : ℝ} {cR : FloatLib.Floats.Formats.Flocq.NF β fexp rnd} {eps : ℝ} (h : |toSpec cR - cS| ≤ eps) {s : Spec.Shape} : approxTensor toSpec (TorchLean.Tensor.full s cS) (TorchLean.Tensor.full s cR) eps

Filling a tensor preserves a scalar approximation budget at every shape.

Although this fact is used heavily when constructing reverse-mode zero contexts, it is a shape fact rather than a backward-mode fact. Keeping it here also makes rounded constants available to normalization, attention, and quantization without importing the reverse-mode implementation.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_full_one {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} : approxTensor toSpec (TorchLean.Tensor.full s 1) (TorchLean.Tensor.full s 1) (FloatLib.Floats.Formats.Flocq.ulp β fexp 1 / 2)

A tensor filled with runtime one differs from exact one by at most one construction rounding.

(1 : R) is NF.ofReal 1, so the scalar bound is the generic approx_ofReal_nf.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_full_zero {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} : approxTensor toSpec (TorchLean.Tensor.full s 0) (TorchLean.Tensor.full s 0) 0

Zero is exactly representable in every valid neural floating-point format.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_replicate {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {s : Spec.Shape} {xS : Spec.SpecTensor Spec.Shape.scalar} {xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) Spec.Shape.scalar} {eps : ℝ} (hx : approxTensor toSpec xS xR eps) : approxTensor toSpec (Spec.replicate xS) (Spec.replicate xR) eps

Filling a tensor with one approximate scalar gives an approximation with the same tolerance.

Broadcasting a constant copies a value rather than computing with it, so no new rounding occurs and the error stays put. That is why eps appears unchanged on both sides.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_broadcastTo {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {s₁ s₂ : Spec.Shape} (cb : s₁.CanBroadcastTo s₂) {xS : Spec.SpecTensor s₁} {xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s₁} {eps : ℝ} (hx : approxTensor toSpec xS xR eps) : approxTensor toSpec (TorchLean.Tensor.broadcastTo cb xS) (TorchLean.Tensor.broadcastTo cb xR) eps

Broadcasting preserves the approximation tolerance: each output entry copies an input.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_applyBoolMask {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} {xS : Spec.SpecTensor s} {xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} (mask : TorchLean.Tensor Bool s) {eps : ℝ} (hx : approxTensor toSpec xS xR eps) : approxTensor toSpec (TorchLean.Tensor.map2Spec (fun (x : Spec.SpecScalar) (allowed : Bool) => if allowed = true then x else 0) xS mask) (TorchLean.Tensor.map2Spec (fun (x : FloatLib.Floats.Formats.Flocq.NF β fexp rnd) (allowed : Bool) => if allowed = true then x else 0) xR mask) eps

Applying the same Boolean mask to exact and rounded tensors preserves the error budget.

Masking is a selection operation, not arithmetic: allowed entries are unchanged and blocked entries are exactly zero in both semantics. In particular, this theorem does not model a finite negative sentinel and introduces no extra ULP term.