pleasure
plain-language theorem explainer
pleasure supplies the Berlyne inverted-U as one minus the J-cost of relative complexity normalized by its maximum value. Aesthetic and qualia researchers cite the definition to ground pleasure directly in RS cost symmetry. The declaration is a single-line abbreviation that subtracts the scaled Jcost term from unity.
Claim. The pleasure function is defined by $pleasure(r, J_{max}) = 1 - J(r)/J_{max}$, where $J(r)$ is the J-cost of the relative complexity ratio $r$.
background
The Berlyne Inverted-U module derives aesthetic pleasure from the reciprocal symmetry of J-cost. J-cost itself is the Quantity CostUnit abbreviation imported from the RS native core measurement module. The module setting states that pleasure(r) equals 1 minus J(r) divided by J(phi) maximum, with the maximum at r equals 1 and symmetric fall-off for r less than 1 and r greater than 1 due to J(r) equals J(r inverse).
proof idea
The declaration is a direct definition that subtracts the normalized J-cost term from 1. It applies the Jcost function from the upstream Cost abbrev in RSNative.Core. No tactics or lemmas are invoked inside the body.
why it matters
This definition feeds the BerlyneInvertedUCert structure that certifies the maximum at one, symmetry under inversion, and acceptance band ratio greater than one. It supplies the valence component for QualiaState and QualiaSpace in the RRF foundation. Within the Recognition framework it realizes the phi-step aesthetic acceptance band of width factor phi, consistent with the reciprocal symmetry law and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.