Dependencies

Assuming SETH or OVC, for every \(\varepsilon {\gt}0\) there exists \(c{\gt}0\) such that \(\mathrm{LSD}_{n,\ell }\) cannot be solved in \(O(n^{2-\varepsilon })\) time for \(\ell \geq c\log n\). The same lower bound holds for bichromatic \(\gamma \)-\(\mathrm{LSD}\) for all \(\gamma \geq 1\) and for \(\mathrm{LSD}_{n,\ell ,t}\) for some \(t\in [0,1]\).

Assuming SETH or OVC, for every \(\varepsilon {\gt}0\) there is a constant \(c{\gt}0\) such that \(\mathrm{MSD}_{n,\ell }\) cannot be solved in \(O(n^{2-\varepsilon })\) time when \(\ell \geq (\log n)^{c\log n/(\log \log n)^2}\). The same lower bound holds for bichromatic \(\gamma \)-\(\mathrm{MSD}\) in the same approximation range and for \(\mathrm{MSD}_{n,\ell ,t}\) for some \(t\in [0,1]\).

Given sets \(A,B\subseteq \{ 0,1\} ^{\ell }\) of size \(n\), an integer threshold \(\alpha \), and an additive gap \(g{\gt}0\), bichromatic \(g\)-Additive-\(\mathrm{Max\mbox{-}IP}\) distinguishes the following promised cases:

and

Given \(A,B\subseteq \{ 0,1\} ^{\ell }\), \(\alpha \in [0,1]\), and an additive gap \(\delta {\gt}0\), bichromatic \(\delta \)-Additive-MSD distinguishes yes instances, where some \((a,b)\in A\times B\) has cosine similarity at least \(\alpha \), from no instances, where every \((a,b)\) has cosine similarity less than \(\alpha -\delta \).

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 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.

The reduction datum \(R_{\rm bi\to mono}\) from bichromatic \(\mathrm{OV}\) to monochromatic \(\mathrm{OV}\) maps a bichromatic input \(A=\{ a_1,\ldots ,a_n\} \) and \(B=\{ b_1,\ldots ,b_n\} \) in \(\{ 0,1\} ^{\ell }\) to the single monochromatic instance in dimension \(\ell +2\) consisting of

It queries monochromatic \(\mathrm{OV}\) on the multiset \(A'\cup B'\) and returns exactly the oracle’s yes/no answer. The construction doubles the number of vectors, increases the dimension by \(2\), and has only linear local overhead in the input encoding size.

Bichromatic \(\mathrm{LSD}\) and its approximate and threshold variants are defined over pairs drawn from two input sets \(A,B\subseteq \{ 0,1\} ^{\ell }\).

Given \(A,B\subseteq \{ 0,1\} ^{\ell }\) of size \(n\), the bichromatic versions of \(\mathrm{Max\mbox{-}IP}\), \(\gamma \)-\(\mathrm{Max\mbox{-}IP}\), and \(\mathrm{Max\mbox{-}IP}_{n,\ell ,t}\) optimize, approximate, or decide over pairs in \(A\times B\).

A rectangular bichromatic Min-IP input consists of two nonempty finite indexed lists

Its principal size is \(N=\max \{ n_A,n_B\} \) and its auxiliary dimension is \(\ell \). The exact optimization version asks for a pair \((i,j)\in \{ 1,\ldots ,n_A\} \times \{ 1,\ldots ,n_B\} \) minimizing \(\left\langle A_i,B_j\right\rangle \). The \(\gamma \)-approximate version, for \(\gamma \geq 1\), asks for a pair \((i^*,j^*)\) satisfying

The threshold version with \(0\leq t\leq \ell \) asks for the Boolean answer

The equal-size paper notation is the special case \(n_A=n_B=n\). The divide-and-recurse reductions below use the rectangular formulation so that canonical balanced splits of an arbitrary input length can be queried without adding artificial vectors that might change the minimum.

Bichromatic \(\mathrm{MSD}\) and its approximate and threshold variants are defined over pairs drawn from two input sets \(A,B\subseteq \{ 0,1\} ^{\ell }\).

In bichromatic \(\mathrm{OV}_{n,\ell }\) one is given \(A=\{ a_1,\ldots ,a_n\} \) and \(B=\{ b_1,\ldots ,b_n\} \) in \(\{ 0,1\} ^{\ell }\) and asks whether some pair \((a_i,b_j)\) satisfies \(\left\langle a_i,b_j\right\rangle =0\).

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 a valid \(P\)-input \(x\), a trace \(t=(q_1,z_1),\ldots ,(q_{r(x)},z_{r(x)}),y\), and a candidate generated state sequence \(G:\{ 0,\ldots ,r(x)\} \to \operatorname {State}_R(x)\), the boundary-equation predicate is the conjunction of exactly the following two equalities:

and

Lean-facing, the declaration \(\operatorname {def\_ composed\_ oracle\_ boundary\_ equations}(x,t,G)\) is a proposition with these equalities as eliminable conjuncts. It cannot be proved by constructing an initialization phase record or a finish phase record unless the displayed equality tying that record to the supplied sequence \(G\) and output \(y\) is also proved.

For a valid \(P\)-input \(x\), a trace \(t=(q_1,z_1),\ldots ,(q_{r(x)},z_{r(x)}),y\), a candidate generated state sequence \(G:\{ 0,\ldots ,r(x)\} \to \operatorname {State}_R(x)\), and oracle first-halting-time data \(U:\{ 1,\ldots ,r(x)\} \to \mathbb {N}\), the per-call-equation predicate holds when the following three facts hold for every oracle-call position \(1\leq s\leq r(x)\):

and

The same preceding state \(G(s-1)\), prefix history \(H(x,t,s)\), query \(q_s\), and oracle answer \(z_s\) must appear in all three conjuncts. In particular, the update equation is not a local statement about an independently built update-phase configuration: it is an equality whose left-hand side is the supplied next state \(G(s)\) from the candidate state sequence.

For fixed data \((R,x,\sigma ,H)\) with \(\sigma \in \operatorname {State}_R(x)\) and \(H\) a full answer history, the finish phase in the composed program is the canonical countdown machine

Its initial configuration is \(\operatorname {FinishSteps}_R(x,\sigma ,H)\), its step map decrements a positive counter and fixes \(0\), its halt predicate is exactly \(k=0\), and its output at the halted configuration is exactly

Thus the final \(P\)-output of the composed program is produced by the displayed final-postprocessing function, not by a separate output parameter.

The halt predicate of the composed program is true exactly on halted finish countdown records:

and it is false on \(\operatorname {InitPhase}\), \(\operatorname {QueryPhase}\), \(\operatorname {OraclePhase}\), and \(\operatorname {UpdatePhase}\) records. The output relation at a halted finish record is

Thus the only possible returned \(P\)-output is the final-postprocessing value for the state and full history stored in the halted finish phase.

For a valid \(P\)-input \(x\), the composed program uses concrete prefix histories, independent of any completed trace selector. The empty history is the unique element

whose finite query-answer list has length \(0\).

For an oracle-call index \(1\leq s\leq r(x)\), a prefix history \(H_s\in \Hist _R(x,s-1)\) before call \(s\), a query \(q\in I_Q\), and an answer \(z\in O_Q(q)\), the append operation is the concrete finite-list append

Its first \(s-1\) query-answer entries are exactly the entries of \(H_s\) in the same order, and its \(s\)th entry is exactly \((q,z)\). Equivalently, for every position \(u{\lt}s\),

and

These equations are definitional branch data for the composed step map. The implementation must not replace the empty history or appended history by an existentially chosen history satisfying a later trace predicate.

The initial configuration of the composed program on a valid \(P\)-input \(x\) is the concrete phase record

This definition has no argument for a starting state, trace, answer history, or precomputed output. The initialization phase begins with the actual initial configuration of the initialization machine of \(R\).

The deterministic operational semantics used by the composed substitution \(R[A_Q]\) is a concrete semantics for the source problem \(P\), denoted

For each valid \(P\)-input \(x\), its configuration carrier, initial configuration, step map, halt predicate, and output relation are exactly

Lean-facing, this node is the declaration \(\operatorname {def\_ composed\_ oracle\_ operational\_ semantics}\) and returns a value of the existing deterministic-operational-semantics type for \(P\) from Definition 45. It is not a new structure packaging a semantics together with a program code, and it does not introduce any declaration named \(\operatorname {def\_ composed\_ oracle\_ program\_ code}\). The five displayed component equations are the complete semantics of the composed run.

For the same data \((x,t,G,U)\), an ordered phase trace is a finite sequence \(\Pi \) of concrete phase records from Definition 77, indexed by the ordered positions

It satisfies the following positional equations. Position \(0\) is an initialization phase whose halted output state is exactly \(G(0)\), and this same state satisfies the equality \(G(0)=\operatorname {init}_R(x)\). For every \(1\leq s\leq r(x)\), the three consecutive positions \(3s-2,3s-1,3s\) are respectively

and

where the query value, oracle answer, and next state obey the per-call equations of Definition 79. The final position \(3r(x)+1\) is

and its output is exactly the trace output \(y=\operatorname {finish}_R(x,G(r(x)),H(x,t,r(x)+1))\).

Thus \(\operatorname {def\_ composed\_ oracle\_ ordered\_ phase\_ trace}(x,t,G,U)\) is a proposition asserting the existence of this single ordered sequence \(\Pi \) together with the displayed positional equalities. It is not satisfied by a collection of phase records constructed independently of \(\Pi \), and it is not satisfied by records whose state arguments differ from the entries of \(G\). The ordered trace is the bridge between the syntactic phase records and the semantic equations in the trace certificate.

Fix a local-phase oracle reduction datum \(R\) from \(P\) to \(Q\) and a concrete deterministic \(Q\)-algorithm \(A_Q\). The configuration carrier of the composed program \(R[A_Q]\) on a valid input \(x\) is the disjoint union of the following concrete phase records, with no additional output-producing case:

and

Here \(c_{\rm init}\) is an initialization configuration of Definition 63. The configurations \(c_{\rm qry}\), \(c_{\rm upd}\), and \(c_{\rm fin}\) are respectively elements of the canonical countdown machines of Definitions 74, 75, and 76. The configuration \(c_Q\) is an actual operational configuration of \(A_Q\) on the displayed concrete query. The phase record stores the previous state and prefix history as separate arguments whenever they are needed; it does not store arbitrary oracle answers or an arbitrary final \(P\)-output.

For fixed \((P,Q,R,A_Q)\) and a valid \(P\)-input \(x\), define

to be exactly the disjoint union of phase records from Definition 77. The five constructors are

with the arguments and component configuration types specified in that definition. There is no sixth constructor, no externally supplied halted output constructor, and no constructor that packages a complete trace certificate.

The deterministic \(P\)-program code underlying the substitution \(R[A_Q]\) is the single concrete program code inside the operational semantics \(\mathsf{Sem}_{R,A_Q}\) of Definition 89. It is denoted

Expanding the code inside that semantics gives exactly the tuple

Lean-facing, this node is exactly the declaration \(\operatorname {def\_ composed\_ oracle\_ program\_ code}\), and it returns only this program-code value. It is not a structure, record, or proposition with fields such as \(\operatorname {Semantics}\), \(\operatorname {code}\), or a “concrete” compatibility proof. No later node may redeclare \(\operatorname {def\_ composed\_ oracle\_ program\_ code}\) as a type of program packages; later nodes must refer to the value defined here, or to the separate semantics value \(\operatorname {def\_ composed\_ oracle\_ operational\_ semantics}\). This declaration contains no correctness proof, no running-time proof, and no externally supplied trace or accounting predicate; those are separate lemmas about this constructed code.

For fixed data \((R,x,s,\sigma ,H_s)\) with \(\sigma \in \operatorname {State}_R(x)\) and \(H_s\) the prefix history before oracle call \(s\), the query phase in the composed program is the canonical countdown machine

Its initial configuration is \(\operatorname {QuerySteps}_R(x,s,\sigma ,H_s)\), its step map sends a positive counter \(k+1\) to \(k\) and fixes \(0\), its halt predicate is exactly \(k=0\), and its output at the halted configuration is exactly

Thus the query phase has no externally supplied query output: the only query it can emit is the state-dependent query constructor from Definition 65, after exactly the displayed number of local countdown steps.

Let \(R\) be a correct oracle reduction datum from \(P\) to \(Q\) with a local-phase presentation, and let \(A_Q\) be a concrete correct deterministic algorithm for \(Q\) with running-time bound \(T_Q\). The composed algorithm

is definitionally the deterministic \(P\)-program code of Definition 90. Lean-facing, the declaration

has exactly the displayed construction arguments and returns the program-code value \(\operatorname {def\_ composed\_ oracle\_ program\_ code}\) inside the semantics value \(\operatorname {def\_ composed\_ oracle\_ operational\_ semantics}\). The configuration carrier, initial configuration, step map, halt predicate, and output relation are respectively the five component equations named in Definitions 89 and 90. Consequently the construction has no parameter for an alternative \(P\)-semantics, no parameter for an arbitrary \(P\)-algorithm, no wrapper type of program packages, and no assumptions asserting that some externally supplied algorithm is equivalent to the composition.

The separate trace characterization for this constructed code is Lemma 91. For every valid input \(x\), natural number \(S\), and output \(y\), that lemma states that the halting predicate of the returned program holds exactly when there exist one trace \(t=(q_1,z_1),\ldots ,(q_{r(x)},z_{r(x)}),y\), one generated state sequence \(G\), one oracle first-halting-time function \(U\), and one local cost \(L\) satisfying the concrete run-equation certificate \(\operatorname {def\_ composed\_ oracle\_ run\_ equations}(x,t,G,U)\), the local phase relation \(\operatorname {def\_ oracle\_ reduction\_ local\_ phases}(x,t,G,L)\), and the exact step-count equation

Each \(U(s)\) is the first halting time of the actual run \(\operatorname {HaltsWith}_{A_Q}(q_s,U(s),z_s)\) on the actual query \(q_s\) from the same trace. Thus oracle answers are not assumed as free data: they are outputs of \(A_Q\) inside the returned program’s step relation.

Therefore a Lean declaration for this node is the code alias above, with its operational projections supplied by Definitions 82, 83, 87, 88, and 90. The trace and accounting statements remain the separate lemmas named in the ist. It is invalid to prove this node by taking arbitrary parameters named like \(\operatorname {SP}\), \(\operatorname {AP}\), \(\operatorname {\_ configuration\_ carrier}\), \(\operatorname {\_ halting\_ output}\), \(\operatorname {\_ trace\_ semantics}\), or \(\operatorname {\_ step\_ count\_ governance}\), or by requiring the caller to supply proof hypotheses that an unrelated program has the desired carrier, trace semantics, output relation, or running-time accounting. Those components are part of the constructed program code above, not external obligations.

The Lean-facing predicate

is the concrete trace certificate generated by the step relation of the composed program \(R[A_Q]\). Its arguments are a valid \(P\)-input \(x\), a trace

a candidate generated state sequence \(G:\{ 0,\ldots ,r(x)\} \to \operatorname {State}_R(x)\), and oracle first-halting-time data \(U:\{ 1,\ldots ,r(x)\} \to \mathbb {N}\). The predicate is definitionally the conjunction of the following three subpredicates:

and

Consequently, eliminating a proof of \(\operatorname {def\_ composed\_ oracle\_ run\_ equations}(x,t,G,U)\) yields all of the following concrete obligations for the same trace \(t\), state sequence \(G\), and oracle time data \(U\):

and a single ordered phase-record sequence \(\Pi =(\operatorname {InitPhase},\operatorname {QueryPhase}, \operatorname {OraclePhase},\operatorname {UpdatePhase},\ldots , \operatorname {FinishPhase})\) whose records carry exactly these same states, histories, queries, oracle answers, and final output in the order specified by Definition 80.

This definition is intentionally not a mere constructor for phase records. A Lean declaration for this node must expose the three displayed conjuncts (or an equivalent proposition from which each displayed equation and the ordered phase trace can be projected). It must not replace the initialization equality, the update equalities, or the ordered run/trace relation by local let-bound phase records, by an existentially chosen unrelated state sequence, or by a predicate that only says the phase records are well typed.

