Canonical mirror even-odd decomposition

Abstract

Normalized mirror spectral projections split the Krein form into even positive energy minus odd positive energy.

Theorem 1.1 (Mirror parity sectors are Hilbert orthogonal).

Lean statement: D5/S3/Midline/Cayley/CanonicalZetaMirrorEvenOddDecomposition.mirror_even_odd_inner_eq_zero

Proof. Machine-checked in Lean as D5/S3/Midline/Cayley/CanonicalZetaMirrorEvenOddDecomposition.mirror_even_odd_inner_eq_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof uses the self-adjoint involution laws rather than introducing an abstract orthogonal decomposition axiom.

Theorem 1.2 (The Krein form is even energy minus odd energy).

Lean statement: D5/S3/Midline/Cayley/CanonicalZetaMirrorEvenOddDecomposition.mirrorKreinForm_re_eq_even_norm_sq_sub_odd_norm_sq

Proof. Machine-checked in Lean as D5/S3/Midline/Cayley/CanonicalZetaMirrorEvenOddDecomposition.mirrorKreinForm_re_eq_even_norm_sq_sub_odd_norm_sq (✓ std3). ∎

Source. Repository-derived.

Commentary.

The normalized projections are idempotent, mutually annihilating, and reconstruct every vector.

References

• Truth anchor: D5/S3/Midline/Cayley/CanonicalZetaMirrorEvenOddDecomposition.mirrorKreinForm_re_eq_even_norm_sq_sub_odd_norm_sq
• Truth anchor: D5/S3/Midline/Cayley/CanonicalZetaMirrorEvenOddDecomposition.mirror_even_odd_inner_eq_zero
• Dependency: D5/S3/Midline/Cayley/CanonicalZetaMirrorFundamentalSymmetry