preferredAspectRatio_gt_one
plain-language theorem explainer
The theorem establishes that the preferred aspect ratio exceeds unity in the Recognition Science model of architectural proportion. Researchers deriving aesthetic preferences from J-cost minimization would cite this inequality to confirm the ratio lies above the square case. The proof is a one-line wrapper that directly invokes the established fact that the golden ratio exceeds one.
Claim. $1 < phi$, where $phi$ denotes the golden ratio defined as the aesthetically preferred aspect ratio for rectangles that minimize J-cost under area constraint.
background
The GoldenSectionInProportion module models architectural aesthetics via the Recognition Science prediction that the minimum J-cost rectangle has aspect ratio phi:1. Here preferredAspectRatio is defined directly as phi. The surrounding development minimizes J(r) = (r + 1/r)/2 - 1 subject to self-similar lattice constraints, yielding the phi-recursion phi = 1 + 1/phi as the point of smallest non-trivial departure from a square.
proof idea
This is a one-line wrapper that applies the lemma one_lt_phi (from Constants, re-exported in PhiSupport) to the definition preferredAspectRatio := phi.
why it matters
The result supplies the ratio_gt_one field of the GoldenSectionCert that collects the structural properties of the golden section. It anchors the RS claim that phi realizes the self-similar fixed point (T6) and the eight-tick octave structure, while the module falsifier remains any large-N study showing aesthetic preference outside phi ± 0.2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.