proportionCost_nonneg
plain-language theorem explainer
Non-negativity of the cost incurred by any positive aspect ratio deviation follows from the corresponding property of the underlying J-cost function. Recognition Science modelers of architectural aesthetics cite this to confirm that all departures from ideal proportions carry non-negative costs. The proof is a one-line wrapper that unfolds the definition and invokes the J-cost non-negativity lemma on the positive ratio of the inputs.
Claim. For positive real numbers $a$ and $i$, the J-cost of the ratio $a/i$ satisfies $0 ≤ J(a/i)$.
background
The Golden Section in Architectural Proportion module develops the Recognition Science claim that the golden ratio φ minimizes J-cost for rectangles under fixed area, yielding human aesthetic preference. proportionCost is defined as the J-cost of the actual-to-ideal ratio. Upstream Jcost_nonneg states that J(x) ≥ 0 for positive x, proved via the representation J(x) = (x-1)^2/(2x) and non-negativity of the square.
proof idea
The proof unfolds the definition of proportionCost to expose Jcost applied to a/i, then applies the Jcost_nonneg lemma to the positive quantity produced by div_pos on the two hypotheses.
why it matters
This result populates the cost_nonneg field inside the GoldenSectionCert that certifies φ:1 rectangles satisfy the architectural criteria. It directly supports the module's structural theorem that the minimum J-cost rectangle occurs at the self-similar fixed point φ, linking to the T5 J-uniqueness and T6 phi forcing steps in the unified chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.