Phase History Bound

Abstract

Actual sequential source moments and a common-center phase-history operator bound.

The source has a two-dimensional complex memory and a fresh blank physical bit at each step. Every emitted bit and the final memory are retained. Bit is Bool, with false denoted 0 and true denoted 1; bit converts these labels to the real numbers 0 and 1. Throughout, p is real with 0<p<1, n and all time indices are natural numbers, and phi and delta are arbitrary real sequences. Space(A) is the complex Euclidean space on the finite type A, e is its coordinate basis, Unitary(A) is its linear isometry equivalence group, and indicator(P) is 1 or 0 according to P.

Definition 1.1 (Memory amplitudes).

$m e m ory (p, 0, 0) = s q r t (1 - p) \land (m e m ory (p, 0, 1) = s q r t (p) \land (m e m ory (p, 1, 0) = 1 \land m e m ory (p, 1, 1) = 0))$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.memory (✓ std3).

Source. Repository-derived.

Commentary.

Rows are indexed by the incoming memory and columns by the outgoing memory. The emitted physical bit copies the incoming memory. These amplitudes are nonnegative.

Definition 1.2 (Squared memory amplitudes).

$t r an s i t i o n (p, 0, 0) = 1 - p \land (t r an s i t i o n (p, 0, 1) = p \land (t r an s i t i o n (p, 1, 0) = 1 \land t r an s i t i o n (p, 1, 1) = 0))$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.transition (✓ std3).

Source. Repository-derived.

Commentary.

The transition matrix is the entrywise square of memory, with rows (1-p,p) and (1,0). Each row sums to one. The probability law below is derived from the physical amplitudes.

Definition 1.3 (The blank-input isometry).

$s t e p (p, g amma, p ai r (j, k), i) = in d i c a t or (j = i) \cdot e x p (ima g ina ry U ni t \cdot g amma \cdot bi t (i)) \cdot m e m ory (p, i, k)$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.step (✓ std3).

Source. Repository-derived.

Commentary.

gamma is real and i,j,k range over Bit. step is a matrix from Bit to Bit x Bit. Its orthonormal columns specify the action of a two-bit unitary on the blank physical input.

Definition 1.4 (A path retains its terminal memory).

$P a t h (0) = B i t \land P a t h (n + 1) = P ro d (B i t, P a t h (n))$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.Path (✓ std3).

Source. Repository-derived.

Commentary.

Path(n) represents (x(0),…,x(n)). Its first n entries are physical archive bits and x(n) is final memory. pathFintype recursively supplies the finite enumeration, and pathDecidableEq recursively decides equality; both use the Bool instances at length zero and product instances at successors.

Definition 1.5 (The initial memory label).

$h e a d (0, i) = i \land h e a d (n + 1, p ai r (i, x)) = i$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.head (✓ std3).

Source. Repository-derived.

Commentary.

head(n,x) is x(0). At length zero the entire path is the memory label.

Definition 1.6 (Real-valued occupation observations).

$o b ser v e d (0, i, s) = bi t (i) \land (o b ser v e d (n + 1, p ai r (i, x), 0) = bi t (i) \land o b ser v e d (n + 1, p ai r (i, x), s + 1) = o b ser v e d (n, x, s))$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.observed (✓ std3).

Source. Repository-derived.

Commentary.

For 0<=s<=n, observed(n,x,s) is the occupation bit x(s). The definition saturates at final memory beyond n; the moment theorem uses only times through n. Write X(s) for the function x mapped to observed(n,x,s).

Definition 1.7 (The source path mass).

$p a t h M a ss (p, 0, i) = 1 \land p a t h M a ss (p, n + 1, p ai r (i, x)) = t r an s i t i o n (p, i, h e a d (n, x)) \cdot p a t h M a ss (p, n, x)$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.pathMass (✓ std3).

Source. Repository-derived.

Commentary.

