III.15 Quantitative leakage from the actual exponential
On this page · Permalink · Source line 1
Let \(A\) be a unital complex C-star algebra, let \(H=H^*\), and let \(P=P^*=P^2\). Put \(Q=1-P\). The checked statement is
The matrix specialization uses the operator norm on the Hilbert space, implemented by Matrix.Norms.L2Operator. It is not an entrywise norm or the row-sum operator norm. The theorem includes the zero projector and empty matrix index type. The theorem also applies at time zero.
III.15.1 Deriving the estimate by differentiation
On this page · Permalink · Source line 8
For a skew-adjoint generator \(G\), define the actual conjugation path
The formalization derives its derivative from the exponential power series and the product rule:
Both exponential factors are proved unitary. Left and right multiplication by a unitary preserve the C-star norm. Therefore
The second inequality follows from the mean value inequality in normed spaces and covers either ordering of \(s\) and \(t\). It is not a finite-difference estimate or a numerical time discretization.
Multiplication by \(\exp(tG)\) gives
For every orthogonal projector, \(\|P\|\le1\) and \(\|1-P\|\le1\). The exact corner identity
then bounds leakage by the exponential commutator. Taking \(G=-iH\) gives the stated theorem because \(\|[G,P]\|=\|[H,P]\|\).
III.15.2 Checked consequences
On this page · Permalink · Source line 35
Unitarity also gives the capped estimate
If \(H=H_0+V\), both summands are self-adjoint, and \([H_0,P]=0\), then
The latter uses \(\|[V,P]\|\le2\|V\|\). Its constant is not claimed to be optimal. Exact commutation gives zero leakage. The work does not include unbounded generators or time-dependent Hamiltonians.
III.16 Actual projected differentiation and curvature
On this page · Permalink · Source line 48
Let \(E,F\) be real normed spaces. Let \(P:E\to\mathcal L(F,F)\) be differentiable with \(P(x)^2=P(x)\) for every \(x\). Let \(s:E\to F\) be \(C^2\) with \(P(x)s(x)=s(x)\), and let \(X,Y:E\to E\) be differentiable vector fields. The checked connection is the actual expression
It is proved to preserve the range condition. It is linear in the vector field direction and obeys the scalar Leibniz rule
for differentiable real scalar functions \(c\). No differentiated projector identities are inserted as hypotheses in the main curvature theorem.
III.16.1 Differentiated projector and section identities
On this page · Permalink · Source line 59
Differentiating \(P^2=P\) and \(Ps=s\) produces
The zero sandwich follows algebraically from the first identity. All products preserve their noncommutative order.
III.16.2 Retaining the bracket of vector fields
On this page · Permalink · Source line 68
Define the actual curvature action by
The source uses the Lie bracket defined through Fréchet derivatives. Symmetry of second derivatives is supplied by the \(C^2\) hypothesis, not postulated separately. Expanding the connection gives
Substituting the section identity and removing the zero sandwich terms proves
Thus the coefficient is precisely \(P({\,\mathrm d} P\wedge{\,\mathrm d} P)P\) with the convention \(({\,\mathrm d} P\wedge{\,\mathrm d} P)(v,w)=DP[v]DP[w]-DP[w]DP[v]\).
III.16.3 Tensor properties and the remaining global boundary
On this page · Permalink · Source line 84
The coefficient is proved bilinear, alternating, and supported on the range on both sides. The chain rule proves the pullback identity
The main theorem has global regularity hypotheses on normed parameter spaces. The pullback identity alone does not supply localization, smooth local trivializations, or gluing. The final supplement constructs the global range bundle and proves that the local connections glue.
III.17 A constructive and total syndrome recovery
On this page · Permalink · Source line 93
Let \(P\) be an orthogonal code projector. The input certificate consists of a finite family \(V_a\) satisfying
These hypotheses state that the operators are partial isometries with orthogonal syndromes. The next supplement derives such a family from arbitrary Knill–Laflamme Gram data.
III.17.1 Constructing the recovery on the whole ambient space
On this page · Permalink · Source line 102
Define the syndrome projectors and their complement by
The source proves self-adjointness, \(S_aS_b=\delta_{ab}S_a\), \(S^2=S\), and \(Q^2=Q=Q^*\). It also proves \(QV_a=0\) and \(V_a^*Q=0\).
The recovery is not left undefined outside the syndrome subspaces. Its explicit Kraus operators are \(R_a=V_a^*\) together with \(R_{\mathrm{extra}}=Q\), giving
They satisfy exact completeness:
For finite complex matrices, trace preservation and complete positivity at every finite auxiliary dimension are proved for this actual map. The amplified map is identified with the Kraus family \(I_J\otimes R_a\), including the complement term. Positivity is not merely checked on a single matrix size.
III.17.2 Exact correction, including coherent errors
On this page · Permalink · Source line 120
For every operator supported on the code, \(P\rho P=\rho\), the central identity is
Consequently normalized mixtures satisfy
The identity is algebraic and is proved for complex weights. Physical mixtures use the nonnegative real case. For a coherent error \(E_z=\sum_a z_aV_a\), the calculation of the cross terms yields
Thus the same map also corrects normalized coherent superpositions. This construction supplies the recovery stage used in the full Knill–Laflamme proof that follows.