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))) : Option (Tensor α (Shape.dim n (Shape.dim n Shape.scalar)))

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

The result is none when the determinant is zero. Returning an unrelated matrix for a singular input would make downstream statistical formulas appear defined when they are not.

PyTorch analogue: torch.linalg.inv, with failure represented explicitly by Option.

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

Approximate the leading eigenpair by 20 steps of power iteration.

The scalar is the final Rayleigh quotient and the tensor is the corresponding normalized iterate. This definition does not claim to compute a full eigendecomposition. Convergence to a dominant eigenvector requires the usual spectral assumptions on matrix and a suitable initial vector.

@[irreducible]

def Spec.leadingEigenpairPowerIterationApproxSpec.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.