Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Collapse Is Expanding

Abstract

The period-block collapse is the general expanding-orbit lemma at one multiplier.

The escape core of the period-block collapse is a fact about any expanding multiplier, and that fact is stated one tier up, where it may not mention this base at all. What remains here is the instantiation: the signed step, which the earlier module states only under absolute value, and the earlier module’s own distance identity reached by the general route. Should either side change, this stops compiling.

The module exists because the link was first written inside the general one, where the generality ordering forbids it. A rule recorded earlier the same day held that a generalisation owes the specific form an in-place link, preferring that to a separate artifact. Under the ordering the in-place link is not available. The obligation stands; the location was wrong.

Theorem 1.1 (The collapse is the general lemma).

Proof. Machine-checked in Lean as D5/S0/Tower/NonPisotFrontier/CollapseIsExpanding.the_collapse_is_the_general_lemma (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed half is that the base is expanding, which is what lets the general lemma apply here at all. The second half is the distance identity, re-derived rather than restated.

References