Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Uniform splitting of all complete binary lifts

Abstract

Uniform splitting of all complete binary lifts.

Definition 1.1 (Construction).

Lean statement: D5/S1/Dynamics/Symbolic/PermutativeLifts/UniversalLiftSplitting.splitting

Formalization. D5/S1/Dynamics/Symbolic/PermutativeLifts/UniversalLiftSplitting.splitting (✓ std3).

Source. Repository-derived.

Commentary.

For every k and every bipermutative binary code of length k+2, the entire inverse image over the same factorial base is homeomorphic to the base times its actual binary prefix set. The continuous transfer conjugates the shift to the base shift times the identity. Distinct constant prefixes give a nonempty proper closed invariant fibre, contradicting minimality. No component is substituted for the entire inverse image.

Theorem 1.2 (Result).

Lean statement: D5/S1/Dynamics/Symbolic/PermutativeLifts/UniversalLiftSplitting.full_lift_not_minimal

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

Source. Repository-derived.

Commentary.

For every k and every bipermutative binary code of length k+2, the entire inverse image over the same factorial base is homeomorphic to the base times its actual binary prefix set. The continuous transfer conjugates the shift to the base shift times the identity. Distinct constant prefixes give a nonempty proper closed invariant fibre, contradicting minimality. No component is substituted for the entire inverse image.

References