preferredAspectRatio
The golden ratio φ is defined as the aesthetically preferred aspect ratio for rectangles under Recognition Science J-cost minimization. Architects and perception researchers cite it when linking human aesthetic judgments to the self-similar fixed point of the forcing chain. The declaration is a direct binding to the upstream constant phi with no additional computation.
claimThe aesthetically preferred aspect ratio is defined to be the golden ratio $φ$, where $φ = (1 + √5)/2$ satisfies the recursion $φ = 1 + 1/φ$ and minimizes the J-cost $J(r) = (r + 1/r)/2 - 1$ for rectangular proportions.
background
In the Golden Section in Architectural Proportion module the J-cost on aspect ratio deviation is $J(r) = (r + 1/r)/2 - 1$. The Recognition Science prediction, drawn from CulturalAestheticFromJCost and VisualBeauty, states that the minimum J-cost rectangle under fixed area has aspect ratio φ:1. This follows from the self-similar fixed point phi forced in the upstream forcing chain (T6) and the Recognition Composition Law.
proof idea
Direct definition that binds preferredAspectRatio to the constant phi imported from Constants. No lemmas or tactics are invoked beyond the binding itself.
why it matters in Recognition Science
This definition supplies the numerical anchor for all downstream architectural proportion results. It is used by GoldenSectionCert (which certifies ratio >1, aesthetic band membership, golden recursion, and zero cost at ideal proportions) and by the theorems preferredAspectRatio_gt_one, preferredAspectRatio_in_aesthetic_band, and phi_golden_recursion. It instantiates the phi-ladder and eight-tick octave landmarks of the forcing chain while leaving open the psychophysical falsifier stated in the module documentation.
scope and limits
- Does not derive the value of φ from the forcing chain inside this module.
- Does not prove uniqueness of the minimum without the area constraint.
- Does not extend the claim to non-rectangular geometries.
- Does not quantify cultural variation in aesthetic preference.
Lean usage
theorem phi_golden_recursion : preferredAspectRatio * (preferredAspectRatio - 1) = 1 := by unfold preferredAspectRatio; exact phi_sq_eqformal statement (Lean)
45def preferredAspectRatio : ℝ := phi
proof body
Definition body.
46