Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Circle Characters on Capacity States

Abstract

Circle Characters on Capacity States.

Theorem 1.1 (Continuity forces finite weighted absolute mass).

Lean statement: D5/S3/Analytic/WeightedCapacity/CircleCharacterContinuity.mass_finite_of_continuousAt

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

Source. Repository-derived.

Commentary.

For any sequence of natural capacities and any total row of circle points, continuity of the associated character at one finite capacity state implies that the sum of each capacity times the absolute centered representative is finite. A finite coordinate neighborhood controls all admissible tail states. Single-coordinate multiples and separate positive and negative sums then bound the tail mass without assigning a group structure to the capacity states.

References