For fixed \((P,Q,R,A_Q)\), valid input \(x\), and a current configuration \(c\in \operatorname {ComposedConfig}_{R,A_Q}(x)\), the branch target of the composed step is the following total case split.

If \(c=\operatorname {InitPhase}(c_{\rm init})\) and \(\operatorname {InitHalt}_R(x,c_{\rm init})\) is false, the target is

If \(c=\operatorname {InitPhase}(c_{\rm init})\) and \(\operatorname {InitHalt}_R(x,c_{\rm init})\) is true, the target ignores any output value carried by the halted initialization configuration and uses the definitionally displayed state \(\operatorname {init}_R(x)\). When \(r(x)=0\) it is

and when \(r(x){\gt}0\) it is

If \(c=\operatorname {QueryPhase}(s,\sigma ,H_s,c_{\rm qry})\) and the query countdown value \(c_{\rm qry}\) is positive, the target is the same query phase with countdown predecessor \(c_{\rm qry}-1\). If \(c_{\rm qry}=0\), define

The target is exactly

If \(c=\operatorname {OraclePhase}(s,\sigma ,H_s,q,c_Q)\) and \(\operatorname {Halt}_{A_Q}(q,c_Q)\) is false, the target is

If \(\operatorname {Halt}_{A_Q}(q,c_Q)\) is true, define

The target is exactly

If \(c=\operatorname {UpdatePhase}(s,\sigma ,H_s,q,z,c_{\rm upd})\) and the update countdown value \(c_{\rm upd}\) is positive, the target is the same update phase with countdown predecessor \(c_{\rm upd}-1\). If \(c_{\rm upd}=0\), define

When \(s{\lt}r(x)\) the target is exactly

and when \(s=r(x)\) the target is exactly

If \(c=\operatorname {FinishPhase}(\sigma ,H,c_{\rm fin})\) and \(c_{\rm fin}\) is positive, the target is the same finish phase with countdown predecessor \(c_{\rm fin}-1\). If \(c_{\rm fin}=0\), the target is exactly the unchanged configuration \(\operatorname {FinishPhase}(\sigma ,H,0)\).

The phrase “the target is exactly” is part of the formal contract: each branch returns the displayed constructor with the displayed arguments. No branch target may be replaced by an existentially chosen phase record, by a field supplied in a structure of step-map data, or by a configuration known only to satisfy a later trace-characterization predicate.

The deterministic step map

is the concrete total function whose value at every configuration is the branch target of Definition 86. Equivalently, it is defined by case analysis on the five phase constructors as follows.

On \(\operatorname {InitPhase}(c)\), if \(c\) has not halted for the initialization machine of \(R\), the next configuration is \(\operatorname {InitPhase}(\operatorname {initStep}_R(x)(c))\). If \(c\) has halted, the next state is the displayed initial state \(\operatorname {init}_R(x)\). If \(r(x)=0\) the step enters the finish countdown phase

and otherwise it enters the first query countdown phase

On a query phase \(\operatorname {QueryPhase}(s,\sigma ,H_s,c_{\rm qry})\), if the query countdown has not halted, the step decrements \(c_{\rm qry}\) inside the same phase. If it has halted, the emitted query is definitionally

and the next configuration is

On an oracle phase \(\operatorname {OraclePhase}(s,\sigma ,H_s,q,c_Q)\), if \(c_Q\) has not halted for the operational semantics of \(A_Q\) on \(q\), the next configuration is

If \(c_Q\) has halted, let \(z\) be the unique output selected by the output relation of \(A_Q\) at this halted configuration, namely \(z=\operatorname {HaltedOut}_{A_Q}(q,c_Q)\). The next configuration is

On an update phase \(\operatorname {UpdatePhase}(s,\sigma ,H_s,q,z,c_{\rm upd})\), if the update countdown has not halted, the step decrements \(c_{\rm upd}\) inside the same phase. If it has halted, define

If \(s{\lt}r(x)\) the next configuration is the query phase for call \(s+1\) with state \(\sigma '\) and history \(H_{s+1}\); if \(s=r(x)\) it is the finish countdown phase with state \(\sigma '\) and full history \(H_{s+1}\).

On a finish phase \(\operatorname {FinishPhase}(\sigma ,H,c_{\rm fin})\), if the finish countdown has not halted, the step decrements \(c_{\rm fin}\) inside the same phase; if it has halted, the step map fixes that halted finish configuration.

These clauses are the complete definition of the step map. The oracle-phase clause invokes the actual step map and output relation of the supplied program \(A_Q\) on the actual query \(q\); no oracle answer is provided as an external parameter to the composed program. Lean-facing, the declaration \(\operatorname {def\_ composed\_ oracle\_ step\_ map}\) must return the function \(\operatorname {ComposedStep}_{R,A_Q}(x)\) itself. It is not a structure with a field named \(\operatorname {ComposedStep}\), \(\operatorname {step}\), \(\operatorname {next}\), or any synonym, and it is not a proposition asserting the existence of a function satisfying branch equations. The five branch equations above are definitional equalities or projection lemmas about this single returned function; they are not caller-supplied axioms and they do not authorize existential branch choices.

For fixed data \((R,x,s,\sigma ,H_s,q,z)\), the update phase in the composed program is the canonical countdown machine

Its initial configuration is \(\operatorname {UpdateSteps}_R(x,s,\sigma ,H_s,q,z)\), its step map decrements a positive counter and fixes \(0\), its halt predicate is exactly \(k=0\), and its output at the halted configuration is exactly the next local state

Hence the update phase cannot choose an independent next state; its only halted output is the state-transition value from Definition 66.

A computational problem \(P\) with principal size parameter \(n\) and auxiliary dimension parameter \(\ell \) consists of the following concrete data: an input type \(I_P\), size functions

a valid-input predicate \(\Valid _P(x)\), an output type \(O_P(x)\) for each input \(x\), and a correctness relation

for \(y\in O_P(x)\). The relation \(\Correct _P(x,y)\) is required to encode the real yes/no, optimization, or approximation condition of the problem, not merely that \(y\) has the right syntactic type. For a decision problem, \(O_P(x)=\{ 0,1\} \) and correctness means output \(1\) exactly on promised yes instances and output \(0\) exactly on promised no instances.

In a trace for a reduction from \(P\) to \(Q\), the oracle answers are correct when every answer \(z_s\) satisfies the target problem’s correctness relation on the concrete query that produced it:

for all oracle-call positions \(s\).

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

Fix a computational problem \(P\). A deterministic computation model for algorithms solving \(P\) consists of a type of program codes, and for each program code \(A\) and input \(x\in I_P\), a concrete configuration type \(\operatorname {Config}_A(x)\) together with: an initial configuration \(\operatorname {init}_A(x)\in \operatorname {Config}_A(x)\), a deterministic step map

a halting predicate \(\operatorname {Halt}_A(x,c)\) on configurations, and an output relation

between halted configurations \(c\) and outputs \(y\in O_P(x)\). The run after \(s\) steps is defined recursively by

The statement

means the run first halts at exactly step \(s\) and returns \(y\):

and, for every \(r{\lt}s\), \(\neg \operatorname {Halt}_A(x,\operatorname {Run}_A(x,r))\). The output relation is functional on halted configurations, and the deterministic run has a unique first halting time: if \(\operatorname {HaltsWith}_A(x,s,y)\) and \(\operatorname {HaltsWith}_A(x,s',y')\), then \(s=s'\) and \(y=y'\). Every halted configuration has a unique output: if \(\operatorname {Halt}_A(x,c)\), then there exists a unique \(y\in O_P(x)\) such that \(\operatorname {Out}_A(x,c,y)\). Hence a halted configuration determines a concrete output value by unique description, not by an externally supplied oracle-answer parameter.

This node is the operational semantics used below. A step count is the finite number \(s\) appearing in \(\operatorname {HaltsWith}_A(x,s,y)\), not an arbitrary field attached to a total function.

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}\), 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 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.

A function \(T:\mathbb {N}\times \mathbb {N}\to \mathbb {R}_{\geq 0}\) is a worst-case running-time bound for an algorithm \(A\) solving \(P\) if for every valid input \(x\) with \(N_P(x)=n\) and \(L_P(x)=\ell \), the execution of \(A\) on \(x\) halts within \(T(n,\ell )\) steps and returns an output satisfying \(\Correct _P(x,A(x))\). The bound is exact for a pair \((n,\ell )\) if it is the maximum of these running times over all valid inputs with those parameters, and it is an upper bound if it is at least that maximum.

Fix \(P,Q,R,A_Q\), a valid \(P\)-input \(x\), a step count \(s\in \mathbb {N}\), and an output \(y\in O_P(x)\). The predicate

is exactly the single proposition

The parameters \(R\), \(A_Q\), and \(s\) are retained only so this predicate has the same witness arguments as the corresponding halting fact; they do not add any alternative program, trace data, or replaceable correctness field.

Fix \(P,Q,R,A_Q\), a valid \(P\)-input \(x\), a step count \(s\in \mathbb {N}\), and an output \(y\in O_P(x)\). The predicate

is exactly the two-conjunct proposition

Expanding the two helper predicates gives exactly

The program in the halting conjunct is the single composed program \(R[A_Q]\) of Definition 93. This predicate has no argument for an alternative \(P\)-algorithm and no field that can replace either displayed fact.

Fix \(P,Q,R,A_Q\), a valid \(P\)-input \(x\), a step count \(s\in \mathbb {N}\), and an output \(y\in O_P(x)\). The predicate

is exactly the single proposition

The program in this halting fact is the single composed program \(R[A_Q]\) of Definition 93. This predicate has no argument for an alternative \(P\)-algorithm, no trace certificate argument, and no field that can replace the displayed halting fact.

Fix \(P,Q,R,A_Q,T_Q\), a valid \(P\)-input \(x\), a step count \(s\in \mathbb {N}\), a trace \(t=((q_1,z_1),\ldots ,(q_{r(x)},z_{r(x)}),y)\), a generated state sequence \(G:\{ 0,\ldots ,r(x)\} \to \operatorname {State}_R(x)\), oracle first-halting-time data \(U:\{ 1,\ldots ,r(x)\} \to \mathbb {N}\), and a local cost \(L\in \mathbb {N}\). The predicate

is exactly the conjunction of

and

Thus the local-phase certificate, the exact first-halting step-count equation, and the induced oracle-cost upper bound are separate eliminable conjuncts for the same trace \(t\), state sequence \(G\), oracle time data \(U\), and local cost \(L\).

Fix \(P,Q,R,A_Q\), a valid \(P\)-input \(x\), an output \(y\in O_P(x)\), a trace

a generated state sequence \(G:\{ 0,\ldots ,r(x)\} \to \operatorname {State}_R(x)\), and oracle first-halting-time data \(U:\{ 1,\ldots ,r(x)\} \to \mathbb {N}\). The predicate

is exactly the conjunction of

and

The entries \(q_i,z_i\) are the query and answer entries of the displayed trace \(t\), and the prefix-history selector \(H\) is the one from the fixed local-phase presentation of \(R\). The oracle halting facts and the final postprocessing equality are conjuncts of this predicate, so they are eliminable from a proof for the same witnesses \((x,y,t,G,U)\) rather than consequences quoted only through a lemma name.

