Golden Logarithmic Scale

Abstract

Nonzero golden integers have an integer logarithmic scale with exact unit shifts.

D5/S1/Scale/Log assigns a scale only when $x \neq = 0$ . Zero is represented by none, never by a fabricated integer.

Proposition 1.1 (Zero has no scale).

$logScale (0) = none$

Proof. Machine-checked in Lean as D5/S1/Scale/Log.logScale_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The option-valued definition returns none at zero.

Proposition 1.2 (Nonzero scale).

$\forall x \in GoldenInt, x \neq = 0 \Rightarrow logScale (x) = some (⌊ lo g_{φ} ∣ embedding (x)∣⌋)$

Proof. Machine-checked in Lean as D5/S1/Scale/Log.logScale_ne_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

For nonzero input the following integer is wrapped in some:

$logScale (x) = some (⌊ lo g_{φ} (∣ embedding (x) ∣) ⌋)$

Proposition 1.3 (Embedding of a unit power).

$\forall n \in Z, \forall x \in GoldenInt, embedding (phiUnitZPowMul (n, x)) = φ^{n} embedding (x)$

Proof. Machine-checked in Lean as D5/S1/Scale/Log.embedding_phiUnitZPowMul (✓ std3). ∎

Source. Repository-derived.

Commentary.

$embedding (phiUnitZPowMul (n, x)) = φ^{n} \cdot embedding (x)$

Theorem 1.4 (Exact scale translation).

$\forall n \in Z, \forall x \in GoldenInt, x \neq = 0 \Rightarrow logScale (phiUnitZPowMul (n, x)) = map (n + \cdot, logScale (x))$

Proof. Machine-checked in Lean as D5/S1/Scale/Log.logScale_phiUnit_zpow_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

At the option level, every integer exponent, including negative powers, translates the scale through map exactly:

$logScale (phiUnitZPowMul (n, x)) = map (n + \cdot, logScale (x))$