Golden Real Embedding

Abstract

The real embedding of golden integers is an injective ring homomorphism.

D5/S1/Scale/Embedding sends the golden integer $a + b \cdot φ$ to the real number with the same coordinate formula.

Proposition 1.1 (Coordinate formula).

$\forall x \in GoldenInt, embedding (x) = x . a + x . b φ$

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

Source. Repository-derived.

Commentary.

$embedding (a + b \cdot φ) = a + b \cdot φ$

The defining identity makes the coordinate map multiplicative; $ψ$ denotes the conjugate root.

$φ^{2} = φ + 1$

$ψ = 1 - φ$

${φ, ψ}$

Theorem 1.2 (Injectivity).

$\forall x, y \in GoldenInt, embedding (x) = embedding (y) \Rightarrow x = y$

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

Source. Repository-derived.

Commentary.

A coordinate collision with $b \neq = 0$ would force the forbidden rational identity

$φ = \frac{- a}{b}$

Theorem 1.3 (Embedding times conjugate).

$\forall x \in GoldenInt, embedding (x) embedding (conj (x)) = norm (x)$

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

Source. Repository-derived.

Commentary.

$embedding (x) \cdot embedding (conj (x)) = norm (x)$

Theorem 1.4 (Absolute norm relation).

$\forall x \in GoldenInt, ∣ embedding (x)∣ ∣ embedding (conj (x))∣ = ∣ norm (x)∣$

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

Source. Repository-derived.

Commentary.

Taking absolute values gives the corresponding multiplicative relation.

$∣ embedding (x) ∣ \cdot ∣ embedding (conj (x)) ∣ = ∣ norm (x) ∣$