Sequential Occupation History

Abstract

Actual occupation transitions prepare the uniform word state, and every exact finite chain factors its cut matrix through its actual memory.

A is an alphabet; each statement records its finiteness and decidable-equality assumptions. a is a multiset of symbols, t and n are natural numbers, and Word(A,n) is Fin n to A. B(a,t) is the existing Boundary subtype: val(b)<=a and card(val(b))=t. Subtraction of multisets removes occupation counts. M(n,r) counts actual words with occupation r; V(n,r,w) is the existing sectorVector, equal to the complex inverse of sqrt(M(n,r)) on legal words and zero elsewhere.

S(a,t) denotes nextStep, a complex matrix with rows (i,c) in A x B(a,t+1) and columns b in B(a,t). Its entry is sqrt(count(a-val(b),i)/(card(a)-t)) when val(c)=val(b)+{i}, and zero otherwise. The subtraction card(a)-t is in natural numbers, and numerator and denominator are included in the reals before division. The nonnegative real square root is then included in C. Dagger denotes conjugate transpose, and 1 denotes the identity matrix.

Theorem 1.1 (Legal extensions are exactly positive remaining counts).

$\forall A \in T y p e, Dec i d ab l e Eq (A) \Rightarrow (\forall a \in M u lt i se t (A), \forall t \in N, \forall b \in B (a, t), \forall i \in A, (\exists c \in B (a, t + 1), v a l (c) = v a l (b) + s in g l e t o n (i)) \Leftrightarrow co u n t (v a l (b), i) < co u n t (a, i))$

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

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

Commentary.

The extension is an actual member of the next occupation carrier. This criterion does not need finiteness of the alphabet or an active-step hypothesis.

Theorem 1.2 (Every active step has identity Gram matrix).

$\forall A \in T y p e, (F in t y p e (A) \land Dec i d ab l e Eq (A)) \Rightarrow (\forall a \in M u lt i se t (A), \forall t \in N, t < c a r d (a) \Rightarrow co nj T r an s p ose (S (a, t)) \cdot S (a, t) = 1)$

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

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

Commentary.

The columns have unit norm and are mutually orthogonal. Different prefixes cannot reach the same next occupation after emitting the same symbol. Summing all remaining symbol counts gives card(a)-t, which is positive on an active step.

Theorem 1.3 (The step induces the canonical quantum channel).

$\forall A \in T y p e, (F in t y p e (A) \land Dec i d ab l e Eq (A)) \Rightarrow (\forall a \in M u lt i se t (A), \forall t \in N, t < c a r d (a) \Rightarrow (\exists c hann e l \in Q u an t u m C hann e l (B (a, t), P ro d (A, B (a, t + 1))), \forall r h o \in M a t r i x (B (a, t), B (a, t), C), t o M a t r i x (t o C o m pl e t e l y P os i t i v e M a p (c hann e l, o f M a t r i x (r h o))) = S (a, t) \cdot r h o \cdot co nj T r an s p ose (S (a, t))))$

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

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

Commentary.

QuantumChannel is FiniteStateChannel.QuantumChannel. ofMatrix is CStarMatrix.ofMatrix and toMatrix is its inverse. The singleton Unit Kraus family uses the frozen finite_kraus_quantum_channel theorem; the action holds on every complex input matrix.

F(a,n,t,w,b) denotes contraction. For n=0 it is 1 when val(b)=a and 0 otherwise. For n+1 it is the finite sum over c in B(a,t+1) of S(a,t)((w(0),c),b) times F(a,n,t+1,Fin.tail(w),c). Thus it multiplies and sums the actual step entries and caps the final memory by the total-occupation basis vector. The initial memory b0(a) is initialBoundary, whose multiset value is empty.

Theorem 1.4 (Every remaining contraction is the normalized suffix state).

$\forall A \in T y p e, (F in t y p e (A) \land Dec i d ab l e Eq (A)) \Rightarrow (\forall a \in M u lt i se t (A), \forall t \in N, \forall n \in N, c a r d (a) = t + n \Rightarrow (\forall w \in W or d (A, n), \forall b \in B (a, t), F (a, n, t, w, b) = V (n, a - v a l (b), w)))$

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

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

Commentary.

The proof follows the unique legal occupation path and uses the actual word-count erasure recurrence for its conditional amplitude. Illegal words give zero. No orthogonality, normalization, or exact-preparation premise is assumed.

