GoldenSectionCert
The GoldenSectionCert structure packages five properties certifying that the golden ratio satisfies the J-cost minimum for rectangular aspect ratios. Visual perception researchers and architectural theorists would cite it when connecting Recognition Science cost minimization to observed human preferences for φ:1 proportions. It is assembled directly from upstream definitions of preferredAspectRatio as phi and proportionCost as Jcost of the ratio deviation.
claimA structure certifying that the preferred aspect ratio $r$ obeys $1 < r$, $1.4 < r < 1.9$, and $r(r-1)=1$, together with the statements that proportion cost vanishes when actual ratio equals ideal ratio and that proportion cost is nonnegative for all positive arguments.
background
The module derives architectural proportions from the J-cost function of Recognition Science. Preferred aspect ratio is defined as the golden ratio phi. Proportion cost is defined as Jcost of the ratio deviation actual/ideal. Upstream cost_nonneg from ObserverForcing states that the cost of any recognition event is nonnegative. The module doc states that minimizing J(r) under area constraint yields the self-similar fixed point satisfying the phi recursion.
proof idea
This is a structure definition that directly assembles five fields from sibling lemmas: the strict inequality from preferredAspectRatio_gt_one, the band membership from preferredAspectRatio_in_aesthetic_band, the recursion from phi_golden_recursion, the vanishing at ideal from proportionCost_at_ideal, and nonnegativity from proportionCost_nonneg.
why it matters in Recognition Science
This definition supplies the certificate object instantiated in the downstream cert definition and shown inhabited by cert_inhabited. It operationalizes the module claim that the golden section minimizes J-cost among rectangles, linking to the forcing chain where J-uniqueness forces the self-similar fixed point phi. It addresses the architectural prediction that human aesthetic preference aligns with phi within the stated band.
scope and limits
- Does not derive the numerical value of phi from the forcing chain.
- Does not prove uniqueness of the minimum beyond the supplied recursion.
- Does not address higher-dimensional or non-rectangular shapes.
- Does not incorporate empirical cultural variation data.
formal statement (Lean)
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