pleasure_symmetric
plain-language theorem explainer
The theorem establishes that the Berlyne pleasure function is invariant under reciprocal transformation of its complexity ratio argument. Aesthetic theorists modeling inverted-U curves would cite this to confirm the symmetric shape between under- and over-complex stimuli. The proof is a one-line wrapper that unfolds the pleasure definition and invokes the J-cost symmetry lemma.
Claim. For $r > 0$ and any $J_{max}$, the pleasure function $1 - J(r)/J_{max}$ equals $1 - J(r^{-1})/J_{max}$, where $J$ is the J-cost function obeying $J(x) = J(x^{-1})$ for $x > 0$.
background
The pleasure function is defined as one minus the J-cost normalized by its maximum value. The upstream Jcost_symm lemma states that Jcost(x) equals Jcost(x inverse) for positive x. This module derives the Berlyne inverted-U from J-cost reciprocal symmetry, with pleasure maximum at r equals 1 and symmetric decay for r and its reciprocal, yielding an acceptance band of width factor phi.
proof idea
The term proof unfolds the pleasure definition, applies congruence twice to isolate the J-cost terms, and invokes the Jcost_symm lemma with the hypothesis that r is positive.
why it matters
This supplies the symmetric property required by the berlyneInvertedUCert certificate, which assembles max_at_one, symmetric, and band_width_gt_one. It fills the reciprocal-symmetry step in the module derivation of the aesthetic acceptance band from the J-cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.