giniCeiling
plain-language theorem explainer
The Gini ceiling is defined to equal the reciprocal of the golden ratio. Economists working with Recognition Science inequality bounds cite this as the predicted upper limit on the Gini coefficient. The definition is a direct alias to phiInv that supplies the value and all inherited algebraic identities without further computation.
Claim. Let φ be the golden ratio. The Gini ceiling is the real number g = 1/φ.
background
The module positions 1/φ as the canonical attractor for negative-rung quantities such as decay rates, target ratios, and the Gini coefficient ceiling. phiInv is the upstream definition supplying the value 1/phi. This giniCeiling re-exports that value for economics use, matching the sibling definition in InequalityCeilingFromSigma whose doc-comment states 'The Gini ceiling = 1/φ (golden ratio reciprocal)'.
proof idea
One-line definition that aliases giniCeiling directly to phiInv.
why it matters
This definition supplies the Gini-specific instance of the 1/φ invariant. It is required by the theorem all_phiInv_instances_equal that equates the five instances and by the certification structure PhiInverseInvariantsCert. It also supports the economics results giniCeiling_eq_phi_minus_one and giniCeiling_in_band that locate the value inside (0.617, 0.623). In the framework it realizes the cross-domain convergence claim for the Gini ceiling as one of the listed 1/φ instances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.