Fix \(P,Q,R\), constants \(\varepsilon '{\gt}0\), \(C'{\gt}0\), and \(b'\in \mathbb {N}\), a valid \(P\)-input \(x\), and a step count \(s\in \mathbb {N}\). The predicate

is the single inequality

This is only the final transferred \(P\)-running-time bound. It contains no trace data, no local-cost data, and no oracle-run data; those are the separate obligations of Definitions 97 and 98.

Fix \(P,Q,R,A_Q,T_Q\) and constants \(\varepsilon '{\gt}0\), \(C'{\gt}0\), and \(b'\in \mathbb {N}\). The predicate

is a proposition with exactly these displayed arguments and no additional program, semantics, trace-characterization, accounting, or helper-proof parameters. It holds exactly when, for every valid \(P\)-input \(x\), there exist concrete data

a generated state sequence \(G:\{ 0,\ldots ,r(x)\} \to \operatorname {State}_R(x)\), oracle first-halting-time data \(U:\{ 1,\ldots ,r(x)\} \to \mathbb {N}\), and a local cost \(L\in \mathbb {N}\) such that all four one-to-one witness obligations hold for those same witnesses:

and

Expanding these four helper predicates gives exactly the original displayed universal-existential proposition: the composed program halts with output \(y\), that output satisfies \(\Correct _P(x,y)\), the trace satisfies \(\operatorname {def\_ composed\_ oracle\_ run\_ equations}(x,t,G,U)\), the same witnesses satisfy \(\operatorname {def\_ oracle\_ reduction\_ local\_ phases}(x,t,G,L)\),

each oracle answer satisfies \(\operatorname {HaltsWith}_{A_Q}(q_i,U(i),z_i)\), the final output satisfies

the induced oracle-cost bound

holds, and the transferred subquadratic bound

holds. The helper predicates do not add a new program, trace, state sequence, or local-cost witness; they only name four individually formalizable conjunct groups of the same proposition.

The Lean-facing fine-grained reduction predicate has the explicit arguments

where \(P\) and \(Q\) are computational problem specifications and

are required baseline-algorithm witnesses from Definition 73. The predicate is not defined for bare problem specifications with no baseline witnesses.

With those baseline witnesses fixed, \(P\) reduces to \(Q\) in the fine-grained subquadratic sense if, for every constant \(\varepsilon {\gt}0\) and every particular correct deterministic \(Q\)-algorithm \(A_Q\) whose actual operational running-time bound satisfies

on valid \(Q\)-instances, there exist an oracle reduction datum \(R\) from \(P\) to \(Q\), a local-phase presentation of \(R\), and constants \(\varepsilon '{\gt}0\), \(C'{\gt}0\), and \(b'\in \mathbb {N}\) such that all of the following obligations hold for this same displayed tuple \((R,A_Q,T_Q,\varepsilon ',C',b')\).

First, \(R\) is a correct oracle reduction: it sends valid \(P\)-inputs to valid \(Q\)-queries and every locally generated trace with correct oracle answers has a final output satisfying \(\Correct _P\), exactly as in Definition 53. Second, \(R\) has the subquadratic transfer budget of Definition 72 against the displayed running-time bound \(T_Q\). Third, the \(P\)-algorithm witnessing the reduction is definitionally the composed algorithm

from Definition 93. Its program code, run relation, output, and step count are the concrete substitution simulation of \(R\) using the actual runs of \(A_Q\) on the actual constructed oracle queries. The reduction is not allowed to existentially choose any other \(P\)-algorithm \(A_P\).

Fourth, the composed witness obligations of Definition 100 hold for that same \(R[A_Q]\). Thus the final subquadratic correctness and time guarantee is not a separate existential consequence: it is the halting, correctness, final-postprocessing, oracle-answer, and step-count accounting certificate of the composed algorithm constructed in the third obligation. Problems are subquadratic equivalent if the same baseline-witnessed reduction predicate holds in both directions.

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 \(\gamma \geq 1\), \(\gamma \)-\(\mathrm{LSD}_{n,\ell }\) asks to find a pair \((i^*,j^*)\) whose cosine similarity is at least the optimum and at most \(\gamma \) times the optimum.

For \(\gamma \geq 1\), \(\gamma \)-\(\mathrm{Max\mbox{-}IP}_{n,\ell }\) asks for a pair whose inner product is a \(\gamma \)-approximation of the maximum inner product.

For \(\gamma \geq 1\), \(\gamma \)-\(\mathrm{Min\mbox{-}IP}_{n,\ell }\) asks to find a pair whose inner product is a \(\gamma \)-approximation of the minimum inner product.

For \(\gamma \geq 1\), \(\gamma \)-\(\mathrm{MSD}_{n,\ell }\) asks to find a pair \((i^*,j^*)\) whose cosine similarity is between \(1/\gamma \) times the optimum and the optimum.

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}\).

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 \(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 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 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 positive integers \(k\) and \(n\), a \(k\)CNF formula on variables \(x_1,\ldots ,x_n\) is a finite conjunction of clauses, where each clause is a disjunction of at most \(k\) literals and each literal is either \(x_i\) or \(\neg x_i\) for some \(i\). An assignment is a function \(\sigma :\{ 1,\ldots ,n\} \to \{ 0,1\} \). It satisfies a positive literal \(x_i\) when \(\sigma (i)=1\), satisfies a negative literal \(\neg x_i\) when \(\sigma (i)=0\), satisfies a clause when it satisfies at least one literal in that clause, and satisfies the formula when it satisfies every clause. The decision problem \(k\mathrm{SAT}\) asks whether a given \(k\)CNF formula has a satisfying assignment.

Given nonzero binary document embeddings \(v_1,\ldots ,v_n\in \{ 0,1\} ^{\ell }\), \(\mathrm{LSD}_{n,\ell }\) asks to find a pair \(i\neq j\) minimizing \(\left\langle v_i,v_j\right\rangle /(\| v_i\| \| v_j\| )\).

Given \(t\in [0,1]\), \(\mathrm{LSD}_{n,\ell ,t}\) asks whether some pair \(i\neq j\) has cosine similarity at most \(t\).

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.

Given binary vectors \(v_1,\ldots ,v_n\in \{ 0,1\} ^{\ell }\), \(\mathrm{Max\mbox{-}IP}_{n,\ell }\) asks to find a pair \(i\neq j\) maximizing \(\left\langle v_i,v_j\right\rangle \).

Given a threshold \(t\), \(\mathrm{Max\mbox{-}IP}_{n,\ell ,t}\) asks whether some pair \(i\neq j\) has \(\left\langle v_i,v_j\right\rangle \geq t\).

Given binary vectors \(v_1,\ldots ,v_n\in \{ 0,1\} ^{\ell }\), \(\mathrm{Min\mbox{-}IP}_{n,\ell }\) asks to find a pair \(i\neq j\) minimizing \(\left\langle v_i,v_j\right\rangle \).

Given a threshold \(0\leq t\leq \ell \), \(\mathrm{Min\mbox{-}IP}_{n,\ell ,t}\) asks whether some pair \(i\neq j\) has \(\left\langle v_i,v_j\right\rangle \leq t\).

For a monochromatic input \(V:\{ 1,\ldots ,n\} \to \{ 0,1\} ^{\ell }\), the balanced split tree is the following concrete finite list of intervals; it is not an arbitrary tree-like structure. An interval is encoded by endpoints \((L,R)\) with \(1\leq L\leq R\leq n\), denoting \(\{ L,\ldots ,R\} \). For every such interval define

The recursive interval-list constructor \(\operatorname {SplitIntervals}_n(L,R)\) is defined by primitive recursion on the length \(R-L+1\). Its Lean-facing defining equations are exactly the following equations, with no hidden tree parameter:

and, when \(L{\lt}R\),

Equivalently, if the recursion is implemented by well-founded recursion rather than by a primitive-recursive syntax form, the recursive calls in the defining body are precisely the two calls on the strict subintervals \((L,M(L,R))\) and \((M(L,R)+1,R)\), and the two displayed equations are projection lemmas for the declaration itself. The split tree for the input size \(n\) is definitionally

It depends on \(V\) only through the row values used by attached queries; the node set depends only on \(n\). The internal-node list is the filter

with inherited list order, and the leaf list is the complementary filter \(L=R\). The child intervals of an internal node \((L,R)\) are exactly

and right child

These two children are nonempty, disjoint, their union is \((L,R)\), and both children occur as the next recursively generated roots in \(\mathcal T_n\). No other intervals are nodes: every node of \(\mathcal T_n\) is produced by exactly one application of the displayed recursion from the root, and the list has no duplicate endpoint pairs.

The parent relation, ancestor relation, depth, and internal-node predicate are derived from this concrete list and these child equations. Consequently the following invariants are part of this definition, not later optional hypotheses: two generated intervals are either disjoint or one contains the other; every non-root node has a unique parent; every internal node has exactly the two displayed children; and every endpoint pair appears at most once in \(\mathcal T_n\).

The bichromatic query attached to an internal node \(I=(L,R)\) is the rectangular instance

of Definition 121, with principal size \(N_I=\max \{ |I_L|,|I_R|\} \leq |I|\) and dimension \(\ell \). The canonical query schedule is the finite list

If \(\operatorname {InternalIntervals}_n[s]=(L_s,R_s)\) and \(M_s=M(L_s,R_s)\), then the \(s\)th query record is definitionally the rectangular bichromatic input

where

and

The principal size and dimension projections of this concrete query are

Lean-facing, the declaration for this node must define the interval list \(\mathcal T_n\), the internal-node filtered list \(\operatorname {InternalIntervals}_n\), the midpoint function \(M\), the two child functions, the query function \(Q_I(V)\), and the query-schedule list \(\operatorname {SplitQueries}_n(V)\) by the displayed equations. The recursive constructor \(\operatorname {SplitIntervals}_n(L,R)\) must be part of this declaration’s exposed definitional data: callers can unfold it at \((L,L)\) and at \((L,R)\) with \(L{\lt}R\) to obtain the two equations above. It is not acceptable for this node to return only a wrapper around an unspecified helper such as \(\operatorname {minipSplitIntervals}\) unless that helper is the same declaration’s exposed recursive component and the base/step equations above are fields or projection lemmas of this node. It must not instead introduce a structure with fields such as \(\operatorname {nodes}\), \(\operatorname {children}\), \(\operatorname {isTree}\), or \(\operatorname {coversPairs}\) that can be instantiated by an arbitrary object. It must also not define \(\operatorname {InternalIntervals}_n\) or \(\operatorname {SplitQueries}_n(V)\) from an arbitrary list satisfying a tree predicate. Extra nodes, duplicate endpoint pairs, missing recursive children, duplicate intervals with the same endpoints, and extra or missing query records are ruled out definitionally by the list recursion and the displayed map from internal intervals to attached rectangular queries.

For the split-tree reduction on input \(V\), define

The initial state is the counter value

At oracle-call phase \(s\), where \(1\leq s\leq m\), the previous compatible state is the counter value \(s-1\), and the update after any well-typed query answer is exactly

This state contains no query answer and no history; the full answer history remains the separate history argument of Definition 54.

For the split-tree reduction on input \(V\), the local-phase presentation is the concrete variant-tagged presentation whose components are exactly the counter schedule, query schedule, and finish functions of Definitions 153, 154, and 155. Its oracle-call count is

its state space is \(\{ 0,\ldots ,r(V)\} \), its initial state is \(0\), its phase-\(s\) query is the \(s\)th split query view, and its update after phase \(s\) is the counter value \(s\).

The finish component is selected by the variant tag before the presentation is formed: exact and \(\gamma \)-approximate variants use the concrete pair-valued beta-minimum scan \(\operatorname {def\_ minip\_ split\_ finish\_ pair} (V,\operatorname {OptHist}(V,H_{\rm raw}))\), while the threshold variant uses the concrete Boolean OR scan \(\operatorname {def\_ minip\_ split\_ finish\_ threshold}(H)\). The local work is precisely split-tree construction, query-view construction, counter updates, and the final scan attached to the selected variant.

Lean-facing, the declaration

returns this concrete local-phase presentation. Its component equations are definitional equations of the returned presentation:

the query at phase \(s\) is exactly the \(s\)th split query view, the update is exactly the counter value \(s\), and the finish function is the variant-specific function displayed in Definition 155. The declaration must not be an abstract tuple of components that can be instantiated independently of these formulas, and it must not return a product of unrelated query, update, and finish components. The returned presentation is connected to the oracle-reduction datum by these displayed equations for all three variants. The threshold case uses only a variant value \(\operatorname {threshold}(t,h_0,h_\ell )\) from Definition 150; hence the same fixed threshold \(t\) is available before the threshold source and target specifications are selected.

At oracle-call phase \(s\) with \(1\leq s\leq m\), the query constructor reads the interval

and returns exactly the valid rectangular query view

independent of the previous history argument \(H_s\) and independent of the previous counter value except for its phase-compatibility role. The query validity and its principal-size and dimension projections are those of Lemma 137.

The final phase of the local presentation is variant tagged. For the exact optimization variant, the output type is the exact promised monochromatic Min-IP distinct-pair type and

For the \(\gamma \)-approximate optimization variant, the output type is the \(\gamma \)-approximate promised monochromatic Min-IP distinct-pair type and

For the threshold decision variant, the output type is Boolean and

There is no common output value containing both pair and Boolean components, and no later projection chooses a component. Each variant has its own finish function with the displayed output type. In the two optimization variants the raw full oracle-answer history is first adapted by Definition 152; therefore the pair scan receives the concrete \(\operatorname {MinIPSplitFullOptimizationHistory}(V)\) required by Definition 147.

Fix one of the three Min-IP variants: exact optimization, \(\gamma \)- approximation for a fixed \(\gamma \geq 1\), or threshold decision represented by a fixed threshold-indexed parameter \(\operatorname {threshold}(t,h_0,h_\ell )\) with \(0\leq t\leq \ell \). The source problem is the corresponding promised monochromatic specification from Definition 136, and the target oracle problem is the corresponding rectangular bichromatic specification from Definition 135. Given a correct rectangular bichromatic solver \(A_{\rm bi}\) for that same variant, the concrete oracle reduction datum \(R_{\rm biMinIP\to monoMinIP}\) is assembled from the helper declarations as follows.

For a valid optimization source input, the promise gives \(n\geq 2\). For a threshold source input with \(n{\lt}2\), the datum has zero oracle calls and final output \(0\). Otherwise it uses the local-phase presentation of Definition 156; hence its oracle-call count is

and its \(s\)th query is exactly the valid rectangular query view

Query validity is provided by Lemma 137. Optimization oracle answers are decoded into original distinct indices by Definition 144; final exact and \(\gamma \) outputs are computed by the deterministic beta-minimum rule of Definition 149 after converting the raw full oracle history with Definition 152; and final threshold outputs are computed by its deterministic Boolean OR rule.

Lean-facing, the declaration

returns a value whose codomain is exactly the oracle-reduction-datum type

from Definition 49, where \(P_{\operatorname {variant}}\) is the selected promised monochromatic source specification and \(Q_{\operatorname {variant}}\) is the selected rectangular bichromatic oracle specification. In the threshold case these two specifications are the aligned pair

from Definition 151. Thus the target problem is not chosen from a threshold-erasing tag and does not default to \(t=0\). It is a concrete datum value, not a proposition, predicate, certificate, or structure saying that some datum exists. In particular, there is no declaration, field, or helper proposition named \(\operatorname {uses\_ oracle\_ reduction\_ data}\), \(\operatorname {exists\_ oracle\_ reduction\_ data}\), \(\operatorname {is\_ oracle\_ reduction\_ data}\), or any synonym. The implementation must not prove this node by introducing

or by returning a wrapper whose only connection to Definition 49 is such an existential proposition.

The returned datum has the following projection equations as part of this definition. Its input map, size functions, output types, and correctness relations are exactly those of Definitions 136 and 135. For an optimization source input \(V\), the valid-input projection includes the promise \(n\geq 2\). For a threshold source input with \(n{\lt}2\), the oracle-call-count projection is \(r(V)=0\) and the final-output projection is \(0\). In every other valid case, the oracle-call-count projection is

the query projection is the total function satisfying, for every \(1\leq s\leq r(V)\),

and the query-size projections are

The state-space, initial-state, query-construction, update, and finish projections of the returned datum are exactly the corresponding projections of \(\operatorname {def\_ minip\_ bi\_ to\_ mono\_ local\_ phase\_ presentation} (\operatorname {variant},V)\), not caller-supplied functions. In the exact and \(\gamma \) variants the final postprocessing projection is precisely

where \(H_{\rm raw}\) is the generic full oracle-answer history received by the oracle-reduction postprocess field and \(\operatorname {OptHist}(V,H_{\rm raw})\) is the adapter of Definition 152. In the threshold variant it is precisely \(\operatorname {def\_ minip\_ split\_ finish\_ threshold}(H)\). Local-to-global decoding of optimization answers is exactly \(\operatorname {DecodePair}_I\) from Definition 144. These equations are eliminable by unfolding the returned datum itself; they are not separate assumptions and not partial constraints on an abstract \(R\).

This node therefore only assembles the concrete components into the oracle reduction datum required by Definition 49. It does not introduce new problem specifications, split-interval validity fields, local-to-global decoding fields, postprocessing fields, or local-phase compatibility fields. All such mathematical content is supplied by the helper nodes in the ist, and the projections of the resulting datum are exactly their displayed equations.

For a valid exact-optimization split-tree run on \(V:\{ 1,\ldots ,n\} \to \{ 0,1\} ^{\ell }\), a full oracle-answer history

is exact-correct when every answer \(z_s=(u_s,w_s)\) is a correct exact rectangular Min-IP answer for the actual query at the same position:

Equivalently, writing \(A_s=\operatorname {SplitLeftRows}_{I_s}(V)\) and \(B_s=\operatorname {SplitRightRows}_{I_s}(V)\), this condition is the concrete family of inequalities

The decoded candidate \(\operatorname {CandPair}(V,H,s)\) and score \(\operatorname {CandBeta}(V,H,s)\) are the functions of Definition 145 applied to this same answer \(z_s\). This contract is not a global correctness tag on \(H\): it exposes one exact optimality inequality for each concrete query-list position and each local cross-pair in that query.

Given a threshold variant

define the threshold split reduction’s paired problem specifications directly from this constructor pattern, not by reusing a possibly threshold-erasing selector:

The projection equations

and

are part of this node’s returned data. For a monochromatic source input \(V:\{ 1,\ldots ,n\} \to \{ 0,1\} ^{\ell }\), the source yes condition is

For every split-tree query \(Q_I(V)=((v_i)_{L\leq i\leq M},(v_j)_{M{\lt}j\leq R})\), the target oracle yes condition for the same fixed \(\theta \) is

The threshold appearing in these two displayed predicates is definitionally the same value \(\operatorname {thresholdOf}(\theta )=t\).

This node is the threshold-source specification restricted to the same fixed \(t\) as the rectangular bichromatic oracle specification. It supplies the declaration

whose output is the concrete tuple

where \(h_P\) and \(h_Q\) are exactly the two displayed specification equalities. The source yes predicate and query yes predicate are projections from these two concrete threshold-\(t\) specifications. They are not independent generic predicates whose threshold happens to be written as \(\operatorname {thresholdOf}(\theta )\) while the source specification itself remains untied to \(t\).

It is not an oracle-reduction datum and it is not a proof of correctness of the whole reduction. It only fixes the matching threshold-bearing source and target specifications so later reduction data cannot instantiate the source as an unapplied threshold family, instantiate the target as \(\operatorname {BiMinIPThresholdSpec}(0)\), as a tag-only threshold problem, or as a specification whose threshold depends on a query answer or on an unrelated source-input field.

For the exact and \(\gamma \) split-tree variants, let \(H_{\rm raw}\in \Hist _R(V,r(V))\) be a full oracle-answer history of the oracle reduction datum whose queries are the split queries \(Q_{\operatorname {InternalIntervals}_n[s]}(V)\) and whose answers are optimization pairs \(z_s=(u_s,w_s)\). Define

to be the concrete full optimization history

in the same list order as \(\operatorname {InternalIntervals}_n\), where each query component and answer component is copied from the raw query-answer entry at position \(s\).

Its defining projection equations are:

and

for every \(1\leq s\leq r(V)\). Consequently the decoded candidates and beta values used by Definition 145 are computed from the actual oracle answers in \(H_{\rm raw}\), at the same positions.

Lean-facing, this node is the function

It is the only adapter from the generic oracle-answer history type to \(\operatorname {MinIPSplitFullOptimizationHistory}(V)\). The exact and \(\gamma \) finish functions must therefore be stated as

not as a fixed fallback pair, an empty-history default, or a call to \(\operatorname {def\_ minip\_ split\_ finish\_ pair}\) on the raw history type itself.

For an internal interval \(I=(L,R)\) of \(\operatorname {InternalIntervals}_n\), write \(M=L+\lfloor (R-L)/2\rfloor \). The local left index type of the attached rectangular query is

and the local right index type is

Define the two concrete affine inclusions

by the equations

If the rectangular query is implemented using the child-range subtype indices \(\{ L,\ldots ,M\} \) and \(\{ M+1,\ldots ,R\} \) instead of local ordinals, these same maps are the coercions to the underlying original row indices. This node defines only the two index maps and their displayed equations.

For an internal interval \(I=(L,R)\) with midpoint \(M\), define the deterministic decoding map

by

where membership in the distinct-pair subtype is certified by Lemma 139. The row-value and inner-product preservation facts for this decoded pair are exactly Lemma 143.

Lean-facing, the declaration

returns this function \(\operatorname {DecodePair}_I\) itself. It is not a proposition, interface, or structure with a caller-supplied decoding field. Its only computational body is the displayed pair of affine index maps; the bounds, distinctness, row-value preservation, and inner-product preservation obligations are separate projection lemmas in the ist.

For a nonempty optimization history \(H\), define the concrete pair-valued finish function by

If a total formal function is required on empty histories, its empty-history branch is an arbitrary fixed distinct-pair default supplied only after a proof that the optimization source is invalid there; the defining equation above is the only equation used for valid optimization histories.

For a threshold history

define the concrete Boolean finish function by the finite OR

For \(m=0\) this OR is the empty finite OR and has value \(0\).

For a full optimization history

in the same list order as \(\operatorname {InternalIntervals}_n\), with optimization oracle answers \(z_s=(u_s,v_s)\), define the decoded candidate at history position \(s\) to be

Define its score by

This node defines only the finite indexed candidate-pair and beta-value functions obtained by decoding each history position.

For a nonempty optimization history \(H\) of length \(m{\gt}0\), define

The selected history position is the natural-order first position attaining this value:

Tie-breaking is by the finite history position \(s\), not by the decoded pair value and not by a list search on pair values. If two different history positions decode to the same global pair, they remain separate positions in this minimum scan.

Lean-facing, this declaration is not just two equations assigning \(\operatorname {MinBeta}\) to the score at some implementation-selected index. It returns the concrete finite-minimum package

with exactly the following eliminable fields. First,

Second, the selected position attains the displayed finite minimum:

Third, the selected value is no larger than every history-position score:

Fourth, the selected position is the natural-order first minimizer:

Equivalently, the pair \((h_{\rm att},h_{\rm first})\) states that \(\operatorname {FirstMinBetaPos}(V,H)\) is the least natural-number position among all positions attaining \(\operatorname {MinBeta}(V,H)\).

These four fields are part of this node’s formal content. A declaration for this label is invalid if it merely chooses an index such as \(\operatorname {minIPSplitFirstIndexByNat}\) and then defines \(\operatorname {MinBeta}\) to be \(\operatorname {CandBeta}\) at that index without proving \(h_{\rm le}\) and \(h_{\rm first}\). The minimum property must quantify over the actual finite position type \(\{ 1,\ldots ,m\} \) of the supplied history \(H\), and the firstness property must use the natural order on those history positions. No decoded-pair tie-breaking, pair-value search, existential minimizer, or caller-supplied proof of optimality may replace these fields.

The deterministic split-history postprocessors are exactly the two concrete functions

defined in Definitions 147 and 148. The exact and \(\gamma \)-approximate variants use the pair-valued first-minimum beta scan; the threshold variant uses the Boolean OR scan.

Lean-facing, this node is not a proposition stating equations about externally supplied functions, and it is not a record accepting \(\operatorname {FinishPair}\) or \(\operatorname {FinishThreshold}\) fields from the caller. It exposes these two already-defined functions as the postprocessing functions for the split-tree reduction. The pair-valued function’s nonempty-history equation and the threshold function’s empty and nonempty OR equations are inherited from the two helper definitions.

Let \(V:\{ 1,\ldots ,n\} \to \{ 0,1\} ^{\ell }\) and let \(I=(L,R)\) be an internal interval with midpoint \(M\). Let

be the actual rectangular query view from Lemma 137. Define

and

to be the first and second row functions obtained by projecting this same query record \(Q_I(V)\) and reindexing its child-range domains by the canonical local ordinal maps

Equivalently,

is the local-ordinal row view of the concrete rectangular query \(Q_I(V)\). This node defines only these two row functions as projections of the actual split-query view. It does not define them by an independent direct lookup into \(V\), does not accept caller-supplied row functions, and does not add any oracle-validity hypothesis beyond the fact that \(I\) is an internal interval whose query view is the one displayed above.

For a fixed dimension \(\ell \), the split-tree Min-IP reduction variant is the following concrete tagged parameter:

Here \(h_\gamma \) is the proof \(\gamma \geq 1\), \(h_0\) is the proof \(0\leq t\), and \(h_\ell \) is the proof \(t\leq \ell \). The threshold tag is not a nullary constructor: it carries the actual natural threshold \(t\) and both displayed bounds. Define

with projection lemmas returning \(h_0\) and \(h_\ell \).

The variant determines the source and target problem specifications by the following equations:

and

Lean-facing, the declaration

is the dependent package consisting of this parameter type and the two specification selectors

defined by case analysis on the displayed constructors. The threshold branch equations of these returned selector functions are definitional projection equations:

The same carried threshold variable \(t\) appears on both right-hand sides, before either specification is formed.

A formalization must not use a frozen constructor \(\operatorname {threshold}\) with no threshold field, must not default the threshold to \(0\), and must not recover \(t\) from a source input after the target oracle specification has already been chosen. It must also not implement \(\operatorname {sourceSpec}_{\ell }(\operatorname {threshold}(t,h_0,h_\ell ))\) by returning a tag-only or tuple-projection specification such as an unapplied threshold component of Definition 136. The threshold selector must apply that source specification to the carried \(t\), so eliminating the threshold case yields the exact equality \(P_{\operatorname {threshold}(t,h_0,h_\ell )} =\operatorname {MonoMinIPThresholdSpec}(t)\), not merely a threshold-family tag. The fixed threshold is part of the variant datum before both \(\operatorname {MonoMinIPThresholdSpec}(t)\) and \(\operatorname {BiMinIPThresholdSpec}(t)\) are formed.

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]\).

