pleasure_max_at_one
plain-language theorem explainer
pleasure_max_at_one shows that the pleasure function reaches its peak value of 1 at normalized complexity r = 1 whenever J_max > 0. Aesthetic modelers following Berlyne's inverted-U would cite it to fix the location of maximum pleasure. The proof is a direct term reduction that substitutes the unit J-cost lemma into the pleasure definition and simplifies.
Claim. Let $J_max > 0$. Define pleasure$(r, J_max) := 1 - Jcost(r)/J_max$. Then pleasure$(1, J_max) = 1$.
background
The BerlyneInvertedU module derives the inverted-U curve from J-cost reciprocal symmetry. The pleasure function is defined as pleasure(r, J_max) = 1 - Jcost(r)/J_max, where Jcost(x) = (x-1)^2/(2x) from the Cost module. This yields a symmetric fall-off around r=1 because J(r) = J(r^{-1}). Upstream, Jcost_unit0 states Jcost(1) = 0 by direct simplification of the squared-ratio expression. The local setting is the zero-sorry derivation of Berlyne's 1971 relation inside Recognition Science, using the forcing chain and Recognition Composition Law for the underlying J.
proof idea
Term-mode proof. Unfolds the pleasure definition, rewrites with the Jcost_unit0 lemma that Jcost(1) = 0, then applies simp to reduce 1 - 0/J_max to 1.
why it matters
Supplies the max_at_one field of berlyneInvertedUCert, which packages the peak, symmetry, and phi-band facts for the inverted-U certificate. It directly implements the module claim that pleasure is maximal where J-cost vanishes at r=1. In the framework it instantiates T5 J-uniqueness and the reciprocal symmetry from the Recognition Composition Law, confirming the aesthetic acceptance band of width factor phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.