Golden Modular Standard Pair

Abstract

The golden modular step squares to a positive definite unimodular operator with reciprocal golden scales.

Theorem 1.1 (The golden first phase forms a finite-dimensional standard pair).

$$\begin{array}{r}letF:\mathrm{Matrix}(\mathrm{Fin}(2),\mathrm{Fin}(2),\mathbb{R})=matrix2(0,1,1,1);\\ letDelt{a}_{\varphi }:\mathrm{Matrix}(\mathrm{Fin}(2),\mathrm{Fin}(2),\mathbb{R})=F^2;\\ F^2=matrix2(1,1,1,2)\wedge \\ \det (Delt{a}_{\varphi })=1\wedge \mathrm{trace}(Delt{a}_{\varphi })=3\wedge \\ \mathrm{PosDef}(Delt{a}_{\varphi })\wedge \mathrm{quadraticValue}(Delt{a}_{\varphi },vector2(1,0))=1\wedge \\ \mathrm{quadraticValue}(Delt{a}_{\varphi },vector2(1,-1))=1\wedge \\ {\phi }^2\cdot \mathrm{inv}({\phi }^2)=1\wedge \\ {\phi }^2+\mathrm{inv}({\phi }^2)=3.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenCoding/GoldenModularStandardPair.golden_modular_standard_pair (✓ std3). ∎

Source. Repository-derived.

Commentary.

The one-step matrix F has rows (0,1) and (1,1). Direct finite matrix multiplication identifies its square Delta_phi with the matrix having rows (1,1) and (1,2).

The squared operator has determinant one and trace three. Its quadratic form is (x_0+x_1)^2+x_1^2, so every nonzero real vector has strictly positive value.

The vectors (1,0) and (1,-1) both give quadratic-form value one. The squared golden ratio and its reciprocal square likewise have product one and sum three.

References

• Truth anchor: D5/S3/Observer/GoldenCoding/GoldenModularStandardPair.golden_modular_standard_pair