IndisputableMonolith.Aesthetics.CulturalAestheticFromJCost

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Cultural Aesthetic Preference from J-Cost on Familiarity Ratio
   7
   8The empirical paradox of cultural aesthetics: humans prefer artifacts
   9that are familiar enough to be parsable but novel enough to reward
  10attention (Berlyne 1971; Reber, Schwarz, Winkielman 2004 fluency-affect
  11model). In RS terms, aesthetic appeal is governed by recognition cost
  12on the familiarity ratio `r := observed_similarity / target_familiarity`.
  13
  14The maximum-appeal point is at `r = 1` (perfect parseability without
  15boredom), J-cost zero. The Berlyne inverted-U over arousal corresponds
  16to J-cost rising symmetrically off `r = 1` in both directions: too
  17familiar (low novelty) and too unfamiliar (low parseability) carry
  18the same cost. Cross-cultural variation in preferred-art genres is
  19the mapping of different sub-populations onto different reference
  20points on the J-cost landscape.
  21
  22Lean status: 0 sorry, 0 axiom.
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Aesthetics
  27namespace CulturalAestheticFromJCost
  28
  29open Constants Cost
  30
  31noncomputable section
  32
  33/-- Aesthetic-appeal J-cost on the familiarity ratio. -/
  34def aestheticCost (r : ℝ) : ℝ := Cost.Jcost r
  35
  36theorem aestheticCost_zero_at_optimum : aestheticCost 1 = 0 :=
  37  Cost.Jcost_unit0
  38
  39/-- Reciprocal symmetry: too-familiar and too-unfamiliar carry equal
  40J-cost penalty per log-step deviation. The Berlyne inverted-U is the
  41RS reciprocal-symmetry signature. -/
  42theorem aestheticCost_reciprocal_symm {r : ℝ} (hr : 0 < r) :
  43    aestheticCost r = aestheticCost r⁻¹ := Cost.Jcost_symm hr
  44
  45theorem aestheticCost_nonneg {r : ℝ} (hr : 0 < r) :
  46    0 ≤ aestheticCost r := Cost.Jcost_nonneg hr
  47
  48theorem aestheticCost_pos_off_optimum {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  49    0 < aestheticCost r := Cost.Jcost_pos_of_ne_one r hr hne
  50
  51structure CulturalAestheticCert where
  52  optimum_zero : aestheticCost 1 = 0
  53  reciprocal_symm :
  54    ∀ {r : ℝ}, 0 < r → aestheticCost r = aestheticCost r⁻¹
  55  cost_nonneg : ∀ {r : ℝ}, 0 < r → 0 ≤ aestheticCost r
  56  pos_off_optimum :
  57    ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < aestheticCost r
  58
  59/-- Cultural-aesthetic certificate. -/
  60def culturalAestheticCert : CulturalAestheticCert where
  61  optimum_zero := aestheticCost_zero_at_optimum
  62  reciprocal_symm := aestheticCost_reciprocal_symm
  63  cost_nonneg := aestheticCost_nonneg
  64  pos_off_optimum := aestheticCost_pos_off_optimum
  65
  66end
  67end CulturalAestheticFromJCost
  68end Aesthetics
  69end IndisputableMonolith
  70