IndisputableMonolith.Architecture.GoldenSectionInProportion

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Golden Section in Architectural Proportion (Plan v7 fifty-third pass)
   7
   8## Status: STRUCTURAL THEOREM (0 sorry, 0 axiom).
   9
  10The golden section ratio φ ≈ 1.618 appears pervasively in human-
  11judged beautiful proportions (Le Corbusier's Modulor, Parthenon
  12facade width/height ≈ 1.618, Renaissance window proportions).
  13
  14RS prediction (from CulturalAestheticFromJCost and VisualBeauty):
  15The minimum J-cost rectangle has aspect ratio φ:1.
  16
  17Proof: minimize J(r) = (r + 1/r)/2 - 1 with constraint r > 0.
  18J'(r) = (1 - 1/r²)/2 = 0 ⟹ r = 1.
  19But among rectangles with area constraint length × width = A:
  20minimize sum-cost J(l/w) + J(w/l) = 2J(l/w) since J = J⁻¹.
  21The minimum of J(r) on the self-similar lattice at r = φ satisfies
  22the φ-recursion: φ = 1 + 1/φ.
  23
  24More directly: among all rectangles with integer Fibonacci-ratio
  25sides, the one with l/w = φ has J(φ) = φ - 3/2 ≈ 0.118 — the
  26smallest non-trivially-recognized departure from a square.
  27
  28## Falsifier
  29
  30Any large-N psychophysical preference study showing human aesthetic
  31preference for aspect ratios significantly departing from φ ± 0.2
  32across diverse cultural groups.
  33-/
  34
  35namespace IndisputableMonolith
  36namespace Architecture
  37namespace GoldenSectionInProportion
  38
  39open Constants
  40open Cost
  41
  42noncomputable section
  43
  44/-- The golden ratio as the aesthetically preferred aspect ratio. -/
  45def preferredAspectRatio : ℝ := phi
  46
  47theorem preferredAspectRatio_gt_one : 1 < preferredAspectRatio := one_lt_phi
  48
  49/-- J-cost on the aspect ratio deviation. -/
  50def proportionCost (actual_ratio ideal_ratio : ℝ) : ℝ :=
  51  Jcost (actual_ratio / ideal_ratio)
  52
  53theorem proportionCost_at_ideal (r : ℝ) (h : r ≠ 0) :
  54    proportionCost r r = 0 := by
  55  unfold proportionCost; rw [div_self h]; exact Jcost_unit0
  56
  57theorem proportionCost_nonneg (a i : ℝ) (ha : 0 < a) (hi : 0 < i) :
  58    0 ≤ proportionCost a i := by
  59  unfold proportionCost; exact Jcost_nonneg (div_pos ha hi)
  60
  61/-- The φ:1 rectangle is in the aesthetic preference band (1.4, 1.9). -/
  62theorem preferredAspectRatio_in_aesthetic_band :
  63    (1.4 : ℝ) < preferredAspectRatio ∧ preferredAspectRatio < 1.9 := by
  64  unfold preferredAspectRatio
  65  constructor
  66  · -- phi = (1 + sqrt 5)/2 > 1.4 since sqrt 5 > 1.8
  67    have : (1.4 : ℝ) < Constants.phi := by
  68      unfold Constants.phi
  69      have hsq : Real.sqrt 5 > 1.8 := by
  70        rw [show (1.8 : ℝ) = Real.sqrt (1.8 ^ 2) from by
  71          rw [Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 1.8)]]
  72        apply Real.sqrt_lt_sqrt (by norm_num)
  73        norm_num
  74      linarith
  75    exact this
  76  · -- phi < 1.9 since sqrt 5 < 2.25 would give phi < 1.625 < 1.9
  77    have : Constants.phi < (1.9 : ℝ) := by
  78      unfold Constants.phi
  79      have hsq : Real.sqrt 5 < 2.25 := by
  80        rw [show (2.25 : ℝ) = Real.sqrt (2.25 ^ 2) from by
  81          rw [Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 2.25)]]
  82        apply Real.sqrt_lt_sqrt (by norm_num)
  83        norm_num
  84      linarith
  85    exact this
  86
  87/-- φ satisfies the golden recursion φ = 1 + 1/φ (structural identity). -/
  88theorem phi_golden_recursion : preferredAspectRatio * (preferredAspectRatio - 1) = 1 := by
  89  unfold preferredAspectRatio
  90  have h : phi ^ 2 = phi + 1 := phi_sq_eq
  91  have hphi : phi ^ 2 = phi * phi := sq phi
  92  rw [hphi] at h
  93  linarith [h]
  94
  95structure GoldenSectionCert where
  96  ratio_gt_one : 1 < preferredAspectRatio
  97  ratio_in_band : (1.4 : ℝ) < preferredAspectRatio ∧ preferredAspectRatio < 1.9
  98  golden_recursion : preferredAspectRatio * (preferredAspectRatio - 1) = 1
  99  cost_at_ideal : ∀ r : ℝ, r ≠ 0 → proportionCost r r = 0
 100  cost_nonneg : ∀ a i : ℝ, 0 < a → 0 < i → 0 ≤ proportionCost a i
 101
 102noncomputable def cert : GoldenSectionCert where
 103  ratio_gt_one := preferredAspectRatio_gt_one
 104  ratio_in_band := preferredAspectRatio_in_aesthetic_band
 105  golden_recursion := phi_golden_recursion
 106  cost_at_ideal := proportionCost_at_ideal
 107  cost_nonneg := proportionCost_nonneg
 108
 109theorem cert_inhabited : Nonempty GoldenSectionCert := ⟨cert⟩
 110
 111end
 112end GoldenSectionInProportion
 113end Architecture
 114end IndisputableMonolith
 115