III.1 Exact packets and arbitrary circuit length
On this page · Permalink · Source line 1
Let \(R\) be a unital ring, not necessarily commutative, and let \(I\) be a finite address set. An exact packet family consists of elements \(P_a\in R\) satisfying
Adjoint conditions are added when needed. For an operator \(U\), define the transfer corner
The target index comes first. Completeness and distributivity give
The second identity uses \(P_c^2=P_c\) when adjacent transfer corners are multiplied.
III.1.1 Circuit paths: source Theorem 4.1
On this page · Permalink · Source line 18
For \(U=U_m\cdots U_1\), the checked result is
The Lean implementation defines a recursive path sum and proves the identity by induction over an arbitrary finite gate list. It is not restricted to a fixed circuit depth. The empty list has circuit operator \(1\) and path value \(P_bP_a\). Summing the source and target indices reconstructs the full circuit.
III.1.2 Adjoint conservation: source Theorem 4.2
On this page · Permalink · Source line 29
Assume a star operation with \(P_a^*=P_a\). Then
The two checked conservation laws are
For the first law, expand each corner, collapse \(P_b^2\) and sum:
The second law follows by the analogous calculation and has its own formal proof. For complex matrices, the adjoint is the conjugate transpose. The order of the operator products is preserved throughout.
III.2 Symmetry and measurement
On this page · Permalink · Source line 52
III.2.1 Exact symmetry: source Theorem 5.1
On this page · Permalink · Source line 53
If \(HP_a=P_aH\) for every packet, then
In a complex Banach algebra, commutation also propagates to the actual exponential:
Consequently,
Taking \(z=-it\) gives evolution in real time. The Lean proof applies the exponential commutation theorem directly, so invariance of the packets is a proved consequence of commutation. Self-adjointness of \(H\) is not needed for the algebraic reducing property, so this result applies more broadly than the Hermitian specialization in the paper.
This result describes exact symmetry. The quantitative leakage estimate when symmetry is broken appears in Theorem 5.2 and requires the separate Duhamel and norm arguments developed later.
III.2.2 Measurements: source Theorem 7.1
On this page · Permalink · Source line 73
For finite complex matrices, define packet dephasing by
The code proves idempotence and trace duality:
Trace duality follows term by term from cyclicity:
Therefore an effect that is diagonal in the packets, \({\mathcal D_P}(E)=E\), satisfies
The proof holds for arbitrary finite complex matrices \(E\) and \(\rho\). Density matrices and positive measurement effects are valid specializations rather than assumptions needed for this trace identity. Taking \(E=1\) also gives trace preservation of packet dephasing.
The full theorem for Kraus channels and the Knill–Laflamme recovery criterion require further arguments about positivity, auxiliary systems, and recovery maps. The trace identity above supplies only the measurement statement.
III.3 Corrected Feshbach resolvent
On this page · Permalink · Source line 99
Write a finite complex matrix in retained and eliminated coordinates:
Set
The effective Hamiltonian is \(H_{\mathrm{eff}}(z)=A+BD_z^{-1}C\), so \(S_z=zI_P-H_{\mathrm{eff}}(z)\).
III.3.1 Correct statement: source Theorem 9.1
On this page · Permalink · Source line 112
Assume both \(D_z\) and \(zI-H\) are invertible. Then \(S_z\) is invertible and
The left side is the submatrix of the full inverse on the retained coordinates. This matches the paper's compressed operator when written in an orthonormal basis of the retained subspace. The proof is valid for arbitrary complex blocks of compatible sizes and does not require Hermiticity.
The checked invertibility criterion is
Thus one may equivalently assume invertibility of \(D_z\) and \(S_z\).
Why the original assumption is insufficient. Take \(z=0\) and \(H={\operatorname{diag}}(0,-1)\), retaining the first coordinate. Then
The eliminated block is invertible, but the full matrix is singular. Hence the original hypothesis does not ensure the existence of its stated resolvent. The Lean counterexample proves invertibility of the scalar \(1\) and noninvertibility of this full \(2\times2\) matrix.
III.3.2 Provenance and limits
On this page · Permalink · Source line 135
The proof of the general block inverse was reused from the checked fifth block of Paper VI and compiled in the Paper VII namespace for the archived formal checkpoint. That formal development also added the counterexample above. The retained checkpoint is dated 6 September 2026. This edition revises the exposition without claiming a new Schur identity or a fresh Lean compilation.
The memory equation in the time domain in Section 9.2, resolvent control uniform in the cutoff, and continuum limits require arguments beyond this finite inverse identity. The source amendment makes the two invertibility assumptions explicit without changing the intended effective Hamiltonian.
III.4 Dispersion with an explicit spacing condition
On this page · Permalink · Source line 142
The grid eigenvalue in source Theorem 11.1 is
The original low-mode condition is \(0\le kh/2\le1\). A nonzero spacing is also required for the quotient to have its intended meaning. For a physical grid, one normally takes \(h>0\).
III.4.1 Checked stronger statement
On this page · Permalink · Source line 149
For every \(k,h\in{\mathbb R}\) with \(h\ne0\),
The code proves this without the low-mode restriction. The bound may be loose away from the low-mode regime, but it remains valid.
The proof begins with an estimate valid for every real argument:
The lower bound follows from \(|\sin x|\le|x|\). For the upper bound, use
Factoring the difference of squares gives
With \(x=kh/2\) and \(h\ne0\),
Every algebraic transformation and inequality in the active source was accepted by Lean.
III.4.2 What this does not establish
On this page · Permalink · Source line 182
This is an exact deterministic error bound for the displayed dispersion relation. The original paper's numerical convergence experiment and spectral dimension measurements provide a different kind of evidence and were not rerun during this prose revision. The bound alone does not select a physical spacetime geometry.
III.5 A constraint diagnostic that vanishes automatically
On this page · Permalink · Source line 187
Section 12 defines the physical projector using the exact common kernel of the constraints. In finite dimensions this gives \(C_aP=0\) for every \(a\). Absorb the factor \(i\) and any structure coefficient into \(f_c\), and write
Proposition III.5.1: Exact common-kernel compression
If \(C_cP=0\) for every \(c\), then
No idempotence or adjoint property of \(P\) is needed for this implication.
Read proof · Read statement and proof side by side · Permalink · Source line 192 · Claim record · Lean coverage · Code · Worked examples
Proof of Proposition III.5.1
Associativity gives
Left multiplication by \(P\) gives the second identity.
Back to statement · Read statement and proof side by side · Permalink · Source line 199 · Claim record · Lean coverage · Code · Worked examples
III.5.1 Compressed vanishing without operator closure
On this page · Permalink · Source line 207
Over the rationals, take
These displayed matrices are symmetric. The code checks that \(P^2=P\), \(P\ne0\) and \(XP=ZP=0\), but
The commutator therefore violates the closure relation with zero structure coefficients outside the physical range, even though its physical compression vanishes exactly.
III.5.2 Interpretation for the paper
On this page · Permalink · Source line 223
Vanishing of the compressed anomaly is automatic for the exact finite common kernel. It therefore cannot by itself certify full operator closure. A nonzero computed compression would instead contradict those exact assumptions or expose an approximation or implementation defect.
Existence of a nontrivial compatible refinement tower and the broader continuum program remain separate questions. A stronger closure claim must test more than this compression, and unbounded constraints need their operator domains specified. This audit is additional to the six checked source items and is not counted as a seventh original theorem.