Theorem 1.5 (Sequential contraction prepares the actual uniform history).

$\forall A \in T y p e, (F in t y p e (A) \land Dec i d ab l e Eq (A)) \Rightarrow (\forall a \in M u lt i se t (A), \forall w \in W or d (A, c a r d (a)), F (a, c a r d (a), 0, w, b 0 (a)) = V (c a r d (a), a, w))$

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

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

Commentary.

This includes the empty alphabet and zero time. At the final time the only feasible occupation is a. The result is an exact equality at every actual word of the original fixed output length.

Theorem 1.6 (A cut factorization bounds rank by its bond size).

$\forall A \in T y p e, (F in t y p e (A) \land Dec i d ab l e Eq (A)) \Rightarrow (\forall a \in M u lt i se t (A), \forall t \in N, \forall s \in N, \forall b e t a \in T y p e, F in t y p e (b e t a) \Rightarrow (\forall P \in M a t r i x (W or d (A, t), b e t a, C), \forall Q \in M a t r i x (b e t a, W or d (A, s), C), coe ff i c i e n tM a t r i x (a, t, s) = P \cdot Q \Rightarrow r ank (coe ff i c i e n tM a t r i x (a, t, s)) \leq F in t y p e C a r d (b e t a)))$

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

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

Commentary.

This companion applies Matrix.rank_mul_le_left and rank_le_card_width. Its factorization premise must be established for any proposed sequential representation before using it as a memory lower bound.

FiniteChain(A,beta) is an actual finite linear chain starting in beta. A terminal constructor stores a covector beta to C. A step stores an arbitrary finite next carrier gamma, a transition A to Matrix(beta,gamma,C), and a remaining chain starting in gamma. Each step emits one symbol. length(c) counts steps; cutBond(c,t) is the actual memory after t steps. All carriers may differ; they need not be nonempty or have a common dimension. No isometry or physical normalization is required of a general chain. Function(X,Y) means maps X to Y.

K(c,v,i) denotes FiniteChain.contract on a list v and initial basis index i. For a terminal chain on the empty list it is the terminal covector at i. For a step with transition T and remaining chain r on x::xs it is the sum over j in the actual next carrier of T(x,i,j) K(r,xs,j). Other constructor/list length mismatches give zero. L(c,t,u,i,b) denotes left: at t=0 it is delta(i,b), and for a step chain at cut t+1 on x::xs it sums T(x,i,j) L(r,t,xs,j,b). R(c,t,v,b) denotes right: it drops t step constructors and contracts v from b with the remaining cap. Only cuts t<=length(c) are asserted below. List append is written append; wordAppend denotes Fin.append on the existing Fin-indexed words, and ofFn lists their entries.

Theorem 1.7 (Actual contraction splits through every cut memory).

$\forall A \in T y p e, \forall b e t a \in T y p e, F in t y p e (b e t a) \Rightarrow \forall c \in F ini t e C hain (A, b e t a), \forall t \in N, t \leq l e n g t h (c) \Rightarrow \forall u \in L i s t (A), \forall v \in L i s t (A), l e n g t h (u) = t \Rightarrow \forall i \in b e t a, K (c, a pp e n d (u, v), i) = b : c u tB o n d (c, t) \sum L (c, t, u, i, b) \cdot R (c, t, v, b)$

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

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

Commentary.

Induction on the cut, generalized over the starting carrier and prefix, derives this identity from the actual recursive sums. The successor step exchanges the next-memory and cut-memory sums; the zero cut uses the delta identity. The suffix list is unrestricted, so incompatible lengths are also handled.

amp(c,initial,w) denotes amplitude, the sum of initial(i) K(c,ofFn(w),i) over i. P(c,initial,t) denotes prefixMatrix with entry P(u,b) equal to the sum of initial(i) L(c,t,ofFn(u),i,b). Q(c,t,s) denotes suffixMatrix with entry Q(b,v)=R(c,t,ofFn(v),b). Their row and column types are respectively Word(A,t) x cutBond(c,t) and cutBond(c,t) x Word(A,s). entry(M,u,v) is M(u,v).

Theorem 1.8 (The word amplitude is the product entry).

