preferredAspectRatio_gt_one
The inequality 1 < preferredAspectRatio confirms that the golden ratio serving as the minimum-J-cost aspect ratio exceeds unity. Recognition Science modelers of architectural proportions and aesthetic theorists would cite this to anchor the phi-ladder above a square. The proof is a direct one-line term application of the established lemma one_lt_phi.
claim$1 < phi$, where $phi$ is the golden ratio defined as the preferred aspect ratio for rectangles minimizing J-cost under area constraint.
background
The Golden Section in Architectural Proportion module defines preferredAspectRatio as phi and derives the minimum J-cost rectangle from the Recognition Composition Law applied to aspect ratios. J-cost is the derivedCost of a multiplicative recognizer comparator, equivalently the J-cost of a recognition event under observer forcing. The module states that among rectangles with fixed area the sum J(r) + J(1/r) is minimized at r = phi satisfying the self-similar recursion phi = 1 + 1/phi.
proof idea
Term-mode proof consisting of the single identifier one_lt_phi, which reduces via the definition of phi to the algebraic inequality 1 < sqrt(5) established in Constants and PhiSupport.
why it matters in Recognition Science
Supplies the ratio_gt_one field of GoldenSectionCert, completing the structural theorem that the golden section realizes the minimum non-trivial J-cost departure from a square. It instantiates the T6 forcing step where phi is the self-similar fixed point and supports the module's prediction that human aesthetic preference concentrates near phi. The module falsifier remains any large-N study showing preference for ratios outside phi ± 0.2.
scope and limits
- Does not prove uniqueness of the J-cost minimum at phi.
- Does not supply the numerical value of J(phi).
- Does not address empirical psychophysical validation.
- Does not extend to non-rectangular geometries.
Lean usage
have h : 1 < preferredAspectRatio := preferredAspectRatio_gt_oneformal statement (Lean)
47theorem preferredAspectRatio_gt_one : 1 < preferredAspectRatio := one_lt_phi
proof body
Term-mode proof.
48
49/-- J-cost on the aspect ratio deviation. -/