gini_jcost_symmetric
plain-language theorem explainer
The theorem establishes symmetry of the J-cost function at the Gini ceiling value. Economists applying Recognition Science to inequality thresholds would cite it to confirm equal recognition costs on either side of the 1/phi boundary. The proof is a one-line wrapper that unfolds the ceiling definition and applies the Jcost symmetry lemma for positive reals.
Claim. $J(1/φ) = J(φ)$
background
In the Economics.InequalityCeilingFromSigma module the Gini ceiling is introduced as the reciprocal of the golden ratio, giniCeiling := phi^{-1}. The J-cost function is defined such that Jcost x = Jcost x^{-1} whenever x > 0, per the Jcost_symm lemma imported from the Cost module. The module setting predicts that under zero sigma the maximum sustainable Gini coefficient across the labour-capital ledger equals 1/phi, with the J-cost symmetry placing this threshold at the recognition boundary.
proof idea
The term proof first unfolds giniCeiling to expose phi^{-1}. It then invokes the Jcost_symm lemma (Jcost x = Jcost x^{-1} for x > 0) at the positive phi argument and takes the symmetric form to obtain the required equality.
why it matters
This declaration supplies the J-cost symmetry field required by the downstream inequalityCeilingCert definition, completing the static certification of the F3 inequality ceiling. It anchors the RS prediction that the Gini threshold coincides with the J-cost value of phi, consistent with the phi-ladder and the recognition composition law. No open scaffolding remains in this component.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.