$\forall A \in T y p e, \forall b e t a \in T y p e, F in t y p e (b e t a) \Rightarrow (\forall c \in F ini t e C hain (A, b e t a), \forall ini t ia l \in F u n c t i o n (b e t a, C), \forall t \in N, \forall s \in N, t \leq l e n g t h (c) \Rightarrow (\forall u \in W or d (A, t), \forall v \in W or d (A, s), am p (c, ini t ia l, w or d A pp e n d (u, v)) = e n t ry (P (c, ini t ia l, t) \cdot Q (c, t, s), u, v)))$

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

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

Commentary.

List.ofFn_fin_append connects the existing actual word concatenation to the proved contraction split. Summing the initial vector and exchanging the two finite sums gives exactly matrix multiplication at every pair of words.

Theorem 1.9 (Every exact chain factors the existing coefficient matrix).

$\forall A \in T y p e, (F in t y p e (A) \land Dec i d ab l e Eq (A)) \Rightarrow (\forall b e t a \in T y p e, F in t y p e (b e t a) \Rightarrow (\forall c \in F ini t e C hain (A, b e t a), \forall ini t ia l \in F u n c t i o n (b e t a, C), \forall a \in M u lt i se t (A), \forall t \in N, \forall s \in N, l e n g t h (c) = t + s \Rightarrow ((\forall w \in W or d (A, t + s), am p (c, ini t ia l, w) = V (t + s, a, w)) \Rightarrow coe ff i c i e n tM a t r i x (a, t, s) = P (c, ini t ia l, t) \cdot Q (c, t, s))))$

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

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

Commentary.

Exactness quantifies over every full word and equates the computed amplitude with sectorVector. It assumes no cut factorization. The existing definition of coefficientMatrix on Fin.append and the proved product entries establish the matrix equality. The chain has the explicit fixed length t+s.

Theorem 1.10 (Every exact chain has a sufficiently large actual cut bond).

$\forall A \in T y p e, (F in t y p e (A) \land Dec i d ab l e Eq (A)) \Rightarrow (\forall b e t a \in T y p e, F in t y p e (b e t a) \Rightarrow (\forall c \in F ini t e C hain (A, b e t a), \forall ini t ia l \in F u n c t i o n (b e t a, C), \forall a \in M u lt i se t (A), \forall t \in N, \forall s \in N, l e n g t h (c) = t + s \Rightarrow ((\forall w \in W or d (A, t + s), am p (c, ini t ia l, w) = V (t + s, a, w)) \Rightarrow r ank (coe ff i c i e n tM a t r i x (a, t, s)) \leq F in t y p e C a r d (c u tB o n d (c, t)))))$

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

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

Commentary.

The preceding constructed factorization supplies the equality premise of coefficient_rank_le_bond. The bound uses the cardinality of this chain’s actual cut carrier, for every finite model satisfying the stated output equality.

Theorem 1.11 (The necessary memory is at least the feasible occupation count).

$\forall A \in T y p e, (F in t y p e (A) \land Dec i d ab l e Eq (A)) \Rightarrow (\forall b e t a \in T y p e, F in t y p e (b e t a) \Rightarrow (\forall c \in F ini t e C hain (A, b e t a), \forall ini t ia l \in F u n c t i o n (b e t a, C), \forall a \in M u lt i se t (A), \forall t \in N, \forall s \in N, c a r d (a) = t + s \Rightarrow (l e n g t h (c) = t + s \Rightarrow ((\forall w \in W or d (A, t + s), am p (c, ini t ia l, w) = V (t + s, a, w)) \Rightarrow c a r d (b o u n d a r i es (a, t)) \leq F in t y p e C a r d (c u tB o n d (c, t))))))$

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

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

Commentary.

The explicit occupation-cardinality condition permits coefficient_rank to identify the coefficient rank with the number of feasible boundaries. No rank equality or factorization is requested from the proposed model.

O(a,n,t) denotes occupationChain. For O(a,n+1,t), the transition is T(i,b,c)=S(a,t)((i,c),b) and the remaining chain is O(a,n,t+1). Its zero-step terminal covector is delta(val(b),a). I0(a) denotes occupationInitial, the delta at initialBoundary(a). Thus this is the already proved occupation construction in the general finite-chain carrier.

Theorem 1.12 (The occupation chain has its declared number of steps).

