cert
The cert definition assembles a concrete FibonacciCompositionCert record by supplying three field proofs for the golden division point. Art historians or Recognition Science researchers modeling composition would cite it to ground the phi-based division in verified properties. It is a direct record construction that populates the structure from three upstream theorems.
claimLet $g = 1/phi$ where $phi$ is the golden ratio. The certificate asserts $0 < g < 1$ together with the subsegment ratio $(1 - g)/g = phi - 1$.
background
The FibonacciInComposition module treats the golden section as the division point $g = phi^{-1}$ for a unit interval. The structure FibonacciCompositionCert packages three required properties: positivity of the division, the division lying strictly below one, and the resulting subsegments standing in the ratio $phi : 1$. The module opening states that Recognition Science predicts this division yields sub-rectangles whose areas are integer powers of $phi$, placing them on the canonical cost lattice.
proof idea
The definition is a one-line wrapper that directly assigns the three fields of FibonacciCompositionCert using the theorems goldenDivision_pos, goldenDivision_lt_one, and goldenDivision_ratio.
why it matters in Recognition Science
This definition supplies the inhabited instance of FibonacciCompositionCert, completing the structural theorem for golden-section composition in the module. It supports the RS claim that phi-based divisions produce area ratios on the cost lattice and aligns with the T6 self-similar fixed point. The module falsifier remains any large-N eye-tracking study showing equal fixation density on golden versus non-golden layouts.
scope and limits
- Does not claim historical artists used the golden section intentionally.
- Does not treat two- or three-dimensional compositions.
- Does not quantify statistical preference in viewing data.
- Does not derive the golden ratio from the forcing chain inside this file.
formal statement (Lean)
60noncomputable def cert : FibonacciCompositionCert where
61 division_pos := goldenDivision_pos
proof body
Definition body.
62 division_lt_one := goldenDivision_lt_one
63 division_ratio := goldenDivision_ratio
64