acceptanceBandRatio
plain-language theorem explainer
Acceptance band ratio is set to the golden ratio φ. Researchers modeling aesthetic pleasure from J-cost reciprocal symmetry cite this definition to fix the half-width of the moderate-complexity window. The assignment is a direct constant definition drawn from the self-similar fixed point.
Claim. The acceptance band ratio is defined as the golden ratio $φ$.
background
The J-cost function is $J(x) = (x + x^{-1})/2 - 1$, which obeys the reciprocal symmetry $J(r) = J(r^{-1})$. Aesthetic pleasure is expressed as pleasure$(r) = 1 - J(r)/J_{max}$ with $r$ the ratio of observed to optimal complexity. The acceptance band is the interval where pleasure exceeds half its maximum value, which holds precisely when $r$ lies in $(1/φ, φ)$ (the φ-step bandwidth).
proof idea
One-line definition that assigns the constant value of the golden ratio φ.
why it matters
It supplies the numerical factor required by band_width_gt_one inside the BerlyneInvertedUCert structure. That structure certifies the full inverted-U properties (maximum at one, symmetry, band ratio greater than one). The definition instantiates the φ-step bandwidth step in the module derivation from J-cost symmetry and connects directly to the T6 forcing of φ as the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.