goldenDivision_pos
plain-language theorem explainer
The theorem establishes positivity of the golden section division point for unit length. Recognition Science researchers modeling artistic composition cite it when assembling certificates that the division lies in (0,1) and yields phi-ratio sub-segments. The proof is a one-line wrapper that applies the inverse-positivity rule directly to the known positivity of phi.
Claim. $0 < phi^{-1}$, where $phi$ is the golden ratio (the self-similar fixed point satisfying $phi = 1 + phi^{-1}$).
background
In the FibonacciInComposition module the golden section of unit length is introduced as the reciprocal of the golden ratio. The upstream definition states: 'Golden section of unit length: 1/φ' and sets goldenDivision := phi^{-1}. This supplies the division point used in the module's RS prediction that optimal 1D composition of length L occurs at L/φ, producing sub-segments in ratio φ:1.
proof idea
The proof is a one-line wrapper that applies inv_pos.mpr to phi_pos.
why it matters
The result supplies the division_pos field inside the FibonacciCompositionCert structure that certifies the golden-division properties. It fills the structural theorem slot in the ArtHistory module that links artistic composition to the phi-ladder arising from the forcing chain (T6 phi fixed point). The module documentation notes that all 2D area ratios become integer powers of phi, matching the canonical RS cost lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.