cert
plain-language theorem explainer
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.
Claim. Let φ 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.