goldenDivision_lt_one
plain-language theorem explainer
The golden section division of unit length is strictly less than one. Art historians modeling composition and RS theorists building the phi-ladder would cite this to locate the division point inside the segment. The proof is a one-line wrapper applying the reciprocal inequality lemma to the established fact that phi exceeds one.
Claim. Let $phi$ be the golden ratio. The golden section division of unit length satisfies $phi^{-1} < 1$.
background
The FibonacciInComposition module treats artistic composition via the golden section. It defines goldenDivision as the point $phi^{-1}$ on a unit interval, so that the two sub-segments stand in ratio $phi:1$. This matches the RS prediction that an optimal 1D division occurs at $L/phi$ from one end, with all area ratios in 2D cases becoming integer powers of $phi$ on the canonical cost lattice. The module documentation states the structural theorem status and supplies a falsifier based on eye-tracking preference studies.
proof idea
The proof is a one-line wrapper that applies inv_lt_one_of_one_lt₀ to the upstream lemma one_lt_phi establishing $1 < phi$.
why it matters
This theorem supplies the division_lt_one field inside the FibonacciCompositionCert definition, which packages the three required properties for the golden section. It completes the local structural theorem for golden-section composition described in the module documentation. In the broader Recognition framework it anchors the phi fixed point (T6) and the self-similar division that feeds the eight-tick octave and D=3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.