A Quantum Roadmap for Softmax Attention: Exact Born-Rule Analogs for Softmax Attention on the Probability Simplex

A Quantum Roadmap for Softmax Attention: Exact Born-Rule Analogs for Softmax Attention on the Probability Simplex Eric A. F. Reinhardt1 and Adam J. Hauser1 1 Department of Physics and Astronomy University of Alabama, Tuscaloosa, AL 35487, USA eareinhardt@crimson.ua.edu

arXiv:2608.11173v1 [quant-ph] 11 Aug 2026

August 12, 2026

Abstract The attention mechanism forms the foundation of many modern AI models such as the Transformer. In one subclass of problems where attention is used, inputs and outputs are bound to the probability simplex so that all outputs sum to one. In this setting, softmax attention admits an exact, component-by-component quantum realization. Attention scores are Hadamard-test statistics on block-encoded projections of amplitude-encoded inputs. The exponential softmax is the interior of a cosine-squared family generated by Born-rule measurement under an exact bijection, whose boundary expresses sparse attention with exact zeros at finite parameter values. The softmax temperature is a repetition count where post-selected measurement rounds realize discretized inverse temperature exactly. Value aggregation is a deterministic column-loading channel that dilates the column-stochastic value matrix. The gated residual is the preparation angle of a single ancilla, with the additive identity at a mixing angle of π/2. Every learnable parameter is a rotation-gate angle. The composed layer is exact in the infinite-shot limit with one measure-and-reload step per attention score; a fully-coherent variant is ε-approximate via quantum singular value transformation in the infinite depth limit. The algebraic core is machine-checked in Lean 4.

1

Introduction

Transformer self-attention [1] has become the dominant architecture in modern machine learning, underlying state-of-the-art large language models and a growing fraction of vision, audio, and scientific-computing systems. Its central operation is dot-product attention with a softmax nonlinearity over inner-product scores, an additive residual connection [2, 3] between sublayer input and output, and a value aggregation step. The success of this architecture has motivated extensive theoretical and empirical studies of its components, including alternatives to the exponential softmax [4, 5]. Quantum machine learning [6, 7] offers an orthogonal computational substrate. Variational quantum circuits operate natively on the unit sphere of a complex Hilbert space, with the Born rule supplying probability normalization without an explicit projection step. This is suggestive: classical transformer attention enforces the simplex structure of its output by applying a softmax, while a quantum circuit’s output lives on the simplex by construction. Special cases of full attention bound the total output of the model to a probability simplex or a collection of simplices where all outputs are enforced to sum to one. This probability simplex setting is actively studied classically: 1

|0⟩S

|0⟩

|i, j⟩

|i⟩A

|0⟩h(ℓ)

Uattn (θ i )

(ℓ) Ry (θij )

|0⟩h

H

H ṼQ /ṼK

|0⟩B

L post-selected rounds

Yiout

=

cos2 η2 xi

+

sin2 η2

X

softmaxj β ⟨qi |kj ⟩ WV xj

j |0⟩ |0⟩C |X⟩

Ry (η)

|j⟩S

H |0⟩B ′

Ufull

|0⟩BV

Uenc UV

Figure 1: The dictionary at a glance: the gated single-head attention layer on the probability simplex, √ √ annotated with the circuit realizing each component (qi ∝ WQ xi , kj ∝ WK xj ; at η = π/2, β = 1 2 the formula reduces to Eq.
1 under the conventions of Remark 2). Softmax: compiled cos Born readout zij /2 with θij = 2 arccos e (Proposition 12); temperature: L post-selected rounds (Corollary 17); scores: Hadamard test (Lemma 9); gating and residual: single-ancilla preparation angle (Theorem 24); values: column-loading channel (Theorem 23).

flow matching on Riemannian manifolds [8, 9] extends naturally to the simplex via the Fisher–Rao metric, Dirichlet flow matching [10] parameterizes simplex-valued generative dynamics directly, and continuous diffusion for categorical data [11] operates on simplex-valued representations of discrete tokens. Whether the structural alignment between this regime and quantum amplitude encoding yields a faithful quantum analogue of transformer attention, and at what operational cost, is the question this paper addresses for the single-head case. Related work on quantum attention. Several recent constructions implement transformer attention as a quantum circuit. Cherrat et al. [12] build quantum vision transformers from parametrized orthogonal layers and matrix-loading circuits, with one variant realizing attention via compound matrices. QSAN [13] replaces classical inner-product similarity with a quantumlogic similarity and represents attention scores as a density matrix produced by circuit evolution. QCSAM [14] realizes self-attention via complex linear combinations of unitaries (LCU) with complex-valued attention weights. Guo et al. [15] give a fault-tolerant route in which self-attention, residual, and feed-forward layers are computed entirely by block-encoded quantum linear-algebra subroutines on amplitude-encoded inputs. None of these works states the cosine-squared / exponential softmax bijection on the simplex interior, characterizes the additive residual as a π/2 slice of a single-ancilla LCU family, or assembles these into an exact single-head equivalence theorem; the construction we present is complementary to and distinct from these prior architectures. Contributions. We give a self-contained construction of a single-head gated transformer attention layer in a probability-space setting compatible with quantum amplitude encoding. The construction is built from six primitives: amplitude encoding, block-encoded query/key projections [16, 17], coherent inner-product computation via the Hadamard test, a softmax map realized by Born-rule readout of controlled-Ry rotations (denoted cRy , where Ry (θ) = e−iθY /2 is the singlequbit Y -axis rotation), value aggregation via a controlled column-loading channel (a Stinespring 2

dilation of the column-stochastic WV ), and a gated single-ancilla residual realized by a LCU [18] with parameterized ancilla preparation. Three consequences of this construction are notable: 1. Cosine-squared softmax is isomorphic to exponential softmax on the simplex interior, and strictly extends it at the boundary. We prove the angle-score bijection
z/2 θ = 2 arccos e realizes the equality of the two softmax maps pointwise on the open simplex. At the boundary, the cosine-squared family expresses exact zeros (sparse attention) at finite parameter values, which the exponential family cannot reach with bounded scores. 2. The classical additive residual identity is the η = π/2 special case of a parameterized single-ancilla construction. A single ancilla prepared in cos(η/2)|0⟩ + sin(η/2)|1⟩, controlledU , Hadamard, and post-select-|0⟩ produces the normalized linear combination cos(η/2)|X⟩ + sin(η/2)U |X⟩, recovering the no-residual (η = 0), additive (η = π/2), and full-sublayer (η = π) cases as specific gate-angle settings. 3. The softmax temperature is measurement repetition. L identical rounds of the postselected Born stage realize exp-softmax at inverse temperature β = L exactly, and positive measurement weights summing to β realize any real temperature (Theorem 16, Corollary 17); the temperature axis, a hyperparameter classically, is a physical repetition count in the quantum realization. Figure 1 annotates the layer formula with the circuit realizing each component; Table 1 in Section 13 collects the full component-by-component dictionary, with the exactness status and certifying result for each entry. The headline algebraic content (the angle-score bijection, the boundary strict extension, the multi-stage post-selection identity with its inverse-temperature generalization, the gated singleancilla circuit, the Hadamard-test amplitude algebra, the stochastic-value-channel diagonal identity, and the polynomial-exponential impossibility behind the coherent no-go) is machine-checked in Lean 4 [19, 20] against the mathlib library. The corresponding theorem statements and their full proofs are embedded with each result. A successful Lean kernel build is the type-theoretic certificate that every embedded theorem holds; the machine-checked artifacts complement the human-readable exposition. Scope and limitations. Two restrictions are essential to the construction. First, the inputoutput domain is the probability simplex (or its Born-rule lift to the positive orthant of the unit sphere), not generic feature space; this matches the natural setting for quantum amplitude encoding and resolves several normalization issues that would otherwise complicate the equivalence. Second, the construction uses one measure-and-reload step per attention scoring: the Hadamardtest outcome zij is sampled, a classical function is applied to obtain the controlled-Ry rotation
angle θij = 2 arccos ezij /2 , and θij is reloaded as a gate parameter for the softmax step. Measureand-reload is a standard quantum-classical interface pattern, the same mechanism used in adaptive measurements, magic-state distillation, and quantum error correction. The overhead it introduces (statistical noise from finite shots, classical-control latency, mid-circuit measurement) is in principle separately optimizable, e.g., via amplitude estimation, low-latency control electronics, or parallel state preparations. The equivalence is exact in the infinite-shot limit; a fully-coherent alternative that removes the measure-and-reload step is ε-approximate via QSVT polynomial dressing (Theorem 20). Exact finite-depth fully-coherent realization without measure-and-reload is provably impossible for affinely-encoded scores within the QSVT circuit family (Theorem 19). The construction also relies on standard variational-circuit expressivity assumptions: specifically, that a sufficiently 3

deep hardware-efficient rotation-CRY circuit class realizes a dense subset of SU (2b+1 ), hence of contractions on the data register. The underlying gate set (arbitrary single-qubit rotations together with an entangling two-qubit gate on a connected coupling graph) is universal [21, 22]; Schuld, Sweke, and Meyer [23] give the complementary function-space statement that data-reuploading circuits realize truncated Fourier series and are universal approximators on bounded domains. We adopt the density as an architectural assumption on the finite-depth family rather than a free claim; the variational realization of the block-encoded W family (Construction 7, Lemma 8) is conditional on this density. The equivalence theorem itself does not require it: the dilation unitary of Lemma 4 admits an exact decomposition into rotation gates and CNOTs by standard synthesis [24], so exactness rests only on the infinite-shot limit of the measure-and-reload step. Organization. Section 2 establishes notation, the probability-space assumption, and the quantum register layout. Section 3 defines the Born-rule encoding. Section 4 introduces block-encoded unitary projections. Section 5 treats coherent inner-product computation. Section 6 establishes the cosine-squared softmax via Born-rule normalization, proves the interior isomorphism with exponential softmax, and characterizes the boundary strict-extension behavior. Section 7 treats value aggregation, and Section 8 establishes the gated single-ancilla LCU residual circuit. Section 9 states the single-head master equivalence theorem. Section 10 discusses the formal verification. Section 11 examines the architectural status of the construction. Section 12 discusses practicality and big-O notation scaling behavior for the construction. Section 13 discusses implications, and Section 14 concludes.

2

Setup and assumptions

2.1

Classical single-head attention with residual

In standard transformer architectures, multi-head attention concatenates several independent singlehead computations, each with its own learned WQ , WK , WV . The construction in this paper treats a single head; extension to multi-head is the obvious parallel composition (one set of variational parameters and one set of ancilla registers per head). We use the unqualified term “attention” throughout to refer to single-head attention. For input X ∈ Rn×d with rows xi , the classical single-head self-attention layer with residual computes Qi = WQ xi ,

Ki = WK xi ,  ⊤  Qi Kj Aij = softmaxj √ , d X Yi = Aij Vj ,

Vi = WV xi ,

(1) (2) (3)

j

Yiout = 12 (Yi + xi ).

2.2

(4)

Probability simplex setting

n×d are row-normalized probability Assumption 1 (Probability-space attention). Inputs PX ∈ R √ d−1 distributions: each row xi ≥ 0 component-wise and j xij = 1. The amplitude lift xi ∈ S+ lies on the positive orthant of the unit sphere. The value matrix WV is column-stochastic (each column is a probability vector), so that Vj = WV xj remains on the simplex.

4

