proportionCost_at_ideal
plain-language theorem explainer
The theorem shows that the J-cost vanishes exactly when a rectangle's actual aspect ratio equals its ideal ratio. Researchers working on Recognition Science predictions for aesthetic proportions cite this to anchor the zero baseline of the cost function before analyzing the golden ratio minimum. The proof is a one-line wrapper that unfolds the definition of proportionCost, simplifies the ratio to 1, and applies the unit lemma for Jcost.
Claim. For any nonzero real number $r$, the J-cost of the aspect ratio deviation for a rectangle with actual ratio $r$ and ideal ratio $r$ is zero: $J(r/r)=0$.
background
In the Golden Section in Proportion module the definition proportionCost(actual_ratio, ideal_ratio) := Jcost(actual_ratio / ideal_ratio) measures deviation from ideal proportions, where Jcost is the Recognition Science cost function. The upstream lemma Jcost_unit0 states that Jcost(1) = 0, providing the zero-deviation baseline. The module documentation frames this within the claim that the golden ratio minimizes J-cost for rectangles under area constraints, with the minimum occurring at the self-similar fixed point satisfying the phi-recursion.
proof idea
The proof is a one-line wrapper. It unfolds proportionCost to expose Jcost(r/r), rewrites the ratio to 1 via div_self using the hypothesis r ≠ 0, and applies the lemma Jcost_unit0 to obtain zero.
why it matters
This supplies the cost_at_ideal field inside the GoldenSectionCert structure used to certify the full set of golden-section properties. It anchors the zero point in the Recognition Science prediction that the minimum J-cost rectangle has aspect ratio phi, consistent with the forcing chain that selects phi as the self-similar fixed point and the eight-tick octave structure. The module documentation identifies the corresponding falsifier as any large-N psychophysical study showing aesthetic preference outside phi ± 0.2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.