visualBeautyCert
plain-language theorem explainer
The visualBeautyCert definition inhabits the VisualBeautyCert structure by supplying concrete values for its six fields. Researchers working on recognition-derived aesthetics or phi-based composition rules would cite it to close the visual side of the J-cost framework. The construction is a direct structure literal that pulls four prior theorems for the field assignments and uses rfl for the lattice match.
Claim. The structure VisualBeautyCert is inhabited where: (i) $B(a,a)=0$ for all $a≠0$, with beauty score $B(x,y):=-J(x/y)$ and $J(z)=(z+1/z)/2-1$; (ii) $B(φ,1)=3/2-φ$; (iii) $0.11<J(φ)<0.12$; (iv) the rule-of-thirds lattice period equals 45; (v) $B≤0$ with equality only at ratio 1; (vi) the φ-ratio is the lowest-J asymmetric case among the listed ratios.
background
The module derives a visual beauty score from the same J-cost used for musical scales. Beauty score is defined as $B(a,b):=-J(a/b)$, where $J$ is the recognition cost function that vanishes at 1 and increases for deviations. The golden ratio φ appears as the first asymmetric minimum because $J(φ)=φ-3/2≈0.118$, so $B(φ,1)≈-0.118$ is the highest score among asymmetric ratios. Upstream theorems supply the concrete evaluations: beautyScore_at_one proves $B(a,a)=0$, beautyScore_at_phi proves the φ value, Jphi_numerical_band proves the numerical interval from $1.61<φ<1.62$, and ruleOfThirds_lattice_period_eq proves the period equals 45 via direct computation.
proof idea
The declaration is a structure constructor. It assigns symmetric_max to the theorem beautyScore_at_one, golden_ratio_score to beautyScore_at_phi, Jphi_band to Jphi_numerical_band, rule_of_thirds_eq_45 to ruleOfThirds_lattice_period_eq, and cortical_lattice_match to the reflexivity tactic rfl. No further reduction or induction is performed; the fields are simply populated from the already-proved siblings.
why it matters
This definition closes the visual-aesthetics row of the module by exhibiting an explicit inhabitant of VisualBeautyCert, thereby completing the partial closure announced in the module header for aesthetics beyond music. It directly uses the J-uniqueness property (T5) and the self-similar fixed point φ (T6) from the forcing chain. With zero downstream uses recorded, the declaration currently serves as a terminal certificate rather than an intermediate lemma; it leaves open the cross-cultural empirical test listed among the module falsifiers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.