Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

First response diamond

Abstract

Equal first-level row and column classes construct an explicit quotient diamond.

Theorem 1.1 (First response row and column diamond).

Lean statement: D5/S3/ConceptDynamics/Coding/FirstResponseDiamond.first_response_diamond

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FirstResponseDiamond.first_response_diamond (✓ std3). ∎

Source. Repository-derived.

Commentary.

Equal-column and equal-row response classes determine a common matrix from class representatives. Their membership and representative matrices recover the original graph, while the class-intersection matrix and the common matrix give an explicit elementary strong shift equivalence between the two first quotients. The factorization is derived from the row and column properties.

References