pathMass is the product of the n squared memory amplitudes. Fixing head(n,x)=i supplies the initial condition; there is no stationary initial distribution.

Definition 1.8 (The physical amplitude along a path).

$p a t h A m pl i t u d e (p, p hi, 0, t, i) = 1 \land p a t h A m pl i t u d e (p, p hi, n + 1, t, p ai r (i, x)) = e x p (ima g ina ry U ni t \cdot p hi (t) \cdot bi t (i)) \cdot m e m ory (p, i, h e a d (n, x)) \cdot p a t h A m pl i t u d e (p, p hi, n, t + 1, x)$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.pathAmplitude (✓ std3).

Source. Repository-derived.

Commentary.

The start time t shifts the phase history. Each factor is the local phase on incoming memory times its transition amplitude.

Definition 1.9 (The full archive-and-memory source matrix).

$so u rce (p, p hi, n, t, x, i) = in d i c a t or (h e a d (n, x) = i) \cdot p a t h A m pl i t u d e (p, p hi, n, t, x)$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.source (✓ std3).

Source. Repository-derived.

Commentary.

source(p,phi,n,t) has rows Path(n) and columns Bit. It includes the final memory and preserves both input columns. At n=0 it is exactly the identity matrix on Bit, independently of p, phi and t.

Definition 1.10 (The path and physical register have the same coordinates).

$re g i s t er (n, x) = p ai r (a rc hi v e (n, x), t er mina l (n, x))$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.register (✓ std3).

Source. Repository-derived.

Commentary.

register(n) is an equivalence from Path(n) to ((Fin(n) to Bit) x Bit): archive lists x(0) through x(n-1), and terminal is x(n). It recursively uses SequentialRegisterCircuit.headRest, with the unique empty archive at zero.

Definition 1.11 (Expectation in a fixed input column).

$e x p ec t a t i o n (p, n, i, f) = x : P a t h (n) \sum in d i c a t or (h e a d (n, x) = i) \cdot p a t h M a ss (p, n, x) \cdot f (x)$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.expectation (✓ std3).

Source. Repository-derived.

Commentary.

f is any real function on Path(n). Write E(n,i,f) for this expectation with p understood. Its weights are the Born probabilities of the actual circuit, and their normalization is a conclusion below.

Definition 1.12 (The nonstationary occupation mean).

$m e an (p, i, s) = \frac{p}{1 + p} + (bi t (i) - \frac{p}{1 + p}) \cdot (- p)^{s}$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.mean (✓ std3).

Source. Repository-derived.

Commentary.

q=p/(1+p) is the equilibrium occupation. The transient (bit(i)-q)(-p)^s retains the deterministic initial bit. Write m(i,s)=mean(p,i,s).

Theorem 1.13 (One actual unitary sequence realizes the path law at every length).

$\forall p \in R, (0 < p \land p < 1) \Rightarrow (\forall p hi \in F u n c t i o n (N, R), \exists U \in F u n c t i o n (N, U ni t a ry (P ro d (B i t, B i t))), (\forall t \in N, \forall i \in B i t, \forall j \in B i t, \forall k \in B i t, U (t, e (p ai r (0, i)), p ai r (j, k)) = s t e p (p, p hi (t), p ai r (j, k), i)) \land ((\forall n \in N, \forall t \in N, \forall i \in B i t, \forall x \in P a t h (n), c i rc u i t (U, n, t, b l ank St a t e (0, n, i), re g i s t er (n, x)) = so u rce (p, p hi, n, t, x, i)) \land ((\forall n \in N, \forall t \in N, \forall i \in B i t, \forall x \in P a t h (n), n or m (so u rce (p, p hi, n, t, x, i))^{2} = in d i c a t or (h e a d (n, x) = i) \cdot p a t h M a ss (p, n, x)) \land ((\forall n \in N, \forall i \in B i t, E (n, i, co n s t an t (1)) = 1) \land ((\forall n \in N, \forall i \in B i t, \forall s \in N, s \leq n \Rightarrow E (n, i, X (s)) = m e an (p, i, s)) \land (\forall n \in N, \forall i \in B i t, \forall s \in N, \forall t \in N, (s \leq t \land t \leq n) \Rightarrow E (n, i, p ro d u c t (X (s), X (t))) - m e an (p, i, s) \cdot m e an (p, i, t) = (- p)^{t - s} \cdot m e an (p, i, s) \cdot (1 - m e an (p, i, s))))))))$

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

