Golden Norm

Abstract

The golden norm is multiplicative and agrees with the scaled mathlib norm.

D5/S0/Carrier/Norm defines N(a+b*phi)=a^2+ab-b^2. Multiplying an element by its conjugate eliminates the phi coordinate and produces this integer, which makes the multiplicativity proof a direct polynomial identity.

Under the doubled Zsqrtd 5 coordinates from the carrier module, the mathlib norm is exactly four times the golden norm. This factor is the expected square of the coordinate scaling.

Remark 1.1 (The two-square norm as a shared interpretive core).

$$\mathrm{gaussianNorm}\left(a,b\right)=a^2+b^2$$

Source. Repository-derived.

Commentary.

The source groups a^2+b^2 under four roles: the defining two-axis norm, the Gaussian norm, the modulus-four obstruction, and the splitting reading modulo a prime. It states that each role has its own theorem and that norm multiplicativity is the pivot used in the composition step. The vocabulary in which primes congruent to one split, primes congruent to three remain inert, and two ramifies is explicitly interpretive: the classification theorem is said not to depend on that Gaussian-integer language. A separate dynamical role is referenced but not added as a claim of this module.

Theorem 1.2 (Norm-Euclidean division).

$$\forall a,b\in \mathbb{Z}[\phi ],b\ne 0\Rightarrow \exists q,r\in \mathbb{Z}[\phi ],a=qb+r\wedge (r=0\vee |\mathrm{norm}(r)|<|\mathrm{norm}(b)|)$$

Proof. Machine-checked in Lean as D5/S0/Carrier/Euclidean.golden_division (✓ std3). ∎

Citation. H. Chatland (1949). On the Euclidean algorithm in quadratic number fields. DOI: 10.1090/S0002-9904-1949-09315-1.

Commentary.

For a and nonzero b, divide a * conj(b) by the nonzero integer N(b) and round both rational coordinates in the integral basis (1, phi). Mathlib’s nearest-integer operation makes the tie rule deterministic.

If the two coordinate errors are x and y, then each has absolute value at most 1/2. Completing squares bounds |x^2 + xy - y^2| by 5/16, so multiplicativity of the norm gives a remainder with strictly smaller absolute norm.

The EuclideanDomain GoldenInt instance uses this quotient and remainder with Euclidean relation (N(r)).natAbs < (N(b)).natAbs.

Theorem 1.3 (Principal ideal domain).

$\mathbb{Z}[\phi ]\text{ is a principal ideal domain.}$

Proof. Machine-checked in Lean as D5/S0/Carrier/PrincipalIdeal.golden_int_is_pid (✓ std3). ∎

Citation. H. Chatland (1949). On the Euclidean algorithm in quadratic number fields. DOI: 10.1090/S0002-9904-1949-09315-1.

Commentary.

The norm-Euclidean structure supplies IsPrincipalIdealRing GoldenInt through mathlib’s generic Euclidean-domain instance, so every ideal of GoldenInt is generated by one element.

Mathlib’s generic principal-ideal-domain instance then supplies UniqueFactorizationMonoid GoldenInt; the formal node records this consequence as golden_int_is_ufd without declaring redundant specialized instances.

This result does not classify the units of GoldenInt. The converse assertion that every norm-unit is a signed integral power of phi remains open in D5-T0008.

Theorem 1.4 (The golden norm is power-multiplicative).

$\forall x\in \mathbb{Z}[\phi ],\forall n\in \mathbb{N},\mathrm{norm}(x^n)=\mathrm{norm}(x{)}^n$

Proof. Machine-checked in Lean as D5/S0/Carrier/NormPowers.norm_pow (✓ std3). ∎

Source. Repository-derived.

Commentary.

The golden norm is a monoid homomorphism from GoldenInt to the integers, packaged as normMonoidHom out of its unit and multiplicativity laws. The norm of a power is therefore the same power of the norm, obtained directly as map_pow normMonoidHom rather than by a coordinate induction.

References

• Truth anchor: D5/S0/Carrier/Euclidean.golden_division
• Truth anchor: D5/S0/Carrier/NormPowers.norm_pow
• Truth anchor: D5/S0/Carrier/PrincipalIdeal.golden_int_is_pid
• Dependency: D5/S0/Carrier/Conj
• Dependency: D5/S0/Carrier/Ring