cert_inhabited
plain-language theorem explainer
The declaration proves the FibonacciCompositionCert structure is inhabited by exhibiting an explicit witness satisfying the three division axioms. Art historians and Recognition Science researchers would cite it when confirming that a golden-section split exists for one-dimensional compositions. The proof is a one-line term that constructs the Nonempty instance directly from the cert definition.
Claim. There exists a FibonacciCompositionCert satisfying $0 <$ goldenDivision, goldenDivision $< 1$, and $(1 - $goldenDivision$)/$goldenDivision$ = $phi$ $- 1$.
background
The module develops the Recognition Science claim that optimal one-dimensional artistic composition divides a length L at L/phi from one end, producing sub-segments in ratio phi:1. The structure FibonacciCompositionCert packages the three required properties: positivity of the division point, its position strictly below one, and the exact ratio condition equaling phi minus one. This rests on the upstream definition of phi as the self-similar fixed point from the constants module and the goldenDivision function.
proof idea
The proof is a term-mode one-liner that applies the Nonempty constructor to the cert instance already defined in the same module.
why it matters
The theorem closes existence for the certificate, supporting the module's structural claim that golden-section divisions yield area ratios that are integer powers of phi. It aligns with the RS prediction for composition and the module falsifier requiring eye-tracking data to show preference for golden sections. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.