Source. Repository-derived.

Commentary.

The same U is chosen before n and t, so it realizes every length and every start time. circuit, blankState, and the unitary Hilbert spaces are those of SequentialRegisterCircuit. The first equation specifies U on its blank-input subspace; the second identifies its actual composed coefficients with source. The remaining equations give squared amplitudes, normalization, mean, and the exact two-time covariance. product denotes pointwise multiplication of real functions. The proof first extends each local isometry to a unitary, then identifies the recursive circuit coefficients and derives the moments by conditioning on the first transition. In particular, at p=1/2, n=2, i=0, s=1, t=2, the covariance is -1/8.

Linearity extends the coefficient identity to every complex memory vector v: the actual initialized circuit coefficient at register(n,x) is the sum over i of v(i)source(p,phi,n,t,x,i). Thus these are coherent source maps, including superpositions of the two memory inputs. An arbitrary finite reference is retained in the operator inequality below.

Definition 1.14 (The uniform history constant).

$hi s t ory C o n s t an t (p) = \frac{\frac{1 + p}{1 - p} + \frac{1}{1 - p ^{2}}}{4}$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.historyConstant (✓ std3).

Source. Repository-derived.

Commentary.

Both denominators are positive for 0<p<1. The first term bounds correlated fluctuations; the second controls the transient displacement from a center shared by the two initial conditions.

Definition 1.15 (The accumulated discrepancy).

$p ha se S u m (d e lt a, n, t, x) = s : F in (n) \sum d e lt a (t + v a l (s)) \cdot o b ser v e d (n, x, v a l (s))$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.phaseSum (✓ std3).

Source. Repository-derived.

Commentary.

This sum includes the n emitted occupations, with start time t. The final memory is retained in the path but adds no extra phase.

Definition 1.16 (One scalar center for both input columns).

$ce n t er (p, d e lt a, n) = \frac{p}{1 + p} \cdot s : F in (n) \sum d e lt a (v a l (s)) + (\frac{1}{2} - \frac{p}{1 + p}) \cdot s : F in (n) \sum d e lt a (v a l (s)) \cdot (- p)^{v a l (s)}$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.center (✓ std3).

Source. Repository-derived.

Commentary.

H is the sum of delta(s)(-p)^s for 0<=s<n. This center is the arithmetic midpoint of the two conditional means of phaseSum(delta,n,0). Their deviations from the center are (bit(i)-1/2)H. The scalar center is independent of the input vector and reference.

Definition 1.17 (The coherently centered source difference).

$error (p, t h e t a, p hi, n, b) = so u rce (p, co n s t an t (t h e t a), n, 0) - e x p (ima g ina ry U ni t \cdot b) \cdot so u rce (p, p hi, n, 0)$

Formalization. D5/S3/Quantum/Entanglement/PhaseHistoryBound.error (✓ std3).

Source. Repository-derived.

Commentary.

theta is the real phase of the constant source and phi is the known virtual phase history. b is one real scalar, multiplying the entire second source matrix by the same complex phase. Write D=error(p,theta,phi,n,center(p,delta,n)).

Theorem 1.18 (Uniform operator and finite-reference bounds).

