Signed Binary Weight

Abstract

The literal minimum over signed-power representations satisfies exact scaling and recurrences.

Definition 1.1 (Minimum signed-power weight).

$$\forall x\in \mathbb{Z},\mathrm{signedWeight}\left(x\right)=\mathrm{sInf}\left(\{k:\mathbb{N}\mid \exists l\in \mathrm{List}\left(\mathrm{Bool}\times \mathbb{N}\right),\mathrm{length}\left(l\right)=k\wedge \mathrm{sum}\left(\mathrm{map}\left(t:\mathrm{Bool}\times \mathbb{N}\mapsto \mathrm{ite}\left(\mathrm{fst}\left(t\right),\mathrm{cast}{\left(2,\mathbb{Z}\right)}^{\mathrm{snd}\left(t\right)},\mathrm{neg}\left(\mathrm{cast}{\left(2,\mathbb{Z}\right)}^{\mathrm{snd}\left(t\right)}\right)\right),l\right)\right)=x\}\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/SignedWeight.signedWeight (✓ std3).

Source. Repository-derived.

Commentary.

A representation is a finite list of pairs consisting of a Boolean sign and a natural exponent. A true sign contributes the positive power; a false sign contributes the negative power. Repetitions are permitted. The natural infimum is the minimum number of terms summing to the integer x.

Theorem 1.2 (Exact arithmetic of the minimum).

$$\left(\left(\left(\left(\mathrm{signedWeight}\left(0\right)=0\wedge \mathrm{signedWeight}\left(1\right)=1\right)\wedge \left(\forall x\in \mathbb{Z},\mathrm{signedWeight}\left(\mathrm{neg}\left(x\right)\right)=\mathrm{signedWeight}\left(x\right)\right)\right)\wedge \left(\forall x\in \mathbb{Z},\forall y\in \mathbb{Z},\mathrm{signedWeight}\left(x+y\right)\le \mathrm{signedWeight}\left(x\right)+\mathrm{signedWeight}\left(y\right)\right)\right)\wedge \left(\forall x\in \mathbb{Z},\mathrm{signedWeight}\left(2\cdot x\right)=\mathrm{signedWeight}\left(x\right)\right)\right)\wedge \left(\forall x\in \mathbb{Z},\mathrm{signedWeight}\left(2\cdot x+1\right)=1+\min \left(\mathrm{signedWeight}\left(x\right),\mathrm{signedWeight}\left(x+1\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Palindromes/PeriodDoubling/SignedWeight.signed_weight_arithmetic (✓ std3). ∎

Source. Repository-derived.

Commentary.

Optimal signed representations exist for every integer. Scaling removes a zero low digit. An odd integer has a positive or negative unit term, giving the exact two-branch recurrence. The argument constructs optimal lists and bounds every signed representation, including repetitions.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/SignedWeight.signedWeight
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/SignedWeight.signed_weight_arithmetic