visual_beauty_one_statement
plain-language theorem explainer
The visual beauty one-statement theorem collects four properties of the J-cost beauty score: it vanishes on symmetric ratios, attains 3/2 minus phi at the golden ratio, places J(phi) inside (0.11, 0.12), and fixes the rule-of-thirds lattice period at 45. Recognition scientists working on aesthetic derivations from the forcing chain would cite this result to close the visual half of the aesthetics module. The proof is a single refine tactic that assembles the four supporting lemmas already established in the same file.
Claim. Let $B(a,b) := -J(a/b)$ with $J(x) := (x + x^{-1})/2 - 1$. Then $B(a,a) = 0$ whenever $a ≠ 0$, $B(φ,1) = 3/2 - φ$, $0.11 < J(φ) < 0.12$, and the rule-of-thirds lattice period equals 45.
background
The module derives visual aesthetics from the same J-cost function used in the musical scale derivation. The beauty score of a composition (a, b) is defined as B(a, b) := -J(a/b), where J is the recognition cost J(x) = (x + 1/x)/2 - 1. This score is maximized at perfect symmetry a = b, where B = 0, and among asymmetric ratios the golden-ratio composition a/b = phi yields the highest score because J attains a local minimum there.
proof idea
The proof is a one-line term-mode wrapper that applies the refine tactic to the four-tuple consisting of beautyScore_at_one, beautyScore_at_phi, Jphi_numerical_band, and ruleOfThirds_lattice_period_eq.
why it matters
This declaration packages the core claims of the visual beauty module into a single theorem, completing the visual side of the aesthetics derivation that parallels the musical scale result. It directly implements the J-cost beauty score introduced in the module documentation for §XXIII.C. Within the Recognition Science framework it connects the J-uniqueness (T5) and phi fixed point (T6) to aesthetic observables, with the 45-period tying into the eight-tick octave and D=3 spatial structure via the consciousness gap. It supports the master certificate VisualBeautyCert defined later in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.