The reduction datum \(R_{\rm mono\to bi}\) from monochromatic \(\mathrm{OV}\) to bichromatic \(\mathrm{OV}\) acts on a monochromatic input \(V=(v_1,\ldots ,v_n)\subseteq \{ 0,1\} ^{\ell }\) as the following concrete one-query-or-zero-query local-phase reduction. The fine-grained regime is \(n\geq 2\); the finitely many inputs with \(n{\lt}2\) are decided by the constant zero-query branch by directly returning no, since no distinct pair of indices exists.

First it computes the Boolean value

by the deterministic nested scan over all entries of the input matrix. The scan step count is exactly bounded by a fixed constant multiple of \(n(1+\ell )\), because each of the \(n\ell \) Boolean coordinates is inspected at most once and the per-row accumulator is updated in constant time.

If \(n\geq 2\) and \(Z(V)\) is true, then the oracle-call count is \(r(V)=0\), there is no bichromatic query, and the final postprocessing output is the yes answer for monochromatic \(\mathrm{OV}\). If \(Z(V)\) is false, then the oracle-call count is \(r(V)=1\) and the unique query is the concrete bichromatic instance

with principal size \(N_Q(q_1(V))=n\) and auxiliary dimension \(L_Q(q_1(V))=\ell \). The copy phase writes the two lists \(A(V)\) and \(B(V)\) coordinatewise, so its step count is also bounded by a fixed constant multiple of \(n(1+\ell )\). The update phase merely stores the oracle answer \(z_1\in \{ 0,1\} \), and the final postprocessing returns exactly \(z_1\) as the monochromatic \(\mathrm{OV}\) answer. Thus every locally generated trace has local non-oracle cost

for an absolute constant \(C_0\), and the oracle-cost sum is either \(0\) in the zero-vector branch or exactly \(T_Q(n,\ell )\) in the one-query branch. These scan, query-size, postprocessing, and cost equalities are part of the datum; they are not deferred to a later opaque reduction predicate.

Given nonzero binary document embeddings \(v_1,\ldots ,v_n\in \{ 0,1\} ^{\ell }\), \(\mathrm{MSD}_{n,\ell }\) asks to find a pair \(i\neq j\) maximizing \(\left\langle v_i,v_j\right\rangle /(\| v_i\| \| v_j\| )\).

Given \(t\in [0,1]\), \(\mathrm{MSD}_{n,\ell ,t}\) asks whether some pair \(i\neq j\) has cosine similarity at least \(t\).

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}}\).

Let \(A_Q\) be the concrete deterministic \(Q\)-program used by the composed reduction, let \(q\in I_Q\), and let \(c_Q\in \operatorname {Config}_{A_Q}(q)\) be an oracle configuration satisfying \(\operatorname {Halt}_{A_Q}(q,c_Q)\). The halted-output selector is the uniquely determined value

such that

