phi_golden_recursion
The golden ratio satisfies the recursion φ(φ − 1) = 1. Aesthetic theorists and architects working within Recognition Science would cite this identity when establishing that the minimum J-cost rectangle has aspect ratio φ. The proof reduces the claim to the quadratic equation for φ via a direct algebraic substitution and linear arithmetic.
claimLet φ be the golden ratio. Then φ(φ − 1) = 1.
background
In the Golden Section in Proportion module, preferredAspectRatio is defined as the golden ratio φ. The module develops the RS prediction that the minimum J-cost rectangle has aspect ratio φ:1, derived by minimizing J(r) = (r + 1/r)/2 − 1 under area constraints. This relies on the upstream result phi_sq_eq, which states that φ² = φ + 1 from the defining equation x² − x − 1 = 0.
proof idea
The proof unfolds the definition of preferredAspectRatio to phi. It invokes the lemma phi_sq_eq to obtain φ² = φ + 1. Then it rewrites using the square identity and applies linear arithmetic to conclude the product equals 1.
why it matters in Recognition Science
This theorem supplies the golden_recursion field in the GoldenSectionCert definition, which certifies the structural properties of the preferred aspect ratio. It fills the step in the Recognition Science chain where φ is forced as the self-similar fixed point (T6). The module falsifier is any psychophysical study showing preference for ratios departing from φ ± 0.2.
scope and limits
- Does not establish uniqueness of the minimum J-cost ratio among all real numbers.
- Does not incorporate empirical data from preference studies.
- Does not extend to higher-dimensional proportions or non-rectangular shapes.
Lean usage
golden_recursion := phi_golden_recursionformal statement (Lean)
88theorem phi_golden_recursion : preferredAspectRatio * (preferredAspectRatio - 1) = 1 := by
proof body
Term-mode proof.
89 unfold preferredAspectRatio
90 have h : phi ^ 2 = phi + 1 := phi_sq_eq
91 have hphi : phi ^ 2 = phi * phi := sq phi
92 rw [hphi] at h
93 linarith [h]
94