FibonacciCompositionCert
The structure bundles three properties of the golden section division point into a single certificate for use in composition models. Researchers applying Recognition Science to art history would cite it to assert that the division at phi inverse is positive, less than one, and satisfies the exact ratio condition derived from the golden ratio. The definition assembles these facts directly from the upstream goldenDivision constant and its lemmas.
claimLet $d = phi^{-1}$. The structure asserts $0 < d$, $d < 1$, and $(1 - d)/d = phi - 1$.
background
The FibonacciInComposition module examines the golden section in artistic composition under Recognition Science. It predicts that the optimal 1D division of length L occurs at L/phi from one end, producing sub-segments in ratio phi:1, and extends this to 2D rectangles with H/W = phi to obtain four sub-rectangles whose areas are integer powers of phi on the canonical cost lattice. Upstream, goldenDivision is defined as phi inverse, described as the golden section of unit length.
proof idea
Structure definition that packages the three properties of goldenDivision: its positivity, its strict upper bound below one, and the division ratio equaling phi minus one. It references the upstream goldenDivision definition together with the lemmas establishing those three facts.
why it matters in Recognition Science
The structure is instantiated by the downstream cert definition and shown inhabited by cert_inhabited. It formalizes the golden section property that the module uses to link artistic composition to the Recognition Science forcing chain, specifically the self-similar fixed point phi (T6) and the phi-ladder for costs. This supports the prediction that area ratios remain integer powers of phi, consistent with the Recognition Composition Law.
scope and limits
- Does not supply empirical eye-tracking data on viewer preference.
- Does not derive the golden section from the forcing chain inside this module.
- Does not extend the certificate to non-rectangular or time-varying compositions.
- Does not claim the golden section is the unique optimal division for all metrics.
formal statement (Lean)
55structure FibonacciCompositionCert where
56 division_pos : 0 < goldenDivision
57 division_lt_one : goldenDivision < 1
58 division_ratio : (1 - goldenDivision) / goldenDivision = phi - 1
59