GPPVerify: Lean 4 Formalization of the Shadow Framework

22 The Golden Ratio as the Minimal Hyperbolic Sector of \(PSL_2(\mathbb {Z})\)

Inversion \(J:x\mapsto x^{-1}\) composed with primitive unit translation \(T:x\mapsto x+1\) gives \(F=T\circ J\), \(F(x)=1+1/x\), whose unique positive fixed point is the golden ratio \(\varphi \). Represented projectively by \(M=\begin{pmatrix} 1 & 1 \\ 1 & 0 \end{pmatrix}\), the square \(A:=M^2=\begin{pmatrix} 2 & 1 \\ 1 & 1 \end{pmatrix}\) is the minimal-trace hyperbolic element of \(SL_2(\mathbb {Z})\). Not claimed: that this sector is the physical fundamental sector of anything else in this project, or that inversion alone (without translation) forces \(\varphi \).

Theorem 22.1 Fixed-Point Characterization of the Golden Ratio
#

For \(x{\gt}0\): \(x=1+1/x \iff x=\varphi \).

Theorem 22.2 The Minimal-Trace Hyperbolic Bound

For any integer \(n\) with \(|n|{\gt}2\): \(|n|\geq 3\). Applied to \(A\) (trace \(3\), determinant \(1\)): \(A\) attains the minimal possible trace of a hyperbolic element of \(SL_2(\mathbb {Z})\).

Theorem 22.3 Characteristic-Polynomial Roots and Discriminant

\(\varphi ^2\) and \(\varphi ^{-2}\) are the roots of \(X^2-(\operatorname {tr}A)X+(\det A)\); the discriminant \((\operatorname {tr}A)^2-4\det A = 5\).

Theorem 22.4 Möbius Fixed Points
#

For \(x\neq -1\): \(\dfrac {2x+1}{x+1}=x \iff x=\varphi \text{ or } x=-\varphi ^{-1}\).

Theorem 22.5 Finite-Place Kernel at the Selected Discriminant

With \(K_{q,1}(s):=(1-q^{-1})/[(1-q^{-s})(1-q^{-(1-s)})]\) (no occurrence of \(\varphi \) in this definition): \(K_{5,1}(1/2)=\varphi ^2\).

Theorem 22.6 Convergence

The expanding eigenvalue of the minimal-trace hyperbolic element and the finite-place shadow kernel at the independently-selected discriminant, evaluated at the principal-series center, are the same real number: \(\varphi ^2\).

Honest boundary. The characteristic-polynomial statements are direct roots of \(X^2-(\operatorname {tr}A)X+\det A\), not connected to Mathlib’s Matrix.charpoly / eigenvalue API (no closed form for \(2\times 2\) matrices was found in the pinned Mathlib). Matrix identities use plain integer matrices, not Mathlib’s SpecialLinearGroup/ModularGroup (which targets the upper-half-plane action, not the real-line Möbius fixed points needed here).