Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Continuity of the Dyadic Readout

Abstract

Continuity of the Dyadic Readout.

Theorem 1.1 (Finite mass, continuity, and extension).

Lean statement: D5/S3/Analytic/WeightedCapacity/ReadoutTopology.result

Proof. Machine-checked in Lean as D5/S3/Analytic/WeightedCapacity/ReadoutTopology.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural capacity sequence, finite total dyadic mass is equivalent to continuity of the real readout at zero, continuity everywhere in the rational probe topology, and existence of a continuous real extension to the full capacity product with its coordinate topology. When the mass is finite, the extension is unique and equals the supremum of the partial dyadic sums. When the mass is infinite, the readout is discontinuous at every finite state. If infinitely many coordinates have positive capacity, every neighborhood of each finite state contains a different state.

References