pith. sign in
module module high

IndisputableMonolith.Economics.LorenzCurveFromSigmaBudget

show as:
view Lean formalization →

This module defines per-decile J-cost on income-share ratios to support Lorenz curve certification in Recognition Science economics. Modelers of inequality and mobility regimes cite it when mapping sigma budgets to observable distributions. It supplies the core decileCost function plus basic algebraic properties via direct definitions.

claimDefine decileCost$(r) = J(r)$ where $r$ is the income-share ratio in a given decile. The module also introduces IsHighInequalityRegime, IsHighMobilityRegime, and LorenzCurveCert as predicates on these costs.

background

The module sits in the Economics domain and imports Constants (where τ₀ = 1 tick is the RS time quantum) together with the Cost module that supplies the J-function. J satisfies J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and is the unique solution to the forcing chain at T5. decileCost applies this J directly to normalized income shares, yielding the per-decile cost that feeds regime classification and Lorenz-curve statements.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions supply the economic observables required by downstream LorenzCurveCert and the regime predicates. They close the link from the J-cost and phi-ladder to concrete inequality measures, consistent with the eight-tick octave and D = 3 spatial setting of the parent framework.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (12)