Sequential Register Circuit

Abstract

Actual time-dependent unitaries on retained physical slots have the coefficients of a finite chain on one common complex memory.

Space(I) is the complex Euclidean Hilbert space on a finite type I; Unitary(I) is its linear isometry equivalence group. e(j) is the coordinate basis vector. delta(i,j) is 1 if i=j and 0 otherwise. Word(A,n)=Fin(n) to A, and Register(A,K,n)=Word(A,n) x K. The same finite complex memory K is used at every time. A and K may inhabit independent universes. U(t) is a unitary on Space(A x K), and t,n,m are natural numbers. No stationarity is assumed.

Theorem 1.1 (Two embedded isometric copies are related by a unitary).

$\forall E \in T y p e, \forall H \in T y p e, C o m pl e x I nn er P ro d u c tSp a ces (E, H) \Rightarrow (F ini t eD im e n s i o na l (C, H) \Rightarrow (\forall so u rce \in L in e a r I so m e t ry (C, E, H), \forall t a r g e t \in L in e a r I so m e t ry (C, E, H), \exists U \in L in e a r I so m e t ry Eq u i v (C, H, H), \forall x \in E, U (so u rce (x)) = t a r g e t (x)))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.exists_unitary_agree (✓ std3). ∎

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

Both spaces are normed additive groups with complex inner products; only H is assumed finite dimensional. The pinned LinearIsometry.extend gives agreement on the range, and injectivity in finite dimension gives surjectivity.

Definition 1.2 (Coordinate embeddings are actual linear isometries).

$\forall E \in T y p e, \forall F \in T y p e, (F in t y p e (E) \land (F in t y p e (F) \land (Dec i d ab l e Eq (E) \land Dec i d ab l e Eq (F)))) \Rightarrow \forall e \in E mb e dd in g (E, F), \forall x \in Sp a ce (E), \forall q \in F, J (e, x, q) = j : E \sum d e lt a (e (j), q) \cdot x (j)$

Formalization. D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.coordinateEmbedding (✓ std3).

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

E and F are finite with decidable equality, and e:E embeds into F. J(e) is the isometry obtained from the matrix delta(e(j),q), whose Gram matrix is the identity. It inserts zero in coordinates outside the range.

Theorem 1.3 (Rectangular isometries extend with exact coordinate support).

$\forall A \in T y p e, \forall E \in T y p e, \forall F \in T y p e, \forall K \in T y p e, ((F in t y p e (A) \land Dec i d ab l e Eq (A)) \land ((F in t y p e (E) \land Dec i d ab l e Eq (E)) \land ((F in t y p e (F) \land Dec i d ab l e Eq (F)) \land (F in t y p e (K) \land Dec i d ab l e Eq (K))))) \Rightarrow (\forall b l ank \in A, \forall e \in E mb e dd in g (E, K), \forall f \in E mb e dd in g (F, K), \forall V \in L in e a r I so m e t ry (C, Sp a ce (E), Sp a ce (P ro d (A, F))), \exists U \in U ni t a ry (P ro d (A, K)), (\forall x \in Sp a ce (E), U (J (b l ank I nj ec t i o n (b l ank, e), x)) = J (o u tp u t I nj ec t i o n (f), V (x))) \land ((\forall x \in Sp a ce (E), \forall i \in A, \forall j \in F, U (J (b l ank I nj ec t i o n (b l ank, e), x), p ai r (i, f (j))) = V (x, p ai r (i, j))) \land (\forall x \in Sp a ce (E), \forall i \in A, \forall k \in K, O u t s i d e R an g e (k, f) \Rightarrow U (J (b l ank I nj ec t i o n (b l ank, e), x), p ai r (i, k)) = 0)))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.rectangular_unitary_coefficients (✓ std3). ∎

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

All four coordinate types are finite with decidable equality. V maps Space(E) isometrically into Space(A x F). blankInjection(j)=(blank,e(j)); outputInjection(i,j)=(i,f(j)). The three conjuncts retain vector agreement, every coefficient in the output range, and zero outside that range.

curry identifies Space(B x C) with the Hilbert direct sum over B of Space(C). block(U) applies U separately in every B slice. lift(e,U) conjugates this block operator by a coordinate equivalence e:R equiv B x C. headRest separates the first physical symbol from (tail word,memory); restHead separates the tail word from (first symbol,memory). First(n,U)=lift(restHead(n),U), while Tail(n,V)=lift(headRest(n),V). compose(f,g) means apply g, then f.

Theorem 1.4 (Lifted operators act in their specified coordinate slice).

$\forall R \in T y p e, \forall B \in T y p e, \forall C \in T y p e, (F in t y p e (R) \land (F in t y p e (B) \land F in t y p e (C))) \Rightarrow (\forall e \in Eq u i v (R, P ro d (B, C)), \forall U \in U ni t a ry (C), \forall x \in Sp a ce (R), \forall r \in R, l i f t (e, U, x, r) = U (j \mapsto x (in v erse (e, p ai r (f s t (e (r)), j))), s n d (e (r))))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.lift_apply (✓ std3). ∎

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