$\forall p \in R, (0 < p \land p < 1) \Rightarrow \forall n \in N, \forall t h e t a \in R, \forall p hi \in F u n c t i o n (N, R), \forall d e lt a \in F u n c t i o n (N, R), (\forall t \in N, t < n \Rightarrow (\exists k \in Z, t h e t a - p hi (t) = d e lt a (t) + k \cdot 2 \cdot π)) \Rightarrow PS D hi s t ory C o n s t an t (p) \cdot s : F in (n) \sum d e lt a (v a l (s))^{2} \cdot i d e n t i t y (B i t) - a d j o in t (D) \cdot D \land \forall J \in T y p e, (F in t y p e (J) \land Dec i d ab l e Eq (J)) \Rightarrow PS D hi s t ory C o n s t an t (p) \cdot s : F in (n) \sum d e lt a (v a l (s))^{2} \cdot i d e n t i t y (P ro d (J, B i t)) - a d j o in t (t e n sor (i d e n t i t y (J), D)) \cdot t e n sor (i d e n t i t y (J), D)$

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

Source. Repository-derived.

Commentary.

Bound is historyConstant(p) times the sum of delta(s)^2 for 0<=s<n. identity(J) is the identity matrix, adjoint is conjugate transpose, and tensor is the matrix Kronecker product; TensorError=identity(J) tensor D. PSD means positive semidefinite. J may be any finite type in any universe, including the empty type. Equivalently, every vector v on Bit and every vector w on J x Bit satisfy squared output norm at most Bound times their squared input norm. This includes arbitrary coherent and reference-entangled inputs without a normalization premise. The congruence condition allows any real representatives delta, without a minimal-distance restriction or a finite upper cutoff on n. For n=0 both sources are the identity, the center and error are zero, and the bound is zero.

For the bound, the exact covariance gives absolute covariance at most p raised to the time separation, divided by 4. Its geometric row sum is bounded by (1+p)/(1-p), controlling the variance of the weighted phase sum. Cauchy-Schwarz bounds H squared by the phase energy divided by (1-p^2). Adding the squared common-center bias H squared/4 gives exactly historyConstant(p). The inequality between a phase chord and its real lift then bounds each column’s squared error. The two columns have disjoint head support, so the error Gram matrix is diagonal. This yields the operator inequality, and tensoring its positive semidefinite remainder with the reference identity proves the reference statement.

Example 1.19 (The original golden memory is the p=alpha squared source).

$a lp ha = \frac{s q r t ( 5 ) - 1}{2} \land p = a lp h a^{2} \land a lp h a^{2} + a lp ha = 1 \land m e m ory (p, 0, 0) = s q r t (a lp ha) \land m e m ory (p, 0, 1) = a lp ha \land hi s t ory C o n s t an t (p) = \frac{\frac{1 + a lp h a ^{2}}{1 - a lp h a ^{2}} + \frac{1}{1 - a lp h a ^{4}}}{4}$

Source. Repository-derived.

Commentary.

alpha=(sqrt(5)-1)/2 lies strictly between zero and one and satisfies alpha squared plus alpha equals one. Consequently sqrt(1-alpha squared)=sqrt(alpha) and sqrt(alpha squared)=alpha, so the memory rows are exactly (sqrt(alpha),alpha) and (1,0). Substituting p=alpha squared into the local step therefore realizes the original memory amplitudes by the same actual unitary circuit for all lengths and start times. The center and history constant are specialized at alpha squared, not at alpha. The bound then applies to every constant theta, virtual history, congruent real lift and finite reference.

References

Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.Path
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.actual_source_moments
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.center
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.error
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.expectation
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.head
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.historyConstant
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.mean
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.memory
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.observed
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.pathAmplitude
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.pathMass
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.phaseSum
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.phase_history_bound
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.register
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.source
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.step
Truth anchor: D5/S3/Quantum/Entanglement/PhaseHistoryBound.transition
Dependency: D5/S3/Quantum/Entanglement/SequentialRegisterCircuit

Keyboard shortcuts

trureturing — Discovering truth

Phase History Bound

Abstract

References