For a positive integer \(d\), a real vector of length \(d\) is represented as a function \(\{ 1,\ldots ,d\} \to \mathbb {R}\), and an \(n\times d\) real matrix is represented as a function \(\{ 1,\ldots ,n\} \times \{ 1,\ldots ,d\} \to \mathbb {R}\). The notation \(v[i]\), \(A_{i,:}\), and \(A_{:,j}\) denotes coordinate projection, row projection, and column projection.

For \(v,w\in \mathbb {R}^d\), \(\left\langle v,w\right\rangle =\sum _i v[i]w[i]\) and \(\| v\| =(\left\langle v,v\right\rangle )^{1/2}\).

A binary vector is an element of \(\{ 0,1\} ^d\). The all-one vector is \(\mathbf{1}_d\). If \(v\in \{ 0,1\} ^d\), then \(\bar v\in \{ 0,1\} ^d\) is defined by \(\bar v[i]=1-v[i]\) for every coordinate \(i\).

For \(v\in \mathbb {R}^a\) and \(w\in \mathbb {R}^b\), the Kronecker product \(v\otimes w\in \mathbb {R}^{ab}\) has coordinates indexed by pairs and satisfies \((v\otimes w)[i,j]=v[i]w[j]\).

For a vector \(v\in \mathbb {R}^d\) and a positive integer \(q\), the \(q\)-fold Kronecker power \(v^{\otimes q}\in \mathbb {R}^{d^q}\) is the vector whose coordinates are indexed by functions \(\alpha :\{ 1,\ldots ,q\} \to \{ 1,\ldots ,d\} \) and whose coordinate value is the concrete product

Equivalently, \(v^{\otimes 1}=v\) under the one-coordinate identification and \(v^{\otimes (q+1)}=v\otimes v^{\otimes q}\) with the coordinate equation of Definition 6. This node defines only the power construction and its coordinate product relation.

For \(v\in \mathbb {R}^a\) and \(w\in \mathbb {R}^b\), the concatenation \(v\circ w\in \mathbb {R}^{a+b}\) is the vector with coordinates

This node defines only concatenation; Kronecker products and Kronecker powers are Definition 6 and Definition 7.

For \(x\in \mathbb {R}^n\),

For \(A\in \mathbb {R}^{n\times n}\), \(\operatorname {softmax}(A)\) is defined row-wise by \(\operatorname {softmax}(A)_{i,:}=\operatorname {softmax}(A_{i,:})\).

A document-similarity instance fixes a type \({\cal D}\) of documents, a type \({\cal K}\) of keywords, and a concrete occurrence predicate

for \(D\in {\cal D}\) and \(k\in {\cal K}\), meaning that keyword \(k\) occurs in document \(D\). The predicate is part of the input model as decidable data: for every pair \((D,k)\) there is a yes/no occurrence decision whose true branch is exactly \(\operatorname {Occurs}(D,k)\) and whose false branch is exactly \(\neg \operatorname {Occurs}(D,k)\).

This occurrence datum contains no length parameter and no built-in keyword list. The Lean-facing structure \(\operatorname {def\_ document\_ keyword\_ occurrence}\) has exactly the following four fields and field names:

and

Thus the tuple is \(({\cal D},{\cal K},\operatorname {Occurs},\operatorname {occurs\_ decidable})\) with the displayed names. The keyword vector used for a particular bag-of-words embedding is supplied separately in Definition 14; it is not a field of this occurrence structure.

For an occurrence datum \(\mathsf{doc}:\operatorname {def\_ document\_ keyword\_ occurrence}\) and a chosen bag-of-words length \(\ell \), a keyword list is the concrete coordinate-indexed function

Formally,

This definition has exactly the displayed inputs \((\mathsf{doc},\ell )\) and returns a type of keyword-vector parameters. It does not construct a default keyword vector, erase the occurrence datum, use an ambient keyword family, or store the vector in \(\mathsf{doc}\). The \(r\)th coordinate of a document embedding refers to the concrete keyword \(K(r)\). Two instances with the same documents and occurrence predicate but different functions \(K\) are different bag-of-words inputs and may produce different embedding matrices.

For an occurrence datum \(\mathsf{doc}:\operatorname {def\_ document\_ keyword\_ occurrence}\), a document \(D:\mathsf{doc}.\mathrm{Document}\), and a keyword \(k:\mathsf{doc}.\mathrm{Keyword}\), define the real-valued occurrence indicator

Lean-facing, this is the function

where the branch is selected by the concrete \(\mathsf{doc}.\mathrm{occurs\_ decidable}(D,k)\) field. No other document encoding or keyword semantics are implicit in this value.

For an occurrence datum \(\mathsf{doc}:\operatorname {def\_ document\_ keyword\_ occurrence}\) and a length \(\ell \), the Lean-facing bag-of-words embedding is the function

defined by the coordinate equation

