beautyScore
plain-language theorem explainer
Beauty score for a rectangular composition with sides a and b is defined as the negation of the J-cost of their aspect ratio. Recognition Science researchers cite it when quantifying symmetry maxima and golden-ratio preferences in visual forms. The declaration is a one-line definition that negates Jcost applied to a/b.
Claim. The beauty score of a composition with side lengths $a$ and $b$ is defined by $B(a,b) := -J(a/b)$, where $J(x) = (x + x^{-1})/2 - 1$ is the recognition cost function.
background
The J-cost function J(x) = (x + x^{-1})/2 - 1 measures recognition effort for a ratio x and attains its minimum value of zero at x = 1. This module extends the same cost model from musical scales to visual aesthetics, defining beauty as the negative of J-cost so that symmetry yields the highest score.
proof idea
The declaration is a one-line definition that negates the J-cost of the ratio a/b.
why it matters
This definition supplies the core quantity for beautyScore_at_one, beautyScore_at_phi, Jphi_numerical_band, and the VisualBeautyCert structure. It realizes the aesthetics extension of the J-cost framework, linking visual beauty to the phi fixed point from the forcing chain and the rule-of-thirds lattice period of 45. It touches the open question of cross-cultural confirmation of the predicted phi preference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.