BerlyneInvertedUCert
plain-language theorem explainer
The Berlyne inverted-U certificate structure asserts that the pleasure function derived from normalized J-cost reaches its peak value of 1 at unit complexity ratio, stays invariant under reciprocal ratios, and has an acceptance band strictly wider than 1. Cognitive scientists or aesthetic theorists modeling inverted-U curves would cite it to embed Berlyne's 1971 observations inside Recognition Science's J-cost framework. The declaration is a structure definition that simply packages three properties already established in sibling lemmas.
Claim. A structure asserting that for the pleasure function $p(r,J_0)=1-J(r)/J_0$, one has $p(1,J_0)=1$ whenever $J_0>0$, $p(r,J_0)=p(r^{-1},J_0)$ for all $r>0$, and the acceptance-band ratio satisfies $1<phi$, where $J$ is the J-cost function and $phi$ is the golden ratio.
background
The module defines pleasure as $1 - $ Cost.Jcost $r / J_max$, which normalizes J-cost to the unit interval. Acceptance band ratio is defined directly as phi. The module documentation states that this yields the inverted-U shape because J-cost obeys reciprocal symmetry: pleasure reaches 1 at $r=1$ and falls symmetrically for $r<1$ and $r>1$, with the half-width fixed by phi so that pleasure exceeds 0.5 precisely on the interval $(1/phi, phi)$.
proof idea
The declaration is a structure definition whose three fields are filled by separate lemmas: max_at_one applies the already-proved pleasure_max_at_one, symmetric applies pleasure_symmetric, and band_width_gt_one applies acceptanceBandRatio_gt_one. No further tactics are required inside the structure itself.
why it matters
The structure supplies the certificate that berlyneInvertedUCert instantiates, thereby embedding the Berlyne curve inside the Recognition framework. It realizes the reciprocal symmetry implied by the Recognition Composition Law and the phi fixed point from the forcing chain (T5-T6), giving a quantitative acceptance band of width phi that matches reported empirical windows of 1.5-1.7. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.