preferredAspectRatio_in_aesthetic_band
plain-language theorem explainer
The golden ratio satisfies 1.4 < φ < 1.9, placing the φ:1 rectangle inside the observed human aesthetic preference band for aspect ratios. Architects and visual cognition researchers cite this when connecting J-cost minimization to empirical proportion judgments. The tactic proof unfolds the definition to φ = (1 + √5)/2 then bounds √5 separately for each side of the inequality via direct comparisons and linarith.
Claim. $1.4 < φ < 1.9$, where $φ = (1 + √5)/2$ is the golden ratio taken as the preferred aspect ratio for minimum J-cost rectangles.
background
The Golden Section in Proportion module predicts that the minimum J-cost rectangle under area constraint has aspect ratio φ:1. Here J(r) = (r + 1/r)/2 - 1, and the self-similar fixed point satisfying φ = 1 + 1/φ yields the lowest non-trivial departure from a square among Fibonacci-ratio candidates. The module notes historical matches such as Parthenon proportions and Le Corbusier’s Modulor, with a falsifier given by any large-N study showing preference outside φ ± 0.2 across cultures.
proof idea
The tactic proof unfolds preferredAspectRatio to expose phi, then splits the conjunction. The lower bound 1.4 < phi is obtained by unfolding phi, proving √5 > 1.8 via Real.sqrt_lt_sqrt and norm_num, then applying linarith. The upper bound phi < 1.9 follows analogously by showing √5 < 2.25 and again using linarith.
why it matters
This result supplies the ratio_in_band component of GoldenSectionCert, which packages the full set of structural properties for the golden section in architecture. It directly realizes the module’s claim that the φ:1 rectangle lies in the aesthetic band, linking J-cost minimization to observed preferences. The placement of phi as self-similar fixed point aligns with the forcing chain step that forces phi from J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.