acceptanceBandRatio_gt_one
plain-language theorem explainer
acceptanceBandRatio_gt_one establishes that the aesthetic acceptance band ratio exceeds 1. Researchers modeling Berlyne's inverted-U curve from complexity would cite it to confirm the width factor is strictly greater than unity. The proof is a one-line wrapper that unfolds the definition to phi and applies the known bound phi > 1.5 via linear arithmetic.
Claim. $1 < phi$ where $phi = (1 + sqrt(5))/2$ is the golden ratio serving as the acceptance band half-width.
background
The module derives the Berlyne inverted-U from J-cost reciprocal symmetry in Recognition Science. Pleasure is given by pleasure(r) = 1 - J(r) / J(phi)_max where r is observed complexity over optimal complexity; the acceptance band is the interval of r where pleasure exceeds 0.5, namely r in (1/phi, phi). This band has width factor phi, consistent with cross-cultural preference windows of approximately 1.5-1.7. acceptanceBandRatio is defined as phi. The upstream lemma phi_gt_onePointFive supplies the tighter bound phi > 1.5, obtained from sqrt(5) > 2. The Constants structure from CPM.LawOfExistence bundles abstract parameters but plays no role in this inequality.
proof idea
The proof unfolds acceptanceBandRatio to phi, introduces the lemma phi_gt_onePointFive as a hypothesis, and closes with linarith on the resulting real-number inequality.
why it matters
This supplies the band_width_gt_one field inside berlyneInvertedUCert, completing the certificate that packages max_at_one, symmetric, and band_width_gt_one. It fills the phi-step bandwidth claim in the module derivation, aligning with the Recognition Science phi-ladder and the T5 J-uniqueness fixed point. No open questions or scaffolding are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.