Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Literal Placements and the Rest Clock

Abstract

The literal capacity trajectory supplies an initialized unbounded rest trace.

Capacities in the literal trajectory are ordered from top to bottom; rest-state capacities are ordered from bottom to top. The initial rest state is endpoint one, capacity list [1], and bin one. This trace theorem relates capacity states and brick indices; it does not assert the original OEIS self-composition identity.

Theorem 1.1 (An Actual Initialized Unbounded Trace).

Lean statement: D5/S3/Combinatorics/GreedyBrick/LiteralRestTrace.literal_trace_realization

Proof. Machine-checked in Lean as D5/S3/Combinatorics/GreedyBrick/LiteralRestTrace.literal_trace_realization (✓ std3). ∎

Source. Repository-derived.

Commentary.

There exists a RestTrace whose next bin is the first zero of its current capacity list, or the new bin when all current capacities are positive. Its reversed capacity list equals the literal trajectory at every endpoint. The endpoints are strictly increasing and cofinal in the natural brick indices. Every intermediate literal placement agrees with that same trajectory, and every positive brick belongs to an event interval. A recursive block coupling supplies the clock, and literal height totality transfers along its cofinal samples to give unbounded rest height. No RestTrace or unbounded-rest-height premise is assumed.

References