Moreover, if \(\operatorname {Out}_{A_Q}(q,c_Q,z')\), then \(z'=\operatorname {HaltedOut}_{A_Q}(q,c_Q)\). This selector is the only oracle answer used by the halted-oracle branch of \(\operatorname {ComposedStep}_{R,A_Q}\). It is not an argument of that branch and it is not chosen by an existential proof of trace consistency.

For an oracle reduction datum \(R\), a valid \(P\)-input \(x\), and a phase index \(s\in \{ 0,\ldots ,r(x)\} \), the answer-history type

is the concrete type of finite query-answer prefixes of length \(s\):

Such an \(H\) is well formed when every \(q_u\) is the \(u\)th query produced by the reduction datum \(R\) on input \(x\) after the earlier answers \(z_1,\ldots ,z_{u-1}\), and every \(z_u\in O_Q(q_u)\). Thus \(\Hist _R(x,0)\) contains the empty history, while \(\Hist _R(x,r(x))\) contains full oracle-answer histories for completed runs of \(R\) on \(x\).

This history type is the only place in the local-phase presentation where raw oracle answers and query-answer pairs live. It is passed as a separate argument to later query, update, and postprocessing functions.

An oracle reduction datum \(R\) from \(P\) to \(Q\) is correct if both of the following universal obligations hold. First, it sends every valid \(P\)-input only to valid \(Q\)-queries in the sense of Definition 51. Second, for every valid \(P\)-input \(x\) and every trace consistent with \(R\) on \(x\), if all oracle answers in that trace are correct for their concrete \(Q\)-queries, then the final output \(y\) in the trace satisfies

This requirement is uniform over all possible correct oracle answers, so the reduced algorithm may not rely on a special choice among multiple valid answers returned by the oracle.

Fix a correct \(Q\)-algorithm with running-time bound \(T_Q\). For a trace \(t=(q_1,z_1),\ldots ,(q_r,z_r),y\) of \(R\) on input \(x\), a candidate generated state sequence \(G\), and a natural number \(L\) satisfying \(\operatorname {def\_ oracle\_ reduction\_ local\_ phases}(x,t,G,L)\), the induced running time of the simulated reduction run is bounded by

If no such \(G\) and \(L\) exist, the trace is not a locally generated trace of the reduction and contributes no valid simulated execution. The oracle-cost term uses the actual principal size and auxiliary dimension of each constructed query, not the parameters of the original \(P\)-input.

An oracle reduction datum \(R\) from \(P\) to \(Q\) assigns to every valid \(P\)-input \(x\) a finite number \(r(x)\) of oracle calls, a sequence of concrete \(Q\)-inputs

and a postprocessing map which turns any sequence of oracle answers \(z_s\in O_Q(q_s(x))\) into a final output

Adaptive reductions are represented by allowing the later query \(q_s\) to be the query produced after the earlier answer values \(z_1,\ldots ,z_{s-1}\) have been fixed; the completed run is still the finite sequence of concrete query-answer pairs and the final output above.

The final postprocessing function of a local-phase presentation is

where \(\sigma \) is an explicitly supplied final local state and \(H\) is an explicitly supplied full query-answer history. Its local step count

counts exactly the non-oracle work needed to produce the final output from those arguments. In a locally generated trace with generated state sequence \(G\), the final state argument is \(G(r)\), the history argument is \(H(x,t,r+1)\), and the final output satisfies

For a concrete trace \(t=(q_1,z_1),\ldots ,(q_r,z_r),y\) of \(R\) on a valid input \(x\), define

to be the predicate on candidate finite state sequences

The predicate holds exactly when \(G\) satisfies the two recursive equations

and for every \(1\leq s\leq r\),

This node is a proposition relating an explicit candidate sequence \(G\) to the update equations. It does not introduce a separate globally named recursive function returning \(G\), and later nodes quantify over such a concrete \(G\).

For a local-phase presentation of \(R\), the initialization computation on a valid \(P\)-input \(x\) is specified by concrete non-oracle operational data, separate from all oracle histories. It consists of a configuration type

an input-reading initial configuration

a deterministic local step map

a halting predicate \(\operatorname {InitHalt}_R(x,c)\) on initialization configurations, and an output relation

between a halted initialization configuration \(c\) and a state \(\sigma \in \operatorname {State}_R(x)\).

The initialization run is defined recursively by

The predicate

means that this non-oracle run first halts at exactly step \(s\) and outputs exactly the state \(\sigma \):

and, for every \(r{\lt}s\),

The output relation is functional on halted initialization configurations, and the deterministic initialization run has a unique first halting time: if \(\operatorname {InitHaltsWith}_R(x,s,\sigma )\) and \(\operatorname {InitHaltsWith}_R(x,s',\sigma ')\), then \(s=s'\) and \(\sigma =\sigma '\).

This node supplies the semantics for the initial-state construction only. It contains no oracle query, oracle answer, answer history, trace prefix, or target-problem output. Its step count is the actual first halting time of this displayed initialization run.

For a local-phase presentation of \(R\), the initial-state constructor and its local step count are not independent data. They are a function

and a natural number \(\operatorname {InitSteps}_R(x)\in \mathbb {N}\) defined for every valid \(P\)-input \(x\), together with the semantic certificate

Equivalently, \(\operatorname {InitSteps}_R(x)\) is the exact first halting time of the concrete initialization run from Definition 62, and \(\operatorname {init}_R(x)\) is exactly the state output by that halted run. The declaration therefore has the following invariant:

Thus an implementation cannot certify this node by choosing an arbitrary natural-number field; the step count must be witnessed by the displayed non-oracle construction of exactly the displayed initial state.

For a local-phase presentation of \(R\), the external local compatibility relation is the proposition

on separate arguments

It holds exactly when \(H\) is a well-formed answer history of length \(s\) and the five projections of \(u\) are the control state, counter store, work-tape contents, work-head positions, and deterministic register store obtained by running the non-oracle part of \(R\) on input \(x\) through the first \(s\) oracle calls using the answer prefix \(H\).

This is a relation, not a field of \(u\) and not a subtype condition in \(\operatorname {Local}_R(x,s)\). The history argument remains external, so compatibility ties a history-independent snapshot to a particular answer prefix without encoding that prefix or any oracle answer inside the snapshot.

A local-phase presentation of an oracle reduction datum \(R\) supplies one global, history-free record of component type families. Lean-facing, the declaration

is a structure with exactly the following six named fields and no others:

For a valid \(P\)-input \(x\), proof \(h_x:\Valid _P(x)\), and phase \(s\in \{ 0,\ldots ,r(x)\} \), the six instantiated history-free component types are therefore

The record itself is indexed only by \((P,Q,R)\). The phase is an argument to each of the six fields, not an enclosing answer-history-dependent parameter. The structure has no field named \(\operatorname {AnswerHistory}\), \(\operatorname {History}\), \(\operatorname {Trace}\), or any synonym, and it has no constructor argument whose type is an oracle-answer history. In particular, the declaration must not include a parameter \(H:\Hist _R(x,s)\), a default parameter \(H:=\Hist _R(x,s)\), a let-bound reference to \(\Hist _R(x,s)\), or any field that returns or stores \(\Hist _R(x,s)\).

These types are parameters of the local presentation at \((R,x,h_x,s)\) and are chosen before any oracle answers are supplied. None of their declarations, indices, constructors, fields, subtype predicates, quotient relations, default arguments, local definitions, or field bodies may mention an answer-history type, a trace prefix, a prefix-history selector, a query produced from an answer prefix, or an oracle answer type \(O_Q(q)\).

The component meanings are fixed as follows. \(\operatorname {Control}_R(x,h_x,s)\) is the control-state type. \(\operatorname {CounterName}_R(x,h_x,s)\to \mathbb {N}\) is the counter store. \(\operatorname {TapeName}_R(x,h_x,s)\to (\mathbb {Z}\to \operatorname {TapeSymbol}_R(x,h_x,s))\) is the work-tape content store, and \(\operatorname {TapeName}_R(x,h_x,s)\to \mathbb {Z}\) is the work-head-position store. \(\operatorname {RegisterName}_R(x,h_x,s)\to \operatorname {RegisterValue}_R(x,h_x,s)\) is the store for all remaining deterministic local registers. These store types are derived in the snapshot-record node from the six component fields above; they are not additional fields of \(\operatorname {def\_ oracle\_ reduction\_ local\_ component\_ types}\). These six component fields are the only data types from which local snapshots are built.

For a trace \(t=(q_1,z_1),\ldots ,(q_r,z_r),y\) of \(R\) on \(x\), define \(\operatorname {def\_ oracle\_ reduction\_ local\_ phases}\) to be the relation between a candidate generated state sequence \(G:\{ 0,\ldots ,r\} \to \operatorname {State}_R(x)\) and a natural number \(L\). It holds exactly when the trace is locally generated using \(G\) in the sense of Definition 69 and \(L\) is the local running-time sum

The query term uses the previous generated state \(G(s-1)\) explicitly, and the update term is tied to the state equation defining \(G(s)\) in Definition 67. The local running-time value \(L\) includes exactly the initial-state construction, every state-dependent query construction, every state update after an oracle answer, and final postprocessing. It does not include the time spent solving the \(Q\)-queries.

For an oracle reduction datum \(R\), a valid \(P\)-input \(x\), and a phase \(s\in \{ 0,\ldots ,r(x)\} \), the type

is definitionally the local snapshot record of Definition 56. Thus an element \(u\in \operatorname {Local}_R(x,s)\) consists exactly of the non-oracle local data held by the reduction after \(s\) oracle calls have been completed: its control state, counter store, work-tape contents, work-head positions, and deterministic register store.

Lean-facing, \(\operatorname {Local}_R(x,s)\) is indexed only by \((R,x,s)\) and is chosen before any particular answer history is supplied. Its declaration is an answer-history-free local state type: no constructor argument, field, projection, invariant, subtype predicate, or field type may mention \(\Hist _R(x,s)\), a prefix-history selector, a trace prefix, or an oracle answer type \(O_Q(q)\) in any position. In particular, a local snapshot may not contain a field such as \(\Hist _R(x,s)\to T\), \(T\to \Hist _R(x,s)\), \(\forall H:\Hist _R(x,s),\, T(H)\), \(\exists H:\Hist _R(x,s),\, T(H)\), a dependent pair over histories, a quotient by a relation using histories, or any analogous function/product/subtype whose domain, codomain, index, or proposition can encode oracle answers. A field named “control state”, “work tape”, or similar is permitted only when its type is built from non-oracle data already available from \((R,x,s)\) and does not contain histories or oracle answers under any type former. In particular, the declaration may not replace the record by \(\operatorname {Unit}\) unless the five displayed component fields themselves are still present with their named projections.

Thus \(\operatorname {Local}_R(x,s)\) stores only history-independent local data. Any semantic fact saying that a local snapshot is the one reached after a particular oracle-answer prefix must therefore be stated as a relation with two separate arguments,

not by storing \(H\) or the answers inside \(u\).

For a local-phase presentation of \(R\), a valid input \(x\), and a phase \(s\in \{ 0,\ldots ,r(x)\} \), the concrete local snapshot record is the product with exactly the following named projections:

Equivalently, the record carrier is

with the displayed projection names. This declaration is not an erased placeholder: any implementation of a local snapshot must provide exactly these non-oracle fields, even when some component type is empty or singleton for a particular reduction and phase.

A trace

is locally generated by the local-phase presentation of \(R\) on \(x\) when there exists an explicit state sequence \(G:\{ 0,\ldots ,r\} \to \operatorname {State}_R(x)\) such that Definition 67 holds for \(G\), the selector \(H(x,t,s)\) is the first \(s-1\) query-answer entries of the trace for every \(s\), and both displayed equations hold:

and

This predicate is the formal link between an oracle reduction trace and the state-dependent local operational data. In particular, the query at call \(s\) is certified from the explicit generated previous state \(G(s-1)\).

At oracle-call position \(s\), the query constructor of a local-phase presentation is a state-dependent function

where \(\sigma \in \operatorname {State}_R(x)\) is the previous local state and \(H_s\) is the prefix history before call \(s\). Its local step count is the function

Thus the query and its construction cost are both allowed to depend on the previous state, not only on \(x\), the call index, and the earlier query-answer pairs. In a locally generated trace, the concrete query at position \(s\) satisfies

For a local-phase presentation of \(R\), the raw state representation on a valid \(P\)-input \(x\) is the phase-indexed dependent sum

It has the named projections

The projection equations are part of the representation contract. A state implementation therefore exposes the phase coordinate and local snapshot by name, rather than only through anonymous dependent-pair eliminators.

For a raw state \(\sigma \in \operatorname {RawState}_R(x)\) and a separately supplied answer history \(H\), the state-history compatibility relation is

Hence compatibility simultaneously asserts that \(H\) is a well-formed history prefix of the state’s named phase and that the state’s named local snapshot is the deterministic non-oracle snapshot reached after that prefix. The relation is external to the state carrier and has the three displayed arguments \((x,\sigma ,H)\).

For a local-phase presentation of an oracle reduction datum \(R\), the state space on a valid \(P\)-input \(x\) is the concrete raw state representation of Definition 59:

Its projections are

with the displayed names. The phase coordinate is bounded by the oracle-call count \(r(x)\) from the reduction datum \(R\), and the local projection has type \(\operatorname {Local}_R(x,\operatorname {phase}_R(x,\sigma ))\), so every state is explicitly tied to a definite point of an \(R\)-run and to the corresponding non-oracle snapshot.

The state type contains only the phase and the non-oracle local snapshot. It does not contain an answer history and does not contain oracle answers. Compatibility with a particular prefix of oracle answers is instead the external relation

from Definition 60, equivalently \(\operatorname {LocalCompatible}_R(x,\operatorname {phase}_R(x,\sigma ), \operatorname {local}_R(x,\sigma ),H)\). Thus the state-space contract consists of the carrier \(\operatorname {State}_R(x)\), the named phase projection, the named local projection, and the named external compatibility relation.

Consequently, later query, update, and postprocessing functions receive \(\sigma \in \operatorname {State}_R(x)\) and the relevant history \(H\) as separate arguments: \(\sigma \) supplies the non-oracle local data, while \(H\) supplies exactly the oracle query-answer prefix determined by \(R\).

After oracle-call position \(s\), the state-transition function is

Its local step count

counts exactly the non-oracle work needed to update the local state after the answer \(z_s\) to query \(q_s\) is available. The next state in the run is

For an oracle reduction datum \(R\) and a valid \(P\)-input \(x\), an oracle reduction trace is the finite sequence

It is consistent with \(R\) when \(r=r(x)\), each \(q_s\) is the query produced by \(R\) at call \(s\) on input \(x\) after the earlier answers in the trace, each \(z_s\in O_Q(q_s)\), and

Define \(\operatorname {def\_ oracle\_ reduction\_ trace\_ prefix\_ history}(P,Q,R)\) to be the type of prefix-history selector functions \(H\). Such an \(H\) takes a valid \(P\)-input \(x\), a trace \((q_1,z_1),\ldots ,(q_r,z_r),y\) of \(R\) on \(x\), and an index \(s\in \{ 1,\ldots ,r+1\} \), and returns the finite list

In particular \(H(x,t,r+1)\) is the full query-answer history.

This declaration is a type of selectors, not a recursively defined function with a hidden body. The equality saying that the selected list is the first \(s-1\) entries of the trace is part of the local trace-consistency predicate below, so later nodes use a concrete selector argument \(H\) rather than an undefined global prefix-history value.

Given binary vectors \(v_1,\ldots ,v_n\in \{ 0,1\} ^{\ell }\), the problem \(\mathrm{OV}_{n,\ell }\) asks whether there are indices \(i\neq j\) with \(\left\langle v_i,v_j\right\rangle =0\).

Fix \(\gamma \geq 1\). The reduction datum is not a single ambiguous “Min-IP solver” interface. It has a source branch

where \(A_{\rm exact}\) is a correct exact \(\mathrm{Min\mbox{-}IP}_{n,\ell }\) program and \(A_{\gamma }\) is a correct \(\gamma \)-\(\mathrm{Min\mbox{-}IP}_{n,\ell }\) program. The two source branches have separate returned-pair selectors and separate halting facts.

Lean-facing, this source is a genuine disjoint sum with branch-dependent payload. An element of \(\operatorname {ExactSource}(A_{\rm exact})\) contains only the exact \(\mathrm{Min\mbox{-}IP}\) program, its exact correctness/halting data, and the exact output selector below. It contains no \(\gamma \)-\(\mathrm{Min\mbox{-}IP}\) program, no approximate correctness proof, no approximate returned-pair selector, and no \(\gamma \)-branch running-time bound. An element of \(\operatorname {GammaSource}(A_{\gamma })\) contains only the \(\gamma \)-\(\mathrm{Min\mbox{-}IP}\) program, its approximate correctness/halting data, and the approximate output selector below. It contains no exact \(\mathrm{Min\mbox{-}IP}\) program, no exact correctness proof, no exact returned-pair selector, and no exact-branch running-time bound. Later declarations quantify over one value \(\operatorname {source}\) of this disjoint sum and eliminate it by cases; they do not take a pair of exact-and-approximate algorithms or a pair of exact-and-approximate runtime hypotheses.

In the exact branch, for every input \(V=(v_1,\ldots ,v_n)\subseteq \{ 0,1\} ^{\ell }\) with \(n\geq 2\), the selector

is exactly the halted output pair of \(A_{\rm exact}\) on the exact Min-IP input \(V\), at that program’s first halting time. Its correctness relation is the exact equality

In the \(\gamma \) branch, for every such \(V\), the selector

is exactly the halted output pair of \(A_{\gamma }\) on the \(\gamma \)-\(\mathrm{Min\mbox{-}IP}\) input \((V,\gamma )\), at that program’s first halting time. Its correctness relation is the approximation inequality

The two selectors are branch-specific data. A formalization must not use \(\operatorname {ExactOutPair}_R(V)\), a field named \(\operatorname {exactPair}\), or any exact-output witness as the halted output of the \(\gamma \)-\(\mathrm{Min\mbox{-}IP}\) program. Conversely, \(\operatorname {GammaOutPair}_R(V)\) is not available in the exact branch.

The induced OV decision program \(R_{\mathrm{Min\mbox{-}IP}\to \mathrm{OV}}[A_{\min }]\) has the following concrete operational phases. On input \(V\), if \(n{\lt}2\) it halts immediately and outputs \(0\). If \(n\geq 2\) and the source is exact, it runs \(A_{\rm exact}\) on \(V\) until the first halting output \(\operatorname {ExactOutPair}_R(V)\) is produced. If \(n\geq 2\) and the source is \(\gamma \)-approximate, it runs \(A_{\gamma }\) on \((V,\gamma )\) until the first halting output \(\operatorname {GammaOutPair}_R(V)\) is produced. In either branch it then performs the deterministic coordinate scan of the branch’s own returned pair:

The scan step count is the concrete value \(\operatorname {LocalScanSteps}_R(V)\) and satisfies the displayed datum inequality

for an absolute constant \(C_0\) supplied by the datum. The branch/output overhead is bounded by an absolute constant \(C_1\). The final Boolean output is \(1\) exactly when the scanned value for the active branch is \(0\), and is \(0\) otherwise.

Thus the only subroutine call is the actual run of the active branch’s program on the original Min-IP input, the returned pair is the active branch’s own first halted output, and the final Boolean is the equality test on the concrete inner product of that same pair. There is no externally supplied OV answer, no abstract correctness-equivalence field, and no shared output-pair field that can be used for both exact and approximate sources.

An algorithm \(A\) for a computational problem \(P\) is a program code in the deterministic operational semantics of Definition 45. Its execution on input \(x\) is the concrete run \(\operatorname {Run}_A(x,s)\) generated by the initial configuration and step map. For a valid input \(x\), the notation \(A(x)\) denotes the unique output \(y\in O_P(x)\) for which there exists a finite step count \(s\) with \(\operatorname {HaltsWith}_A(x,s,y)\); this notation is defined only from the halting relation and the uniqueness guaranteed by the operational semantics.

The algorithm halts on promised inputs when, for every valid \(x\), there exist \(s\in \mathbb {N}\) and \(y\in O_P(x)\) such that \(\operatorname {HaltsWith}_A(x,s,y)\). It is correct when

for every input \(x\). Its running-time witness is a function \(T_A:\mathbb {N}\times \mathbb {N}\to \mathbb {R}_{\geq 0}\) such that on every valid input \(x\) there are \(s\in \mathbb {N}\) and \(y\in O_P(x)\) with

Thus the claimed running time is semantically linked to the first halting time of the operational execution, and the returned value is linked to the problem’s correctness relation. The structure does not permit an unconstrained \(\operatorname {computation\_ steps}\) witness or an arbitrary total function unrelated to execution.

The monochromatic exact and \(\gamma \)-approximate Min-IP source specifications used in the recursive reduction have the input type \(V:\{ 1,\ldots ,n\} \to \{ 0,1\} ^{\ell }\) but are valid only under the promise

This promise is part of the valid-input predicate, because the output type for both optimization variants is the distinct-pair subtype

The exact correctness relation requires the returned distinct pair \((i^*,j^*)\) to satisfy

The \(\gamma \)-approximate correctness relation, for \(\gamma \geq 1\), requires

The threshold source specification \(\operatorname {MonoMinIPThresholdSpec}(t)\) has Boolean output type and may be evaluated for all \(n\); when \(n{\lt}2\) its yes condition is false because there is no feasible distinct pair. For \(n\geq 2\) it asks exactly whether some distinct pair has inner product at most \(t\). Thus the optimization sources never quantify over an infeasible distinct pair type, while the decision source keeps the paper’s constant-time \(n{\lt}2\) no branch.

A computational problem \(P\) has a quadratic-time baseline algorithm if there is a concrete deterministic algorithm \(B_P\) for \(P\), a worst-case running-time bound \(T_{B_P}:\mathbb {N}\times \mathbb {N}\to \mathbb {R}_{\geq 0}\) for the actual operational execution of \(B_P\), and constants \(C{\gt}0\), \(b\in \mathbb {N}\), and \(n_0\in \mathbb {N}\) such that \(B_P\) halts correctly on every valid input and

for every \(n\geq n_0\) and every auxiliary dimension \(\ell \) in the domain of \(P\).

Lean-facing, the proposition

contains the displayed witnesses \((B_P,T_{B_P},C,b,n_0)\) and the two displayed obligations: semantic correctness of \(B_P\) in the sense of Definition 46, and the quadratic polynomial upper bound above. It is not a name tag on \(P\) and it is not automatically true for an arbitrary computational-problem specification.

From the rectangular input record of Definition 121 we form three concrete computational-problem specifications. Their input type is the same rectangular record

with validity condition \(n_A\geq 1\) and \(n_B\geq 1\), principal size \(N(X)=\max \{ n_A,n_B\} \), and auxiliary dimension \(L(X)=\ell \).

The exact oracle specification \(\operatorname {BiMinIPExactSpec}\) has output type \(\{ 1,\ldots ,n_A\} \times \{ 1,\ldots ,n_B\} \). Its correctness relation \(\operatorname {exact\_ correct}(X,(i^*,j^*))\) is exactly

The \(\gamma \)-approximate oracle specification \(\operatorname {BiMinIPGammaSpec}(\gamma )\), for \(\gamma \geq 1\), has the same output type. Its correctness relation \(\operatorname {gamma\_ correct}(X,(i^*,j^*))\) is exactly

The threshold oracle specification \(\operatorname {BiMinIPThresholdSpec}(t)\), for \(0\leq t\leq \ell \), has output type \(\{ 0,1\} \). Its correctness relation \(\operatorname {threshold\_ correct}(X,z)\) is exactly

and \(z=0\) in the negation of this condition.

These are real computational-problem specifications in the sense of Definition 44. They are not aliases for a family tag and they do not require any additional abstract correctness fields: the only output and correctness relations are the three displayed relations named \(\operatorname {exact\_ correct}\), \(\operatorname {gamma\_ correct}\), and \(\operatorname {threshold\_ correct}\).

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.

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

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

An oracle reduction datum \(R\) has a subquadratic transfer budget from \(P\) to \(Q\) if the following implication holds for every valid \(P\)-input \(x\) with \(N_P(x)=n\) and \(L_P(x)=\ell \). Whenever the assumed \(Q\)-algorithm has running time

every trace of \(R\) on \(x\) satisfies a bound

for every locally generated trace and every local-cost witness \(\operatorname {def\_ oracle\_ reduction\_ local\_ phases}(x,t,G,L)\), for some constants \(\varepsilon '{\gt}0\), \(C'{\gt}0\), and \(b'\in \mathbb {N}\) that depend only on \(\varepsilon ,C,b\) and the reduction, not on the particular input \(x\) or oracle answers. Thus the number of calls, query sizes, and all local construction, update, and postprocessing costs are explicitly included in the transfer.

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.

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.

A nonnegative running-time bound \(T:\mathbb {N}\to \mathbb {R}\) is truly subquadratic in \(n\) if there exist constants \(\varepsilon {\gt}0\), \(C{\gt}0\), and \(n_0\in \mathbb {N}\) such that for every \(n\geq n_0\),

When an auxiliary dimension \(\ell \) is present, a bound \(T:\mathbb {N}\times \mathbb {N}\to \mathbb {R}\) is truly subquadratic up to polynomial factors in \(\ell \) if there are \(\varepsilon {\gt}0\), \(C{\gt}0\), an exponent \(b\in \mathbb {N}\), and \(n_0\) such that

for all \(n\geq n_0\) and all allowed \(\ell \).

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.

An oracle reduction datum \(R\) sends valid \(P\)-inputs to valid \(Q\)-queries if for every valid \(P\)-input \(x\) and every trace consistent with \(R\) on \(x\), each query in the trace satisfies \(\Valid _Q(q_s)\).

Bichromatic \((\log n)/\ell \)-Additive-MSD in dimension \(\ell =O(\log n)\) and bichromatic \((\log n)\)-Additive-Max-IP in dimension \(O(\log n)\) are subquadratic equivalent.

Fix an integer threshold \(1\leq t\leq \ell \). Let the raw sentinel row be

and let the target attention-space sentinel row be

with \(\ell \) leading zero coordinates and last coordinate \(t+1\). On the finite valid row set consisting of all binary rows in \(\{ 0,1\} ^{\ell }\) and the sentinel row \(s_t\), there exists a continuous \(f:\mathbb {R}^\ell \to \mathbb {R}^{\ell +1}\) such that

Suppose \(n\geq 2\), \(\gamma \geq 1\), and the \(\gamma \)-\(\mathrm{Min\mbox{-}IP}\) algorithm in Definition 122 halts on \(V\) with a pair \((i^*,j^*)\) satisfying

Then the final test \(\left\langle v_{i^*},v_{j^*}\right\rangle =0\) outputs \(1\) exactly on OV yes instances and outputs \(0\) exactly on OV no instances.

If \(m\geq d_{\rm in}\), then for any scalar \(\lambda \) there exist \(Q,K\in \mathbb {R}^{d_{\rm in}\times m}\) with \(QK^\top =\lambda I_{d_{\rm in}}\).

For any fixed baseline witnesses for bichromatic \(\mathrm{OV}\) and monochromatic \(\mathrm{OV}\), the datum \(R_{\rm bi\to mono}\) satisfies

In particular, substituting any truly subquadratic monochromatic \(\mathrm{OV}\) algorithm into the composed program \(R_{\rm bi\to mono}[A_{\rm mono}]\) gives the concrete bichromatic \(\mathrm{OV}\) algorithm certified by Definition 101. More explicitly, the witness for this reduction includes the following eliminable obligations:

the iff

and the answer-transfer statement that every correct oracle answer on \(q_1(A,B)\) is the correct final answer for \((A,B)\) because final postprocessing returns that same answer.

For the reduction \(R_{\rm bi\to mono}\) on a valid bichromatic input \((A,B)\), the oracle-call count is \(1\), the unique oracle query is the monochromatic instance \(Q(A,B)=A'\cup B'\) from Definition 113, and final postprocessing returns exactly the oracle answer \(z_1\).

Consequently, every correct yes/no answer \(z_1\) for the monochromatic query \(Q(A,B)\) is the correct yes/no answer for the original bichromatic OV input \((A,B)\). Equivalently, if \(z_1=1\), then \(Q(A,B)\) has an orthogonal pair and hence \((A,B)\) has a cross orthogonal pair; if \(z_1=0\), then \(Q(A,B)\) has no orthogonal pair and hence \((A,B)\) has no cross orthogonal pair.

Let \(A=\{ a_1,\ldots ,a_n\} \) and \(B=\{ b_1,\ldots ,b_n\} \) be a valid bichromatic OV input in dimension \(\ell \), and let

be the transformed rows in the single monochromatic query \(Q(A,B)=A'\cup B'\). Then the query has an orthogonal pair of distinct rows if and only if the original bichromatic input has a cross orthogonal pair:

More granularly, for all \(i,i'\) and \(j,j'\),

and

Thus every orthogonal witness in the monochromatic query is necessarily a cross pair with one row from \(A'\) and one row from \(B'\).

A truly subquadratic algorithm for bichromatic \(\mathrm{Max\mbox{-}IP}_{n,\ell }\) implies a truly subquadratic algorithm for \(\mathrm{OV}_{n,\ell }\), up to polynomial factors in \(\ell \).

Truly subquadratic algorithms for bichromatic MSD or LSD variants imply truly subquadratic algorithms for the corresponding monochromatic variants.

If \(v,w\in \{ 0,1\} ^d\) and \(\| v\| _1=\sum _i v[i]\), then \(\left\langle v,\bar w\right\rangle =\| v\| _1-\left\langle v,w\right\rangle \).

For every occurrence datum \(\mathsf{doc}\), document \(D:\mathsf{doc}.\mathrm{Document}\), coordinate-indexed keyword vector \(K:\{ 1,\ldots ,\ell \} \to \mathsf{doc}.\mathrm{Keyword}\), and coordinate \(r\),

For every occurrence datum \(\mathsf{doc}\), document \(D:\mathsf{doc}.\mathrm{Document}\), coordinate-indexed keyword vector \(K:\{ 1,\ldots ,\ell \} \to \mathsf{doc}.\mathrm{Keyword}\), and coordinate \(r\),

For every occurrence datum \(\mathsf{doc}\), document \(D:\mathsf{doc}.\mathrm{Document}\), coordinate-indexed keyword vector \(K:\{ 1,\ldots ,\ell \} \to \mathsf{doc}.\mathrm{Keyword}\), and coordinate \(r\),

For every occurrence datum \(\mathsf{doc}\), document \(D:\mathsf{doc}.\mathrm{Document}\), coordinate-indexed keyword vector \(K:\{ 1,\ldots ,\ell \} \to \mathsf{doc}.\mathrm{Keyword}\), and coordinate \(r\),

For real finite-dimensional vectors \(v,w\), \(|\left\langle v,w\right\rangle |\leq \| v\| \, \| w\| \).

In the trace characterization of a halting execution of \(R[A_Q]\), if the simulated oracle calls halt at first halting times \(u_1,\ldots ,u_r\), then the first halting step count \(s\) of the composed execution is exactly

If \(A_Q\) has worst-case running-time bound \(T_Q\), then the same execution satisfies the induced cost bound

The step count \(s\) is the first-halting time supplied by the \(\operatorname {HaltsWith}\) predicate of Definition 45 for the composed operational semantics and code value of Definitions 89 and 90. This accounting lemma does not introduce or require any separate program-code wrapper; it uses the same concrete code value as Lemma 91.

For every valid input \(x\), step count \(S\), and output \(y\), the operational halting fact

holds if and only if there exist a trace

a generated state sequence \(G:\{ 0,\ldots ,r\} \to \operatorname {State}_R(x)\), oracle first-halting-time data \(U:\{ 1,\ldots ,r\} \to \mathbb {N}\), and a local cost \(L\) such that

and

In particular, any such certificate includes the displayed local-phase equations

the final-output equation

and the actual oracle-run facts

Equivalently, every halting execution of the composed program is represented by exactly such a trace certificate, and any trace certificate satisfying \(\operatorname {def\_ composed\_ oracle\_ run\_ equations}(x,t,G,U)\), \(\operatorname {def\_ oracle\_ reduction\_ local\_ phases}(x,t,G,L)\), with step count \(S=L+\sum _s U(s)\) is a halting execution of the same composed program \(R[A_Q]\) with output \(y\). Here \(\operatorname {HaltsWith}_{R[A_Q]}\) is the concrete first-halting predicate from Definition 45 applied to the semantics \(\operatorname {def\_ composed\_ oracle\_ operational\_ semantics}\) and to its code value \(\operatorname {def\_ composed\_ oracle\_ program\_ code}\). This lemma introduces no new type, structure, or compatibility predicate named \(\operatorname {def\_ composed\_ oracle\_ program\_ code}\); that name is already the concrete code value of Definition 90. It is invalid to formalize this trace-characterization node by replacing the existing code value with a fresh package whose fields are \(\operatorname {Semantics}\) and \(\operatorname {code}\), or by adding a second declaration named \(\operatorname {def\_ composed\_ oracle\_ program\_ code}\). The only formal declaration for this node is the lemma \(\operatorname {lem\_ composed\_ oracle\_ trace\_ characterization}\).

For \(a{\lt}b\) there is a continuous function \(f:\mathbb {R}^\ell \to \mathbb {R}\) such that \(f(x)=1\) if some coordinate \(x[i]\geq b\), and \(f(x)=0\) if all coordinates satisfy \(x[i]{\lt}a\).

If \(v,w\in \{ 0,1\} ^d\) are nonzero binary vectors, then their cosine similarity lies in \([0,1]\).

For all positive integers \(n\) and \(\ell \), every occurrence datum \(\mathsf{doc}\), document family \(D:\{ 1,\ldots ,n\} \to \mathsf{doc}.\mathrm{Document}\), coordinate-indexed keyword vector \(K:\{ 1,\ldots ,\ell \} \to \mathsf{doc}.\mathrm{Keyword}\), row \(i\in \{ 1,\ldots ,n\} \), and coordinate \(r\in \{ 1,\ldots ,\ell \} \),

With \(a'\) and \(b'\) as in Lemma 193,

Consequently an additive Max-IP threshold \(\alpha \) and gap \(g\) become the additive MSD threshold \(\alpha /\ell \) and gap \(g/\ell \).

Let \(a,b\in \{ 0,1\} ^{\ell }\). Define

Then \(a',b'\in \{ 0,1\} ^{3\ell }\), each has exactly \(\ell \) ones, and \(\left\langle a',b'\right\rangle =\left\langle a,b\right\rangle \).

In the exact source case \(\operatorname {source}=\operatorname {ExactSource}(A_{\rm exact})\), the concrete program \(R_{\mathrm{Min\mbox{-}IP}\to \mathrm{OV}}[A_{\rm exact}]\) has a correctness certificate

with exactly the following content. If \(n{\lt}2\), the program makes no Min-IP call and outputs \(0\). If \(n\geq 2\), it runs only the exact program \(A_{\rm exact}\) on the exact \(\mathrm{Min\mbox{-}IP}\) input \(V\) until the first halted output \(\operatorname {ExactOutPair}_R(V)\), scans that same pair, and outputs \(1\) exactly when the scanned inner product is \(0\):

It outputs \(0\) exactly in the negation of this condition, and its local first-halting-time equation is

This node has no parameters or hypotheses for a \(\gamma \)-\(\mathrm{Min\mbox{-}IP}\) program, no \(\gamma \)-branch returned pair, and no runtime bound for either branch. It is a correctness and local first-halting certificate for the exact branch alone.

Suppose \(n\geq 2\) and the exact \(\mathrm{Min\mbox{-}IP}\) algorithm in Definition 122 halts on \(V\) with a pair \((i^*,j^*)\) satisfying

Then the final test \(\left\langle v_{i^*},v_{j^*}\right\rangle =0\) outputs \(1\) exactly on OV yes instances and outputs \(0\) exactly on OV no instances.

Fix \(n,\ell \) and \(t\in [0,1]\). Among nonzero binary vectors in \(\{ 0,1\} ^{\ell }\), the set of possible cosine similarities is finite. Therefore, for \(\mathrm{MSD}_{n,\ell ,t}\), either a pair has similarity at least \(t\), or there is a number \(\Delta {\gt}0\) such that every pair has similarity at most \(t-\Delta \). Similarly, for \(\mathrm{LSD}_{n,\ell ,t}\), either a pair has similarity at most \(t\), or there is a number \(\Delta {\gt}0\) such that every pair has similarity at least \(t+\Delta \).

Let \(S\subset \mathbb {R}^a\) be a finite set of valid row inputs, and assign a target vector \(y_s\in \mathbb {R}^b\) to every \(s\in S\). There exists a continuous function \(f:\mathbb {R}^a\to \mathbb {R}^b\) such that \(f(s)=y_s\) for every \(s\in S\).

In the approximate source case \(\operatorname {source}=\operatorname {GammaSource}(A_{\gamma })\), the concrete program \(R_{\mathrm{Min\mbox{-}IP}\to \mathrm{OV}}[A_{\gamma }]\) has a correctness certificate

with exactly the following content. If \(n{\lt}2\), the program makes no Min-IP call and outputs \(0\). If \(n\geq 2\), it runs only the \(\gamma \)-\(\mathrm{Min\mbox{-}IP}\) program \(A_{\gamma }\) on the approximate input \((V,\gamma )\) until the first halted output \(\operatorname {GammaOutPair}_R(V)\), scans that same approximate output pair, and outputs \(1\) exactly when the scanned inner product is \(0\):

It outputs \(0\) exactly in the negation of this condition, and its local first-halting-time equation is

This node has no parameters or hypotheses for an exact \(\mathrm{Min\mbox{-}IP}\) program, no exact-branch returned pair, and no runtime bound for either branch. It is a correctness and local first-halting certificate for the \(\gamma \) branch alone. Every occurrence of the returned pair in this statement is \(\operatorname {GammaOutPair}_R(V)\).

For every occurrence datum \(\mathsf{doc}\), document \(D:\mathsf{doc}.\mathrm{Document}\), and keyword \(k:\mathsf{doc}.\mathrm{Keyword}\),

For every occurrence datum \(\mathsf{doc}\), document \(D:\mathsf{doc}.\mathrm{Document}\), and keyword \(k:\mathsf{doc}.\mathrm{Keyword}\),

For nonzero vectors \(v,w\) and positive integer \(q\),

For finite real vectors \(v,w\) and every positive integer \(q\),

For every finite real vector \(v\) and positive integer \(q\), \(\| v^{\otimes q}\| =\| v\| ^q\).

If \(\mathrm{LSD}_{n,\ell ,t}\) is truly subquadratic for every threshold \(t\), then \(\mathrm{LSD}_{n,\ell }\) is truly subquadratic.

For fixed \(n,\ell ,t\), use the same augmented raw sentinel row \(s_t=(0,\ldots ,0,t+2)\), normalized document rows, and positive target sentinel row \(\tau _t=(0,\ldots ,0,t+1)\) as in Lemma 216. Choose \(Q,K\) so that \(QK^\top =-\lambda I_{\ell +1}\) for a sufficiently large \(\lambda {\gt}0\), and choose the value vector \((1,\ldots ,1,0)\). Then yes instances of \(\mathrm{LSD}_{n,\ell ,t}\) produce some attention output at least \(1/(n+1)\), while no instances produce all attention outputs below \(1/(2(n+1))\).

For nonzero binary vectors \(v,w\), their cosine similarity is \(0\) if and only if \(\left\langle v,w\right\rangle =0\).

If any bichromatic Max-IP variant has a truly subquadratic algorithm, then the corresponding monochromatic variant has a truly subquadratic algorithm, up to polynomial factors in \(\ell \).

For \(1\leq t\leq \ell \), evaluate the transformer on \(\operatorname {Aug}_{s_t}(E)\), where \(s_t=(0,\ldots ,0,t+1)\in \mathbb {R}^\ell \) is the raw sentinel row from Lemma 205. After the input MLP, the first \(n\) rows are \(x_i=(v_i,1)\) and the last row is \(\tau _t=(0,\ldots ,0,t+1)\in \mathbb {R}^{\ell +1}\). With the attention parameters of Appendix C, choose a scale \(\lambda {\gt}0\) with \(n\ell \exp (-\lambda ){\lt}1/(2(n+1))\). The attention output has a gap of at least \(1/(n+1)\) versus below \(1/(2(n+1))\) between yes and no instances of \(\mathrm{Max\mbox{-}IP}_{n,\ell ,t}\) and \(\mathrm{Min\mbox{-}IP}_{n,\ell ,t}\).

Fix \(\gamma \geq 1\), one active source branch

from Definition 122. Let \(A_{\min }(\operatorname {source})\) denote the program carried by that branch: it is \(A_{\rm exact}\) in the exact case and \(A_{\gamma }\) in the \(\gamma \) case. Let \(T_{\min }\) be a semantic worst-case bound for this same active program and for no other source branch. Suppose there are constants \(\varepsilon {\gt}0\), \(C{\gt}0\), \(b\in \mathbb {N}\), and \(n_0\) such that

for every \(n\geq n_0\) and every allowed dimension \(\ell \).

The concrete run-and-test program \(R_{\mathrm{Min\mbox{-}IP}\to \mathrm{OV}}[A_{\min }(\operatorname {source})]\) directly certifies an OV solver together with the inherited subquadratic running-time certificate. Lean-facing, the conclusion of this node is exactly the ordered pair

The first component is the branch-specific correctness certificate of Lemma 130: direct small-input behavior, active subroutine first-halting output, scanned active pair, OV yes/no correctness, and first-halting-time-plus-scan accounting. The second component is the inherited runtime component of Lemma 131: the concrete piecewise bound \(T_{\mathrm{OV}}^R\), the semantic worst-case proof for the actual constructed OV program, and the constants \(\varepsilon '{\gt}0\), \(C'{\gt}0\), \(b'\in \mathbb {N}\), and \(n_0'\) proving

for all \(n\geq n_0'\) and every allowed \(\ell \).

Thus the declaration for this label has exactly one active source parameter, one active semantic bound \(T_{\min }\) for the program in that source, and hypotheses for \(C\), \(\varepsilon \), \(b\), and \(n_0\) about that same bound. In the exact case it may require the exact program’s correctness and the exact bound; it must not require any \(\gamma \)-program correctness or runtime hypothesis. In the \(\gamma \) case it may require the \(\gamma \) program’s correctness and the \(\gamma \) bound; it must not require any exact-program correctness or runtime hypothesis. A statement with simultaneous hypotheses for both branches, such as both \(h_{\rm Exact}\) and \(h_{\rm Gamma}\) or both \(T_{\rm exact}\) and \(T_{\gamma }\), is strictly stronger than this node and is not a valid formalization of this label.

For every \(\gamma \geq 1\) and every active source branch

from Definition 122, the concrete run-and-test program for that one active branch returns the OV answer on every valid OV input. This node contains only the correctness and local first-halting behavior of the constructed program. It has no worst-case running-time hypotheses and no inactive-branch hypotheses.

More precisely, it returns the certificate

defined by case analysis on the displayed disjoint sum:

Eliminating the exact branch yields exactly Lemma 126; eliminating the \(\gamma \) branch yields exactly Lemma 127. A Lean statement for this label must therefore have one active source argument and must not require hypotheses named like \(h_{\rm Exact}\) and \(h_{\rm Gamma}\) simultaneously. In particular, it must not ask for a semantic worst-case-running-time bound for the inactive exact branch in the \(\gamma \) case, nor for a semantic worst-case-running-time bound for the inactive \(\gamma \) branch in the exact case.

Fix \(\gamma \geq 1\) and one active source branch

from Definition 122. Let \(A_{\min }(\operatorname {source})\) be the exact program in the exact case and the \(\gamma \)-\(\mathrm{Min\mbox{-}IP}\) program in the \(\gamma \) case. Let \(T_{\min }:\mathbb {N}\times \mathbb {N}\to \mathbb {R}_{\geq 0}\) be a semantic worst-case bound for that active Min-IP program. Suppose there are constants \(\varepsilon {\gt}0\), \(C{\gt}0\), \(b\in \mathbb {N}\), and \(n_0\) such that

for every \(n\geq n_0\) and every allowed dimension \(\ell \).

Then the constructed OV program \(R_{\mathrm{Min\mbox{-}IP}\to \mathrm{OV}}[A_{\min }(\operatorname {source})]\) has the inherited runtime component

which is exactly the certificate supplied by Lemma 129. Eliminating it gives the concrete bound

a proof that \(T_{\mathrm{OV}}^R\) bounds the actual first-halting time of the same constructed OV program, and constants \(\varepsilon '{\gt}0\), \(C'{\gt}0\), \(b'\in \mathbb {N}\), and \(n_0'\) with

This node has the explicit parameters \(T_{\min }\), \(C\), \(\varepsilon \), \(b\), and \(n_0\) for the active source only; the runtime component is not derivable from branch-local accounting alone and is not an assumed property of an arbitrary OV bound. It must not require a runtime bound for the inactive source branch.

For each of the exact, \(\gamma \)-approximate, and threshold Min-IP variants, any truly subquadratic rectangular bichromatic solver induces the concrete monochromatic solver \(R_{\rm biMinIP\to monoMinIP}[A_{\rm bi}]\) of Definition 157. The induced solver’s oracle queries are exactly the split-tree queries \(Q_I(V)\), every distinct original pair is covered as a cross-pair in exactly one such query, the final answer is combined by the displayed minimum or Boolean-OR rule, and its total running time remains truly subquadratic up to polynomial factors in \(\ell \).

Let \(H\) satisfy Definition 158. Fix a query position \(s\) with interval \(I_s\) and answer \(z_s=(u_s,w_s)\). For every local cross-pair \(u,w\) in the same query, let

be the decoded global pair, and let

be the decoded global pair for \((u,w)\). Then

In particular, if a distinct original pair \((p,q)\) occurs as a cross-pair in the query at position \(s\), the decoded exact oracle answer at position \(s\) has score no larger than \(\left\langle v_p,v_q\right\rangle \).

For every binary-vector input \(V=(v_1,\ldots ,v_n)\) with \(n\geq 2\),

Assume that every internal query \(Q_I(V)\) is answered by a \(\gamma \)-approximate cross minimizer and let \((p^*,q^*)\) be a global monochromatic minimizer. If \(I_0\) is the unique internal node whose query contains \((p^*,q^*)\) as a cross-pair, then the optimum value of \(Q_{I_0}(V)\) equals the global optimum value. Consequently the final postprocessing rule of Definition 157 returns a distinct pair whose inner product is at most \(\gamma \) times the global optimum and at least the global optimum.

Suppose the rectangular bichromatic solver has running-time bound

for some fixed \(\varepsilon {\gt}0\). Then every locally generated trace of \(R_{\rm biMinIP\to monoMinIP}[A_{\rm bi}]\) has total time

for constants \(\varepsilon '{\gt}0\), \(C'{\gt}0\), and \(b'\in \mathbb {N}\) depending only on \(\varepsilon ,C,b\) and the fixed reduction, not on \(V\) or on oracle answers.

Let \(V:\{ 1,\ldots ,n\} \to \{ 0,1\} ^{\ell }\) be a valid exact-optimization monochromatic Min-IP source input, so \(n\geq 2\). Let \(H\) be the full exact-optimization oracle-answer history generated by the concrete reduction datum of Definition 157, in the same order as \(\operatorname {InternalIntervals}_n\), and assume \(H\) satisfies the exact split-history oracle-answer contract of Definition 158. Let

be the exact variant’s final postprocessing output. Then \((a^*,b^*)\) is a valid distinct pair and

Equivalently, the exact split-tree reduction’s deterministic finish scan returns a global minimizer for monochromatic \(\mathrm{Min\mbox{-}IP}\).

At every depth \(h\) of the balanced split tree, the internal-node intervals are disjoint and have total size at most \(n\). Each query at depth \(h\) has principal size at most the size of its parent interval. Therefore, for any \(\varepsilon \in (0,1]\),

up to an absolute constant accounting for the floor/ceiling imbalance.

In the threshold variant of Definition 157, the final Boolean OR of the internal-node oracle answers is \(1\) if and only if the original monochromatic input has a distinct pair \(i\neq j\) with \(\left\langle v_i,v_j\right\rangle \leq t\).

For every internal interval \(I=(L,R)\) with midpoint \(M\), every \(u\in \{ 1,\ldots ,M-L+1\} \), and every \(v\in \{ 1,\ldots ,R-M\} \),

Consequently both indices are original input indices in \(\{ 1,\ldots ,n\} \) and

Let \(V:\{ 1,\ldots ,n\} \to \{ 0,1\} ^{\ell }\) and let \(I=(L,R)\) be an internal interval with midpoint \(M\). Let

be exactly the local left and right answer-index types introduced in Definition 138. In the query

let the public row functions be exactly the local-ordinal projections of this query record:

Thus \(A\) and \(B\) are the rows produced by the split-query view, not caller-supplied functions and not independent direct lookups into \(V\). For every

Therefore

Lean-facing, the declaration \(\operatorname {lem\_ minip\_ split\_ answer\_ row\_ preservation}\) must quantify directly over these displayed local ordinal types:

Here \(A\) and \(B\) are fixed by the preceding displayed equations as \(\operatorname {SplitLeftRows}_I(V)\) and \(\operatorname {SplitRightRows}_I(V)\), the two projections of the actual query \(Q_I(V)\). The declaration has no premise asserting validity of an unrelated oracle problem instance and no parameter supplying alternate row functions. It is not enough to quantify over implementation-list indices such as \(\operatorname {Fin}(\operatorname {leftRows.length})\) and \(\operatorname {Fin}(\operatorname {rightRows.length})\) with extra caller-supplied bound hypotheses. If the rectangular query is internally stored as lists, the implementation must first expose the definitional identification of those list index types with \(U_I\) and \(W_I\), and the preservation lemma for this label must still have \(u:U_I\) and \(v:W_I\) as its public quantified variables. No hypotheses named like \(h_u\), \(h_v\), \(\operatorname {hu}\), or \(\operatorname {hv}\) may be required to turn an implementation-list index into a valid local answer index.

For every nonempty optimization history \(H\) of length \(m{\gt}0\), let

and let

Then for every history position \(1\leq s\leq m\),

Thus the concrete finish function returns a decoded candidate whose score is no larger than the score of any decoded oracle-answer candidate in the same history.

Let \(V:\{ 1,\ldots ,n\} \to \{ 0,1\} ^{\ell }\) and let \(I=(L,R)\) be an internal interval with midpoint \(M\). For every \(u\in \{ 1,\ldots ,M-L+1\} \),

Let \(V:\{ 1,\ldots ,n\} \to \{ 0,1\} ^{\ell }\) and let \(I=(L,R)\) be an internal interval with midpoint \(M\). For every \(w\in \{ 1,\ldots ,R-M\} \),

Let \(V:\{ 1,\ldots ,n\} \to \{ 0,1\} ^{\ell }\) and let \(I=(L,R)\) be an internal interval of \(\operatorname {InternalIntervals}_n\). With \(M=L+\lfloor (R-L)/2\rfloor \), the left child range \(\{ L,\ldots ,M\} \) and the right child range \(\{ M+1,\ldots ,R\} \) are both nonempty. The concrete query view

is therefore a valid rectangular input for each of \(\operatorname {BiMinIPExactSpec}\), \(\operatorname {BiMinIPGammaSpec}(\gamma )\), and \(\operatorname {BiMinIPThresholdSpec}(t)\). Its principal size and dimension are exactly

The query uses row views into the original input with the displayed index maps; it does not pad, copy to an arbitrary list, or hide validity behind an existential rectangular-input witness.

For every distinct pair of indices \(p\neq q\) in \(\{ 1,\ldots ,n\} \), there is a unique endpoint pair \((L,R)\) in the concrete filtered list \(\operatorname {InternalIntervals}_n\) of Definition 133 such that \(L\leq p,q\leq R\) and the two indices lie in different displayed children:

Equivalently, the unordered pair \(\{ p,q\} \) appears as a cross-pair in exactly one attached bichromatic query \(Q_{(L,R)}(V)\) from the canonical split-tree query schedule. The uniqueness quantifier ranges only over the recursively generated list \(\operatorname {InternalIntervals}_n\); there is no arbitrary split-tree value in the statement.

The query-schedule form of the same uniqueness is also part of the lemma. For every monochromatic input \(V:\{ 1,\ldots ,n\} \to \{ 0,1\} ^{\ell }\) and every distinct pair \(p\neq q\), there is a unique query-list position

such that, writing \(\operatorname {InternalIntervals}_n[s]=(L_s,R_s)\) and \(M_s=M(L_s,R_s)\), the query at that position is exactly

and the pair \((p,q)\) is represented in this concrete query with one index in its left row list and one index in its right row list:

If a second query-list position \(s'\) has the same property, then \(s'=s\) and hence

as the same attached rectangular bichromatic query record, not merely as the same endpoint pair. Conversely, if a query record in \(\operatorname {SplitQueries}_n(V)\) contains \((p,q)\) as such a left-right cross-pair, then its position is this unique \(s\).

More explicitly, if \((L,R)\) and \((L',R')\) are both internal intervals from \(\operatorname {InternalIntervals}_n\) satisfying the displayed separation predicate for the same pair \((p,q)\), then \(L=L'\) and \(R=R'\). If \((L,R)\) is the unique interval, the pair occurs in the query

with one index on each side, and it occurs in no other query in the query list.

Lean-facing, the formal statement for this label must expose both uniqueness results: uniqueness of the separating generated interval and uniqueness of the corresponding element of the concrete list \(\operatorname {SplitQueries}_n(V)\). It must not replace the query-list uniqueness conclusion by a second copy of endpoint-pair uniqueness, and it must not state only that some endpoint pair could be used to build a query. The query conclusion must identify the actual attached bichromatic query record, including its left vector list, right vector list, principal size, and dimension projections inherited from Definition 133.

With fixed quadratic-baseline witnesses for the monochromatic and bichromatic OV problem specifications, there are fine-grained reductions in both directions:

and

Consequently a truly subquadratic algorithm for \(\mathrm{OV}_{n,\ell }\) exists if and only if a truly subquadratic algorithm for bichromatic \(\mathrm{OV}_{n,\ell }\) exists, up to polynomial factors in \(\ell \).

For every valid monochromatic OV input \(V=(v_1,\ldots ,v_n)\), the oracle-answer correctness obligation for \(R_{\rm mono\to bi}\) is exactly branch-sensitive.

If \(n{\lt}2\), then \(r(V)=0\), the final postprocessing output is \(0\), and this is the correct monochromatic OV answer because no distinct pair of input rows exists. If \(n\geq 2\) and \(Z(V)\) is true, then \(r(V)=0\), there is no query and no oracle answer to quantify over, the final postprocessing output is \(1\), and this is the correct monochromatic OV answer.

If \(n\geq 2\) and \(Z(V)\) is false, then \(r(V)=1\) and the unique query is

In this one-query branch, and only in this branch, every correct yes/no oracle answer \(z_1\) for the bichromatic query \(q_1(V)\) is the correct yes/no answer for the original monochromatic instance \(V\). Equivalently, in the nonzero branch the final postprocessing value \(\operatorname {finish}_{R_{\rm mono\to bi}}(V,\sigma _1,H_2)=z_1\) satisfies the monochromatic OV correctness relation whenever \(z_1\) satisfies the bichromatic OV correctness relation on \(q_1(V)\).

The zero-vector branch has no proposition of the form “every correct oracle answer on \(q_1(V)\) gives the correct original answer”, because \(q_1(V)\) is not constructed there. In particular, the correctness proof must not use the self-query \((V,V)\) in the zero-vector branch, where that query could contain self-pair artefacts and is irrelevant to the reduction run.

For any fixed baseline witnesses for monochromatic \(\mathrm{OV}\) and bichromatic \(\mathrm{OV}\), the datum \(R_{\rm mono\to bi}\) satisfies

In particular, substituting any truly subquadratic bichromatic \(\mathrm{OV}\) algorithm into the composed program \(R_{\rm mono\to bi}[A_{\rm bi}]\) gives the concrete monochromatic \(\mathrm{OV}\) algorithm certified by Definition 101. More explicitly, the witness for this reduction includes the following eliminable obligations:

the zero-vector scan and copy construction have local cost at most \(C_0n(1+\ell )\), and the oracle-answer correctness obligation is exactly the branch-sensitive obligation of Lemma 110: the \(n{\lt}2\) and zero-vector branches have no query and their direct final outputs are correct, while in the nonzero one-query branch every correct oracle answer on the displayed query \(q_1(V)=(V,V)\) gives the correct monochromatic \(\mathrm{OV}\) answer. There is no universal correctness obligation for an oracle answer on \((V,V)\) in the zero-vector branch. Finally, any oracle bound \(T_Q(n',\ell ')\leq C(n')^{2-\varepsilon }(1+\ell ')^b\) transfers to a composed running-time bound \(C'n^{2-\varepsilon '}(1+\ell )^{b'}\) for fixed constants \(\varepsilon '{\gt}0,C'{\gt}0,b'\).

Suppose a bichromatic \(\mathrm{OV}\) algorithm has a semantic running-time bound

on valid bichromatic inputs. For every locally generated trace of \(R_{\rm mono\to bi}\) on a monochromatic input of size \((n,\ell )\), the composed reduction run has total time

Consequently, for every fixed \(\varepsilon {\gt}0\) there are constants \(\varepsilon '{\gt}0\), \(C'{\gt}0\), and \(b'\in \mathbb {N}\) such that the same total time is at most

for all sufficiently large \(n\). In particular, a truly subquadratic bichromatic OV solver transfers to a truly subquadratic monochromatic OV solver with only polynomial overhead in \(\ell \).

For every monochromatic OV input \(V=(v_1,\ldots ,v_n)\) with \(n\geq 2\), the two branches of \(R_{\rm mono\to bi}\) preserve the yes/no condition as follows. If \(Z(V)\) is true, then \(V\) is a yes instance of monochromatic \(\mathrm{OV}\). If \(Z(V)\) is false, then the unique query \((V,V)\) is a yes instance of bichromatic \(\mathrm{OV}\) if and only if \(V\) is a yes instance of monochromatic \(\mathrm{OV}\).

If \(\mathrm{MSD}_{n,\ell ,t}\) is truly subquadratic for every threshold \(t\), then \(\mathrm{MSD}_{n,\ell }\) is truly subquadratic.

A truly subquadratic algorithm for the approximate MSD regime of Theorem 198 would imply a truly subquadratic OV algorithm in logarithmic dimension.

For fixed \(n,\ell ,t\), evaluate the transformer on \(\operatorname {Aug}_{s_t}(E)\), where \(s_t=(0,\ldots ,0,t+2)\in \mathbb {R}^\ell \) is the raw sentinel row from Lemma 206. The input MLP maps the first \(n\) nonzero binary rows to \((v_i/\| v_i\| ,1)\) and maps the sentinel to \(\tau _t=(0,\ldots ,0,t+1)\in \mathbb {R}^{\ell +1}\). Choose \(Q,K\) so that \(QK^\top =\lambda I_{\ell +1}\) for a sufficiently large \(\lambda {\gt}0\), and choose the value vector \((1,\ldots ,1,0)\). Then yes instances of \(\mathrm{MSD}_{n,\ell ,t}\) produce some attention output at least \(1/(n+1)\), while no instances produce all attention outputs below \(1/(2(n+1))\).

If \(\gamma \)-\(\mathrm{MSD}_{n,\ell }\) in dimension \(\ell =(\log n)^{c\log n/(\log \log n)^2}\) is solvable in \(O(n^{2-\varepsilon })\) time for all constants \(c{\gt}0\) and \(\gamma \leq (1+1/\log \log n)^{\log n/(\log \log n)^2}\), then \((1+1/\log \log n)\)-\(\mathrm{MSD}_{n,(\log n)^k}\) is solvable in truly subquadratic time for every constant \(k{\gt}0\).

Fix a threshold \(t\in [0,1]\). Let the raw sentinel row be

and let the target attention-space sentinel row be

with \(\ell \) leading zero coordinates and last coordinate \(t+1\). On the finite set consisting of all nonzero binary document rows and \(s_t\), there exists a continuous \(f:\mathbb {R}^\ell \to \mathbb {R}^{\ell +1}\) such that

and

For nonzero binary document embeddings \(v,w\), if the input MLP maps document rows to \(x_v=(v/\| v\| ,1)\) and \(x_w=(w/\| w\| ,1)\), then

If the raw sentinel row is mapped to the target attention-space row \(\tau _t=(0,\ldots ,0,t+1)\) with \(\ell \) leading zeros, then \(\left\langle x_v,\tau _t\right\rangle =t+1\).

In the OV construction of Theorem 211, with raw sentinel row \(s=0^\ell \), augmented attention input \(\operatorname {Aug}_s(E)\in \mathbb {R}^{(n+1)\times \ell }\), \(QK^\top =-\lambda I_\ell \) for a concrete scale \(\lambda {\gt}0\), and \(V\) the all-one column, the \(i\)th attention output for every document row \(1\leq i\leq n\) equals

Fix \(\gamma \geq 1\) and one active source branch of Definition 122. Suppose the active exact or \(\gamma \)-approximate Min-IP program is a correct algorithm with semantic worst-case bound \(T_{\min }\), and suppose there are constants \(\varepsilon {\gt}0\), \(C{\gt}0\), \(b\in \mathbb {N}\), and \(n_0\) such that

for every \(n\geq n_0\) and every allowed dimension \(\ell \).

Then the concrete induced OV program

from Definition 122 has the explicit inherited running-time certificate

consisting of exactly the following data and facts:

a proof that \(T_{\mathrm{OV}}^R\) is a semantic worst-case running-time bound for the actual first-halting execution of the same program \(A_{\mathrm{OV}}^R\), and constants

together with a constant \(C'{\gt}0\) and threshold \(n_0'\) such that

for every \(n\geq n_0'\) and every allowed dimension \(\ell \).

This certificate is part of the conclusion, not a hypothesis. The worst-case-bound proof is derived from the branch-specific first-halting-time equations of Lemma 128; the subquadratic inequality is derived from the displayed bound on \(T_{\min }\). The same constructed program \(A_{\mathrm{OV}}^R\) appears in the correctness certificate, the worst-case-bound certificate, and the truly subquadratic certificate. Lean-facing, a declaration for this node must return the tuple

with the displayed meanings. It must not assume \(\operatorname {def\_ truly\_ subquadratic}(T_{\mathrm{OV}})\) for an arbitrary externally supplied \(T_{\mathrm{OV}}\), and it must not prove only branch-local inequalities without producing the global worst-case bound \(T_{\mathrm{OV}}^R\) for \(A_{\mathrm{OV}}^R\).

Let \(R\) be the concrete reduction datum of Definition 122. The running-time statement is a branch-by-branch theorem about the induced OV program \(R_{\mathrm{Min\mbox{-}IP}\to \mathrm{OV}}[A_{\min }]\), not an assumption about an externally supplied \(T_{\mathrm{OV}}\).

In the exact branch, suppose \(A_{\rm exact}\) has semantic worst-case bound \(T_{\min }\) in the sense of Definition 47. Then for every valid OV input \(V\) with \(n\geq 2\), the first halting time of the induced OV program on \(V\) is exactly

where \(s_{\rm exact}(V)\) is the first halting time of \(A_{\rm exact}\) on the exact Min-IP input \(V\), and its halted output is \(\operatorname {ExactOutPair}_R(V)\). Therefore

In the \(\gamma \) branch, suppose \(A_{\gamma }\) has semantic worst-case bound \(T_{\min }\) on \(\gamma \)-\(\mathrm{Min\mbox{-}IP}\) inputs. Then for every valid OV input \(V\) with \(n\geq 2\), the first halting time of the induced OV program on \(V\) is exactly

where \(s_{\gamma }(V,\gamma )\) is the first halting time of \(A_{\gamma }\) on the approximate input \((V,\gamma )\), and its halted output is \(\operatorname {GammaOutPair}_R(V)\). Therefore

In the small-input branch \(n{\lt}2\), the induced OV program makes no Min-IP call and halts within the same absolute overhead constant \(C_1\). Hence the total worst-case bound for the constructed OV program is the concrete function

for \(n\geq 2\), with the constant branch bound for \(n{\lt}2\). If

for some \(\varepsilon {\gt}0\), then this displayed constructed bound \(T_{\mathrm{OV}}^R\) is truly subquadratic in \(n\) up to polynomial factors in \(\ell \), after decreasing the exponent and increasing the polynomial factor if necessary.

Lean-facing, this lemma must expose the two branch conclusions above. It must derive the \(T_{\mathrm{OV}}^R\) bound from the first-halting time of the active Min-IP program plus \(\operatorname {LocalScanSteps}_R(V)\) and \(C_1\). It must not take as hypotheses a predicate named \(\operatorname {runtime\_ accounting}\), an assumed inequality for an arbitrary \(T_{\mathrm{OV}}\), or a small-input bound for an externally supplied OV solver. In the \(\gamma \) branch, every halting fact and every scan equation must use \(\operatorname {GammaOutPair}_R(V)\), not \(\operatorname {ExactOutPair}_R(V)\) or any field named \(\operatorname {exactPair}\).

If the OV instance has no orthogonal pair, then every attention output entry in the OV construction is at most \(n\ell \exp (-\lambda )\). In particular, if \(\lambda \) is chosen so that \(n\ell \exp (-\lambda ){\lt}1/(2(n+1))\), then every no-instance output entry is below \(1/(2(n+1))\).

If the OV instance has an orthogonal pair, then some attention output entry in the OV construction is at least \(1/(n+1)\).

If \(A\) is a correct algorithm for \(P\) with worst-case running-time bound \(T\), then for every valid promised input \(x\), \(A(x)\) halts within \(T(N_P(x),L_P(x))\) steps and \(\Correct _P(x,A(x))\) holds.

If \(\operatorname {ValidBOW}_{\mathsf{doc}}(D,K,E)\) holds, then for every \(i\in \{ 1,\ldots ,n\} \) and \(r\in \{ 1,\ldots ,\ell \} \),

If \(\operatorname {ValidBOW}_{\mathsf{doc}}(D,K,E)\) holds, then for every \(i\in \{ 1,\ldots ,n\} \) and \(r\in \{ 1,\ldots ,\ell \} \),

If \(\operatorname {ValidBOW}_{\mathsf{doc}}(D,K,E)\) holds, then for every \(i\in \{ 1,\ldots ,n\} \) and \(r\in \{ 1,\ldots ,\ell \} \), exactly the concrete occurrence decision for \((D(i),K(r))\) determines the entry value:

If \(\operatorname {ValidBOW}_{\mathsf{doc}}(D,K,E)\) holds, then for every \(i\in \{ 1,\ldots ,n\} \) and \(r\in \{ 1,\ldots ,\ell \} \),

If \(\operatorname {ValidBOW}_{\mathsf{doc}}(D,K,E)\) holds, then for every \(i\in \{ 1,\ldots ,n\} \) and \(r\in \{ 1,\ldots ,\ell \} \),

If bichromatic \((\log n)\)-Additive-Max-IP in dimension \(c\log n\) is truly subquadratic for every constant \(c{\gt}0\), then \(\mathrm{OV}_{n,c'\log n}\) is truly subquadratic for every constant \(c'{\gt}0\), contradicting OVC and SETH.

Assuming SETH, for every \(\varepsilon {\gt}0\) there exists \(c{\gt}0\) such that bichromatic \(\mathrm{MSD}_{n,\ell }\) cannot be solved in \(O(n^{2-\varepsilon })\) time when \(\ell =c\log n\).

The least-similar-document problem and its listed variants require quadratic time under SETH in the logarithmic-dimensional regime stated in the introduction.

The most-similar-document problem and its threshold and approximation variants require quadratic time under SETH in the quasipolylogarithmic-dimensional regime stated in the introduction.

A single unit of standard attention with input and output MLPs and embedding dimension \(\ell +1\) solves \(\mathrm{OV}_{n,\ell }\), \(\mathrm{MSD}_{n,\ell ,t}\), and \(\mathrm{LSD}_{n,\ell ,t}\) for every \(0\leq t\leq 1\) under the explicit sentinel-augmented input encoding of Definition 41.

Approximate \(\mathrm{Max\mbox{-}IP}\) in the parameter ranges used by Appendix B is hard under OVC/SETH.

If \((1+1/\log \log n)\)-\(\mathrm{MSD}_{n,(\log n)^k}\) is truly subquadratic for every constant \(k{\gt}0\), then bichromatic \((\log n)\)-Additive-Max-IP in dimension \(c\log n\) is truly subquadratic for every constant \(c{\gt}0\).

Assuming SETH or OVC, for every \(\varepsilon {\gt}0\) there exists a constant \(c{\gt}0\) such that for every \(\gamma \geq 1\), \(\gamma \)-\(\mathrm{LSD}_{n,\ell }\) cannot be solved in \(O(n^{2-\varepsilon })\) time when \(\ell =c\log n\).

Assuming SETH or OVC, for every \(\varepsilon {\gt}0\) there is a constant \(c{\gt}0\) such that \(\gamma \)-\(\mathrm{MSD}_{n,\ell }\) cannot be solved in \(O(n^{2-\varepsilon })\) time when

If SETH holds, then OVC holds.

An attention unit with input and output MLPs and parameters \(d=\ell \), \(d_{\rm in}=\ell +1\), \(d_{\rm out}=1\), \(m\geq \ell +1\), and the raw sentinel row \(s_t=(0,\ldots ,0,t+1)\in \mathbb {R}^\ell \) solves \(\mathrm{Max\mbox{-}IP}_{n,\ell ,t}\) and \(\mathrm{Min\mbox{-}IP}_{n,\ell ,t}\) for \(1\leq t\leq \ell \) in the sentinel-augmented sense of Definition 41.

An attention unit with input and output MLPs and parameters \(d=\ell \), \(d_{\rm in}=\ell +1\), \(d_{\rm out}=1\), \(m\geq \ell +1\), and the raw sentinel row \(s_t=(0,\ldots ,0,t+2)\in \mathbb {R}^\ell \) solves \(\mathrm{MSD}_{n,\ell ,t}\) and \(\mathrm{LSD}_{n,\ell ,t}\) for every \(t\in [0,1]\) in the sentinel-augmented sense of Definition 41.

An attention unit with input and output MLPs and parameters \(d=\ell \), \(d_{\rm in}=\ell \), \(d_{\rm out}=1\), \(m\geq \ell +1\), and one fixed raw sentinel row \(0^\ell \) solves \(\mathrm{OV}_{n,\ell }\) in the sentinel-augmented sense of Definition 41.