IndisputableMonolith.CrossDomain.JEquilibriumUniversality
This module shows that Nash, market, and health equilibrium statements are identical specializations of the single condition Jcost 1 = 0 to different domain labels. Cross-domain researchers cite it to establish that the three equilibria are literally the same theorem in Lean. The module consists of domain-labeled definitions plus direct reduction theorems that make the identity explicit.
claimThe propositions NashEquilibrium, MarketEquilibrium, and HealthEquilibrium each reduce to $J_{ m cost}(1)=0$ when the domain label is instantiated accordingly; Lean therefore treats the three statements as definitionally identical.
background
The module imports the Cost module, which supplies the definition of Jcost as the Recognition Science cost functional whose zero set marks equilibrium states. It then introduces three domain-specific equilibrium declarations (Nash, market, health) that differ only by a label parameter. The local theoretical setting is the cross-domain extension of the J-equilibrium concept, where the same algebraic condition is reused without modification across fields.
proof idea
This is a definition module whose argument consists of three parallel declarations of equilibrium propositions followed by reduction theorems (nash_eq, market_eq, health_eq) that each substitute the appropriate domain label into Jcost 1 = 0. The remaining theorems (nash_eq_market, all_three_equal, etc.) are one-line wrappers that apply the shared reduction to establish literal equality of the statements.
why it matters in Recognition Science
The module supplies the explicit unification step required for any cross-domain application of Recognition Science equilibria. It directly implements the claim that the three equilibria are the same theorem, thereby feeding the broader universality argument that appears in downstream cross-domain work. No parent theorem is listed in the used-by graph, but the module closes the gap between the base Jcost definition and domain-labeled statements.
scope and limits
- Does not prove existence of any equilibrium state.
- Does not compute numerical values of Jcost in specific models.
- Does not extend the reduction beyond the three listed domains.
- Does not derive Jcost itself from the forcing chain.