This assumption matches the natural setting for quantum amplitude encoding of probability data (e.g., images interpreted as probability distributions under the Born rule) and resolves three potential issues simultaneously: row-normalization is automatic; the mixed-state output of partial trace is directly the desired probability vector; the LCU residual operates on the same simplex as the classical residual. Remark 2 (Lifted-feature, normalized-score, and row-shift conventions). Three conventions connect Eq. 1 to the quantum primitives that follow. (i) Lifted features. The block-encoded projec√ tions act on the amplitude lift: the circuit computes WQ xi (componentwise square root), not WQ xi . Throughout, Eq. 1 is therefore read with the convention that the feature vector presented √ to the projections is the lift xi ; equivalently, the classical layer is defined on the amplitude (Hellinger) representation of each simplex point. (ii) Normalized scores. Post-selected block encodings output normalized states, so the Hadamard test of Lemma 9 returns the normalized overlap zij = Re⟨qi |kj ⟩ with ∥qi ∥ = ∥kj ∥ = 1; the score in Eq. 1 is read as this normalized bilinear form. √ The input-dependent norms ∥W∗ xi ∥ are observable as block-encoding post-selection rates and can √ be reintroduced classically if unnormalized scores are required, at additional shot cost. The 1/ d temperature is a fixed scalar absorbed into the classical conversion of the measure-and-reload step; equivalently, it can be realized physically as post-selected measurement weight
(Corollary 17). (iii) Row shift. The overlap zij ∈ [−1, 1] can be positive, while θ = 2 arccos ez/2 requires z ≤ 0; the reload step therefore first applies the softmax-invariant row shift zij 7→ zij −maxl zil . Operationally, all n scores of row i are collected before any angle for that row is reloaded.

2.3

Quantum registers

Set a = ⌈log2 n⌉, b = ⌈log2 d⌉. The construction uses register

qubits

role

A, A′ BQ , BK B′ BV ancQ , ancK S h h(ℓ) C

a each b each b b 1 each, recyclable via reset a 1 1, reused 1

token query, key indices per-token feature amplitudes (score pathway) value-channel feature register, traced out (may recycle BK ) value-channel output; diagonal carries Yi block-encoding ancillas (the value channel needs none) attention-weight register overlap (Hadamard-test) ancilla, reusable Trotter post-selection ancilla residual gating ancilla (the single ancilla)

3

Encoding (Born-rule lift)

Definition 3 (Sequence-amplitude encoding). Define |X⟩AB ∈ HA ⊗ HB by n−1

1 X |X⟩AB = √ |i⟩A ⊗ |xi ⟩B , n i=0

|xi ⟩B =

d−1 X √

xij |j⟩B .

(5)

j=0

The state preparation is unitary; the marginal over A is uniform 1/n, and the conditional state on B given outcome i is the unit-amplitude lift of token xi .

5

|0⟩ |0⟩. .. |0⟩

B xi

|xi ⟩B

Figure 2: Born-rule encoding diagram.

P The Born-rule simplex constraint i |αi |2 = 1 replaces the classical softmax simplex projection automatically: |xi ⟩B is unit-norm by construction. This is visualized in fig. 2 where B represents the Born-rule lift operation state preparation unitary.

4

Q, K projections via block encoding

The classical WQ is a generic real matrix; a unitary VQ maps unit vectors to unit vectors. To realize a generic W as the action of a unitary on the encoded subspace, we use block encoding (see fig. 3). Lemma 4 (Block-encoded unitary). For any W ∈ Rd×d with ∥W ∥op ≤ 1, there exists a unitary V ∈ U (2b+1 ) on b + 1 qubits (with W zero-padded to dimension 2b when d < 2b ) such that ⟨0|anc ⊗ ⟨s′ |B · V · |0⟩anc ⊗ |s⟩B = Ws′ s ,

(6)

i.e., the upper-left d × d block of V equals W .   W ∗ exists for any W with ∥W ∥op ≤ 1; the ∗ blocks are constructed by orthogProof. V = ∗ ∗ onalizing rows/columns to make V V † = I. The operator-norm bound is enforced classically by absorbing a scale factor: encode W/∥W ∥op and store the scale as a classical multiplier on the readout. Corollary 5 (Q, K via block encodings). For classical weight matrices WQ , WK , there exist unitaries ṼQ , ṼK (on b + 1 qubits each, one block-encoding ancilla per matrix) such that, when applied to the encoded input, (⟨0|anc∗ ⊗ IB )Ṽ∗ (|0⟩anc∗ ⊗ |xi ⟩B ) = W∗ |xi ⟩B , (7) for ∗ ∈ {Q, K}, i.e., the post-selected B-register state is the linear action of W∗ on the encoded P √ amplitude vector |xi ⟩B = j xij |j⟩. The value matrix WV is deliberately not realized by block √ encoding: the score pathway needs the amplitude-level states W∗ xi , which block encoding provides, whereas value aggregation needs the probability-level WV xj , which it cannot provide (Construction 22); the column-stochastic WV is instead realized exactly as a quantum channel in Section 7. Remark 6 (Parallel projection). Applying ṼQ on B ⊗ ancQ acts in parallel on every |xi ⟩ in the superposition: a classical projection cost of Θ(nd2 ) is replaced by a single unitary application whose gate-count and depth depend on the structure of WQ via the chosen block-encoding scheme; for a generic dense WQ the depth scales polynomially in d, while sparse or structured WQ admit polylog(d)-depth implementations.

6

|0⟩ |0⟩anc∗ |xi ⟩. ..

Ṽ∗

W∗ |xi ⟩

Figure 3: Q, K projection diagram.

4.1

Variational realization via rotation-CRY ansatz

Lemma 4 guarantees a unitary V realizing W as its upper-left block, but is non-constructive. The implementation uses a parameterized circuit family that makes the construction explicit and trainable. Construction 7 (Hardware-efficient rotation-CRY ansatz). On b + 1 qubits (data register B plus one block-encoding ancilla), define UL (Θ) by L repetitions of the layer 1. Per-qubit Rot(φl,q , θl,q , ωl,q ) = Rz (ωl,q ) Ry (θl,q ) Rz (φl,q ) for q ∈ {0, . . . , b}; 2. Anchor entanglers CRY(αl,q ) with ancilla controlling each data qubit q ∈ {0, . . . , b − 1}; 3. Brick entanglers CRY(βl,q ) data q → q + 1 for q ∈ {0, . . . , b − 2}, followed by a final layer of per-qubit Rot. Define the variational block-encoded operator WL (Θ) := (⟨0|anc ⊗ IB ) UL (Θ) (|0⟩anc ⊗ IB ). Lemma 8 (Variational realization of the block-encoded operator). The family {WL (Θ)}L,Θ has the following properties. 1. Validity. For every L and every Θ, ∥WL (Θ)∥op ≤ 1, so WL is a valid block-encoded operator in the sense of Lemma 4. 2. Identity at the origin. UL (0) = I2d and WL (0) = Id . 3. Density. For every contraction W ∈ Cd×d with ∥W ∥op ≤ 1 and every ε > 0, there exist Lε ∈ N and parameters Θε such that ∥WLε (Θε ) − W ∥op < ε. Proof. Part (1) is immediate: the top-left block of any unitary in U (2d) acts as a contraction on Cd — for unit X ∈ Cd , lifting to Y = (X, 0) ∈ C2d gives ∥Y ∥ = 1 and ∥UL Y ∥ = 1 (unitarity), so by Pythagoras ∥WL X∥2 = ∥P0 UL Y ∥2 ≤ ∥UL Y ∥2 = 1. Part (2) is algebraic: Ry (0) = Rz (0) = I2 (from cos 0 = 1, sin 0 = 0, e0 = 1) and CRY(0) = I4 identically, so each gate at zero parameter is identity and their product on b + 1 qubits is I2d . Hence WL (0) = (⟨0|anc ⊗ IB )I2d (|0⟩anc ⊗ IB ) = Id . The algebraic core of part (2) is Lean-verified below. Part (3) is the density of the variational family in the closed unit ball of d × d contractions. The gate set generating each layer (arbitrary single-qubit rotations plus CRY entanglers on a connected coupling graph) is universal [21, 22], so the rotation-CRY family {UL (Θ)} is dense in SU (2b+1 ) in the operator-norm topology as L → ∞. By unitary-dilation (Sz.-Nagy–Halmos) surjectivity, the top-left d × d block of U (2d) traces out exactly the closed unit ball of contractions in Cd×d , hence {WL } is dense in this ball. Density is a topological / Lie-group statement and is not formalized in Lean here. The ancilla’s per-qubit Rot gates are essential: without them, the ancilla would remain in |0⟩ throughout, post-selection would succeed with probability 1, and WL ≡ I for every parameter setting. The anchor CRY gates combined with ancilla rotations are precisely what gives the variational family access to non-trivial contractions. 7

The Lean-verified algebraic core of part (2): the constituent gates at zero parameters are identity operations on every qubit state. theorem applyRy_zero (x : Qubit) : applyRy 0 x = x := by simp [applyRy] theorem applyRz_zero (x : Qubit) : applyRz 0 x = x := by simp [applyRz] theorem applyRot_zero (x : Qubit) : applyRot 0 0 0 x = x := by unfold applyRot rw [applyRz_zero, applyRy_zero, applyRz_zero] theorem applyCRy_zero (control : Fin 2) (target : Qubit) : applyCRy 0 control target = target := by unfold applyCRy by_cases h : control = 1 all_goals simp [h, applyRy_zero] theorem variational_origin_is_identity (control : Fin 2) (x : Qubit) : applyRot 0 0 0 (applyCRy 0 control x) = x := by rw [applyCRy_zero, applyRot_zero]

5

Pairwise overlaps via Hadamard test

The attention score inner product of queries and keys zij = Re⟨qi |kj ⟩ is extracted from the encoded states by a state-overlap Hadamard test on a shared data register (see fig. 4) [25]. Lemma 9 (State-overlap Hadamard test). Let B be a single data register, h a single-qubit ancilla, and let ctrl-prepij denote the unitary that, conditioned on token indices |i⟩A |j⟩A′ , loads |qi ⟩B when the ancilla is |0⟩h branch and |kj ⟩B on the |1⟩h branch. The circuit Hh · ctrl-prepij · Hh applied to |i, j⟩|0⟩B |0⟩h produces
|i, j⟩ ⊗ 21 |0⟩h (|qi ⟩ + |kj ⟩)B + |1⟩h (|qi ⟩ − |kj ⟩)B , (8) with marginal probability |0⟩h Pij (|0⟩h ) = 14 |qi ⟩ + |kj ⟩

2

= 12 1 + Re⟨qi |kj ⟩ .

(9)

Proof. Starting from |0⟩h |0⟩B , the first Hh produces √1 (|0⟩h + |1⟩h ) ⊗ |0⟩B . 2

Applying ctrl-prepij branch-by-branch yields √12 (|0⟩h |qi ⟩B + |1⟩h |kj ⟩B ), and the second Hh gives the displayed branch decomposition. The marginal |0⟩h probability is the squared norm of the |0⟩h -branch data coefficient:
1 2 2 2 1 1 1 ∥ |q ⟩ + |k ⟩ ∥ = (2 + 2 Re⟨q |k ⟩) = ∥q ∥ + ∥k ∥ + 2 Re⟨q |k ⟩ = 2 (1 + Re⟨qi |kj ⟩), i j i j i j i j 4 4 4 where the last equality uses ∥qi ∥2 = ∥kj ∥2 = 1. 8

|0⟩h |0⟩B .. .

H

H ∝ |qi ⟩+|kj ⟩ on h=0 branch

ctrl-prepij

Figure 4: Hadamard-/swap-test diagram.

