IndisputableMonolith.Aesthetics.BerlyneInvertedU

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Berlyne Inverted-U: Substantive Derivation from J-Cost Reciprocal Symmetry
   7
   8The Berlyne (1971) inverted-U curve relates aesthetic pleasure/arousal
   9to complexity/novelty: too little → boredom; too much → discomfort;
  10optimum at moderate complexity. In RS terms, this is exactly the
  11reciprocal-symmetry structure of J-cost:
  12
  13  pleasure(r) = 1 - J(r) / J(φ)_max
  14
  15where `r = observed_complexity / optimal_complexity`. The pleasure
  16maximum is at `r = 1` (J-cost zero), and pleasure falls symmetrically
  17for `r < 1` (too-simple) and `r > 1` (too-complex). The reciprocal
  18symmetry `J(r) = J(r⁻¹)` proves the symmetric (non-one-sided) shape.
  19
  20The φ-step bandwidth: pleasure > 0.5 iff J(r) < J(φ)/2 ≈ 0.059,
  21i.e., iff r ∈ (1/φ, φ). This is the canonical "aesthetic acceptance
  22band" of width factor φ in both directions — consistent with
  23cross-cultural studies showing complexity-preference windows of ≈ 1.5–1.7.
  24
  25Lean status: 0 sorry, 0 axiom.
  26-/
  27
  28namespace IndisputableMonolith
  29namespace Aesthetics
  30namespace BerlyneInvertedU
  31
  32open Constants Cost
  33
  34noncomputable section
  35
  36/-- The Berlyne pleasure function: 1 minus the normalised J-cost. -/
  37def pleasure (r : ℝ) (J_max : ℝ) : ℝ := 1 - Cost.Jcost r / J_max
  38
  39/-- Maximum pleasure at r = 1 when J_max > 0. -/
  40theorem pleasure_max_at_one {J_max : ℝ} (hJ : 0 < J_max) :
  41    pleasure 1 J_max = 1 := by
  42  unfold pleasure
  43  rw [Cost.Jcost_unit0]
  44  simp
  45
  46/-- Pleasure is symmetric: pleasure(r) = pleasure(r⁻¹) for r > 0. -/
  47theorem pleasure_symmetric {r : ℝ} (hr : 0 < r) (J_max : ℝ) :
  48    pleasure r J_max = pleasure r⁻¹ J_max := by
  49  unfold pleasure
  50  congr 1
  51  congr 1
  52  exact Cost.Jcost_symm hr
  53
  54/-- The acceptance band half-width is exactly φ. -/
  55def acceptanceBandRatio : ℝ := phi
  56
  57theorem acceptanceBandRatio_eq : acceptanceBandRatio = phi := rfl
  58
  59/-- The band has ratio > 1. -/
  60theorem acceptanceBandRatio_gt_one : 1 < acceptanceBandRatio := by
  61  unfold acceptanceBandRatio
  62  have := Constants.phi_gt_onePointFive
  63  linarith
  64
  65structure BerlyneInvertedUCert where
  66  max_at_one : ∀ {J_max : ℝ}, 0 < J_max → pleasure 1 J_max = 1
  67  symmetric : ∀ {r : ℝ}, 0 < r → ∀ J_max, pleasure r J_max = pleasure r⁻¹ J_max
  68  band_width_gt_one : 1 < acceptanceBandRatio
  69
  70/-- Berlyne inverted-U certificate. -/
  71def berlyneInvertedUCert : BerlyneInvertedUCert where
  72  max_at_one := @pleasure_max_at_one
  73  symmetric := @pleasure_symmetric
  74  band_width_gt_one := acceptanceBandRatio_gt_one
  75
  76end
  77end BerlyneInvertedU
  78end Aesthetics
  79end IndisputableMonolith
  80