$\forall A \in T y p e, Dec i d ab l e Eq (A) \Rightarrow (\forall a \in M u lt i se t (A), \forall n \in N, \forall t \in N, l e n g t h (O (a, n, t)) = n)$

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

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

Commentary.

This structural identity holds for all n and t; the alphabet need only have decidable equality.

Theorem 1.13 (Every occupation chain cut has the actual boundary size).

$\forall A \in T y p e, Dec i d ab l e Eq (A) \Rightarrow (\forall a \in M u lt i se t (A), \forall n \in N, \forall t \in N, \forall k \in N, k \leq n \Rightarrow F in t y p e C a r d (c u tB o n d (O (a, n, t), k)) = c a r d (b o u n d a r i es (a, t + k)))$

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

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

Commentary.

Induction selects the stored carrier at the requested legal cut. This counts the actual dependent memory type, including empty carriers when the occupation constraints have no solution.

Theorem 1.14 (The generic chain computes the existing occupation contraction).

$\forall A \in T y p e, Dec i d ab l e Eq (A) \Rightarrow (\forall a \in M u lt i se t (A), \forall n \in N, \forall t \in N, \forall w \in W or d (A, n), \forall b \in B (a, t), K (O (a, n, t), o f F n (w), b) = F (a, n, t, w, b))$

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

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

Commentary.

The recursive finite sums agree at every word and every starting occupation. No cardinality or active-step hypothesis is needed for this identification.

Theorem 1.15 (The actual occupation chain is an exact model).

$\forall A \in T y p e, (F in t y p e (A) \land Dec i d ab l e Eq (A)) \Rightarrow (\forall a \in M u lt i se t (A), \forall w \in W or d (A, c a r d (a)), am p (O (a, c a r d (a), 0), I 0 (a), w) = V (c a r d (a), a, w))$

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

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

Commentary.

The initial delta selects the existing history_sequential_preparation theorem. The exactness premise of the universal chain theorems is therefore realized by the proved occupation construction, including length zero.

Definition 1.16 (Maximum of the actual chain bonds).

$\forall A \in T y p e, \forall b e t a \in T y p e, F in t y p e (b e t a) \Rightarrow (\forall c \in F ini t e C hain (A, b e t a), ma x im u m B o n d (c) = F in se tS u p (r an g e (l e n g t h (c) + 1), t \mapsto F in t y p e C a r d (c u tB o n d (c, t))))$

Formalization. D5/S3/Quantum/Entanglement/SequentialOccupationHistory.maximumBond (✓ std3).

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

Commentary.

FinsetSup(range(length(c)+1),f) includes every cut from zero through length(c). In particular a zero-step chain still has its actual initial/terminal bond.

Theorem 1.17 (Every exact chain needs the target maximum bond).

$\forall A \in T y p e, (F in t y p e (A) \land Dec i d ab l e Eq (A)) \Rightarrow (\forall b e t a \in T y p e, F in t y p e (b e t a) \Rightarrow (\forall c \in F ini t e C hain (A, b e t a), \forall ini t ia l \in F u n c t i o n (b e t a, C), \forall a \in M u lt i se t (A), l e n g t h (c) = c a r d (a) \Rightarrow ((\forall w \in W or d (A, c a r d (a)), am p (c, ini t ia l, w) = V (c a r d (a), a, w)) \Rightarrow b o u n d a ry M a x im u m (a) \leq ma x im u m B o n d (c))))$

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

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

Commentary.

The starting finite type may lie in any universe, independent of the alphabet. Every legal cut uses sequential_memory_necessity with remaining length card(a)-t. No factorization, isometry, normalized cap, or attaining chain is assumed.

Theorem 1.18 (The occupation chain attains the target maximum).

$\forall A \in T y p e, Dec i d ab l e Eq (A) \Rightarrow (\forall a \in M u lt i se t (A), ma x im u m B o n d (O (a, c a r d (a), 0)) = b o u n d a ry M a x im u m (a))$

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

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

Commentary.

occupation_chain_bond_card identifies every actual carrier in the same finite supremum, and occupation_chain_length identifies the endpoint.

Definition 1.19 (Achievable maximum bonds include actual exact preparations).

