ZeroData Hilbert presentation transport

Abstract

The unique zero-preserving reindexing lifts to a unitary transport of mirror Krein and Cayley geometry.

Theorem 1.1 (The Hilbert transport intertwines mirror symmetry).

Lean statement: D5/S3/Midline/Cayley/ZeroDataHilbertPresentationTransport.zeroHilbertPresentationUnitary_intertwines_mirror

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

Source. Repository-derived.

Commentary.

The coordinate equivalence is the unique zero-preserving reindexing lifted through analytic multiplicity fibers.

Theorem 1.2 (The Hilbert transport preserves the Krein form).

Lean statement: D5/S3/Midline/Cayley/ZeroDataHilbertPresentationTransport.zeroHilbertPresentationUnitary_preserves_krein

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

Source. Repository-derived.

Commentary.

The same unitary also intertwines the zero Cayley operators, so the operator geometry is presentation independent.

References

• Truth anchor: D5/S3/Midline/Cayley/ZeroDataHilbertPresentationTransport.zeroHilbertPresentationUnitary_intertwines_mirror
• Truth anchor: D5/S3/Midline/Cayley/ZeroDataHilbertPresentationTransport.zeroHilbertPresentationUnitary_preserves_krein
• Dependency: D5/S3/Midline/Cayley/CanonicalZetaCayleyJUnitary