One computable family of periodic dissociated-cluster tensors

The paired-cluster construction uses a size-dependent order chosen by bounded search. Admissibility simultaneously bounds coefficient bit length and the finite rank error. The definition is independent of any requested approximation to the leading coefficient. This is a computable formula, not a machine-level polynomial-time certificate.

def Algebraic.Tensor3.Dissociated.selectionSize (p : ℕ) : ℕ

Enough indices for a dissociated cluster of size 2p+1.

Equations

• Algebraic.Tensor3.Dissociated.selectionSize p = 3 ^ (2 * p) + 1

def Algebraic.Tensor3.Dissociated.blockLength (p : ℕ) : ℕ

The block length makes the relative survivor loss exactly 1/(p+1).

Equations

• Algebraic.Tensor3.Dissociated.blockLength p = (p + 1) * Algebraic.Tensor3.Dissociated.selectionSize p

def Algebraic.Tensor3.Dissociated.rowPeriod (p : ℕ) : ℕ

Slice-label period.

Equations

• Algebraic.Tensor3.Dissociated.rowPeriod p = Algebraic.Tensor3.Dissociated.blockLength p + 1

def Algebraic.Tensor3.Dissociated.columnPeriod (p : ℕ) : ℕ

Column-label period.

Equations

• Algebraic.Tensor3.Dissociated.columnPeriod p = p * Algebraic.Tensor3.Dissociated.blockLength p + 1

def Algebraic.Tensor3.Dissociated.Admissible (k p : ℕ) : Prop

The finite checks needed for the rank estimate and linear coefficient bit bound.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Algebraic.Tensor3.Dissociated.instDecidableAdmissible (k p : ℕ) : Decidable (Admissible k p)

Equations

• Algebraic.Tensor3.Dissociated.instDecidableAdmissible k p = id inferInstance

def Algebraic.Tensor3.Dissociated.candidates (k : ℕ) : Finset ℕ

The finite search considers at most logarithmically many orders.

Equations

• Algebraic.Tensor3.Dissociated.candidates k = Finset.filter (Algebraic.Tensor3.Dissociated.Admissible k) (Finset.range (Nat.log 2 (2 * k + 1) + 1))

def Algebraic.Tensor3.Dissociated.order (k : ℕ) : ℕ

The largest admissible order, or zero before the first admissible order appears.

Equations

• Algebraic.Tensor3.Dissociated.order k = (Algebraic.Tensor3.Dissociated.candidates k).sup id

def Algebraic.Tensor3.Dissociated.oddEntry (k a j l : ℕ) : ℕ

Integer coordinates of the odd-dimensional tensor, with zero below the onset.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Tensor3.Dissociated.oddTensor (k : ℕ) : Tensor3 (Fin (2 * k + 1)) (Fin (2 * k + 1)) (Fin (2 * k + 1))

The odd-dimensional complex tensor has the specified integer coordinates.

Equations

• Algebraic.Tensor3.Dissociated.oddTensor k a j l = ↑(Algebraic.Tensor3.Dissociated.oddEntry k ↑a ↑j ↑l)

def Algebraic.Tensor3.Dissociated.coreIndex (m : ℕ) : ℕ

The odd-dimensional core used at an arbitrary ambient dimension.

Equations

• Algebraic.Tensor3.Dissociated.coreIndex m = (m - 1) / 2

def Algebraic.Tensor3.Dissociated.entry (m a j l : ℕ) : ℕ

Integer entries in every dimension, padding the odd core by zeros.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Tensor3.Dissociated.tensor (m : ℕ) : Tensor3 (Fin m) (Fin m) (Fin m)

A single tensor family indexed by its full ambient dimension.

Equations

• Algebraic.Tensor3.Dissociated.tensor m a j l = ↑(Algebraic.Tensor3.Dissociated.entry m ↑a ↑j ↑l)