berlyneInvertedUCert
plain-language theorem explainer
This definition supplies the Berlyne inverted-U certificate by packaging three properties of the pleasure function derived from J-cost. Aesthetic theorists or Recognition Science researchers modeling perceptual preference would cite it when grounding the classic inverted-U curve in cost symmetry. The construction proceeds by record field assignment from the module's maximum, symmetry, and bandwidth results.
Claim. The certificate asserts that pleasure attains its maximum value of 1 at normalized complexity ratio 1 whenever the maximum J-cost is positive, that pleasure at ratio $r$ equals pleasure at its reciprocal for any positive $r$, and that the acceptance band ratio is strictly greater than 1.
background
In this module the pleasure function is defined as 1 minus the normalized J-cost, where J-cost is the Recognition Science cost function satisfying the reciprocal symmetry $J(r) = J(r^{-1})$ for $r > 0$. The local setting derives the inverted-U shape directly from this symmetry, which forces pleasure to peak at $r = 1$ and decline symmetrically on either side, with the acceptance band given by the interval where pleasure exceeds one-half. Upstream results establish the maximum at unity via the unit-zero property of J-cost, the symmetry via the J-cost symmetry lemma, and the band ratio greater than 1 via the fact that phi exceeds 1.5.
proof idea
The definition is a direct structure constructor that populates the three fields of the Berlyne inverted-U certificate using the theorem establishing the maximum at unity, the theorem establishing reciprocity of pleasure, and the theorem establishing the band ratio exceeds one.
why it matters
This certificate realizes the module's derivation of the Berlyne inverted-U from J-cost reciprocity, filling the role described in the module documentation for substantiating aesthetic pleasure curves within the Recognition Science framework. It connects to the J-uniqueness property and the phi fixed point that set the acceptance band width factor. No downstream uses are recorded and no open questions are flagged in the supplied results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.