Elementwise tensor operations (Spec.Tensor.*_spec)

This file defines shape-preserving, elementwise operations on Tensor α s.

Naming convention:

• foo_spec means “pure spec definition” (no runtime side effects).
• most functions are defined by recursion on the tensor structure via map_spec / map2_spec.

Domain / smoothness notes

Some ops are inherently domain-sensitive or non-smooth:

• sqrt_spec uses sqrt (max x 0) to stay total on ordered rings.
• log_spec is total as a function call, but analytic properties require positivity assumptions.
• relu / clamp / comparisons are non-smooth; analytic backprop theorems treat these via pointwise assumptions, or by switching to smooth surrogates in verification workflows.

The spec layer is where these semantics are defined; the proof layer decides which assumptions/variants to use for theorems.

def Spec.Tensor.mapSpec {α : Type} {s : Shape} (f : α → α) : Tensor α s → Tensor α s

Map a scalar function over a tensor (shape preserved).

This is the core "structural recursion" combinator for spec tensors. Most elementwise ops are direct instances of mapSpec f.

PyTorch analogy: f applied pointwise (like torch.<op> broadcasting over all entries), but here shape is fixed and enforced by the type.

def Spec.Tensor.map2Spec {α β γ : Type} (f : α → β → γ) {s : Shape} : Tensor α s → Tensor β s → Tensor γ s

Map a binary function over two tensors of the same shape.

This is the "zipWith" combinator for the spec tensor tree. It is intentionally shape-preserving: if the shapes differ, the term is not well-typed.

PyTorch analogy: elementwise binary ops when tensors already have the same shape (no broadcasting). Broadcasting is handled separately in NN/Spec/Core/TensorReductionShape.lean.

def Spec.Tensor.addSpec {α : Type} [Add α] {s : Shape} (T₁ T₂ : Tensor α s) : Tensor α s

Element‑wise addition (shape preserved).

@[implicit_reducible]

instance Spec.Tensor.instAdd {α : Type} [Add α] {s : Shape} : Add (Tensor α s)

Add instance for shape-indexed tensors: add pointwise, preserving the shape.

def Spec.Tensor.mulSpec {α : Type} [Mul α] {s : Shape} (T₁ T₂ : Tensor α s) : Tensor α s

Element‑wise multiplication (shape preserved).

@[implicit_reducible]

instance Spec.Tensor.instMul {α : Type} [Mul α] {s : Shape} : Mul (Tensor α s)

Mul instance for shape-indexed tensors: multiply pointwise, preserving the shape.

def Spec.Tensor.subSpec {α : Type} [Sub α] {s : Shape} : Tensor α s → Tensor α s → Tensor α s

Element‑wise subtraction (shape preserved).

@[implicit_reducible]

instance Spec.Tensor.instSub {α : Type} [Sub α] {s : Shape} : Sub (Tensor α s)

Sub instance for shape-indexed tensors: subtract pointwise, preserving the shape.

def Spec.Tensor.divSpec {α : Type} [Context α] {s : Shape} : Tensor α s → Tensor α s → Tensor α s

Element‑wise division (shape preserved).

@[implicit_reducible]

instance Spec.Tensor.instDiv {α : Type} [Context α] {s : Shape} : Div (Tensor α s)

Div instance for shape-indexed tensors: divide pointwise, preserving the shape.

def Spec.Tensor.safedivSpec {α : Type} [Context α] {s : Shape} (t1 t2 : Tensor α s) : Tensor α s

Safe division with epsilon protection (x / (y + ε)).

def Spec.Tensor.scaleSpec {α : Type} [Mul α] {s : Shape} (t : Tensor α s) (scalar : α) : Tensor α s

Scale a tensor by a scalar.

def Spec.Tensor.squareSpec {α : Type} [Context α] {s : Shape} (t : Tensor α s) : Tensor α s

Square each element of a tensor.

def Spec.Tensor.sqrtSpec {α : Type} [Context α] {s : Shape} (t : Tensor α s) : Tensor α s

Square root of each element (clamped to max x 0 to stay total).

def Spec.Tensor.absSpec {α : Type} [Context α] {s : Shape} (t : Tensor α s) : Tensor α s

Absolute value of each element.

def Spec.Tensor.logSpec {α : Type} [Context α] {s : Shape} (t : Tensor α s) : Tensor α s

Element‑wise natural log.

def Spec.Tensor.expSpec {α : Type} [Context α] {s : Shape} (t : Tensor α s) : Tensor α s

Element‑wise exponential.

def Spec.Tensor.negSpec {α : Type} [Context α] {s : Shape} (t : Tensor α s) : Tensor α s

Element‑wise negation.

@[implicit_reducible]

instance Spec.Tensor.instNeg {α : Type} [Context α] {s : Shape} : Neg (Tensor α s)

Neg instance for shape-indexed tensors: negate pointwise, preserving the shape.

