NF Tensor Approximation Plumbing #
Shape-generic lemmas for approxTensor and linfNorm. The later NF proof files use these lemmas
to turn scalar absolute-error facts into tensor-level forward-error bounds.
Tensor Approximation Plumbing #
Enlarge an existing tensor approximation budget.
Composed operators often prove a row- or coordinate-level estimate and then embed it into a global infinity-norm budget. This lemma records that monotonicity once, without unfolding the tensor distance predicate at every use site.
linfNorm is always nonnegative.
Componentwise bound for linfNorm on a dimensioned tensor.
The norm of any component t[i] is bounded by the norm of the whole tensor.
Scalar characterization of approxTensor on scalar tensors.
This rewrites approxTensor (Tensor.scalar x) (Tensor.scalar xR) eps into the usual absolute-error
inequality |toSpec xR - x| ≤ eps.
Scalar characterization of approxTensor stated for arbitrary rank-zero tensors.
Projection lemma for approxTensor on dimensioned tensors.
If xS approximates xR within eps, then each component xS[i] approximates xR[i] within
eps.
Every valid tensor approximation has a nonnegative error budget.
This fact is independent of the executable scalar type. Keeping it at the plumbing layer avoids repeating the same norm argument in each backend-specific development.
Assemble a dimensioned tensor approximation from uniform componentwise approximations.
The premise uses one common infinity-norm budget for every component. This is the converse of
approxTensor_dim_get and is deliberately polymorphic in the runtime element representation, so NF,
IEEE execution, interval, and future quantized backends can share the same structural proof.
Lift a scalar approximation bound to an elementwise mapSpec.
Given a scalar bound of the form
|toSpec (fR xR) - fS x| ≤ bnd (toSpec xR) eps
and an input approximation approxTensor xS xR eps, this produces an approximation bound for
map_spec fS xS vs map_spec fR xR, with an output epsilon computed by taking the linfNorm of
the pointwise bound.
Lift a domain-restricted scalar approximation bound to an elementwise mapSpec.
The predicate is carried by Tensor.Forall, so callers can certify operations such as square root
once at the scalar level without rebuilding an elementwise tensor proof for every operation.
Lift a scalar approximation bound that depends on the original runtime scalar.
This variant is useful when the certified budget observes representation-specific runtime
intermediates that cannot be reconstructed from toSpec xR.
Lift a scalar approximation bound to an elementwise map2Spec.
This is the binary analogue of approxTensor_map_spec_of_scalar_bound, used for elementwise
arithmetic (add, sub, mulElem, etc.).