Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Mechanical Readout Uniform Limit

Abstract

Geometric mechanical readouts approach their slope uniformly as the weights flatten.

Theorem 1.1 (One-sided slope approximation and a joint error budget).

Lean statement: D5/S1/Words/Mechanical/MechanicalReadoutUniformLimit.geometric_readout_uniform_slope_bound

Proof. Machine-checked in Lean as D5/S1/Words/Mechanical/MechanicalReadoutUniformLimit.geometric_readout_uniform_slope_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every slope in [0,1), every real phase, and every geometric ratio in [0,1), the completed readout differs from the slope by an amount between (1-r)*(fract(x)-1) and (1-r)fract(x). The cumulative floor discrepancy is exactly fract(x)-fract(x+kalpha). Finite Abel summation weights these discrepancies by nonnegative successive weight drops whose total is 1-r, and the geometric tail passes the one-sided bounds to the infinite readout. In particular, its absolute error is at most 1-r. For any target slope and finite horizon n, the truncated readout differs from the target by at most r^n plus 1-r plus the parameter distance. These estimates hold uniformly in phase, including phases where the fixed-ratio readout jumps as a function of slope.

References