pith. machine review for the scientific record. sign in
def definition def or abbrev high

giniCeiling

show as:
view Lean formalization →

Recognition Science sets the Gini ceiling to the reciprocal of the golden ratio. Economists working in this framework cite the value as the upper bound on sustainable inequality when recognition variance sigma equals zero. The definition is a direct assignment of phi inverse drawn from the upstream invariants module.

claimThe Gini ceiling equals $phi^{-1}$, where $phi$ is the golden ratio fixed point satisfying $phi^2 = phi + 1$.

background

The Economics.InequalityCeilingFromSigma module predicts that the maximum sustainable Gini coefficient under sigma equals zero is one over phi, approximately 0.618. Above this threshold the recognition system undergoes a sigma-cascade and institutional collapse; below it the system maintains stable recognition equilibrium. The definition imports phi inverse from CrossDomain.PhiInverseInvariants, where the same quantity is named phiInv, and aligns with the zero J-cost identity event from ObserverForcing.

proof idea

The declaration is a direct noncomputable definition that assigns phi inverse. It inherits the golden ratio reciprocal identity from the upstream phi inverse definition and the equality theorem proved in the same module.

why it matters in Recognition Science

This definition supplies the core constant for the inequality ceiling theorems, including equality to phi minus one, band membership in (0.617, 0.622), and J-cost symmetry. It feeds the PhiInverseInvariantsCert structure and the unification theorem that equates all five instances of one over phi. In the Recognition framework it instantiates the T6 self-similar fixed point phi as an economic observable, consistent with the RCL and the eight-tick octave.

scope and limits

formal statement (Lean)

  28noncomputable def giniCeiling : ℝ := phi⁻¹

proof body

Definition body.

  29
  30/-- 1/φ = φ - 1 (golden ratio identity: φ² = φ + 1 → φ - 1 = 1/φ). -/

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.