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

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.

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.

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.

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.

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.

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

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

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

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.

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.

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

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

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

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.

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.

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

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

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

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

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.

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

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.

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.

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.

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.

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

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

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.

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

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.

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.

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.

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.

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

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

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.

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.

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

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.

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

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.

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.

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.

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

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.

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.

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

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

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.

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.

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

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.

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.

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

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.

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

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

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.

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

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

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

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.

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

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