Remark 10 (Oracle status of ctrl-prep and the composed variant). Lemma 9 treats ctrl-prepij as an oracle for the normalized states |qi ⟩, |kj ⟩. In the composed circuit these are post-selected blockencoding outputs, and post-selection cannot be nested inside a controlled unitary. The operational circuit instead applies controlled-ṼQ and controlled-ṼK (which are unitaries) and post-selects the block-encoding ancilla once at the end; conditional on that success, the ancilla marginal becomes ! √ 2 aq ak Re⟨qi |kj ⟩ 1 √ Pij (|0⟩h ) = 1+ , aq = ∥WQ xi ∥, ak = ∥WK xj ∥, (10) 2 2 2 aq + ak with |qi ⟩, |kj ⟩ normalized as in the lemma. The norms a2q , a2k are separately observable as singlebranch post-selection rates (Remark 2(ii)), so the normalized score zij = Re⟨qi |kj ⟩ is classically recoverable within the same measure-and-reload step, at additional shot cost. The lemma as stated is the idealized oracle form; the composed form differs from it only by this classically invertible reweighting. A SWAP-test variant on separate registers BQ , BK (using Hh · CSWAPh→(BQ ,BK ) ·Hh ) yields instead P (|0⟩h ) = 12 (1 + |⟨qi |kj ⟩|2 ), the squared overlap. For real-amplitude states such as those arising from amplitude encoding of probability vectors, ⟨qi |kj ⟩ is real, so squared-overlap and signedoverlap differ by a sign that the SWAP test discards; the controlled-prep variant in Lemma 9 is 2 ) is the desired output. therefore the appropriate route when the score zij = ⟨qi |kj ⟩ itself (and not zij √ 2 The algebraic identity |(1 + z)/ 2| = (1 + 2 Re(z) + |z|2 )/2, formalized in Lean below, √ is a partial step in this calculation: it gives the squared norm of the scalar combination (1 + z)/ 2. The full Hadamard-test probability 12 (1 + Re(z)) follows from this identity together with unitarity, which contributes a −|z|2 term from the |1⟩h -branch component that cancels the |z|2 in the algebraic identity. theorem hadamard_amplitude_squared (z : C) : Complex.normSq (((1 : C) / (Real.sqrt 2 : C)) * (1 + z)) = (1 + 2 * z.re + Complex.normSq z) / 2 := by have h_sqrt : (Real.sqrt 2) ^ 2 = 2 := Real.sq_sqrt (by norm_num : (2:R) ≥ 0) have h_norm : Complex.normSq ((1 : C) / (Real.sqrt 2 : C)) = 1 / 2 := by rw [Complex.normSq_div, Complex.normSq_one, Complex.normSq_ofReal] rw [show ((Real.sqrt 2) * (Real.sqrt 2)) = 2 by rw [← sq]; exact h_sqrt] rw [Complex.normSq_mul, h_norm] have h_expand : Complex.normSq (1 + z) = 1 + 2 * z.re + Complex.normSq z := by rw [Complex.normSq_apply] simp [Complex.add_re, Complex.add_im, Complex.one_re, Complex.one_im, Complex.normSq_apply]

9

|i⟩A |0⟩⊗a S

Uattn (θ i )

j ∼ P (j | i)

Figure 5: Quantum attention diagram.

ring rw [h_expand] ring

6

Born-rule normalization is a softmax

Definition 11 (Quantum attention map). Let θij be an angle parameter, supplied either by the measure-and-reload step (Theorem 27) or as a free learnable parameter (Theorem 14). Define the unitary Uattn on HA ⊗ HS by X X Uattn |i⟩A |0⟩S = |i⟩A e aij |j⟩S , |e aij |2 = 1. (11) j

j

Proposition 12 (cos2 -softmax). For controlled-Ry rotation angles θij on S indexed by A, with e aij ∝ cos(θij /2), the Born-rule attention pattern is cos2 (θij /2) P (j | i) = P 2 ℓ cos (θiℓ /2)

(12)

which is row-stochastic by construction (Born-rule simplex). Proof. The angles θij are classical at compile time (reloaded measure-and-reload outputs, or free p P 2 parameters), so the normalized amplitudes e aij = cos(θij /2) ℓ cos (θiℓ /2) are classically computable, and Uattn is compiled as an i-controlled state preparation realizing them on the a-qubit register S (a standard rotation-tree synthesis with O(n) gates per row); no post-selection is inP volved. Born-rule readout of S then returns j with probability |e aij |2 = cos2 (θij /2)/ ℓ cos2 (θiℓ /2), the boxed pattern. An alternative realization applies a literal controlled-Ry (θij ) per branch on a fresh ancilla and post-selects; see Remark 18. We represent this by a single unitary shown in fig. 5.

6.1

cos2 - and exp-softmax: isomorphism on the interior, strict extension on the closure

The two softmax forms agree on the interior of the simplex but differ at the boundary. We make both statements precise. Theorem 13 (Interior isomorphism). On the interior of the row-stochastic simplex (where every entry satisfies Aij > 0 strictly), the cos2 -softmax and exp-softmax distribution families are equal as sets, related by the angle-score bijection   θij = 2 arccos ezij /2 , zij = 2 logcos(θij /2), (13) 10

defined for zij ∈ (−∞, 0] and θij ∈ [0, π]. Under this bijection, the single-stage cos2 -softmax exactly equals the exp-softmax pointwise: cos2 (θij /2) ezij P P . = 2 zil l cos (θil /2) le

(14)

Proof. Substituting cos2 (θij /2) = ezij into the cos2 -softmax form gives the exp-softmax form directly. The map is a bijection on the open domain zij ∈ (−∞, 0) to θij ∈ (0, π), with softmax shift invariance ensuring zij ≤ 0 is achievable without loss of expressivity. theorem master_interior_isomorphism {n : N} (z : Fin n → Fin n → R) (hz : ∀ i j, z i j ≤ 0) : ∀ i j, cosSqSoftmax (fun a b => angleFromScore (z a b)) i j = expSoftmax z i j := fun i j => cosSqSoftmax_eq_expSoftmax_under_bijection z hz i j

Theorem 14 (cos2 strictly extends exp at the boundary). With free angle parameterization θij ∈ [0, π], restricted to rows with at least one θil ̸= π so that every row distribution is defined, the cos2 -softmax distribution family reaches the closure of the simplex, including boundary distributions where some entries Aij are exactly 0. With finite-valued score parameterization zij ∈ R, the exp-softmax distribution family reaches only the interior of the simplex (Aij > 0 for every i, j). Therefore (15) {Pcos2 (θ) : θ ∈ [0, π]n×n } ⊋ {Pexp (z) : z ∈ Rn×n }, the inclusion being strict. Proof. Setting θij = π for any specific (i, j) gives cos2 (π/2) = 0, so Aij = 0 at finite parameter value (the Lean witness sets θij = π at a single entry and 0 elsewhere in the row, so the row denominator is n − 1 > 0). By contrast, ezij > 0 for all finite zij , so Aij > 0 strictly under exp-softmax with finite parameters. Boundary distributions (where some entries are exactly zero) are witness to the strict inclusion. theorem strict_extension (n : N) (hn : 1 < n) : ∃ θ : Fin n → Fin n → R, ∀ z : Fin n → Fin n → R, ∃ i j : Fin n, cosSqSoftmax θ i j ̸= expSoftmax z i j := by obtain ⟨θ, i, j, h_zero⟩ := exists_cosSqSoftmax_zero n hn refine ⟨θ, fun z => ⟨i, j, ?_⟩⟩ rw [h_zero] exact (expSoftmax_pos z i j).ne

A single-stage cos2 -softmax with free angle parameterization has strictly greater expressivity than single-stage exp-softmax with finite scores: it can express “hard” attention patterns where some weights are exactly zero, which exp-softmax can only approximate asymptotically. On the interior, the two are isomorphic representations. The cos2 primitive is therefore a natural extension to the quantum setting that subsumes exp-softmax as a special case (interior distributions) while adding boundary expressivity (sparse / hard-attention distributions).

11

···

|i, j⟩ |0⟩h(1)

|0⟩

(1)

Ry (θij ) |0⟩

|0⟩h(2)

(2)

Ry (θij ) |0⟩ (L) Ry (θij )

|0⟩h(L)

Figure 6: Trotter factorization diagram.

6.2

Trotter as one of infinitely many factorizations

The single-stage equivalence above is the simplest realization. Multi-stage post-selected constructions provide a continuous family of equivalent realizations, with the equal-angle Trotter form (fig. 6) being the canonical and simplest member. Construction 15 (L-stage post-selected factorization). For score zij ≤ 0, integer L ≥ 1, and any P L positive weights {αℓ }ℓ=1 with ℓ αℓ = β for a target inverse temperature β > 0, set the per-stage angle   (ℓ) (16) θij = 2 arccos eαℓ zij /2 , ℓ = 1, . . . , L. (ℓ)

At each stage, prepare a fresh ancilla h(ℓ) in |0⟩, apply the controlled rotation cRy (θij ) on h(ℓ) conditioned on |i, j⟩, measure, post-select |0⟩. Theorem 16 (Exact exp-softmaxPat inverse temperature β via L-stage post-selection). Under Construction 15 with total weight ℓ αℓ = β > 0, conditional on all L post-selections succeeding, eβzij P (j | i) = P βz = softmaxj (β zij ). il le

(17)

The equivalence is exact at any finite L ≥ 1 and for any positive weights; the case β = 1 recovers the unit-temperature exp-softmax of Eq. 1. (ℓ)

Proof. Stage ℓ post-selection probability per pair: cos2 (θij /2) = eαℓ zij . Independent post-selections P Q multiply: ℓ eαℓ zij = e( ℓ αℓ )zij = eβzij . Conditioning on i and normalizing across j gives the expsoftmax at inverse temperature β. theorem trotter_temperature {L : N} (α : Fin L → R) (z β : R) P (hα_sum : l, α l = β) : Q l, exp (α l * z) = exp (β * z) := by rw [← exp_sum] congr 1 rw [← sum_mul, hα_sum] theorem Q trotter_repeated_measurement (L : N) (z : R) : _l : Fin L, exp z = exp ((L : R) * z) := by have h := trotter_temperature (fun _ : Fin L => (1 : R)) z L (by simp) simpa using h

12

Corollary 17 (Measurement count as inverse temperature).
Take L identical rounds of the unitz /2 ij weight stage (αℓ = 1, per-stage angles θij = 2 arccos e ). Conditional on all L post-selections succeeding, eLzij β = L. (18) PL (j | i) = P Lz = softmaxj (β zij ), il le The number of repeated Born measurements is the inverse temperature of the attention distribution, exactly at every finite L; non-integer β is reached by any positive weights summing to β (Theorem 16). The endpoints anchor exactly: zero rounds leave the uniform superposition (β = 0, infinite temperature), and β → ∞ is the hard-attention limit. √ Three consequences follow. First, the 1/ d temperature convention of Remark 2(ii) acquires a native physical realization as post-selected measurement weight, rather than a classical rescaling of P the score. Second, the per-row post-selection success probability is Zi (β)/n with Zi (β) = l eβzil : the post-selection rate measures the Gibbs partition function at inverse temperature β, so cooling the attention distribution (lowering its entropy) is paid for in rejected shots, at per-pair success rate eβzij . Third, exp-softmax reaches the simplex boundary (hard attention) only as β → ∞, that is, only after infinitely many measurement rounds, whereas the free-angle cos2 family reaches the boundary at the single finite parameter θ = π (Theorem 14); the boundary strict extension is thus the statement that the quantum parameterization reaches the zero-temperature endpoint at finite parameter values. Physically, each round multiplies the branch amplitudes by ezij /2 , one step of imaginary-time evolution under the effective Hamiltonian H = −z. The correspondence is specific to the post-selected route: in the measure-and-reload route, β is simply a classical scalar multiplied into the score before the arccos. Remark 18 (Special cases). The construction includes L = 1, α1 = 1 as the single-stage postselected case: one round of post-selection on a single ancilla, realizing
the same distribution as the z/2 , at per-row success probability compiled state preparation of Proposition 12 via θ = 2 arccos e P Zi /n with Zi = l ezil ∈ [1, n] after the row shift of Remark 2. Run over the query-index superposition in A, this post-selection tilts the A-marginal from uniform to ∝ Zi while leaving each conditional P (j | i) exact. The construction further includes L ≥ 2, αℓ = 1/L as the standard Trotter form (equal angles, simplest multi-stage construction), and any other positive partition as a non-uniform variant. The equivalence is mathematically identical across all choices; operational considerations (depth, success probability, robustness) determine which is preferred.

6.3

Coherent finite-depth no-go (qualified)

Theorem 19 (Coherent no-go for affinely-encoded scores). Fix c > 0 and suppose the scores enter coherently through an affine encoding: the block-encoded operator presents singular values σij = f (zij ) with f affine and non-constant (e.g., σ = (z + c)/(2c) on z ∈ [−c, 0]), and the score domain contains an open interval. Let UL be a QSVT circuit of depth L on this block encoding, so that its output amplitudes are P P (σij ) for a (definite-parity) polynomial P of degree ≤ L [16], followed P by Born-rule readout P (σij )2 / l P (σil )2 . No finite L realizes the exp-softmax z 7→ ezij / l ezil exactly on all score matrices with entries in the domain. Proof. Exact realization on the row with all entries equal forces P (f (z)) ̸= 0 throughout the domain (a zero would produce attention weight 0 ̸= 1/n). Now hold every entry of a row except one at a fixed reference score z0 and vary the remaining entry: exactness of the readout forces the ratio P (f (z))2 /P (f (z0 ))2 = ez /ez0 , i.e., P (f (z))2 = C ez with C = P (f (z0 ))2 e−z0 > 0 a constant, for every z in an open interval. Writing σ = f (z) with f affine and invertible, the polynomial 13

Q(σ) := P (σ)2 of degree 2L agrees with Ceaσ+b , a ̸= 0, on an open interval of σ. Agreement of smooth functions on an open interval forces equality of all derivatives at any interior point σ0 ; but d2L+1 aσ+b Q(2L+1) ≡ 0 while dσ = C a2L+1 eaσ0 +b ̸= 0, a contradiction. 2L+1 Ce σ0 The algebraic core (a polynomial cannot agree with a genuine exponential on an open interval) is Lean-verified. The formal proof uses an even shorter route than the derivative count above: differentiating the assumed identity once gives Q′ = aQ on the interval, so the polynomial Q′ −aQ has infinitely many roots and is identically zero, contradicting deg(Q′ ) < deg(Q) for the nonvanishing Q. lemma hasDerivAt_expAffine (C a b σ : R) : HasDerivAt (fun t => C * Real.exp (a * t + b)) (a * (C * Real.exp (a * σ + b))) σ := by have h1 : HasDerivAt (fun t : R => a * t + b) a σ := by simpa using ((hasDerivAt_id σ).const_mul a).add_const b have h2 := ((Real.hasDerivAt_exp (a * σ + b)).comp σ h1).const_mul C convert h2 using 1 ring theorem no_polynomial_matches_exponential (Q : Polynomial R) (C a b s t : R) (hC : C ̸= 0) (ha : a ̸= 0) (hst : s < t) (hagree : ∀ σ ∈ Set.Ioo s t, Q.eval σ = C * Real.exp (a * σ + b)) : False := by obtain ⟨σ 0 , hσ 0 ⟩ := Set.nonempty_Ioo.mpr hst have hQne : Q ̸= 0 := by intro h have h0 := hagree σ 0 hσ 0 rw [h, Polynomial.eval_zero] at h0 exact (mul_ne_zero hC (Real.exp_ne_zero _)) h0.symm have hderiv : ∀ σ ∈ Set.Ioo s t, Q.derivative.eval σ = a * Q.eval σ := by intro σ hσ have hnhds : (fun y => Q.eval y) =f [nhds σ] (fun y => C * Real.exp (a * y + b)) := Filter.eventually_of_mem (isOpen_Ioo.mem_nhds hσ) hagree have heq := hnhds.deriv_eq rw [(Polynomial.hasDerivAt Q σ).deriv, (hasDerivAt_expAffine C a b σ).deriv] at heq rw [heq, hagree σ hσ] have hRroots : {x | (Q.derivative - Polynomial.C a * Q).IsRoot x}.Infinite := by apply (Set.Ioo_infinite hst).mono intro σ hσ show (Q.derivative - Polynomial.C a * Q).IsRoot σ simp only [Polynomial.IsRoot, Polynomial.eval_sub, Polynomial.eval_mul, Polynomial.eval_C] rw [hderiv σ hσ] ring have hR0 : Q.derivative - Polynomial.C a * Q = 0 := Polynomial.eq_zero_of_infinite_isRoot _ hRroots have hQd : Q.derivative = Polynomial.C a * Q := sub_eq_zero.mp hR0 have hlt : Q.derivative.degree < Q.degree := Polynomial.degree_derivative_lt hQne rw [hQd, Polynomial.degree_C_mul ha] at hlt

14

exact lt_irrefl _ hlt

Theorem 20 (ϵ-approximation via QSVT for quantum-loaded scores). Suppose the scores are bounded, |zij | ≤ c, and are not extracted via the measure-and-reload step but must be processed coherently in-circuit (no mid-circuit measurement). Then there exists a quantum circuit of depth p
O max{c, log(1/ϵ)} log(1/ϵ) above the cos2 baseline that approximates exp-softmax to accuracy ϵ via Chebyshev polynomial dressing of cos(θ/2) (QSVT with one extra ancilla). This is the fullycoherent alternative to the measure-and-reload realization in Theorem 27; the trade-off is exactness (measure-and-reload) versus full coherence (ε-approximate QSVT). Proof sketch. On [−1, 1] the rescaled exponential x 7→ ec(x−1) equals e−y punder y = c(1−x) ∈ [0, 2c],
−y and e on [0, 2c] admits a polynomial approximation of degree O max{c, log(1/ϵ)} log(1/ϵ) √ with uniform error ϵ [26, Theorem 4.1]; the c dependence is optimal among polynomials by the Markov-type lower bounds surveyed there, and such polynomials are part of the standard QSVT toolbox [16]. QSVT applies this polynomial to the singular value cos(θ/2) of the block-encoded score rotation using one extra ancilla, producing amplitudes ϵ-close (uniformly) to ez/2 up to a global normalization; Born-rule readout of the dressed register then yields each attention row to accuracy O(ϵ) in total variation. Remark 21 (The encoding is where the hardness lives). Theorem 19 cannot be strengthened to arbitrary encodings: under the reparameterized encoding σ = ez/2 , which is precisely the anglescore bijection of Theorem 13, the degree-one polynomial P (σ) = σ already satisfies P (σ)2 = ez , and Born readout returns exp-softmax exactly. The obstruction sits entirely in the non-polynomial reparameterization z 7→ ez/2 , and the two realizations in this paper are the two ways of paying for it: classically, as one arccos per score in the measure-and-reload step (exact; Theorem 27), or p coherently, as QSVT polynomial dressing from an affine encoding (ε-approximate at degree O( max{c, log(1/ε)} log(1/ε)); Theorem 20). Theorems 19 and 20 are in this sense a matched pair: the same map that no finite-degree polynomial reaches exactly is reached to accuracy ε at the cited degree.

6.4

Why multi-stage post-selection might still be useful

Although mathematically not unique, multi-stage post-selection has operational features that distinguish it:
1. Smaller per-stage rotation angles (θ = 2 arccos eαz/2 with small α) keep individual rotations near π/2, benign for noisy hardware and trainability. Q α z
2. Multiplicative probability composition matches the e ℓ = ez structure directly, useful for explicitly Trotter-style architectures. 3. Errors partially average out across stages in the presence of noise. None of these are mathematical advantages; they are implementation-time properties. With ideal classical simulation or noiseless hardware, the single-stage construction of Theorem 13 is operationally simpler.

15

|j⟩S |0⟩⊗b B′

Uenc

|0⟩⊗b BV

UV

ρi , diag ρi = Yi

Figure 7: Stochastic value channel diagram.

7

Weighted-sum value loading

P Construction 22 (Stochastic value channel). After the attention map produces |i⟩A j e aij |j⟩S |0⟩B ′ |0⟩BV , apply two unitaries. First, the j-controlled token encoding Uenc : |j⟩S |0⟩B ′ → |j⟩S |xj ⟩B ′ (the encoding oracle of Definition 3, conditioned on S). Second, the value channel Xp |wm ⟩BV = UV : |m⟩B ′ |0⟩BV 7→ |m⟩B ′ ⊗ |wm ⟩BV , (WV )km |k⟩, (19) k

which conditions on the feature index m and loads the amplitude lift of the m-th column of WV ; the column lifts |wm ⟩ are valid unit states because WV is column-stochastic (Assumption 1). UV is a Stinespring dilation of the classical channel WV : tracing out B ′ leaves on BV , for each token j, a mixed state whose computational-basis diagonal is exactly (WV xj )k (Theorem 23), at unit success probability with no post-selection. This is shown in fig. 7. The rotation angles of the d column state-preparation trees are the learnable parameters ΘV ; column-stochasticity of the realized WV holds automatically for every angle setting (the columns are Born-squared amplitudes), and UV is input-independent, compiled once per trained model. A block encoding of WV would not serve √ here: it acts at the amplitude level, producing WV xj , whereas value aggregation requires the √ √ probability-level WV xj , and WV x ̸= WV x in general. Theorem 23 (Weighted-sum equivalence). Tracing out S and B ′ , the reduced state on BV conditional on outcome i in A is X X ρi = xjm |wm ⟩⟨wm |. (20) |e aij |2 j

m

Under Assumption 1, the diagonal of ρi in the computational basis equals the classical attention P output Yi = j Aij Vj , Vj = WV xj , as a probability vector. Proof. After loads of Construction 22, the joint state on S ⊗B ′ ⊗BV (conditional P the twoPcontrolled √ on i) is j e aij |j⟩S m xjm |m⟩B ′ |wm ⟩BV . The S- and B ′ -register basis states are orthonormal, so tracing them out eliminates all j ̸= j ′ P and m ̸=Pm′ cross terms, leaving P thePdisplayed ρi . Its 2 2 computational-basis diagonal is ⟨k|ρi |k⟩ = j |e aij | m xjm |⟨k|wm ⟩| = j Aij m xjm (WV )km = P 2 d−1 V )km , which holds because each column of WV lies on ∆ j Aij (WV xj )k , using |⟨k|wm ⟩| = (W P p (Assumption 1) so that |wm ⟩ = k (WV )km |k⟩ is a valid unit state. The channel involves no post-selection: the diagonal is exact at unit success probability. The channel-diagonal identity at the heart of the proof is Lean-verified.

16

noncomputable def valueFromChannel {n d : N} (W : Fin d → Fin d → R) P(x : Fin n → Fin d → R) (j : Fin n) (k : Fin d) : R := m, W k m * x j m theorem channel_diagonal {n d : N} (W : Fin d → Fin d → R) (hW : ∀ k m, 0 ≤ W k m) (x : Fin n → Fin d → R) (j P : Fin n) (k : Fin d) : m, x j m * (Real.sqrt (W k m)) ^ 2 = valueFromChannel W x j k := by unfold valueFromChannel apply Finset.sum_congr rfl intro m _ rw [Real.sq_sqrt (hW k m), mul_comm]

8

The gated single-ancilla LCU residual

This is the central new construction: the residual “gate” is realized by the preparation angle of a single ancilla qubit, shown in fig. 8. Theorem 24 (Gated single-ancilla LCU residual). Let Ufull denote the unitary cascade of Sections 3–7 up to (but excluding) the partial trace of Theorem 23, followed by a terminal SWAP(B, BV ) that relocates the value register into the data register B holding the input lift, acting on encoded |X⟩ (with S, B ′ , and BV initialized to |0⟩). The terminal SWAP is what makes the residual well-posed: without it, the identity branch of the LCU below carries its data in B (with BV = |0⟩) while the sublayer branch carries its data in BV , and the two branches would combine states living in different registers; with it, both branches present their output in B, and every residual readout below refers to B. Let η be a learnable angle. The circuit (i)

prepare |η⟩C = cos(η/2)|0⟩C + sin(η/2)|1⟩C ,

(21)

(ii)

controlled-Ufull conditioned on |1⟩C ,

(22)

(iii)

Hadamard on C,

(23)

(iv)

post-select |0⟩C ,

(24)

produces |y out ⟩ ∝ cos(η/2) |X⟩ + sin(η/2) Ufull |X⟩, the parameterized residual sum with gate angle η. The success probability is
psucc = 21 1 + sin η Re⟨X|Ufull |X⟩ . Proof. After step (i) the joint state is
cos(η/2)|0⟩C + sin(η/2)|1⟩C |X⟩. After step (ii), with controlled-Ufull conditioned on |1⟩C , cos(η/2)|0⟩C |X⟩ + sin(η/2)|1⟩C Ufull |X⟩. Step (iii) Hadamards the ancilla, mapping {|0⟩, |1⟩} → {|+⟩, |−⟩}:
√1 |0⟩C cos(η/2)|X⟩ + sin(η/2)Ufull |X⟩ 2
+ √12 |1⟩C cos(η/2)|X⟩ − sin(η/2)Ufull |X⟩ . 17

(25)

(26)

|0⟩ |0⟩C |X⟩

Ry (η)

H ∝ cos(η/2)|X⟩ + sin(η/2) Ufull |X⟩

Ufull

Figure 8: Gated single-ancilla linear combination of unitaries residual addition diagram.

Step (iv) projects onto |0⟩C , giving (after normalization) cos(η/2)|X⟩ + sin(η/2)Ufull |X⟩. The success probability is the squared norm of the unnormalized |0⟩C -branch amplitude, 12 cos(η/2)|X⟩ +
2 sin(η/2)Ufull |X⟩ = 12 1 + sin η Re⟨X|Ufull |X⟩ . theorem lcu_circuit_correct {N : N} (η : R) (U : Fin N → Fin N → C) (X : State N) (i : Fin N) : lcuCircuit η U X i = ((1 : C) / (Real.sqrt 2 : C)) * ((Real.cos (η / 2) : C) * X i + (Real.sin (η / 2) : C) * applyU U X i) := by have h0 : ((⟨0, by omega⟩ : Fin 2).val = 0) = True := by simp have h1 : ((⟨1, by omega⟩ : Fin 2).val = 0) = False := by decide unfold lcuCircuit projectZero hadamardAncilla simp only [h0, if_true] unfold controlledU simp only [h0, h1, if_true, if_false] unfold initState simp only [h0, h1, if_true, if_false] unfold applyU P rw [show j, U i j * ((Real.sin P (η/2) : C) * X j) = (Real.sin (η/2) : C) * j, U i j * X j from by rw [Finset.mul_sum]; congr 1; funext j; ring]

8.1

Special cases of the gate angle

Corollary 25 (Gate-angle interpretations). The gate angle η in Theorem 24 produces the following residual modes: • η = 0: identity residual; the output equals the input |X⟩. The sublayer is bypassed entirely. • η = π: full sublayer; the output equals Ufull |X⟩. No residual. • η = π/2: equal-weight LCU residual; the output is the symmetric sum ∝ |X⟩ + Ufull |X⟩. This is the standard transformer additive identity. • η learnable: a quantum-native gated residual, generalizing both the additive identity (η = π/2 fixed) and the convex-combination soft gate (any η ∈ (0, π)). The classical-style soft gate g · U |X⟩ + (1 − g)|X⟩ with g ∈ [0, 1] realizes the same family of output states (after L2 renormalization) as the LCU output of Theorem 24, related by the bijective parameter correspondence g = tan(η/2), 1−g

equivalently 18

g =

sin(η/2) . sin(η/2) + cos(η/2)

(27)

The endpoints match the LCU special cases: η = 0 ↔ g = 0 (bypass), η = π/2 ↔ g = 1/2 (symmetric LCU), η = π ↔ g = 1 (full sublayer). Proof. Direct substitution of the special values into the form of Theorem 24. For the parameter correspondence, two unit-norm states proportional to cos(η/2)|X⟩ + sin(η/2)U |X⟩ and (1 − g)|X⟩ + g U |X⟩ coincide iff their coefficient ratios match, i.e., sin(η/2)/ cos(η/2) = g/(1 − g). Corollary 25 establishes that the soft-gated residual is realized entirely by the parameterized ancilla preparation as a unitary operation. The gate-fixed-at-0.5 LCU corresponds to η = π/2, the no-residual case to η = 0, and the full-sublayer case to η = π. Remark 26 (Incoherent variant recovers the probability-level residual exactly). The coherent LCU √ √ of Theorem 24 interferes amplitudes: at η = π/2 the Born readout of ∝ x + y (componentwise, for positive lifts) is in general not the probability-level average 12 (x + y) of Eq. 1; for example, x = (1, 0) and y = ( 12 , 21 ) give readout (0.854, 0.146) ̸= (0.75, 0.25). The probability-level residual is recovered exactly by the incoherent variant of the same circuit: prepare the gating ancilla in cos(η/2)|0⟩ + sin(η/2)|1⟩, apply controlled-Ufull , and trace out the ancilla (no Hadamard, no post† ; reducing selection). The joint state is then the mixture cos2 (η/2) |X⟩⟨X|+sin2 (η/2) Ufull |X⟩⟨X|Ufull ′ onto the data register B (tracing out S, B , and BV , with the terminal SWAP of Theorem 24 ensuring both branches present their data in B) gives a state whose computational-basis diagonal is exactly cos2 (η/2) x + sin2 (η/2) y; at η = π/2 this is 21 (x + y), with unit success probability. The equivalence theorem below uses the incoherent variant for its exactness claim; the coherent postselected LCU is the strictly-larger amplitude-level generalization, coinciding with the incoherent readout for generic inputs only at the endpoints η ∈ {0, π}.

9

Equivalence theorem

The per-primitive correspondences of Sections 3–8 compose into the full single-head equivalence below. Theorem 27 (Quantum equivalent of single-head attention with residual). Adopt Assumption 1 and the conventions of Remark 2, and assume the variational register has at least ⌈log2 d⌉ + 1 qubits. Permit one measure-and-reload step per attention scoring: the Hadamard-test outcome zij is
sampled, the row shift of Remark 2 is applied, and the resulting rotation angle θij = 2 arccos ezij /2 is reloaded as the controlled-Ry gate parameter of the softmax step. For any input X satisfying the assumption, there exists a quantum circuit Q and learnable parameters {ΘQ , ΘK , ΘV , η} (all rotation-gate angles) such that the Born-rule readout of Q(X) equals the classical single-head self-attention layer with residual T res (X) (Eq. 1, read under the conventions of Remark 2) exactly in the infinite-shot limit under the measure-and-reload step, via the following primitive correspondences: • Encoding: Definition 3. • Q, K projections: block-encoded WQ , WK (Lemma 4); the dilation unitary admits an exact decomposition into rotation gates and CNOTs by standard synthesis [24, 21], so the exactness of this correspondence does not rest on the density assumption. The rotation-CRY ansatz (Construction 7, Lemma 8) is the trainable finite-depth family for the same objects, conditional on Lemma 8(3). • Softmax: cos2 -Born readout (Proposition 12) with θij from the measure-and-reload step exactly reproduces exp-softmax (Theorem 13); Theorem 16 gives an equivalent multi-stage realization. 19

• Value aggregation: the column-stochastic WV realized exactly as a quantum channel via controlled column loading (Construction 22), with the column state-preparation angles as the learnable P parameters ΘV ; the diagonal of the partial trace equals the classical probability vector Yi = j Aij WV xj exactly and deterministically (Theorem 23). • Residual: the incoherent gated-ancilla mixture at η = π/2 reproduces the probability-level residual of Eq. 1 exactly (Remark 26); the coherent single-ancilla LCU (Theorem 24) is the amplitude-level generalization within the same circuit topology (Corollary 25). The fully-coherent alternative that removes the measure-and-reload step is ε-approximate via QSVT polynomial dressing (Theorem 20); exact finite-depth fully-coherent realization is provably impossible for affinely-encoded scores within the QSVT circuit family (Theorem 19). Proof. Composition of the per-primitive correspondences listed. Each correspondence is established in its respective theorem; under the probability-space assumption and the qubit-count condition the composition realizes the classical attention layer’s softmax pattern and value aggregation exactly (in the infinite-shot limit under the measure-and-reload step) and its additive residual exactly via the incoherent gating variant (Remark 26). The measure-and-reload step is the bridge from the Hadamard-test outcome zij to the controlled-Ry rotation angle θij via the angle bijection of Theorem 13, after the row shift of Remark 2. Measure-and-reload as a standard quantum-classical interface. The measure-and-reload step is a generic quantum-computing pattern: an intermediate ancilla is measured, a classical function is applied to the outcome, and the result is reloaded into the circuit as a downstream gate parameter. The same mechanism appears in adaptive quantum measurements [27, 28], quantum error correction syndrome extraction [29, 30], magic-state distillation [31], and more generally in any algorithm where a piece of classical information extracted from one stage drives the parameter of a later stage. Its overhead of finite-shot statistical noise on the measurement, mid-circuit classical-control latency, and the requirement of mid-circuit measurement capability on the hard√ ware is separately optimizable in principle: amplitude estimation [32] gives N shot scaling, lowlatency classical-control electronics reduce dispatch time, and mid-circuit measurement is a routine primitive on contemporary superconducting platforms [33, 34]. The equivalence of Theorem 27 is therefore exact (in the infinite-shot limit), with the practical accuracy bounded by the shot budget allocated to each measure-and-reload step. An expanded step-by-step audit of the construction’s classical-side operations (initial state preparation, gate parameter loading at compile time, per-scoring measure-and-reload, and terminal Born-rule readout) appears in Section 11. theorem single_head_master_summary (n : N) (hn : 1 < n) (z : Fin n → Fin n → R) (hz : ∀ i j, z i j ≤ 0) : -- 1. Interior isomorphism: (∀ i j, cosSqSoftmax (fun a b => angleFromScore (z a b)) i j = expSoftmax z i j) ∧ -- 2. Strict extension at boundary: (∃ θ : Fin n → Fin n → R, ∀ z’ : Fin n → Fin n → R, ∃ i j : Fin n, cosSqSoftmax θ i j ̸= expSoftmax z’ i j) ∧ -- 3. Trotter algebraic identity for exp-softmax: (∀ (L → R) (i j : Fin n), P: N) (α : Fin L Q ( l, α l = 1) → l, exp (α l * z i j) = exp (z i j)) := by refine ⟨?_, ?_, ?_⟩ · exact master_interior_isomorphism z hz

20

|X⟩ |0⟩C

|Y out ⟩ |0⟩

Ufull Ry (η)

H

Figure 9: Complete single-head quantum attention and residual addition diagram. · exact strict_extension n hn · intro L α i j hα exact trotter_post_selection z α hα i j

At the macro level, the full circuit is the LCU residual sandwich applied to the unitary cascade Ufull that realizes encoding, the cos2 -softmax (controlled-Ry on the attention register S with angles supplied by the measure-and-reload step), and the value channel (controlled column loading onto BV ) (see fig. 9). The unitary Ufull expands as Vxi → Uattn (θ i ) → Uenc → UV → SWAP(B, BV ) across the diagrams of Sections 3–7, with the partial traces over S and B ′ deferred to readout. The measure
and-reload step sets θ i = 2 arccos ezi /2 from the Hadamard-test outcomes; the LCU at η = π/2 realizes the additive residual.

10

Formal verification in Lean 4

The Lean code listings embedded with each theorem above are the actual machine-checked proofs accepted by the Lean 4 kernel against mathlib. The full library compiles successfully with lake build (zero errors). Scope of verification. The verified primitive identities are (i) the angle-score bijection on the simplex interior (Theorem 13), (ii) the boundary strict-extension claim with explicit witness (Theorem 14), (iii) the multi-stage post-selection algebraic identity for any positive weights, including the inverse-temperature generalization and the repeated-measurement special case (Theorem 16, Corollary 17), (iv) the gated single-ancilla circuit producing the parameterized residual sum (Theorem 24), (v) the Hadamard-test post-selection probability identity (Lemma 9), (vi) the identity-atorigin property of the rotation-CRY block-encoding ansatz (Lemma 8, part 2), (vii) the polynomialexponential impossibility at the algebraic core of the coherent no-go (Theorem 19), (viii) the channel-diagonal identity of the stochastic value channel (Theorem 23), and (ix) the residual LCU success bound psucc ≥ 12 in the simplex setting (Section 12). The composition into the full singlehead equivalence at the algebraic level is also Lean-formalized, as full single head equivalence in Master.lean: cos2 -softmax under the angle bijection, composed with the weighted-sum value aggregation and the convex residual, equals the classical exp-softmax attention layer pointwise; the channel-instantiated form full single p head equivalence channel carries the same equivalence end-to-end from the Born amplitudes (WV )km of the value channel. Each is proved from first principles using only mathlib primitives such as Real.exp, Real.cos, Real.arccos, Real.cos arccos, Finset.sum, and Complex.normSq. def classicalAttentionOutput {n d : N} (z : Fin n → Fin n → R) (V : Fin n → Fin d → R) (x P : Fin n → Fin d → R) (i : Fin n) (k : Fin d) : R := (( j, expSoftmax z i j * V j k) + x i k) / 2

21

def quantumAttentionOutput {n d : N} (z : Fin n → Fin n → R) (V : Fin n → Fin d → R) (x P : Fin n → Fin d → R) (i : Fin n) (k : Fin d) : R := (( j, cosSqSoftmax (fun a b => angleFromScore (z a b)) i j * V j k) + x i k) / 2 theorem full_single_head_equivalence {n d : N} (z : Fin n → Fin n → R) (hz : ∀ i j, z i j ≤ 0) (V : Fin n → Fin d → R) (x : Fin n → Fin d → R) (i : Fin n) (k : Fin d) : quantumAttentionOutput z V x i k = classicalAttentionOutput z V x i k := by unfold quantumAttentionOutput classicalAttentionOutput congr 1 congr 1 apply Finset.sum_congr rfl intro j _ rw [master_interior_isomorphism z hz i j] theorem full_single_head_equivalence_channel {n d : N} (z : Fin n → Fin n → R) (hz : ∀ i j, z i j ≤ 0) (W : Fin d → Fin d → R) (hW : ∀ k m, 0 ≤ W k m) (xP : Fin n → Fin d → R) (i : Fin n) (k : Fin d) : (( j, cosSqSoftmax (fun a b => angleFromScore (z a b)) i j * P ( m, x j m * (Real.sqrt (W k m)) ^ 2)) + x i k) / 2 = classicalAttentionOutput z (valueFromChannel W x) x i k := by have P h : ∀ j : Fin n, ( m, x j m * (Real.sqrt (W k m)) ^ 2) = valueFromChannel W x j k := fun j => channel_diagonal W hW x j k simp_rw [h] exact full_single_head_equivalence z hz (valueFromChannel W x) x i k

Imported as standard results. The construction relies on standard quantum-computing infrastructure not currently formalized in mathlib: data-reuploading universal-approximation results [23], the Solovay–Kitaev theorem, and the QSVT framework underlying the ϵ-approximation theorem. These are cited as established results, qualified by the architectural assumptions of their respective theorems. Out of scope. The architectural-level account of the classical-side interface operations (Section 11) is an expository description, not a theorem. Density of the rotation-CRY ansatz in SU (2b+1 ) (Lemma 8, part 3) and the QSVT ε-approximation (Theorem 20) are cited from the literature. The amplitude-level gate-sequence realization of the residual (Theorem 24) is Leanchecked at the LCU sandwich identity but not composed gate-by-gate with the value-aggregation circuit; the algebraic equivalence above takes the convex residual as given at the probability level, in agreement with Eq. 1 and realized exactly by the incoherent gating variant (Remark 26), with the coherent amplitude-level analog given by the LCU at η = π/2. Reproducing the build. The Lean project is a standard Lake build pinned to the Lean 4 toolchain at version v4.30.0-rc2, with mathlib4 as a dependency (auto-fetched via Lake). Running lake build yields a successful kernel check, which serves as a type-theoretic certificate that 22

every embedded theorem term has the type asserted by its signature; the Lean kernel rejects any step not reducible to mathlib axioms. Code availability. The Lean project (sources, lakefile, and toolchain pin) is available at ⟨repository URL⟩, commit ⟨hash⟩; running lake build at that commit reproduces the kernel check reported here.

11

Quantum vs. classical operations

Every step of the construction (Theorem 27) is either a unitary gate operation, a coherent ancillamediated transformation, or one of four standard quantum-classical interface operations: initial state preparation, gate parameter loading at compile time, the measure-and-reload step that supplies the softmax angle θij from the Hadamard-test outcome zij , and terminal Born-rule readout. What the quantum circuit does, step by step. 1. Encoding. Unitary state preparation VX : |0⟩⊗(a+b) 7→ |X⟩AB ; the classical input X is loaded once at the start. 2. Q, K block encoding. Each score projection W∗ (Θ∗ ), ∗ ∈ {Q, K}, is realized as a depth-L rotation-CRY ansatz on b + 1 qubits (Construction 7) with the block-encoding ancilla postselected on |0⟩. The learned angles Θ∗ are gate parameters, not classical features; the ancilla is recycled across Q and K via reset between projections. 3. Pairwise overlap. The Hadamard test (Lemma 9) on a second ancilla produces a joint state whose ancilla |0⟩-branch probability equals (1 + Re⟨qi | kj ⟩)/2. Sampling this ancilla yields zij (the measure step of measure-and-reload).
4. Classical conversion and reload. A classical control system computes θij = 2 arccos ezij /2 from each sampled zij (after the row-max shift of Remark 2, so all n scores of row i are collected first) and reloads θij as the rotation angle of the controlled-Ry softmax gate (the reload step). The fixed bijection (Theorem 13) carries no learned parameters; the conversion is a deterministic arithmetic step on the classical control system, separate from any optimizer. 5. Softmax. Controlled-Ry (θij ) on the attention register S realizes cos2 -Born readout (Proposition 12) which under the reloaded angles reproduces exp-softmax exactly (Theorem 13). 6. Value channel and aggregation. The j-controlled token encoding and the column-loading channel UV (Construction 22), followed by partial trace over S and B ′ , give the classical Yi on the diagonal of the reduced density matrix (Theorem 23). The channel is deterministic (no post-selection), and its learned angles ΘV are input-independent compile-time parameters. 7. Gated residual. Gated single-ancilla LCU at η = π/2 (Theorem 24) realizes the additive residual at the amplitude level. 8. Readout. A single round of Born-rule measurement of the data register returns the output probability vector.

23

Classical-side operations. The construction uses four classical-side operations, all of which are standard quantum-computing interface primitives: Initial state preparation. The classical input X is loaded once via a unitary state-prep circuit. This is the standard amplitude-encoding interface that many quantum machine learning algorithms use to ingest classical data. Gate parameter loading at compile time. The learned rotation angles Θ and any fixed circuit parameters are stored on the classical control system and deposited into the rotation-gate parameter fields at circuit-compilation time. This is identical to how common variational quantum algorithms (VQE, QAOA, QCBM) treat their learned parameters; the parameters are circuit constants set once per shot. Measure-and-reload (per
scoring pair). The Hadamard-test ancilla is sampled, the classical function θ = 2 arccos ez/2 is computed on the control system, and θ is reloaded as a downstream controlled-Ry angle. Mid-circuit measurement is a routine primitive on contemporary superconducting hardware [33, 34]. The overhead from finite-shot statistical noise on z, classical-control latency, √ and reload bandwidth is in principle separately optimizable (amplitude estimation [32] gives N shot scaling; low-latency control electronics shorten the reload cycle). Final measurement. A single Born-rule measurement at the end of the circuit returns the output probability vector. No subsequent quantum operation follows. The fully-coherent alternative that replaces the measure-and-reload step with a coherent polynomial dressing of cos(θ/2) is ε-approximate via QSVT (Theorem 20), and exact finite-depth fullycoherent realization is provably impossible for affinely-encoded scores within the QSVT circuit family (Theorem 19). Coherence caveat. The construction of Theorem 27 is exact but
not fully coherent. The measure-and-reload step supplies the softmax angle θij = 2 arccos ezij /2 from the classical outcome of the HadamardPtest. Removing this step and demanding a fully-coherent finite-depth realization of z 7→ exp(z)/ l exp(zil ) from quantum-loaded scores runs into Theorem 19. There are two regimes which escape the no-go depending on the number of tokens n: • n = 1: the softmax is trivially uniform on a single element and no coherent computation is required. This is the degenerate case where “fully quantum” holds, but it is not the setting of practical attention. • n ≥ 2: Theorem 20 gives a fully-coherent ε-approximate route via QSVT polynomial dressing, p at cost O( max{c, log(1/ε)} log(1/ε)) in additional circuit depth for scores bounded by c The measure-and-reload construction is what enables representation of the non-trivial n ≥ 2 cases.

12

Practicality and scaling

The equivalence theorem (Theorem 27) is stated in the infinite-shot limit and in gate-count-agnostic primitives (block-encoded projections, Hadamard tests, controlled state preparation). This section audits the near-term cost of that construction with focus on three critical scaling considerations: state-preparation and oracle model, success probability of the post-selection steps and whether amplitude amplification is needed, and heuristic finite-shot error propagation into the reload angle and softmax weights. We make no claims of a hardware roadmap but instead provide heuristic estimates of resource scaling. 24

12.1

State-preparation and oracle model

The construction takes as an oracle a state-preparation unitary Bxi for each classical input token xi ∈ ∆d−1 . The cost of realizing Bxi depends on which oracle model is used. P For an arbitrary √ d-dimensional probability vector with no exploitable structure, preparing |xi ⟩ = j xi,j |j⟩ from |0⟩⊗b , b = ⌈log2 d⌉ requires O(d) two-qubit gates in the worst case [24]. Repeated over n tokens, one preparation of the encoded input costs O(nd) gates; because preparation is repeated on every shot, the per-layer state-preparation cost is O(nd) multiplied by the shot budget of the finite-shot analysis below (see the scaling summary at the end of this section). Under a QRAM oracle [35], a coherent superposition query costs O(log d) time after an O(nd)-gate one-time preprocessing. QRAM at meaningful scale is not currently available but is a common assumption when considering practical scaling of quantum algorithms for future systems [12, 15]. If the classical input X is itself the output of an upstream quantum computation (a preceding attention layer, a quantum feature map, or a QSVT projection), state preparation is free by construction and the oracle model reduces to standard unitary composition. The block-encoded projections WQ , WK are realized by depth-L rotation-CRY ansätze on b + 1 qubits (Construction 7). Each has O(Lb) = O(L log d) gates. Under the density assumption of Lemma 8(3), L = poly(d) is sufficient for a target Frobenius error on W∗ . The exact polynomial degree is unknown. The value channel UV (Construction 22) is an input-independent multiplexed state preparation, O(d2 ) two-qubit gates in the worst case [24], compiled once per trained model. The single-ancilla LCU residual and the Hadamard test are O(1)-gate primitives on top of the block encodings they wrap.

12.2

Success probability and amplitude amplification

Block-encoding post-selection. Each of WQ , WK uses one ancilla with block-encoding postselection; the value channel involves no post-selection at all (Theorem 23). The success probability is ∥W∗ |x⟩∥2 = tr(W∗† W∗ ρx ), where ρx is the density in x, bounded by the largest singular value of W∗ . For projections into the unit ball this is O(1) for generic |x⟩. Amplitude amplification boosts a √ lower bound success probability p = Ω(1) to near-unity in O(1/ p) = O(1) upper bound of Grover iterations [32]. Fixed-point amplitude amplification [36] gives the same asymptotic scaling with less fragility compared to the original construction. Softmax post-selection.

Two routes are available for the exp-softmax:

• Single-stage exact route (Theorem 13). Because the reloaded angles are classical, the normalized attention state is compiled directly as an i-controlled state preparation (Proposition 12), and the cos2 -Born readout returns j with the correct exp-softmax marginal in a single measurement with no rejection; the cost lives entirely in the shot budget of the preceding Hadamard test. The literal controlled-Ry variant with ancilla post-selection (Remark 18) √ instead succeeds with probability Zi /n ≥ 1/n, requiring O( n) amplitude-amplification iterations in the worst case. • L-stage post-selected route (Theorem 16). Per-pair success ezij , which is exponentially small in |zij | for heavily-suppressed token pairs. Per-pair amplitude amplification gives O(e|zij |/2 ) Grover iterations, the standard quadratic speedup over the O(e|zij | ) shots required at success probability ezij .

25

Residual LCU post-selection. The single-ancilla LCU (Theorem 24) has ancilla-|0⟩ success
1 probability psucc = 2 1 + sin η Re⟨X|Ufull |X⟩ . For a generic unitary this can vanish: at η = π/2 with Ufull |X⟩ = −|X⟩, the additive-residual point has success probability zero. The simplex setting rules this case out: every computational-basis amplitude of both |X⟩ and Ufull |X⟩ is nonnegative (positive-orthant p lifts; cos(θ/2), sin(θ/2) ≥ 0 for θ ∈ [0, π] acting on registers initialized in |0⟩; value amplitudes Vjk ≥ 0; and post-selection only renormalizes a nonnegative vector), so Re⟨X|Ufull |X⟩ ≥ 0 and psucc ≥ 12 for every η. Amplitude amplification is not needed. The bound is Lean-verified: theorem lcu_success_probability_bound {N : N} (η : R) (hη 0 : 0 ≤ η) (hηπ : η ≤ π) (u v : Fin N → R) (hu : ∀ i, 0 ≤Pu i) (hv : ∀ i, 0 ≤ v i) : (1 : R) / 2 ≤ (1 + Real.sin η * i, u i * v i) / 2 := by have hsin : 0 ≤ P Real.sin η := Real.sin_nonneg_of_nonneg_of_le_pi hη 0 hηπ have hsum : 0 ≤ i, u i * v i := Finset.sum_nonneg fun i _ => P mul_nonneg (hu i) (hv i) have hprod : 0 ≤ Real.sin η * i, u i * v i := mul_nonneg hsin hsum linarith

12.3

Heuristic finite-shot error

The measure-and-reload step samples the ancilla marginal Pij (|0⟩) = (1 + Re⟨qi |kj ⟩)/2 = (1 + zij )/2 from a Bernoulli distribution. A shot-averaged estimator over N shots has variance σzb2 = (1 − z 2 )/N√ ≤ 1/N on the recovered score zbij . Amplitude estimation gives σzb = O(1/N ) instead of O(1/ N ) at the cost of an O(N )-deep phase-estimation dressing [32]. Because all n scores of a row are collected before any reload and the row shift of Remark 2 subtracts the empirical maximum,
every shifted score satisfies zbij − maxl zbil ≤ 0 by construction: the reload map θ = 2 arccos ez/2 is always defined, and no clipping rule is needed. The shift itself introduces no bias: softmax is exactly invariant under any common shift of a row, including a P random one, so the composite readout is exactly the exp-softmax of the noisy scores, ezbij / l ezbil . The Jacobian of the reload map on z ∈ (−∞, 0], ∂θ ez/2 ez/2 = − = −√ , ∂z sin(θ/2) 1 − ez diverges as z → 0− , but the divergence is a coordinate artifact of angle space, not an amplification of shot noise. The weight-space sensitivity is √ the composition ∂A/∂z = (∂A/∂θ)(∂θ/∂z) with √ A = cos2 (θ/2): near z = 0− one has θ ≈ 2 −z and ∂A/∂θ = − sin(θ)/2 ≈ − −z, so the two factors cancel and ∂A/∂z = ez ≤ 1 is uniformly bounded on the whole domain. The same cancellation protects against control noise on the angle itself: ∂A/∂θ → 0 exactly where ∂θ/∂z diverges. Heavily-suppressed pairs (z ≪ 0) are further damped by the factor ez . The only bias 2 that survives normalization is the Jensen bias of exponentiation, E[ezb] = ez eσzb/2 : its row-common part cancels between numerator and denominator to first order, leaving a differential contribution of order (σzb2ij − σ̄i2 )/2 = O(1/N ) from the score dependence of the Bernoulli variance, subdominant p to the O( n/N ) row-TV fluctuation computed next. Downstream, the softmax weight Aij = cos2 (θbij /2) = ezbij has delta-method variance Var(Aij ) ≈ 2 2 )/N ≤ A2 /N . Summing over a row of length n, the total-variation error Aij · Var(b zij ) = A2ij (1 − zij ij on the attention row is p bi − Ai ∥TV ≲ n/N E∥A 26

so achieving row-Total-Variation (row-TV) error ε requires N = Ω(n/ε2 ) shots per row under naive Bernoulli sampling, or N = Ω(n/ε) under amplitude estimation. Across all n rows, the total measurement budget per layer is Ω(n2 /ε2 ) shots (naive) or Ω(n2 /ε) with amplitude estimation. The residual gate angle η is a compile-time parameter with no per-inference measurement and contributes no shot-noise term. Order-of-magnitude example. For inference at target attention-weight precision ε = 10−2 on an n = 64-token sequence, naive sampling needs ∼ 6 × 105 shots per row and ∼ 4 × 107 shots per attention pass. Amplitude estimation reduces this to ∼ 6 × 103 shots per row and ∼ 4 × 105 per pass at the cost of ∼ 102 -deeper phase-estimation dressing. These budgets are the practicality bottleneck for an ℓ-layer transformer where the total budget accumulates as ℓ× (per-layer). Scaling summary. For inference on classical data, the honest per-layer accounting multiplies gates by shots: each shot re-prepares the input (O(nd) gates without QRAM), and the shot budget is Ω(n2 /ε2 ) (naive) or Ω(n2 /ε) (amplitude estimation), for a per-layer total of Ω(n3 d/ε2 ) (respectively Ω(n3 d/ε)) gate applications against the classical O(n2 d) FLOPs. There is no cost regime in which this construction outperforms classical evaluation for single-layer inference on classical data; the contribution of Theorem 27 is structural (an exactness statement), not a speedup claim. The accounting changes category when the input is quantum-native (produced by an upstream quantum layer, feature map, or QSVT projection), since classical evaluation is then unavailable without tomography; in that regime the layer adds only polynomial overhead on top of the pipeline that produced its input, and the relevant comparison is to other quantum layers, not to classical attention.

13

Discussion

Classical attention’s outputs are generally unbounded and, by definition, that regime cannot be recovered by a purely quantum ansatz. For models whose outputs are bounded or renormalized to the probability simplex, however, the result of this paper is stronger than representability: every mechanism of the classical single-head layer has a specific quantum analog that recovers it exactly, and the analogs compose into the full layer. Table 1 collects the dictionary established in Sections 3–8, entry by entry, with the exactness status and the certifying result for each. Three entries are not merely recoveries but strict extensions or physical reinterpretations of the classical mechanism: the cosine-squared softmax reaches boundary distributions that exponential softmax cannot reach at finite scores (Theorem 14); the gated ancilla interpolates a one-parameter family of residual modes of which the classical additive identity is the η = π/2 slice (Corollary 25); and the temperature axis, a hyperparameter classically, is realized physically as post-selected measurement weight (Corollary 17). Softmax as a slice of the simplex. Classical softmax projects a vector of unconstrained real scores onto the probability simplex via the exponential map, which requires unbounded scores to express extreme cases and never produces exact zeros at finite parameters. The cosine-squared softmax obtained from Born-rule measurement reaches the same interior distributions and additionally includes the boundary, where attention weights are exactly zero at finite parameter values. Existing sparse-attention variants such as sparsemax [37, 38] and entmax [39] achieve hard zeros through projection or α-entmax thresholding; the cosine-squared parameterization achieves the same boundary

27

classical mechanism

quantum analog

status

result

simplex input projections

Born-rule amplitude lift block-encoded contractions Hadamard-test ancilla marginal Born-rule readout of amplitudes repeated post-selected measurement controlled column-loading channel single-ancilla preparation angle

exact exact†

Def. 3 Lem. 4, 8

exact (infinite shot)

Lem. 9

exact; strictly extended

Thm. 13, 14

exact (post-selected)

Thm. 16, Cor. 17 Con. 22, Thm. 23 Thm. 24, Rem. 26

attention score exp. softmax temperature value application residual with gate

sparse/hard attention

boundary angles θ = π

exact, deterministic exact (incoherent); amplitude-level generalization (coherent) strict extension

Thm. 14

Table 1: The quantum-classical dictionary for single-head attention on the probability simplex. † Existence of the block encoding is exact (Lemma 4); its variational realization is conditional on the gate-set density assumption of Lemma 8(3). Scores are read in the normalized amplitude-lift (Hellinger) convention of Remark 2.

expressivity through a smooth function with no exponentials or underflow concerns. The temperature axis itself is realized physically in this construction: the number of repeated post-selected Born measurements is exactly the inverse temperature of the attention distribution (Corollary 17), and hard attention sits at a finite angle rather than at the zero-temperature limit of an anneal. Whether the cosine-squared form is competitive with these classical sparse-attention variants in practice is an empirical question the equivalence theorem motivates, independent of any quantum implementation. Ancilla as a tool to replace classical operations. Residual connections in deep learning have taken several forms: highway gates [3], ResNet’s pure additive identity [2], gated linear units [40], and various softer or learnable variants. The single-ancilla LCU construction maps each of these to a specific ancilla preparation: |0⟩ for bypass, |+⟩ for the additive identity, |1⟩ for the full sublayer, and a parameterized superposition cos(η/2)|0⟩ + sin(η/2)|1⟩ for a learnable gate. All four are realized by the same circuit topology, namely one ancilla, controlled-U , Hadamard, and post-select, differing only in the preparation angle. The unification places these four residual variants in a single one-parameter family. The ancilla also functions to carry out query and key block encoding, attention score inner product calculation using the Hadamard test, and Trotter decomposition to improve fidelity in single-gate noise which can increase with large angle rotations. All of these operations can be carried out by recycling the same ancilla with measurement or reset between algorithm steps. Implications and open directions. For empirical work on quantum hardware, the construction identifies the operational primitives required on hardware: block encoding for the projections, the Hadamard test for inner products, and the gated single-ancilla LCU for the residual. These are all well-studied operations, but their composition into a transformer attention layer has not previously been laid out as an exact construction with verification. Trainability under barren28

plateau constraints [41, 42] is a real concern that the formal proof does not resolve; the proof says nothing about whether the variational parameters are easy to learn, only that the architecture has the expressivity to match its classical counterpart in principle. A separate direction is on the classical side. The cosine-squared softmax with free angle parameterization is strictly more expressive than exponential softmax at finite parameter values, because it reaches boundary points of the simplex with exact zero attention weights. To our knowledge, cosine-squared softmax has not been studied as a drop-in attention parameterization. This suggests a separate classical direction: testing whether the same boundary expressivity that arises naturally from Born-rule normalization provides practical benefits in simplex-valued attention models. The probability simplex setting is the natural fit: classical generative models that operate directly on the simplex (Riemannian flow matching [9], Dirichlet flow matching [10], and continuous diffusion for categorical data [11]) would be the most direct testbed for cos2 -softmax as a drop-in replacement for the standard exponential softmax in their attention layers. No quantum advantage is claimed; whether the cosine-squared form yields measurable improvements in classical training is an empirical question outside the scope of this paper. Multi-head extension. The construction is single-head. Extension to multi-head attention is the standard parallel composition: H independent copies of the single-head circuit run with independent variational parameters {Θ(h) }H h=1 and independent ancilla registers, with the perhead outputs combined classically at readout (matching how multi-head attention concatenates head outputs in the classical setting). The mathematical content of this paper transfers head-byhead; what does not transfer is the hardware-resource accounting, which scales linearly with H in qubit count and gate count. Whether parameter sharing across heads (e.g., a single block-encoded WQ with head-indexed projection) admits a more economical realization is a natural follow-up.

14

Conclusion

We have constructed an exact equivalence, in the infinite-shot limit, between the classical singlehead attention layer with residual connection on the probability simplex and a quantum circuit in which every learnable parameter is a rotation-gate angle. The equivalence is a dictionary rather than a simulation: scores, softmax, temperature, value aggregation, and the gated residual each correspond to a specific quantum primitive (Figure 1, Table 1), with the softmax and residual families strictly extending their classical counterparts and the temperature axis realized physically as measurement repetition. The classical side of the interface reduces to state preparation, compiletime parameter loading, one measure-and-reload step per attention score, and a terminal Born-rule measurement. Exact fully-coherent realization at finite depth is provably impossible for affinelyencoded scores (Theorem 19), while QSVT dressing recovers it to accuracy ε (Theorem 20); the obstruction in both directions is the single non-polynomial reparameterization z 7→ ez/2 , paid either classically or coherently. The algebraic core of the dictionary is machine-checked in Lean 4 against mathlib. The probability simplex is the domain in which Riemannian and Dirichlet flow matching [9, 10] and categorical diffusion [11] already operate, so the primitives identified here connect directly to an active classical research thread. In particular, the cosine-squared softmax is a strictly larger family than exponential softmax at finite parameter values and may merit study as a classical parameterization in its own right.

29

15

AI Use Statement

Claude Opus 4.6 was used for Lean code generation for proof verification. Claude Opus 4.8 was used for simulated journal review/criticism, spell-check, and grammar editing.

References [1] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in Neural Information Processing Systems, pages 5998–6008, 2017. [2] Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. Deep residual learning for image recognition. In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pages 770–778, 2016. [3] Rupesh Kumar Srivastava, Klaus Greff, and Jürgen Schmidhuber. Highway networks, 2015. [4] Krzysztof Choromanski, Valerii Likhosherstov, David Dohan, Xingyou Song, Andreea Gane, Tamas Sarlos, Peter Hawkins, Jared Davis, Afroz Mohiuddin, Lukasz Kaiser, David Belanger, Lucy Colwell, and Adrian Weller. Rethinking attention with Performers. In International Conference on Learning Representations (ICLR), 2021. [5] Yao-Hung Hubert Tsai, Shaojie Bai, Makoto Yamada, Louis-Philippe Morency, and Ruslan Salakhutdinov. Transformer dissection: An unified understanding for transformer’s attention via the lens of kernel. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNLP-IJCNLP), pages 4344–4353, 2019. [6] Maria Schuld and Francesco Petruccione. Supervised Learning with Quantum Computers. Quantum Science and Technology. Springer, 2018. [7] Thomas R. Bromley, Juan Miguel Arrazola, Soran Jahangiri, Josh Izaac, Nicolás Quesada, Alain Delgado Gran, Maria Schuld, Jeremy Swinarton, Zeid Zabaneh, and Nathan Killoran. Applications of near-term photonic quantum computers: software and algorithms. Quantum Science and Technology, 5(3):034010, 2020. [8] Yaron Lipman, Ricky T. Q. Chen, Heli Ben-Hamu, Maximilian Nickel, and Matthew Le. Flow matching for generative modeling. In International Conference on Learning Representations (ICLR), 2023. [9] Ricky T. Q. Chen and Yaron Lipman. Flow matching on general geometries. In International Conference on Learning Representations (ICLR), 2024. [10] Pavel Avdeyev, Chenlai Shen, Charles Slater, Vinay Birodkar, Adam Lerer, and Andreas Krause. Dirichlet flow matching with applications to DNA sequence design, 2024. [11] Sander Dieleman, Laurent Sartran, Arman Roshannai, Nikolay Savinov, Yaroslav Ganin, Pierre H. Richemond, Arnaud Doucet, Robin Strudel, Chris Dyer, Conor Durkan, Curtis Hawthorne, Rémi Leblond, Will Grathwohl, and Jonas Adler. Continuous diffusion for categorical data, 2022.

