VisualBeautyCert
plain-language theorem explainer
The visual beauty master certificate bundles five properties of the J-cost beauty score: perfect symmetry at equal sides yields score zero, the golden-ratio aspect ratio yields score three-halves minus phi, J of phi lies between 0.11 and 0.12, the rule-of-thirds lattice period equals 45, and this period equals three times three times five. Researchers extending the Recognition Science framework to visual aesthetics would cite it to confirm consistency with observed composition rules. The structure is defined directly from lemmas on the beauty s
Claim. The structure asserts: for every nonzero real $a$, the beauty score $B(a,a)=0$; $B(phi,1)=3/2-phi$; $0.11<J(phi)<0.12$; the rule-of-thirds lattice period equals 45; and the rule-of-thirds lattice period equals $3 times 3 times 5$.
background
The module lifts the J-cost framework from musical scales to visual aesthetics. Beauty score of sides a and b is defined as B(a,b) := -J(a/b), where J(x) = (x + x^{-1})/2 - 1 is the canonical recognition cost. This score reaches its maximum of zero precisely when a equals b (perfect symmetry) and the golden-ratio ratio a/b = phi yields the highest score among the listed asymmetric compositions because J attains a local minimum there.
proof idea
The declaration is a structure definition that packages five independent properties. Each field is a direct reference to a prior lemma or definition: symmetric_max follows from beautyScore_at_one, golden_ratio_score from beautyScore_at_phi, Jphi_band from Jphi_numerical_band, and the two rule-of-thirds statements from ruleOfThirds_lattice_period_eq and reflexivity.
why it matters
This certificate closes the visual aesthetics row in the Recognition Science framework by confirming that the J-cost formalism reproduces the golden-ratio preference and the rule-of-thirds periodicity. It feeds directly into the inhabited instance that supplies the master certificate for downstream use. The construction relies on the J-uniqueness property and the self-similar fixed point phi, extending the eight-tick octave structure to spatial aesthetics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.