Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite mirror Krein index

Abstract

A finite symmetric zero window has one strictly negative odd coordinate per nonfixed mirror pair and analytic multiplicity.

Theorem 1.1 (The finite mirror index vanishes exactly on critical windows).

Lean statement: D5/S3/Midline/Cayley/FiniteMirrorKreinIndex.finite_mirror_krein_index_zero_iff_critical

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

Source. Repository-derived.

Commentary.

The smaller index in each two-point mirror orbit selects one representative, while multiplicity supplies the odd-coordinate fiber.

Theorem 1.2 (The finite odd-sector form is strictly negative).

Lean statement: D5/S3/Midline/Cayley/FiniteMirrorKreinIndex.finiteMirrorOddQuadratic_strictly_negative

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

Source. Repository-derived.

Commentary.

The odd-coordinate type has cardinality kappa_T and carries the standard negative norm-square form.

References