30

[12] El Amine Cherrat, Iordanis Kerenidis, Natansh Mathur, Jonas Landman, Martin Strahm, and Yun Yvonna Li. Quantum vision transformers. Quantum, 8:1265, 2024. [13] Jinjing Shi, Ren-Xin Zhao, Wenxuan Wang, Shichao Zhang, and Xuelong Li. QSAN: A nearterm achievable quantum self-attention network, 2022. [14] Fu Chen, Qinglin Zhao, Li Feng, Longfei Tang, Yangbin Lin, and Haitao Huang. Quantum complex-valued self-attention model, 2025. [15] Naixu Guo, Zhan Yu, Matthew Choi, Yizhan Han, Aman Agrawal, Kouhei Nakaji, Alán Aspuru-Guzik, and Patrick Rebentrost. Quantum transformer: Accelerating model inference via quantum linear algebra, 2024. [16] András Gilyén, Yuan Su, Guang Hao Low, and Nathan Wiebe. Quantum singular value transformation and beyond: exponential improvements for quantum matrix arithmetics. In Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing (STOC), pages 193–204, 2019. [17] Andrew M. Childs, Robin Kothari, and Rolando D. Somma. Quantum algorithm for systems of linear equations with exponentially improved dependence on precision. SIAM Journal on Computing, 46(6):1920–1950, 2017. [18] Andrew M. Childs and Nathan Wiebe. Hamiltonian simulation using linear combinations of unitary operations. Quantum Information and Computation, 12(11–12):901–924, 2012. [19] Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28, volume 12699 of Lecture Notes in Computer Science, pages 625–635. Springer, 2021. [20] The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pages 367–381, 2020. [21] Adriano Barenco, Charles H. Bennett, Richard Cleve, David P. DiVincenzo, Norman Margolus, Peter Shor, Tycho Sleator, John A. Smolin, and Harald Weinfurter. Elementary gates for quantum computation. Physical Review A, 52(5):3457–3467, 1995. [22] Michael J. Bremner, Christopher M. Dawson, Jennifer L. Dodd, Alexei Gilchrist, Aram W. Harrow, Duncan Mortimer, Michael A. Nielsen, and Tobias J. Osborne. Practical scheme for quantum computation with any two-qubit entangling gate. Physical Review Letters, 89(24):247902, 2002. [23] Maria Schuld, Ryan Sweke, and Johannes Jakob Meyer. The effect of data encoding on the expressive power of variational quantum machine learning models. Physical Review A, 103(3):032430, 2021. [24] Vivek V. Shende, Stephen S. Bullock, and Igor L. Markov. Synthesis of quantum-logic circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 25(6):1000– 1010, 2006. [25] Harry Buhrman, Richard Cleve, John Watrous, and Ronald de Wolf. Quantum fingerprinting. Physical Review Letters, 87(16), Sept 2001. 31

