module module moderate

`IndisputableMonolith.GameTheory.MechanismDesignFromSigma`

This module introduces mechanism design primitives built from the sigma cost function, including bid vectors for n agents along with winner, payment, and utility maps. Game theorists seeking incentive-compatible mechanisms in an RS-derived setting would reference these objects when analyzing DSIC properties or sigma conservation. The module consists entirely of definitions and short lemmas with no complex proofs.

claimA bid vector $B = (b_1, eta_2, eta_3)$ for $n$ agents together with maps $w(B)$ selecting the winner, $p(B)$ the payment, and $u_i(B)$ the utility of agent $i$, all derived from the sigma cost function so that truthful reporting conserves sigma and forms a Nash equilibrium.

background

The module imports Constants, where the fundamental RS time quantum is defined as τ₀ = 1 tick, and Cost, which supplies the underlying cost function. It introduces the bid vector as the central object and defines associated maps for winner selection, payments, and utilities. The local setting is mechanism design in which sigma conservation is required to hold for truthful agents, with sibling definitions covering DSIC properties for agents zero and one.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the base objects for mechanism design from sigma and connects directly to the Cost module. No downstream theorems are listed in the used_by block, indicating it functions as a foundational layer for later game-theoretic results on truthful equilibria and welfare optimality.

scope and limits

Does not derive payment rules from optimization.
Does not treat repeated or dynamic mechanisms.
Does not compute equilibria for continuous bid distributions.
Does not address more than two agents in the core lemmas.

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