pith. machine review for the scientific record. sign in
def definition def or abbrev high

proportionCost

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  50def proportionCost (actual_ratio ideal_ratio : ℝ) : ℝ :=

proof body

Definition body.

  51  Jcost (actual_ratio / ideal_ratio)
  52

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.