The lambda is included by WithLp.toLp(2). This is an equality for arbitrary input vectors and coordinate equivalences, not a premise about a target state.

Definition 1.5 (The full circuit is independent unitary operator composition).

$\forall A \in T y p e, \forall K \in T y p e, (F in t y p e (A) \land F in t y p e (K)) \Rightarrow (\forall U \in F u n c t i o n (N, U ni t a ry (P ro d (A, K))), \forall n \in N, \forall t \in N, C (U, 0, t) = i d e n t i t y (R e g i s t er (A, K, 0)) \land C (U, n + 1, t) = co m p ose (T ai l (n, C (U, n, t + 1)), F i rs t (n, U (t))))$

Formalization. D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.circuit (✓ std3).

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

Every physical slot remains part of the full Hilbert space. This recursive definition uses only actual unitary operators, without a desired coefficient formula or a chain contraction in its definition.

Definition 1.6 (Partial circuits retain the full register).

$\forall A \in T y p e, \forall K \in T y p e, (F in t y p e (A) \land F in t y p e (K)) \Rightarrow (\forall U \in F u n c t i o n (N, U ni t a ry (P ro d (A, K))), \forall n \in N, \forall m \in N, \forall t \in N, P (U, 0, m, t) = i d e n t i t y (R e g i s t er (A, K, 0)) \land (P (U, n + 1, 0, t) = i d e n t i t y (R e g i s t er (A, K, n + 1)) \land P (U, n + 1, m + 1, t) = co m p ose (T ai l (n, P (U, n, m, t + 1)), F i rs t (n, U (t)))))$

Formalization. D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.partialCircuit (✓ std3).

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

P(U,n,m,t) denotes partialCircuit. It applies the next m gates, stopping if no slots remain. It always acts on Space(Register(A,K,n)).

Definition 1.7 (One gate acts on one slot and the common memory).

$\forall A \in T y p e, \forall K \in T y p e, (F in t y p e (A) \land F in t y p e (K)) \Rightarrow (\forall U \in U ni t a ry (P ro d (A, K)), \forall n \in N, Sl o t (U, n + 1, 0) = F i rs t (n, U) \land (\forall q \in F in (n), Sl o t (U, n + 1, s u cc (q)) = T ai l (n, Sl o t (U, n, q))))$

Formalization. D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.slotGate (✓ std3).

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

At length zero there is no slot index (Fin(0)), so that branch is empty. Slot denotes slotGate and is independent of the input or desired output state.

Theorem 1.8 (All other physical coordinates stay fixed).

$\forall A \in T y p e, \forall K \in T y p e, (F in t y p e (A) \land F in t y p e (K)) \Rightarrow (\forall U \in U ni t a ry (P ro d (A, K)), \forall n \in N, \forall r \in F in (n), \forall x \in Sp a ce (R e g i s t er (A, K, n)), \forall w \in W or d (A, n), \forall k \in K, Sl o t (U, n, r, x, p ai r (w, k)) = U (p \mapsto x (p ai r (u p d a t e (w, r, f s t (p)), s n d (p))), p ai r (w (r), k)))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.slot_gate_apply (✓ std3). ∎

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

The vector lambda p is included with WithLp.toLp(2). Only the selected symbol and memory coordinate vary inside the slice supplied to U.

Theorem 1.9 (A successor applies the next gate on the same full space).

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.partial_circuit_succ_gate (✓ std3). ∎

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

m<n supplies the Fin(n) slot index. The time of this local gate is t+m.

Theorem 1.10 (Applying every slot equals the full circuit).

$\forall A \in T y p e, \forall K \in T y p e, (F in t y p e (A) \land F in t y p e (K)) \Rightarrow (\forall U \in F u n c t i o n (N, U ni t a ry (P ro d (A, K))), \forall n \in N, \forall t \in N, P (U, n, n, t) = C (U, n, t))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.partial_circuit_all (✓ std3). ∎

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

This equality identifies the independently defined recursive full circuit with the successive same-register slot applications.

blankState(blank,n,j)=e((constant(blank),j)). initialized(blank,n) embeds Space(K) at this constant physical word. B(blank,n,j) and I(blank,n,x) denote these states. The blank symbol is an explicit parameter in the following statements; the occupation companion handles zero slots without asking for one.

Definition 1.11 (Initialization embeds any memory vector).

$\forall A \in T y p e, \forall K \in T y p e, (F in t y p e (A) \land F in t y p e (K)) \Rightarrow (\forall b l ank \in A, \forall n \in N, \forall x \in Sp a ce (K), I (b l ank, n, x) = J (b l ank I nj ec t i o n (co n s t an t (b l ank, n), i d e n t i t y E mb e dd in g (K)), x))$

Formalization. D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.initialized (✓ std3).

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

This is an actual coordinate linear isometry. No normalization of x is needed to define it or to establish the coefficient identity.

Definition 1.12 (The chain reads local operator matrix coefficients).

