Icosahedral Hodge Representations

Abstract

The two Hodge eigenspaces carry conjugate real A5 representations and split the wedge.

Definition 1.1 (The positive Hodge projector selects one eigenspace).

Lean statement: D5/S3/Factorization/Icosahedral/ExteriorSquareRepresentations.positiveProjection

Formalization. D5/S3/Factorization/Icosahedral/ExteriorSquareRepresentations.positiveProjection (✓ std3).

Source. Repository-derived.

Commentary.

The positive spectral projector selects the square-root-of-five Hodge eigenspace that carries one A5 representation.

Definition 1.2 (The negative Hodge projector selects the conjugate eigenspace).

Lean statement: D5/S3/Factorization/Icosahedral/ExteriorSquareRepresentations.negativeProjection

Formalization. D5/S3/Factorization/Icosahedral/ExteriorSquareRepresentations.negativeProjection (✓ std3).

Source. Repository-derived.

Commentary.

The negative spectral projector selects the conjugate Hodge eigenspace that carries the second A5 representation.

Definition 1.3 (One quadratic action has two conjugate real embeddings).

Lean statement: D5/S3/Factorization/Icosahedral/ExteriorSquareRepresentations.RepresentationsAreQ5GaloisConjugate

Formalization. D5/S3/Factorization/Icosahedral/ExteriorSquareRepresentations.RepresentationsAreQ5GaloisConjugate (✓ std3).

Source. Repository-derived.

Commentary.

The carrier records a single exact matrix family over Q of square root five whose two embeddings give the two real coordinate actions.

Definition 1.4 (The exterior square is explicitly the product of its Hodge eigenspaces).

Lean statement: D5/S3/Factorization/Icosahedral/ExteriorSquareRepresentations.exteriorSquareDecomposition

Formalization. D5/S3/Factorization/Icosahedral/ExteriorSquareRepresentations.exteriorSquareDecomposition (✓ std3).

Source. Repository-derived.

Commentary.

Spectral projectors and the coordinate equivalence assemble an explicit A5-equivariant product decomposition.

Truth anchor: D5/S3/Factorization/Icosahedral/ExteriorSquareRepresentations.RepresentationsAreQ5GaloisConjugate
Truth anchor: D5/S3/Factorization/Icosahedral/ExteriorSquareRepresentations.exteriorSquareDecomposition
Truth anchor: D5/S3/Factorization/Icosahedral/ExteriorSquareRepresentations.negativeProjection
Truth anchor: D5/S3/Factorization/Icosahedral/ExteriorSquareRepresentations.positiveProjection
Dependency: D5/S3/Factorization/Icosahedral/ExteriorSquareCoordinates