pith. sign in
module module high

IndisputableMonolith.Economics.InequalityCeilingFromSigma

show as:
view Lean formalization →

This module derives the Gini coefficient upper bound of 1/φ from the Recognition Science cost function and symmetry properties. Economists modeling inequality bounds within RS would cite the equality and band results. The module consists of a definition for giniCeiling together with direct algebraic equalities and band checks imported from the Cost module.

claim$G_{\max} = \phi^{-1}$, where $\phi$ is the self-similar fixed point and the bound follows from J-cost symmetry.

background

The module imports the RS time quantum $\tau_0 = 1$ tick from Constants. It draws the J-cost function and Recognition Composition Law from the Cost module to define economic inequality measures. The setting applies the phi-ladder and forcing chain (T5-T6) to derive a ceiling on the Gini coefficient.

proof idea

This is a definition module containing the giniCeiling definition, the equality theorem giniCeiling_eq_phi_minus_one, the band check giniCeiling_in_band, and the symmetric J-cost relation gini_jcost_symmetric. Each result is obtained by algebraic reduction using the imported Cost definitions.

why it matters in Recognition Science

The module supplies the Gini ceiling for economic applications inside the Recognition framework. It connects the phi fixed point (T6) to inequality via the J-cost. No downstream theorems are listed yet.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)