goldenDivision_ratio
plain-language theorem explainer
Golden section division of unit length produces sub-segments whose ratio equals phi minus one. Recognition Science researchers modeling artistic composition cite this result to justify the phi-based split point in paintings and architecture. The proof is a short algebraic reduction that unfolds the definition as the reciprocal of phi, invokes the nonzero property of phi, rewrites the division, and closes with linear arithmetic after canceling the inverse.
Claim. $ (1 - phi^{-1}) / phi^{-1} = phi - 1 $, where phi is the golden ratio and the left-hand side is the ratio of the two sub-segments created by the golden division point of unit length.
background
The module develops structural theorems for Fibonacci and golden section rules in artistic composition. Recognition Science predicts that the optimal 1D division of length L occurs at L/phi from one end, yielding sub-segments in ratio phi:1; the 2D case with aspect phi produces area ratios that are integer powers of phi. goldenDivision is defined as phi inverse, the golden section point of unit length. Upstream lemmas from Constants, PhiLadderLattice, and PhiSupport.Lemmas each establish phi_ne_zero by reduction to phi_pos, supplying the nonzero fact required for division manipulations.
proof idea
The term-mode proof unfolds goldenDivision to obtain phi inverse. It calls phi_ne_zero to produce hphi_ne, derives that the inverse is nonzero via inv_ne_zero, rewrites the division equation with div_eq_iff, cancels using mul_inv_cancel_0 to reach phi times inverse equals one, and finishes with nlinarith on the resulting linear relation.
why it matters
This theorem supplies the division_ratio field inside the FibonacciCompositionCert definition, which certifies the golden section properties for composition models. It realizes the module claim that the golden section yields sub-segments in ratio phi:1 and connects directly to the phi-ladder lattice and constants used throughout the Recognition framework. It touches no open scaffolding questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.