Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A persistent seven-cycle entry collision

Abstract

A persistent seven-cycle entry collision

Theorem 1.1 (Failure of universal finite-future separation).

Lean statement: D5/S1/Digit/Infinite/SevenCycleCollisionResult.result

Proof. Machine-checked in Lean as D5/S1/Digit/Infinite/SevenCycleCollisionResult.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

A positive observation budget strictly below the critical radius admits an actual rival with primitive window period seven. Its original singleton orbit belongs to the complete endpoint graph. Two different first labels admit first colors one and two against that same rival, and one fixed literal first tail survives every finite future horizon. The actual entry records have fixed common future errors and a uniform positive margin. The sources are not eventually null. This refutes the universal unconditional finite-future separation assertion.

References