III.6 One seed for the computational basis
On this page · Permalink · Source line 1
Manuscript item 2.4. ComputationalSeed.lean 14 declarations
For \(n\geq 0\), let
For an address \(a\in A_n\), define the standard coordinate vector
The seed is \(\psi_0={\left|0\right\rangle}\). Define a translation operator by
At position \(j\), the local Pauli \(X\) is \(X_j=T_{e_j}\), where \(e_j\) has a single nonzero binary coordinate. The formal circuit uses the identity when \(a_j=0\) and \(X_j\) when \(a_j=1\).
Supplementary statement
For every binary address \(a\),
The family \((W_a\psi_0)_{a\in A_n}\) is linearly independent, spans \(V_n\), and has exactly \(2^n\) elements. It is the standard computational basis.
Read proof · Read statement and proof side by side · Permalink · Source line 19 · Claim record · Lean coverage · Code · Worked examples
Proof of Supplementary statement
Composition gives \(T_aT_b=T_{a+b}\), and direct evaluation gives \(T_a{\left|b\right\rangle}={\left|a+b\right\rangle}\). Every binary address satisfies \(a+a=0\), so each translation is an involution. In particular, the local operator changes precisely the addressed bit:
The selected factor at \(j\) equals translation by the address supported at \(j\) with value \(a_j\). Induction on a list proves that the product of translations is translation by their sum. Each of these addresses contributes one coordinate, and their sum is \(a\). Thus \(W_a=T_a\) and \(W_a\psi_0={\left|a\right\rangle}\).
Lean identifies the resulting family with Pi.basisFun over \({\mathbb C}\). Its standard basis theorems supply linear independence and full span. The finite function-space cardinality gives \(|A_n|=2^n\).
Back to statement · Read statement and proof side by side · Permalink · Source line 28 · Claim record · Lean coverage · Code · Worked examples
Formal scope. The proof constructs the sequence of gates that produces each addressed state and then identifies the resulting family with the standard coordinate basis. It includes the empty circuit for \(n=0\). Orthogonality belongs to the usual computational basis interpretation. The formal endpoint records the basis identification, together with separate explicit theorems for span and linear independence.
III.7 Tensor and polyphase refinement
On this page · Permalink · Source line 44
Manuscript item 3.2. TensorRefinement.lean 11 declarations
Let \(F\) be an arbitrary finite set of factors and let \(D_i\) be a finite coordinate index for factor \(i\). For matrix families \(A_i\), define the coordinate tensor product on the product index space by
The proof first establishes the laws for multiplication, identity, adjoints, and finite sums. These laws apply to any finite number of factors with the stated finite coordinate sets.
Suppose \(N>0\) and each factor has a complete orthogonal self-adjoint projector family \((P^{(i)}_j)_{j\in\mathbb Z/N\mathbb Z}\). For a fine address \(a:F\to\mathbb Z/N\mathbb Z\), set
Supplementary statement
The fine and coarse families are complete orthogonal self-adjoint projector systems. In particular,
Each coarse projector is exactly the displayed sum of its fine descendants.
Read proof · Read statement and proof side by side · Permalink · Source line 60 · Claim record · Lean coverage · Code · Worked examples
Proof of Supplementary statement
Expanding the finite product of sums gives
Consequently, if two fine addresses differ in any coordinate, the corresponding product contains a zero factor. If the addresses agree, the product is the same fine projector. The adjoint passes through the finite coordinate product, so \(Q_a^*=Q_a\). Summing over all address functions and using the same expansion yields
A separate algebraic regrouping theorem applies to any finite orthogonal family and any address map into a finite set. In the double sum for \(C_rC_s\), orthogonality removes all terms with different fine addresses. A surviving address can lie in both classes only when \(r=s\). Completeness follows by summing each fine projector exactly once. Adjoint preservation follows term by term. Specializing the address map to total residue proves the claim.
Back to statement · Read statement and proof side by side · Permalink · Source line 69 · Claim record · Lean coverage · Code · Worked examples
Formal scope. Residue grouping is proved for every positive modulus and arbitrary finite factor dimensions. It assumes the supplied local projector laws. Constructing those local projectors from cyclic characters, as in item 3.1, requires the separate proof in the next supplement.
III.8 Differentiated moving coordinates
On this page · Permalink · Source line 87
Manuscript item 6.1. MovingFrames.lean 9 declarations
Fix a real time \(t\) and a finite complex coordinate space. Let \(U(s)\) be a unitary matrix curve, differentiable entrywise at \(t\), and let \(\psi(s)\) be differentiable componentwise at \(t\). Write \(\dot U\) and \(\dot\psi\) for those derivatives. Suppose
Only the value of the Hamiltonian at the chosen time is needed. No derivative of \(H\) is assumed.
Supplementary statement
The explicitly defined coordinate curve
is differentiable at \(t\), with
It satisfies
The connection term \(-iU(t)^*\dot U\) is Hermitian. If \(H^*=H\), then \(H_{\mathrm{eff}}^*=H_{\mathrm{eff}}\).
Read proof · Read statement and proof side by side · Permalink · Source line 96 · Claim record · Lean coverage · Code · Worked examples
Proof of Supplementary statement
Applying the product rule entry by entry proves the differentiation formulas for matrix products and for matrices acting on vectors. Since the parameter is real, conjugation commutes with differentiation, giving the stated derivative of \(U^*\) and hence of \(y\).
Differentiate \(U^*U=I\) using those rules and uniqueness of derivatives:
Thus \((U^*\dot U)^*=-U^*\dot U\), so multiplication by \(-i\) produces a Hermitian matrix.
The identity \(UU^*=I\) gives \(\psi=Uy\) for the constructed coordinate curve. Differentiating and inserting the original equation yields
Multiplying by \(U^*\) and using \(U^*U=I\) gives the transformed equation, with the negative sign on the connection term. Finally, conjugation by \(U\) preserves Hermiticity of \(H\), and the sum of the two Hermitian terms is Hermitian.
Back to statement · Read statement and proof side by side · Permalink · Source line 113 · Claim record · Lean coverage · Code · Worked examples
Formal scope. The main certificate constructs \(y\) and its derivative rather than assuming a separate derivative witness for the desired answer. Both unitary identities are explicit. The proofs are pointwise and apply at any time where the stated hypotheses hold. They do not assert existence of a global solution to an evolution equation.
III.9 The canonical packet connection
On this page · Permalink · Source line 135
Manuscript item 6.3. CanonicalConnection.lean 9 declarations
Let \(P_a(s)\) be a finite family in a normed real algebra with a continuous compatible adjoint. Assume actual derivatives \(D_a=\dot P_a(t)\) exist and, for all parameter values under consideration,
In the supplied Lean theorem, the curves are defined on \({\mathbb R}\) and the projector laws hold at every real parameter. The algebraic formulation applies to matrices and bounded operators whenever they satisfy the stated typeclass hypotheses.
Supplementary statement
Define \(C=\sum_aD_aP_a(t)\). Then
and, for every \(b\),
Read proof · Read statement and proof side by side · Permalink · Source line 144 · Claim record · Lean coverage · Code · Worked examples
Proof of Supplementary statement
The derivative product rule and uniqueness of derivatives give
Differentiating completeness and adjoint invariance gives
These are proved derivative consequences, not additional axioms supplied in place of differentiation.
On the diagonal, \(D_aP_a+P_aD_a=D_a\). Summing shows
This proves the formula involving half the sum of commutators, together with \(C^*=-C\).
Orthogonality directly yields \(CP_b=D_bP_b\). For the left product, multiply the differentiated identity for \((b,a)\) on the right by \(P_a\) and sum over \(a\). Completeness reduces the result to
Subtracting this equation from the identity for multiplication on the right gives \(CP_b-P_bC=D_b\).
Back to statement · Read statement and proof side by side · Permalink · Source line 155 · Claim record · Lean coverage · Code · Worked examples
Formal scope. The proof derives the differentiated identities before using their algebraic consequences, so the role of the derivative hypotheses remains explicit. It establishes the canonical connection identity for one parameter. The range bundle over a parameter manifold, the exterior differential calculus, and the curvature theorem of item 6.4 are developed in the later supplements.
III.10 Finite Kraus channels and full amplification
On this page · Permalink · Source line 185
Manuscript item 7.2. KrausChannels.lean 7 declarations
For a finite family of complex matrices \(K_a\), define
The formalization constructs this as a complex-linear map and proves the following properties directly in the finite matrix representation.
Supplementary statement
The map \(\Phi\) is completely positive. If
then \({\operatorname{tr}}\Phi(\rho)={\operatorname{tr}}\rho\) for every matrix \(\rho\). In particular, positive semidefinite matrices of trace one are mapped to positive semidefinite matrices of trace one.
Read proof · Read statement and proof side by side · Permalink · Source line 194 · Claim record · Lean coverage · Code · Worked examples
Proof of Supplementary statement
Matrix multiplication distributes across addition and scalar multiplication, which gives complex linearity. If \(\rho\succeq0\), each term \(K_a\rho K_a^*\) is positive semidefinite, hence so is their finite sum.
To prove complete positivity rather than positivity alone, let \(J\) be an arbitrary finite auxiliary index set. For a matrix \(X\) indexed by \(J\times n\), define its blockwise amplification by
The explicit index calculation proves the identity
The displayed identity identifies the defined amplification with tensoring by the identity, which is the operation needed for complete positivity. Every summand on the right is positive when \(X\) is positive, and this holds for every finite \(J\).
Finally, cyclicity and linearity of the trace give
Positivity together with trace preservation gives the stated conclusion for density matrices.
Back to statement · Read statement and proof side by side · Permalink · Source line 202 · Claim record · Lean coverage · Code · Worked examples
Formal scope. Complete positivity is proved for every finite auxiliary dimension. Normalization is required only for trace preservation and the conclusion about density matrices. The converse representation theorem for arbitrary completely positive maps lies outside this argument.