Common helpers (spec models)

This file centralizes small utilities used across multiple spec‑level models:

• simple matrix operations (minor, determinant, inverse),
• distance functions for KNN,
• normalization helpers,
• and other "model glue" functions.

Intent / tradeoffs

These definitions prioritize:

• mathematical clarity, and
• shape safety (via Spec.Tensor), over performance.

In particular, determinant_spec uses Laplace expansion, which is exponentially expensive and is only meant for small matrices (e.g. 2×2, 3×3) and/or proof‑oriented reference code. If you need large‑scale linear algebra, use the runtime layer with array‑backed kernels.

theorem Spec.actual_index_lt {n : ℕ} (skip : ℕ) (i : Fin (n - 1)) : (if ↑i < skip then ↑i else ↑i + 1) < n

Helper lemma for minor/index computations.

When forming a matrix minor, we "skip" a row/column and map an index i : Fin (n-1) to the corresponding original index in Fin n by either leaving it unchanged (if it is before the skipped index) or shifting it by +1 (if it is at/after the skipped index). This lemma proves the resulting index is still < n.

def Spec.getMinorSpec {α : Type} {n : ℕ} (matrix : Tensor α (Shape.dim n (Shape.dim n Shape.scalar))) (row col : ℕ) : Tensor α (Shape.dim (n - 1) (Shape.dim (n - 1) Shape.scalar))

Matrix minor: delete row and col from an n × n matrix, producing an (n-1) × (n-1) matrix.

This is used by determinant_spec (Laplace expansion) and the adjugate-based inverse below.

def Spec.determinantSpec {α : Type} [Context α] {n : ℕ} : Tensor α (Shape.dim n (Shape.dim n Shape.scalar)) → Tensor α Shape.scalar

Determinant of an n × n matrix (spec-level reference implementation).

This uses Laplace expansion (cofactor expansion) along the first row, with special-cased base cases for n = 0, 1, 2. It is mathematically clear but exponentially slow, so it is intended only for very small n and/or proof-oriented reference code.

def Spec.inverseSpec {α : Type} [Context α] {n : ℕ} (matrix : Tensor α (Shape.dim n (Shape.dim n Shape.scalar))) : Tensor α (Shape.dim n (Shape.dim n Shape.scalar))

Matrix inverse via the adjugate formula (spec-level reference implementation).

If det(A) == 0, this returns the identity matrix as a "safe default" for singular matrices. Otherwise it computes adj(A) / det(A) using cofactors and a transpose.

PyTorch analogue: torch.linalg.inv (but note the singular-case behavior differs).

def Spec.eigendecompSpec {α : Type} [Context α] {n : ℕ} (matrix : Tensor α (Shape.dim n (Shape.dim n Shape.scalar))) : Tensor α (Shape.dim n Shape.scalar) × Tensor α (Shape.dim n (Shape.dim n Shape.scalar))

Reference eigendecomposition via power iteration (largest eigenpair only).

This returns a pair (eigenvalues, eigenvectors) where only the first eigenvalue/eigenvector slot is populated (the rest are zeros). It is intended as simple, proof-friendly reference code rather than a full-featured numerical linear algebra routine.

@[irreducible]

def Spec.eigendecompSpec.power_iteration {α : Type} [Context α] {n : ℕ} (matrix : Tensor α (Shape.dim n (Shape.dim n Shape.scalar))) (v : Tensor α (Shape.dim n Shape.scalar)) (iter : ℕ) : Tensor α (Shape.dim n Shape.scalar) × α

def Spec.euclideanDistanceSpec {α : Type} [Context α] {nFeatures : ℕ} (x y : Tensor α (Shape.dim nFeatures Shape.scalar)) : α

Euclidean (L2) distance between two feature vectors.

PyTorch analogue: torch.linalg.vector_norm(x - y) or torch.cdist (batched).

def Spec.squaredEuclideanDistanceSpec {α : Type} [Context α] {nFeatures : ℕ} (x y : Tensor α (Shape.dim nFeatures Shape.scalar)) : α

Squared Euclidean distance (avoids the final square root).

def Spec.manhattanDistanceSpec {α : Type} [Context α] {nFeatures : ℕ} (x y : Tensor α (Shape.dim nFeatures Shape.scalar)) : α

Manhattan (L1) distance between two feature vectors.

