Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Continuous finite-action transfers for the balanced subshift

Abstract

Continuous finite-action transfers for the balanced subshift.

Definition 1.1 (transfer).

Lean statement: D5/S1/Dynamics/Symbolic/PermutativeLifts/BalancedCoboundary.transfer

Formalization. D5/S1/Dynamics/Symbolic/PermutativeLifts/BalancedCoboundary.transfer (✓ std3).

Source. Repository-derived.

Commentary.

Read the prefix holonomy at zero in the unique actual balanced marked tiling.

Theorem 1.2 (transfer_shift).

Lean statement: D5/S1/Dynamics/Symbolic/PermutativeLifts/BalancedCoboundary.transfer_shift

Proof. Machine-checked in Lean as D5/S1/Dynamics/Symbolic/PermutativeLifts/BalancedCoboundary.transfer_shift (✓ std3). ∎

Source. Repository-derived.

Commentary.

The public generic tile-state transition law supplies the coboundary equation whenever both tile holonomies are neutral.

Theorem 1.3 (permutationTransfer_shift).

Lean statement: D5/S1/Dynamics/Symbolic/PermutativeLifts/BalancedCoboundary.permutationTransfer_shift

Proof. Machine-checked in Lean as D5/S1/Dynamics/Symbolic/PermutativeLifts/BalancedCoboundary.permutationTransfer_shift (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite permutation action, the symbolic cardinal bound selects a neutral level of the same fixed balanced base.

Theorem 1.4 (trivializing_conjugacy).

Lean statement: D5/S1/Dynamics/Symbolic/PermutativeLifts/BalancedCoboundary.trivializing_conjugacy

Proof. Machine-checked in Lean as D5/S1/Dynamics/Symbolic/PermutativeLifts/BalancedCoboundary.trivializing_conjugacy (✓ std3). ∎

Source. Repository-derived.

Commentary.

The generic fibre change conjugates the balanced skew step to the balanced base shift with the original fibre fixed.

References