Equivariant Diagonal Escape

Abstract

Equivariant diagonal escape counts factor exactly over the action orbits.

Lemma 1.1 (Equivariant diagonals are orbit-constant).

$$g\left(\mathrm{smul}\left(sigma,a\right),\mathrm{smul}\left(sigma,a\right)\right)=g\left(a,a\right)$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/EquivariantEscape.equivariant_diagonal_constant (✓ std3). ∎

Source. Repository-derived.

Commentary.

Simultaneous equivariance in the row and column coordinates makes the diagonal value unchanged under transport by any group element. Thus each address orbit contributes one diagonal coordinate.

Theorem 1.2 (Equivariant escape counts factor by address orbit).

$$\mathrm{card}\left(\mathrm{escapedEquivariantListings}\left(f\right)\right)=\mathrm{productOrbits}\left(\mathrm{card}{\left(Y\right)}^{{omega}_i}-\mathrm{card}\left(\mathrm{Fix}\left(f\right)\right),i\right)$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/EquivariantEscape.equivariant_escaped_card (✓ std3). ∎

Source. Repository-derived.

Commentary.

Choose explicit stabilizer-orbit coordinates for the equivariant listings. After revealing the orbit-diagonal values, each address orbit has one forbidden off-diagonal row exactly when its diagonal value is fixed by the twist. Finite sums of these independent row choices separate into the product of card(Y)^omega_i minus the fixed-point count.

Theorem 1.3 (Transitive actions have one escape factor).

$$\mathrm{card}\left(\mathrm{escapedEquivariantListings}\left(f\right)\right)=\mathrm{card}{\left(Y\right)}^{{omega}_i}-\mathrm{card}\left(\mathrm{Fix}\left(f\right)\right)$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/EquivariantEscape.transitive_equivariant_escaped_card (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a transitive action the address-orbit quotient has one element, so the general product reduces to the single factor determined by the stabilizer-orbit count.

Theorem 1.4 (Trivial orbit data recovers the free count).

$$\mathrm{productAddresses}\left(\mathrm{card}{\left(Y\right)}^{\mathrm{card}\left(A\right)}-\mathrm{card}\left(\mathrm{Fix}\left(f\right)\right)\right)=\mathrm{card}\left(\mathrm{escapedListings}\left(f\right)\right)$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/EquivariantEscape.trivial_action_recovers_escaped_listing_card (✓ std3). ∎

Source. Repository-derived.

Commentary.

When every address is its own orbit and each stabilizer-orbit block has the full address cardinality, the product side is the frozen unrestricted escaped-listing count.

References

• Truth anchor: D5/S0/Diagonal/EquivariantEscape.equivariant_diagonal_constant
• Truth anchor: D5/S0/Diagonal/EquivariantEscape.equivariant_escaped_card
• Truth anchor: D5/S0/Diagonal/EquivariantEscape.transitive_equivariant_escaped_card
• Truth anchor: D5/S0/Diagonal/EquivariantEscape.trivial_action_recovers_escaped_listing_card
• Dependency: D5/S0/Diagonal/EscapeCount