Hardy Block Conservation

Abstract

Hardy compression and leakage conserve the projected input norm.

Theorem 1.1 (Hardy blocks conserve the input projection).

$$T=PUP,H=I-PUP,P^{\ast }=P\wedge P^2=P\wedge U^{\ast }U=I\Rightarrow T^{\ast }T+H^{\ast }H=P.$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Bogoliubov/HardyBlockConservation.hardy_block_conservation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let P be a finite-dimensional Hermitian idempotent and U an isometry. The compressed block T = PUP and complementary leakage block H = (I-P)UP satisfy the exact Gram identity T* T + H* H = P.

The proof uses the conjugate-transpose product, subtraction, and identity laws from Mathlib, then the projection and isometry hypotheses.

The source writes I on the right while displaying the blocks as ambient operators. In that ambient representation the correct right side is P; I is recovered only after restricting inputs to the range of P.

Theorem 1.2 (Conservation is the identity on projected inputs).

$$Pv=v\Rightarrow T^{\ast }T+H^{\ast }Hv=v.$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Bogoliubov/HardyBlockConservation.hardy_block_conservation_on_projected_input (✓ std3). ∎

Source. Repository-derived.

Commentary.

If Pv = v, applying the ambient Gram sum to v gives v. This is the precise finite-dimensional version of the source identity on the selected Hardy input sector.

Theorem 1.3 (A proper projection refutes the ambient identity).

$$\exists P,T,H\in {\mathcal{M}}_2(\mathbb{C}),P\ne 0\wedge P\ne I\wedge P^{\ast }=P\wedge P^2=P\wedge T=PIP\wedge H=I-PIP\wedge T^{\ast }T+H^{\ast }H=P\wedge T^{\ast }T+H^{\ast }H\ne I.$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Bogoliubov/HardyBlockConservation.ambient_identity_rhs_counterexample (✓ std3). ∎

Source. Repository-derived.

Commentary.

The first-coordinate projection on C^2 is nonzero, differs from I, is Hermitian and idempotent, and with U = I makes the Gram sum equal P rather than I. This is a concrete counterexample to the unqualified ambient formulation.

References

• Truth anchor: D5/S3/Quantum/Bogoliubov/HardyBlockConservation.ambient_identity_rhs_counterexample
• Truth anchor: D5/S3/Quantum/Bogoliubov/HardyBlockConservation.hardy_block_conservation
• Truth anchor: D5/S3/Quantum/Bogoliubov/HardyBlockConservation.hardy_block_conservation_on_projected_input