Dyadic Capacity Level Closures

Abstract

Dyadic Capacity Level Closures.

Theorem 1.1 (Closure of a finite-state dyadic level).

Lean statement: D5/S3/Analytic/WeightedCapacity/DyadicTailFilling.closure_level_eq_sublevel

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

Source. Repository-derived.

Commentary.

Let each natural coordinate have an arbitrary finite natural capacity and weight two to the negative coordinate index. If the total weighted capacity is infinite, the closure of the finite-support states with any prescribed nonnegative dyadic sum is exactly the set of all bounded states whose extended sum is at most that value. In the finite-support carrier, the relative closure is the real readout sublevel. The product topology has discrete coordinate factors. The construction preserves any prescribed finite set of coordinates and fills the remaining deficit at the first capacity crossing; zero capacity gaps require no restriction.

References

• Truth anchor: D5/S3/Analytic/WeightedCapacity/DyadicTailFilling.closure_level_eq_sublevel