cert
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.