Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Countdown Memory and an All-Time Noise Lower Bound

Abstract

A finite countdown hides a long block of weak target memory from every noisy return observation.

Definition 1.1 (Readout of the actual truncated shift).

Lean statement: D5/S3/Analytic/GoldenTomography/CountdownMemoryNoiseLowerBound.countdownMemory

Formalization. D5/S3/Analytic/GoldenTomography/CountdownMemoryNoiseLowerBound.countdownMemory (✓ std3).

Source. Repository-derived.

Commentary.

The hidden state is supported on 0,…,J-1. One update shifts it by one coordinate and multiplies it by theta, discarding the last coordinate. The initial state is the first basis vector; output weight i is delta/theta^i. The target is defined by propagating this state and applying that readout, with no assumed eigenbasis.

Theorem 1.2 (A nilpotent propagation yields J constant taps).

Lean statement: D5/S3/Analytic/GoldenTomography/CountdownMemoryNoiseLowerBound.countdown_memory_eq

Proof. Machine-checked in Lean as D5/S3/Analytic/GoldenTomography/CountdownMemoryNoiseLowerBound.countdown_memory_eq (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural J,n and every nonzero real theta, the actual readout is delta when n<J and zero otherwise. The proof first computes the whole hidden orbit by induction, then evaluates its finite readout. Repeated eigenvalues and zero coupling are included. The theorem does not claim a stochastic or operator-norm bound for arbitrary parameters.

Definition 1.3 (Return response generated by the memory).

Lean statement: D5/S3/Analytic/GoldenTomography/CountdownMemoryNoiseLowerBound.renewalResponse

Formalization. D5/S3/Analytic/GoldenTomography/CountdownMemoryNoiseLowerBound.renewalResponse (✓ std3).

Source. Repository-derived.

Commentary.

The normalized response starts at one. Its first-return masses are delta at times 2,…,J+1. The well-founded recurrence separates the direct first return from renewals through strictly earlier positive times. Thus the memory taps have a two-time-step offset from the first-return distribution.

Definition 1.4 (The zero-memory competitor).

Lean statement: D5/S3/Analytic/GoldenTomography/CountdownMemoryNoiseLowerBound.noReturnResponse

Formalization. D5/S3/Analytic/GoldenTomography/CountdownMemoryNoiseLowerBound.noReturnResponse (✓ std3).

Source. Repository-derived.

Commentary.

The competing response equals one at time zero and zero at every positive time. It is the return response of a visible state which is killed on its first step and cannot return.

Definition 1.5 (Absolute target loss on a finite prefix).

Lean statement: D5/S3/Analytic/GoldenTomography/CountdownMemoryNoiseLowerBound.prefixLoss

Formalization. D5/S3/Analytic/GoldenTomography/CountdownMemoryNoiseLowerBound.prefixLoss (✓ std3).

Source. Repository-derived.

Commentary.

This is the sum of absolute differences over the first J memory coefficients. The lower bound also applies to a full-memory loss when that loss dominates this prefix sum. No convergence hypothesis is needed for the finite lower bound.

Theorem 1.6 (No estimator can resolve the two targets below J delta / 2).

Lean statement: D5/S3/Analytic/GoldenTomography/CountdownMemoryNoiseLowerBound.countdown_noise_lower_bound

Proof. Machine-checked in Lean as D5/S3/Analytic/GoldenTomography/CountdownMemoryNoiseLowerBound.countdown_noise_lower_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume delta>=0, theta nonzero, and Jdelta<=1/2. There exists one observation sequence within delta of both true return responses at every natural time. For every estimated target sequence f, the larger of its two prefix losses is at least Jdelta/2.

Strong induction on the actual renewal recurrence proves that all positive-time responses lie between zero and 2*delta. The common data are the midpoint of the responses. A coefficientwise triangle inequality, summed over the J actual taps, gives the minimax obstruction. The all-time quantifier makes additional observations at the same worst-case precision insufficient to remove it.

Here J ranges over arbitrary natural values subject to the stated hypothesis J*delta<=1/2. The theorem lower-bounds the first-J absolute (l1) loss, and also any full-memory loss that dominates that prefix. It makes no claim about losses outside those scopes.

A killed Markov realization, a similarity realization with strictly contractive full Hilbert dynamics, and matching asymptotic upper and lower rates are outside this module and are not established here.

References