decileCost_zero_at_equal
plain-language theorem explainer
The theorem shows that the per-decile J-cost vanishes exactly when the income-share ratio equals one. Economists building Lorenz-curve certificates under sigma-budget conservation cite this as the equality base case. The proof is a one-line wrapper that invokes the unit lemma for the underlying J-cost function.
Claim. The per-decile J-cost on the income-share ratio satisfies $J(1)=0$, where $J(x)=(x-1)^2/(2x)$.
background
In the module on Lorenz curves from sigma-budget conservation, each decile receives a J-cost computed from its income-share ratio $r_k$ (observed share divided by equal share). The sibling definition decileCost(r) simply applies the core J-cost function. Upstream, Jcost_unit0 states that Jcost 1 = 0 and records the explicit form $J(x)=(x-1)^2/(2x)$. The module states that the Gini coefficient is the integral of these J-costs across deciles and identifies the mobility threshold with the interval $J(φ)∈(0.11,0.13)$.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module; that lemma itself reduces by simp on the J-cost definition.
why it matters
This supplies the equal_zero field inside the LorenzCurveCert definition, which collects the structural axioms for the Lorenz-curve inequality certificate. It anchors the base case for the module's claim that Gini values at or below $J(φ)$ correspond to higher intergenerational mobility, matching the Great Gatsby Curve. The result instantiates the J-uniqueness property (T5) at the unit point for the economic domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.