proportionCost
plain-language theorem explainer
This definition assigns the J-cost to the normalized deviation between an actual aspect ratio and a chosen ideal ratio. Aesthetic theorists and architects working within recognition-based models would cite it to quantify departures from optimal proportions such as the golden section. It is implemented as a direct one-line application of the J-cost function to the ratio of the two inputs.
Claim. The cost of a proportion with actual ratio $a$ and ideal ratio $i$ is defined by $J(a/i)$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The module treats the golden section ratio φ as the self-similar fixed point that minimizes J-cost for rectangles of fixed area. J-cost is the function satisfying the recognition composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and is applied here to aspect-ratio deviations. The local setting is the prediction that the minimum-J-cost rectangle has aspect ratio φ:1, with the φ-recursion φ = 1 + 1/φ arising from the forcing chain.
proof idea
The definition is a one-line wrapper that applies the J-cost function directly to the ratio of the actual aspect ratio to the ideal aspect ratio.
why it matters
It supplies the cost measure used inside the GoldenSectionCert structure to certify that the preferred aspect ratio satisfies the golden recursion, lies in the band (1.4, 1.9), and yields zero cost when actual equals ideal. The definition thereby anchors the RS claim that φ emerges as the fixed point of minimal non-trivial J-cost, consistent with the self-similar lattice and the phi-ladder. The module notes a falsifier consisting of large-N psychophysical studies showing aesthetic preference outside φ ± 0.2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.