def Spec.cosineDistanceSpec {α : Type} [Context α] {nFeatures : ℕ} (x y : Tensor α (Shape.dim nFeatures Shape.scalar)) : α

Cosine distance 1 - cos(theta) between two feature vectors.

If either vector has zero norm, this returns 1.

def Spec.minkowskiDistanceSpec {α : Type} [Context α] {nFeatures : ℕ} (p : α) (x y : Tensor α (Shape.dim nFeatures Shape.scalar)) : α

Minkowski distance of order p between two feature vectors.

This generalizes L1 (Manhattan) and L2 (Euclidean). For p = 1 this is the L1 norm, and for p = 2 it is the L2 norm.

def Spec.normalizeProbsSpec {α : Type} [Context α] {n : ℕ} (probs : Tensor α (Shape.dim n Shape.scalar)) : Tensor α (Shape.dim n Shape.scalar)

Normalize a vector of (nonnegative) scores into a probability distribution.

If the total is 0, this returns the uniform distribution.

PyTorch analogue: probs / probs.sum() (with an explicit zero-sum guard).

def Spec.normalizeL2Spec {α : Type} [Context α] {n : ℕ} (vector : Tensor α (Shape.dim n Shape.scalar)) : Tensor α (Shape.dim n Shape.scalar)

L2-normalize a vector.

If the norm is 0, this returns the input unchanged.

def Spec.normalizeZscoreSpec {α : Type} [Context α] {n : ℕ} (vector : Tensor α (Shape.dim n Shape.scalar)) : Tensor α (Shape.dim n Shape.scalar)

Z-score normalization: subtract mean and divide by standard deviation.

If the standard deviation is 0, this returns the mean-centered vector.

def Spec.argsortDescendingSpec {α : Type} [Context α] {n : ℕ} (values : Tensor α (Shape.dim n Shape.scalar)) : Tensor ℕ (Shape.dim n Shape.scalar)

Argsort in descending order (returns indices as a Nat tensor).

PyTorch analogue: torch.argsort(values, descending=True).

def Spec.gatherSpec {α : Type} [Context α] {n : ℕ} (values : Tensor α (Shape.dim n Shape.scalar)) (indices : Tensor ℕ (Shape.dim n Shape.scalar)) : Tensor α (Shape.dim n Shape.scalar)

Gather elements from a 1-D tensor using a 1-D tensor of indices.

Out-of-bounds indices produce 0.

PyTorch analogue: values[indices] (with an explicit out-of-bounds guard).

def Spec.gatherColumnsSpec {α : Type} [Context α] {m n : ℕ} (matrix : Tensor α (Shape.dim m (Shape.dim n Shape.scalar))) (indices : Tensor ℕ (Shape.dim n Shape.scalar)) : Tensor α (Shape.dim m (Shape.dim n Shape.scalar))

Gather columns of an m × n matrix using a length-n index vector.

Out-of-bounds indices produce 0 entries.

def Spec.sliceColumnsSpec {α : Type} [Context α] {m n : ℕ} (matrix : Tensor α (Shape.dim m (Shape.dim n Shape.scalar))) (start end_p : ℕ) (h : end_p ≤ n) : Tensor α (Shape.dim m (Shape.dim (end_p - start) Shape.scalar))

Slice a contiguous block of columns from an m × n matrix.

The resulting matrix has end_p - start columns. Entries outside the [start, end_p) range are filled with 0 (this matches the "safe default" style used by other helpers in this file).

def Spec.sliceValuesSpec {α : Type} [Context α] {n : ℕ} (values : Tensor α (Shape.dim n Shape.scalar)) (start end_p : ℕ) (h : end_p ≤ n) : Tensor α (Shape.dim (end_p - start) Shape.scalar)

Slice a contiguous subvector from values, returning length end_p - start.

Entries outside the [start, end_p) range are filled with 0.

def Spec.orientComponentsSpec {α : Type} [Context α] {m n : ℕ} (components : Tensor α (Shape.dim m (Shape.dim n Shape.scalar))) (h : 0 < n) : Tensor α (Shape.dim m (Shape.dim n Shape.scalar))

Orient component vectors to have a deterministic sign.

Many decompositions (PCA, ICA, eigenvectors) are sign-ambiguous: both v and -v are valid. This helper flips each component so its first entry is nonnegative, making the result stable for display/comparison in small specs.