giniCeiling_eq_phi_minus_one
plain-language theorem explainer
Golden ratio properties establish that the Gini ceiling equals φ minus one. Economists modeling recognition-based inequality limits cite this to fix the maximum sustainable Gini coefficient at 1/φ. The proof unfolds the definition of giniCeiling, invokes the phi square equation, applies field simplification with phi nonzero, and closes with linear arithmetic.
Claim. The Gini ceiling satisfies $g = φ - 1$, where $g := φ^{-1}$ and $φ$ is the golden ratio obeying $φ^2 = φ + 1$.
background
The module Economics.InequalityCeilingFromSigma derives an economic inequality ceiling from the sigma parameter. The Gini ceiling is introduced as giniCeiling := phi^{-1}, the reciprocal of the golden ratio. Upstream results include phi_sq_eq stating φ² = φ + 1 and phi_ne_zero asserting φ ≠ 0. The module also imports giniCeiling from CrossDomain.PhiInverseInvariants as phiInv.
proof idea
The term proof unfolds giniCeiling to its definition as phi inverse. It obtains phi_sq_eq, then applies field_simp with phi_ne_zero to clear the inverse. Linear arithmetic with phi_sq_eq confirms equality to phi minus one.
why it matters
This theorem supplies the gini_eq field for inequalityCeilingCert, which bundles the ceiling equality, the band (0.617, 0.622), and J-cost symmetry. It realizes the second structural point listed in the module documentation. In the Recognition Science framework it anchors the economic ceiling prediction to the phi fixed point and T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.