[26] Sushant Sachdeva and Nisheeth K. Vishnoi. Faster algorithms via approximation theory. Foundations and Trends in Theoretical Computer Science, 9(2):125–210, 2014. [27] B. L. Higgins, D. W. Berry, S. D. Bartlett, H. M. Wiseman, and G. J. Pryde. Entanglement-free Heisenberg-limited phase estimation. Nature, 450(7168):393–396, 2007. [28] Howard M. Wiseman and Gerard J. Milburn. Quantum Measurement and Control. Cambridge University Press, 2009. [29] Austin G. Fowler, Matteo Mariantoni, John M. Martinis, and Andrew N. Cleland. Surface codes: Towards practical large-scale quantum computation. Physical Review A, 86(3):032324, 2012. [30] Barbara M. Terhal. Quantum error correction for quantum memories. Reviews of Modern Physics, 87(2):307–346, 2015. [31] Sergey Bravyi and Alexei Kitaev. Universal quantum computation with ideal Clifford gates and noisy ancillas. Physical Review A, 71(2):022316, 2005. [32] Gilles Brassard, Peter Høyer, Michele Mosca, and Alain Tapp. Quantum amplitude amplification and estimation. Contemporary Mathematics, 305:53–74, 2002. [33] A. D. Córcoles, Maika Takita, Ken Inoue, Scott Lekuch, Zlatko K. Minev, Jerry M. Chow, and Jay M. Gambetta. Exploiting dynamic quantum circuits in a quantum algorithm with superconducting qubits. Physical Review Letters, 127(10):100501, 2021. [34] L. C. G. Govia, P. Jurcevic, C. J. Wood, N. Kanazawa, S. T. Merkel, and D. C. McKay. A randomized benchmarking suite for mid-circuit measurements. New Journal of Physics, 25(12):123016, 2023. [35] Vittorio Giovannetti, Seth Lloyd, and Lorenzo Maccone. Quantum random access memory. Physical Review Letters, 100(16):160501, 2008. [36] Theodore J. Yoder, Guang Hao Low, and Isaac L. Chuang. Fixed-point quantum search with an optimal number of queries. Physical Review Letters, 113(21):210501, 2014. [37] André F. T. Martins and Ramón Fernandez Astudillo. From softmax to sparsemax: A sparse model of attention and multi-label classification. In Proceedings of the 33rd International Conference on Machine Learning (ICML), volume 48 of Proceedings of Machine Learning Research, pages 1614–1623, 2016. [38] Gonçalo M. Correia, Vlad Niculae, and André F. T. Martins. Adaptively sparse transformers. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNLPIJCNLP), pages 2174–2184, 2019. [39] Ben Peters, Vlad Niculae, and André F. T. Martins. Sparse sequence-to-sequence models. In Proceedings of the 57th Annual Meeting of the Association for Computational Linguistics (ACL), pages 1504–1519, 2019. [40] Yann N. Dauphin, Angela Fan, Michael Auli, and David Grangier. Language modeling with gated convolutional networks. In Proceedings of the 34th International Conference on Machine Learning (ICML), volume 70 of Proceedings of Machine Learning Research, pages 933–941, 2017. 32

[41] Jarrod R. McClean, Sergio Boixo, Vadim N. Smelyanskiy, Ryan Babbush, and Hartmut Neven. Barren plateaus in quantum neural network training landscapes. Nature Communications, 9:4812, 2018. [42] M. Cerezo, Akira Sone, Tyler Volkoff, Lukasz Cincio, and Patrick J. Coles. Cost function dependent barren plateaus in shallow parametrized quantum circuits. Nature Communications, 12:1791, 2021.

33

Related documents

• A Quantum Roadmap for Softmax Attention: Exact Born-Rule Analogs for Softmax Attention on the Probability Simplex#974533
• A Quantum-Bayesian Route to Quantum-State Space#110610
• Abstention and Noise Filtering: Two Missing Primitives of Softmax Attention#1036392
• Abstention and Noise Filtering: Two Missing Primitives of Softmax Attention#1006838
• MALOQ: Massively Accelerated Learning of Operators for Quantum Transport#321813