We write this output as \(\mathrm{BOW}_{\mathsf{doc}}(D,K):\{ 1,\ldots ,\ell \} \to \mathbb {R}\). The keyword vector \(K\) is an explicit argument of this definition, not a field of the occurrence datum, and the codomain is the real vector space \(\mathbb {R}^\ell \) used by the paper rather than a Boolean-valued coordinate type.

For an occurrence datum \(\mathsf{doc}\), a document \(D:\mathsf{doc}.\mathrm{Document}\), a coordinate-indexed keyword vector \(K:\{ 1,\ldots ,\ell \} \to \mathsf{doc}.\mathrm{Keyword}\), and a row vector \(e\in \mathbb {R}^\ell \), the predicate

holds exactly when \(e\) is the concrete bag-of-words embedding of \(D\) with respect to \(K\):

This predicate has exactly the displayed inputs \((\mathsf{doc},D,K,e)\). It has no matrix index, no occurrence-value expansion, no nonzero-row promise, and no access to an ambient keyword vector stored in the occurrence datum.

For a matrix \(E\in \mathbb {R}^{n\times \ell }\) and an index \(i\in \{ 1,\ldots ,n\} \), the row vector

is defined coordinatewise by

This is only the concrete row-projection function from a finite matrix to a finite vector.

For an occurrence datum \(\mathsf{doc}\), a document family \(D:\{ 1,\ldots ,n\} \to \mathsf{doc}.\mathrm{Document}\), a coordinate-indexed keyword vector \(K:\{ 1,\ldots ,\ell \} \to \mathsf{doc}.\mathrm{Keyword}\), and a matrix \(E\in \mathbb {R}^{n\times \ell }\), define

to be the concrete matrix-entry relation

Lean-facing, the document input is the single finite-indexed function \(D\), not a variadic tuple of fields. The predicate has exactly the displayed inputs \((\mathsf{doc},D,K,E)\), with \(K\) explicit. It contains no nonzero-row hypothesis and no occurrence-value expansion; those are separate consequences proved below. Thus a valid document-similarity input is a real matrix whose entries are precisely the bag-of-words coordinates for the displayed document family and keyword vector. Consequently, any later proof needing an entry equality specializes this definition directly at the relevant row and coordinate; Lemma 26 records that specialization as a separate one-line formal interface. There is no alternate rowwise validity predicate.

For an occurrence datum \(\mathsf{doc}\), a document family \(D:\{ 1,\ldots ,n\} \to \mathsf{doc}.\mathrm{Document}\), keyword vector \(K:\{ 1,\ldots ,\ell \} \to \mathsf{doc}.\mathrm{Keyword}\), and matrix \(E\in \mathbb {R}^{n\times \ell }\), the separate predicate

means that every document embedding row used in a cosine-similarity instance is nonzero:

and no other condition. The matrix argument \(E\) is present only so that \(\operatorname {NonzeroRows}_{\mathsf{doc}}(D,K,E)\) has the same displayed instance parameters as \(\operatorname {ValidBOW}_{\mathsf{doc}}(D,K,E)\); the predicate itself does not inspect entries of \(E\) and does not require a proof of \(\operatorname {ValidBOW}\). This is the standing promise for MSD and LSD instances, but it is not an argument of \(\operatorname {ValidBOW}_{\mathsf{doc}}\).

For nonzero document embeddings \(v,w\in \mathbb {R}^d\), their cosine similarity is

For \(d_{\rm in},d_{\rm out},m\in \mathbb {N}\), matrices \(Q,K\in \mathbb {R}^{d_{\rm in}\times m}\) and \(V\in \mathbb {R}^{d_{\rm in}\times d_{\rm out}}\) define an attention map \(A_{Q,K,V}:\mathbb {R}^{n\times d_{\rm in}}\to \mathbb {R}^{n\times d_{\rm out}}\) by

The family \(\mathcal A_{d_{\rm in},m,d_{\rm out}}\) consists of all maps \(A_{Q,K,V}\) with \(Q,K\in \mathbb {R}^{d_{\rm in}\times m}\) and \(V\in \mathbb {R}^{d_{\rm in}\times d_{\rm out}}\).

For positive integers \(a\) and \(b\), an \((a,b)\) multi-layer perceptron is a continuous function

equivalently a continuous map \(\mathbb {R}^a\to \mathbb {R}^b\) on the corresponding finite-dimensional real vector spaces. For every number of rows \(n\), its row-wise matrix lift is the map

defined by the coordinate equality

Thus the lifted output has entries \((\varphi ^{[n]}(X))[i,j]=\varphi (X_{i,:})[j]\).

Fix positive integers \(n,d,d_{\rm in},d_{\rm out},m\). A transformer in the paper’s simplified single-attention-unit model is the following concrete data: an input MLP \(\varphi _1:\mathbb {R}^d\to \mathbb {R}^{d_{\rm in}}\), matrices \(Q,K\in \mathbb {R}^{d_{\rm in}\times m}\) and \(V\in \mathbb {R}^{d_{\rm in}\times d_{\rm out}}\), and an output MLP