$\forall A \in T y p e, \forall K \in T y p e, (F in t y p e (A) \land F in t y p e (K)) \Rightarrow (\forall U \in F u n c t i o n (N, U ni t a ry (P ro d (A, K))), \forall b l ank \in A, \forall k \in K, \forall n \in N, \forall t \in N, Q (U, b l ank, k, 0, t) = t er mina l (j \mapsto d e lt a (j, k)) \land Q (U, b l ank, k, n + 1, t) = s t e p (i \mapsto j \mapsto l \mapsto U (t, e (p ai r (b l ank, j)), p ai r (i, l)), Q (U, b l ank, k, n, t + 1)))$

Formalization. D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.unitaryChain (✓ std3).

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

Q(U,blank,k,n,t) is unitaryChain, a FiniteChain(A,K) whose next carrier is again K at every step. Its terminal covector selects k. contract takes a list of symbols; amp(Q,x,w) sums x(j) times contract(Q,ofFn(w),j).

Theorem 1.13 (Actual circuit coefficients equal chain contractions).

$\forall A \in T y p e, \forall K \in T y p e, (F in t y p e (A) \land F in t y p e (K)) \Rightarrow (\forall U \in F u n c t i o n (N, U ni t a ry (P ro d (A, K))), \forall b l ank \in A, \forall n \in N, \forall t \in N, \forall j \in K, \forall k \in K, \forall w \in W or d (A, n), C (U, n, t, B (b l ank, n, j), p ai r (w, k)) = co n t r a c t (Q (U, b l ank, k, n, t), o f F n (w), j))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.circuit_basis_coefficients (✓ std3). ∎

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

The live induction on the remaining slots uses first_tail_blank to sum over the actual common memory. The zero case is the actual register identity. This derived identity connects independent operator and chain definitions.

Theorem 1.14 (Every initial pure memory has the derived chain amplitude).

$\forall A \in T y p e, \forall K \in T y p e, (F in t y p e (A) \land F in t y p e (K)) \Rightarrow (\forall U \in F u n c t i o n (N, U ni t a ry (P ro d (A, K))), \forall b l ank \in A, \forall n \in N, \forall t \in N, \forall x \in Sp a ce (K), \forall w \in W or d (A, n), \forall k \in K, C (U, n, t, I (b l ank, n, x), p ai r (w, k)) = am p (Q (U, b l ank, k, n, t), x, w))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.circuit_initialized_coefficients (✓ std3). ∎

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

Basis expansion and linearity extend the proved basis coefficients to arbitrary x, including non-normalized vectors. The physical necessity companion uses this identity for normalized initial and terminal memory.

Theorem 1.15 (Unvisited slots still contain the homogeneous blank).

$\forall A \in T y p e, \forall K \in T y p e, (F in t y p e (A) \land F in t y p e (K)) \Rightarrow (\forall U \in F u n c t i o n (N, U ni t a ry (P ro d (A, K))), \forall b l ank \in A, \forall n \in N, \forall m \in N, \forall t \in N, \forall j \in K, \forall k \in K, \forall w \in W or d (A, n), \forall r \in F in (n), (m \leq v a l (r) \land N e (w (r), b l ank)) \Rightarrow P (U, n, m, t, B (b l ank, n, j), p ai r (w, k)) = 0)$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.unused_slots_zero (✓ std3). ∎

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

No m<=n premise is needed: the existence of r with m<=val(r)<n already bounds m. The statement is an exact vanishing coefficient.

Theorem 1.16 (Unit normalization survives initialization and the circuit).

$\forall A \in T y p e, \forall K \in T y p e, (F in t y p e (A) \land F in t y p e (K)) \Rightarrow (\forall U \in F u n c t i o n (N, U ni t a ry (P ro d (A, K))), \forall b l ank \in A, \forall n \in N, \forall t \in N, \forall x \in Sp a ce (K), n or m (x) = 1 \Rightarrow (n or m (I (b l ank, n, x)) = 1 \land n or m (C (U, n, t, I (b l ank, n, x))) = 1))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.initialized_norm (✓ std3). ∎

Citation. David Raveh and Rafael I. Nepomechie (2024). Dicke states as matrix product states. DOI: 10.1103/PhysRevA.110.052438.

Commentary.

Both conjuncts follow from actual isometry norm preservation. No desired output equation, rank bound, or occupation constraint is a premise.

References

Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.circuit
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.circuit_basis_coefficients
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.circuit_initialized_coefficients
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.coordinateEmbedding
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.exists_unitary_agree
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.initialized
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.initialized_norm
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.lift_apply
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.partialCircuit
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.partial_circuit_all
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.partial_circuit_succ_gate
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.rectangular_unitary_coefficients
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.slotGate
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.slot_gate_apply
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.unitaryChain
Truth anchor: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit.unused_slots_zero
Dependency: D5/S3/Quantum/Entanglement/SequentialOccupationHistory

Keyboard shortcuts

trureturing — Discovering truth

Sequential Register Circuit

Abstract

References