def Spec.Tensor.mulConstantSpec {α : Type} [Context α] {s : Shape} (t : Tensor α s) (constant : α) : Tensor α s

Multiply tensor by a constant.

def Spec.Tensor.powSpec {α : Type} [Context α] {s : Shape} (t1 t2 : Tensor α s) : Tensor α s

Element‑wise power.

def Spec.Tensor.greaterThanSpec {α : Type} [Context α] {s : Shape} (x y : Tensor α s) : Tensor Bool s

Element‑wise comparisons (returning Bool tensors).

def Spec.Tensor.lessEqualSpec {α : Type} [Context α] {s : Shape} (x y : Tensor α s) : Tensor Bool s

Element‑wise ≤ test, implemented via ¬(>) so we only depend on DecidableRel (·>·).

def Spec.Tensor.lessThanSpec {α : Type} [Context α] {s : Shape} (x y : Tensor α s) : Tensor Bool s

Element‑wise < test (defined as y > x).

def Spec.Tensor.greaterEqualSpec {α : Type} [Context α] {s : Shape} (x y : Tensor α s) : Tensor Bool s

Element‑wise ≥ test (defined as ¬(y > x)).

def Spec.Tensor.notSpec {s : Shape} (x : Tensor Bool s) : Tensor Bool s

Boolean NOT, pointwise on a Bool tensor.

def Spec.Tensor.invSpec {α : Type} [Context α] {s : Shape} (x : Tensor α s) : Tensor α s

Element‑wise reciprocal (1/x).

def Spec.Tensor.clampSpec {α : Type} [Context α] {s : Shape} (x : Tensor α s) (min_val max_val : α) : Tensor α s

Element‑wise clamp into [min_val, max_val].

def Spec.Tensor.minSpec {α : Type} [Context α] {s : Shape} (t1 t2 : Tensor α s) : Tensor α s

Element‑wise minimum.

def Spec.Tensor.maxSpec {α : Type} [Context α] {s : Shape} (t1 t2 : Tensor α s) : Tensor α s

Element‑wise maximum.

def Spec.Tensor.signSpec {α : Type} [Context α] {s : Shape} (t : Tensor α s) : Tensor α s

Element‑wise sign function: returns -1, 0, or 1.

def Spec.Tensor.coshSpec {α : Type} [Context α] {s : Shape} : Tensor α s → Tensor α s

Element‑wise cosh.

def Spec.Tensor.sinhSpec {α : Type} [Context α] {s : Shape} : Tensor α s → Tensor α s

Element‑wise sinh.

def Spec.Tensor.clampDerivativeSpec {α : Type} [Context α] {s : Shape} (x : Tensor α s) (min_val max_val : α) : Tensor α s

Derivative mask for clamp: 1 strictly inside (min_val, max_val), else 0.

def Spec.Tensor.gtMaskSpec {α : Type} [Context α] {s : Shape} (a b : Tensor α s) : Tensor α s

Numeric mask: 1 where a > b, else 0.

def Spec.Tensor.ltMaskSpec {α : Type} [Context α] {s : Shape} (a b : Tensor α s) : Tensor α s

Numeric mask: 1 where a < b, else 0.

def Spec.Tensor.boolToAlphaSpec {α : Type} [One α] [Zero α] : Bool → α

Convert a Bool to α using 1/0.

def Spec.Tensor.mulBoolMaskSpec {α : Type} [Mul α] [One α] [Zero α] {s : Shape} (t : Tensor α s) (mask : Tensor Bool s) : Tensor α s

Multiply a tensor by a Bool mask (casts the mask to 0/1).

def Spec.Tensor.clampHuberMaskSpec {α : Type} [Context α] {s : Shape} (t : Tensor α s) (mask : Tensor Bool s) (delta : α) : Tensor α s

Apply a Huber-style clamp on entries selected by mask (leaves others unchanged).

def Spec.Tensor.updateTensorSpec {α : Type} {s : Shape} : Tensor α s → List ℕ → α → Tensor α s

Update a tensor at a (runtime) index path.

The index path is interpreted outermost-first. Out-of-bounds indices leave the tensor unchanged. This is an executable convenience helper; most proof-facing code prefers total, shape-indexed access.

def Spec.Tensor.updateTensorWithTensorSpec {α : Type} {s : Shape} : Tensor α s → List ℕ → Tensor α s → Tensor α s

Like update_tensor_spec, but replaces a subtree with another tensor.

def Spec.Tensor.updateSpec {α : Type} {n : ℕ} {s : Shape} : Tensor α (Shape.dim n s) → List ℕ → α → Tensor α (Shape.dim n s)

Specialization of update_tensor_spec for a top-level vector dimension.

def Spec.Tensor.sliceVectorSpec {α : Type} {n : ℕ} (v : Tensor α (Shape.dim n Shape.scalar)) (start len : ℕ) (h : start + len ≤ n := by decide) : Tensor α (Shape.dim len Shape.scalar)

Slice a vector [start, start+len) (with a proof that the slice stays in-bounds).