where an \(n\times d_{\rm out}\) matrix is identified with its flattened vector in \(\mathbb {R}^{n d_{\rm out}}\). Its value on a matrix input \(E\in \mathbb {R}^{n\times d}\) is

Equivalently, the computation first applies \(\varphi _1\) row-wise, producing a matrix in \(\mathbb {R}^{n\times d_{\rm in}}\); then applies the attention map \(A_{Q,K,V}\) from Definition 35, producing a matrix in \(\mathbb {R}^{n\times d_{\rm out}}\); then applies the continuous output MLP to the flattened finite-dimensional matrix.

For document-similarity tasks the transformer input dimension is exactly the bag-of-words length. Concretely, the parameters satisfy \(d=\ell \), the document data consist of an occurrence datum \(\mathsf{doc}\), a document family \(D:\{ 1,\ldots ,n\} \to \mathsf{doc}.\mathrm{Document}\), and a coordinate-indexed keyword vector \(K:\{ 1,\ldots ,\ell \} \to \mathsf{doc}.\mathrm{Keyword}\). The Lean-facing contract is the single predicate

defined by exactly the bag-of-words validity condition

It has precisely the displayed data arguments \((\mathsf{doc},D,K,E)\), with \(n\) and \(\ell \) supplied by the finite index types. Its only input hypothesis is \(\operatorname {ValidBOW}_{\mathsf{doc}}(D,K,E)\); it has no conjunct, premise, field, or hidden promise asserting that rows are nonzero. In particular, the general transformer input contract must still hold for valid bag-of-words matrices with zero rows, because those are legitimate transformer inputs even though cosine similarity may be undefined for them.

From this contract and Lemma 26, every entry \(E[i,r]\) is the corresponding bag-of-words coordinate, and by Lemma 28 it is the real-valued occurrence indicator \(\operatorname {OccVal}_{\mathsf{doc}}(D(i),K(r))\). By Lemma 29, present keywords give entry value \(1\); by Lemma 30, absent keywords give entry value \(0\). Lemma 31 records the complete decidable case split for each entry. The scalar answer to the document-similarity instance is the pure transformer value \({\rm TF}(E)\) from Definition 38 evaluated on this concretely determined bag-of-words matrix. Thus the model never evaluates a document-similarity task on an unconstrained abstract row encoding, and the matrix column type of the transformer is the same finite coordinate type as the keyword list.

For a base matrix \(E\in \mathbb {R}^{n\times d}\) and a concrete sentinel row \(s\in \mathbb {R}^d\), the sentinel augmentation data is the concrete finite object

with the following four components.

First, \(\operatorname {Aug}_s(E)\) is the matrix

defined by the row equalities

Second, the problem-row predicate on augmented row indices is

Thus row \(n+1\) is definitionally not a problem row.

Third, the admissible witness-pair predicate on augmented row indices is

Consequently no pair containing the sentinel index \(n+1\) is admissible. Explicitly, for every augmented index \(r\),

Every underlying document, OV, Max-IP, Min-IP, MSD, or LSD witness predicate is evaluated only on pairs satisfying this displayed predicate, so it ranges over exactly the original first \(n\) rows. In predicate form, for every base pair relation \(W_E\) on indices of \(E\),

and

Fourth, for any base matrix decision predicates \(\Valid ,\Yes ,\No :\mathbb {R}^{n\times d}\to \operatorname {Prop}\), the lifted predicates attached to this augmentation are not new predicates on arbitrary \((n+1)\times d\) matrices. They are the three concrete precompositions

Hence appending the sentinel preserves the original size-\(n\) yes/no condition by definition: the augmented encoding is valid, yes, or no exactly when the base matrix \(E\) is valid, yes, or no. The sentinel row is only a fixed computational token supplied to the transformer construction; it is never part of the mathematical problem instance.

A sentinel-augmented transformer for a matrix decision problem with base input shape \(n\times d\) consists of a fixed sentinel row \(s\in \mathbb {R}^d\) and a single-attention-unit transformer whose sequence length parameter is \(n+1\). It solves predicates \(\Valid (E)\), \(\Yes (E)\), and \(\No (E)\) on base matrices \(E\in \mathbb {R}^{n\times d}\) when both concrete correctness implications hold after augmentation:

Thus appending the sentinel is part of the fixed input encoding of the constructed transformer, while the mathematical decision problem remains the original problem on the first \(n\) rows.

A matrix decision problem with input shape \(n\times d\) consists of predicates \(\Valid (E)\), \(\Yes (E)\), and \(\No (E)\) on matrices \(E\in \mathbb {R}^{n\times d}\) such that every valid instance is classified exactly once:

A transformer \({\rm TF}:\mathbb {R}^{n\times d}\to \mathbb {R}\) solves this decision problem if both correctness implications hold for every matrix input:

The no-instance implication is an independent requirement; it is not conditional on the existence of a yes-instance witness.