beautyScore_at_phi
plain-language theorem explainer
beautyScore_at_phi shows that the beauty score of a golden-ratio composition equals 3/2 minus phi. Researchers working on visual aesthetics in Recognition Science cite this when confirming the phi-composition as the minimum-cost asymmetric case. The tactic proof unfolds beautyScore and Jcost, derives the phi inverse from phi_sq_eq, and finishes with ring.
Claim. Let $B(a,b) := -J(a/b)$ where $J(x) := (x + x^{-1})/2 - 1$. Then $B(phi, 1) = 3/2 - phi$.
background
beautyScore is defined as the negation of the recognition cost Jcost(a/b), where Jcost(x) = (x + x^{-1})/2 - 1. The constant phi satisfies phi^2 = phi + 1 by phi_sq_eq, which yields the inverse identity phi^{-1} = phi - 1 used in the reduction. The module extends the J-cost framework from musical scales to visual compositions, with the module doc stating that the phi-composition is the minimum-cost asymmetric case because J increases away from 1.
proof idea
The proof unfolds beautyScore, rewrites division by one, unfolds Jcost, asserts phi positive, derives the inverse equality from phi_sq_eq via nlinarith and field_simp, rewrites the inverse, and applies ring.
why it matters
This result supplies the golden_ratio_score field of visualBeautyCert and is invoked by visual_beauty_one_statement to assemble the one-statement visual beauty theorem. It realizes the module doc claim that B(phi, 1) equals 3/2 - phi. The equality connects to J-uniqueness (T5) and the forcing of phi as self-similar fixed point (T6) in the UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.