$\forall A \in T y p e, (F in t y p e (A) \land Dec i d ab l e Eq (A)) \Rightarrow (\forall a \in M u lt i se t (A), \forall m \in N, m \in a c hi e v ab l e M a x im u m B o n d s (a) \Leftrightarrow (\exists b e t a \in T y p e, \exists f ini t e \in F in t y p e (b e t a), \exists c \in F ini t e C hain (A, b e t a), \exists ini t ia l \in F u n c t i o n (b e t a, C), l e n g t h (c) = c a r d (a) \land ((\forall w \in W or d (A, c a r d (a)), am p (c, ini t ia l, w) = V (c a r d (a), a, w)) \land ma x im u m B o n d (c) = m)))$

Formalization. D5/S3/Quantum/Entanglement/SequentialOccupationHistory.achievableMaximumBonds (✓ std3).

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

Commentary.

The existential beta ranges over types in the alphabet’s universe. Its finite instance, chain, initial vector, length equality, pointwise exact output, and actual maximumBond value are all part of the witness. The universal necessity theorem also applies to carriers in any other universe.

Theorem 1.20 (The least achievable maximum is attained).

$\forall A \in T y p e, (F in t y p e (A) \land Dec i d ab l e Eq (A)) \Rightarrow (\forall a \in M u lt i se t (A), I s L e a s t (a c hi e v ab l e M a x im u m B o n d s (a), b o u n d a ry M a x im u m (a)))$

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

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

Commentary.

IsLeast includes membership and a lower bound for every member. Membership is witnessed here by beta=B(a,0), occupationChain(a,card(a),0), and the actual occupationInitial delta. occupation_chain_preparation supplies the exact output, and the previous theorem supplies its maximum. This holds also for empty occupation and the empty alphabet.

Theorem 1.21 (The concrete attained minimum is twelve).

$I s L e a s t (a c hi e v ab l e M a x im u m B o n d s (a s t), 12)$

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

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

Commentary.

ast is the existing occupation5040 on Option(Fin(3)), with actual counts (4;2,1,1). This specializes the general attained theorem using the transported landed maximum.

Theorem 1.22 (An actual eight-step preparation attains twelve).

$l e n g t h (O (a s t, c a r d (a s t), 0)) = 8 \land (ma x im u m B o n d (O (a s t, c a r d (a s t), 0)) = 12 \land (\forall w \in W or d (Opt i o n (F in (3)), c a r d (a s t)), am p (O (a s t, c a r d (a s t), 0), I 0 (a s t), w) = V (c a r d (a s t), a s t, w)))$

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

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

Commentary.

ConcreteChain is O(ast,card(ast),0). The actual initial carrier is Boundary(ast,0), with its empty-occupation delta, and the terminal cap selects ast in the full boundary carrier. Both have one element. Every full word has exactly the target amplitude, and card(ast)=8.

The necessity theorem concerns arbitrary algebraic FiniteChains with complex caps. The attaining occupation construction additionally has the active-step identity Gram matrices and canonical quantum channels proved above. This establishes the source’s finite MPS and variable-bond sequential-isometry scope. A unitary implementation on one fixed twelve-dimensional physical register would also need compatible embeddings and unitary extensions; those are not constructed. No time-homogeneous prediction-memory claim, or identification with dimension sixteen from the different prediction model, follows. These are known Dicke-state constructions from Raveh and Nepomechie, with no novelty claim.

References

Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.achievableMaximumBonds
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.chain_amplitude_append
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.chain_contract_append
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.coefficient_rank_le_bond
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.contraction_eq_sector
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.extension_exists_iff
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.history_5040_minimum_maximum_bond
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.history_5040_occupation_chain_attainment
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.history_sequential_preparation
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.maximumBond
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.maximum_bond_necessity
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.minimum_maximum_bond_characterization
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.next_step_gram
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.next_step_quantum_channel
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.occupation_chain_bond_card
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.occupation_chain_contract
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.occupation_chain_length
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.occupation_chain_maximum_bond
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.occupation_chain_preparation
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.sequential_coefficient_factorization
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.sequential_memory_necessity
Truth anchor: D5/S3/Quantum/Entanglement/SequentialOccupationHistory.sequential_rank_necessity
Dependency: D5/S3/Quantum/Entanglement/CoherentHistorySchmidt
Dependency: D5/S3/Quantum/Foundation/FiniteKrausChannel

Keyboard shortcuts

trureturing — Discovering truth

Sequential Occupation History

Abstract

References