pith. sign in
module module high

IndisputableMonolith.Aesthetics.VisualBeauty

show as:
view Lean formalization →

The VisualBeauty module defines a beauty score for compositional pairs as the negation of the J recognition cost on their ratio. It records the maximum value of zero at equal components and the explicit value 3/2 - phi at the golden ratio. This is a definition module that supplies the aesthetic measure for later visual analyses in Recognition Science.

claimThe beauty score of a composition $(a,b)$ is given by $-J(a/b)$, where $J$ is the recognition cost function. The score is bounded above by zero and attains this bound precisely when $a=b$. At the ratio $a/b=phi$ the score equals $3/2-phi$.

background

Recognition Science obtains all physical structure from the single functional equation satisfied by the J-cost, with the golden ratio phi fixed as the self-similar point under the forcing chain. The imported Constants module supplies the base time quantum tau_0 equal to one tick. The imported Cost module supplies the definition of J together with the Recognition Composition Law that governs products and quotients.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the aesthetic measure that converts recognition cost into a signed beauty score for visual compositions. It directly supports the VisualBeautyCert and visual_beauty_one_statement declarations that appear as siblings. The construction rests on T5 J-uniqueness and the phi fixed point of the eight-tick octave.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)