cert
The cert definition assembles a complete certificate asserting that the preferred aspect ratio satisfies the golden section properties required by Recognition Science. Aesthetic theorists and architects working in the RS framework would cite it to confirm the J-cost minimum occurs at ratio φ. The construction is a direct structure instance that references five supporting theorems on ratio bounds, recursion, and cost nonnegativity.
claimLet φ denote the golden ratio. The definition cert supplies an instance of GoldenSectionCert asserting that 1 < φ, that 1.4 < φ < 1.9, that φ(φ − 1) = 1, that the proportion cost vanishes for all r ≠ 0 when the two arguments are equal, and that the proportion cost is nonnegative whenever both arguments are positive.
background
The Golden Section in Architectural Proportion module predicts that the rectangle of minimum J-cost has aspect ratio φ:1, where J(x) = (x + x^{-1})/2 − 1. ProportionCost a i is the J-cost of the ratio a/i. The module imports Constants for φ and Cost for the underlying Jcost primitives. Upstream, phi_golden_recursion proves φ(φ − 1) = 1 from the quadratic identity φ² = φ + 1. preferredAspectRatio_in_aesthetic_band places φ inside (1.4, 1.9) by direct comparison with √5, while proportionCost_at_ideal and proportionCost_nonneg establish the cost properties via Jcost_unit0 and Jcost_nonneg.
proof idea
The definition constructs the GoldenSectionCert structure instance by direct field assignment. It supplies preferredAspectRatio_gt_one for the strict inequality 1 < φ, preferredAspectRatio_in_aesthetic_band for the aesthetic interval, phi_golden_recursion for the recursion identity, proportionCost_at_ideal for the zero-cost diagonal, and proportionCost_nonneg for nonnegativity. No additional tactics are required beyond the structure syntax.
why it matters in Recognition Science
This definition packages the core properties of the golden section certificate that underpins the architectural proportion claim in Recognition Science. It supports the prediction that the minimum J-cost rectangle occurs at φ:1, consistent with T5 J-uniqueness and T6 phi fixed point. The module doc states the falsifier as any large-N psychophysical study showing human preference for aspect ratios outside φ ± 0.2 across cultures. No downstream uses are recorded.
scope and limits
- Does not derive the value of φ from J-cost minimization.
- Does not prove uniqueness of φ as the aesthetic minimum.
- Does not connect the aesthetic band to empirical data.
- Does not address non-rectangular or higher-dimensional forms.
formal statement (Lean)
102noncomputable def cert : GoldenSectionCert where
103 ratio_gt_one := preferredAspectRatio_gt_one
proof body
Definition body.
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