pith. sign in
module module moderate

IndisputableMonolith.Economics.LaborEconomicsFromRS

show as:
view Lean formalization →

The LaborEconomicsFromRS module derives labor equilibrium in Recognition Science by setting the J-cost to zero. Economists extending the framework to social domains would cite it to link labor markets to the J-uniqueness property. The module consists of definitions and theorems that build directly on the imported Cost module.

claimLabor market equilibrium in the RS framework satisfies $J=0$, where $J$ denotes the cost function from the Recognition Composition Law.

background

The module imports Mathlib and IndisputableMonolith.Cost. The upstream Cost module supplies the J-cost function and related definitions. The doc comment states the core claim as 'Labor equilibrium: J = 0.' This places the module in the economics domain, applying the forcing chain landmarks to derive equilibrium conditions without introducing new constants or ladders.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds sibling declarations such as LaborMarketTheory and labor_equilibrium in the same file. It supplies the J=0 condition that connects labor economics to T5 J-uniqueness in the UnifiedForcingChain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)