module module high

`IndisputableMonolith.GameTheory.MechanismDesignFromSigma`

This module defines the core objects and properties for mechanism design in Recognition Science, including bid vectors for n agents, winner selection, payments, utilities, DSIC conditions, pivot identity, and sigma conservation. Game theorists applying RS to incentive-compatible mechanisms would cite these when building truthful strategies from the sigma functional. The module consists of definitions and direct lemmas that follow algebraically from the imported Cost and Constants structures.

claimDefines BidVector as a vector in $R^n$ for $n$ agents, with associated functions winner, payment, utility, and lemmas establishing DSIC for agents zero and one, pivot identity, sigma conservation under truthful bidding, welfare optimality, and that truthful strategies form a Nash equilibrium.

background

The module sits in the GameTheory domain and imports Mathlib for basic structures, IndisputableMonolith.Constants supplying the RS time quantum with doc-comment 'The fundamental RS time quantum (RS-native). τ₀ = 1 tick.', and IndisputableMonolith.Cost for the underlying cost model. It introduces BidVector, winner, payment, utility, dsic_agent_zero, dsic_agent_one, pivot_identity, sigma_conservation_truthful, welfare_optimal_truthful, truthful_is_nash, and sigma_cost_to_agent_0. These rest on the J-cost and Recognition Composition Law from upstream Cost and Constants modules.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the foundational objects for mechanism design derived from the sigma functional in Recognition Science. It feeds parent results on truthful Nash equilibria and welfare-optimal mechanisms that connect to the J-uniqueness and phi-ladder structures in the forcing chain. The constructions enable application of dominant-strategy incentive compatibility to RS-native economic models without additional hypotheses.

scope and limits

Does not treat continuous or infinite agent sets.
Does not incorporate stochastic or repeated mechanisms.
Does not prove budget balance beyond sigma conservation.
Does not derive equilibrium existence outside the listed truthful cases.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (18)

theorem was L12
abbrev BidVector L104
def winner L121
def payment L126
def utility L135
theorem dsic_agent_zero L147
theorem dsic_agent_one L171
theorem pivot_identity L199
theorem sigma_conservation_truthful L216
theorem welfare_optimal_truthful L239
theorem truthful_is_nash L254
def sigma_cost_to_agent_0 L272
def sigma_cost_to_agent_1 L276
theorem vcg_payment_eq_sigma_cost L280
structure VCGCert L311
def vcgCert L335
theorem vcg_one_statement L358
structure is L388