Golden units for Kimberling row intersections

Abstract

Golden integer units have signed integral powers and an oriented small-unit description.

Definition 1.1 (Golden power rows).

$$\forall i\in \mathrm{Nat},\forall N\in \mathrm{Nat},N\in \mathrm{row}\left(i\right)\iff \left(\exists k\in \mathrm{Nat},1\le k\wedge N=\lfloor {\mathrm{goldenRatio}}^i\cdot k\rfloor \right)$$

Formalization. D5/S1/Recurrence/KimberlingArrayRowPairs.row (✓ std3).

Source. Repository-derived.

Commentary.

Row i consists of the natural floors of positive integral multiples of the ith golden power.

Definition 1.2 (Lucas trace).

$$\forall n\in \mathrm{Nat},\mathrm{lucas}\left(n\right)=\mathrm{toNat}\left(\mathrm{goldenLucas}\left(n\right)\right)$$

Formalization. D5/S1/Recurrence/KimberlingArrayRowPairs.lucas (✓ std3).

Source. Repository-derived.

Commentary.

The natural Lucas number is the nonnegative integral trace of the nth golden power. Its initial values are two and one.

Theorem 1.3 (Integral unit powers).

$$\forall s\in \mathrm{Int},\mathrm{embedding}\left(\mathrm{coe}\left({\mathrm{phiUnit}}^s\right)\right)={\mathrm{goldenRatio}}^s$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/KimberlingArrayRowPairs.embedding_phiUnit_zpow (✓ std3). ∎

Source. Repository-derived.

Commentary.

The distinguished unit evaluates to the golden ratio for all integral exponents.

Theorem 1.4 (Inverse powers).

$$\forall r\in \mathrm{Nat},\mathrm{coe}\left({\mathrm{phiUnit}}^{0-r}\right)={\left(0-1\right)}^r\cdot \mathrm{conj}\left({\mathrm{phi}}^r\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/KimberlingArrayRowPairs.phiUnit_neg_nat (✓ std3). ∎

Source. Repository-derived.

Commentary.

Inverse powers have the signed conjugate coordinates.

Theorem 1.5 (Orientation of small units).

$$\forall z\in \mathrm{GoldenInt},\forall i\in \mathrm{Nat},\left(\mathrm{norm}\left(z\right)=1\vee \mathrm{norm}\left(z\right)=0-1\right)\Rightarrow \left(b\left(z\right)<0\Rightarrow \left(\mathrm{abs}\left(\mathrm{embedding}\left(z\right)\right)<\mathrm{inv}\left({\mathrm{goldenRatio}}^i\right)\Rightarrow \left(\exists r\in \mathrm{Nat},i+1\le r\wedge \left(z=\mathrm{conj}\left({\mathrm{phi}}^r\right)\wedge \mathrm{embedding}\left(z\right)={\left(0-1\right)}^r\cdot \mathrm{inv}\left({\mathrm{goldenRatio}}^r\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/KimberlingArrayRowPairs.golden_small_unit (✓ std3). ∎

Source. Repository-derived.

Commentary.

A negative golden coefficient fixes the orientation of a sufficiently small unit to the conjugate of a positive power.

References

• Truth anchor: D5/S1/Recurrence/KimberlingArrayRowPairs.embedding_phiUnit_zpow
• Truth anchor: D5/S1/Recurrence/KimberlingArrayRowPairs.golden_small_unit
• Truth anchor: D5/S1/Recurrence/KimberlingArrayRowPairs.lucas
• Truth anchor: D5/S1/Recurrence/KimberlingArrayRowPairs.phiUnit_neg_nat
• Truth anchor: D5/S1/Recurrence/KimberlingArrayRowPairs.row
• Dependency: D5/S1/Scale/Embedding