giniCeiling_in_band
plain-language theorem explainer
The theorem establishes that the Gini ceiling, defined as the reciprocal of the golden ratio, lies strictly between 0.617 and 0.623. Economists modeling sustainable inequality thresholds in Recognition Science would cite this bound to locate the onset of sigma-cascade collapse. The proof unfolds the definition, invokes the tight numerical bounds on phi, and applies reciprocal comparison rules with linear arithmetic.
Claim. Let $phi$ be the golden ratio. Then $0.617 < phi^{-1} < 0.623$.
background
The module Economics.InequalityCeilingFromSigma develops the Recognition Science prediction that the maximum sustainable Gini coefficient under sigma equal to zero is 1 over phi. The local definition sets giniCeiling to phi inverse, which equals phi minus one by the golden ratio identity. Upstream lemmas supply the tighter bounds 1.61 less than phi and phi less than 1.62, which translate directly into the target interval for the ceiling.
proof idea
The proof unfolds giniCeiling to obtain the reciprocal of phi. It obtains the lemmas phi greater than 1.61 and phi less than 1.62. The conjunction is split. Each conjunct rewrites via the reciprocal inequality commutation rules lt_inv_comm0 and inv_lt_comm0, then finishes by linarith.
why it matters
This theorem supplies the gini_band field inside the InequalityCeilingCert definition, which aggregates the equality to phi minus one, the numerical band, and the J-cost symmetry. It realizes the third structural item in the module documentation: 1 over phi in (0.617, 0.622) as the canonical Gini ceiling band. The bound anchors the economic application of the phi fixed point within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.