vcgCert
plain-language theorem explainer
This definition constructs the inhabited VCGCert structure for the two-agent single-item second-price auction, delivering DSIC for each agent over all real bids, the pivot payment rule, sigma conservation of total surplus, and welfare-maximizing allocation. Mechanism designers and game theorists working inside Recognition Science cite it as the concrete sigma-conserving auction. The construction is a direct field-by-field assembly of the module's sibling lemmas.
Claim. The VCG mechanism certificate for the two-agent single-item auction asserts dominant-strategy incentive compatibility for both agents over the full bid space, the pivot identity that the winner pays the loser's bid, conservation of total surplus on the utility ledger equaling the winner's valuation, and welfare optimality of the truthful allocation.
background
VCGCert is the structure whose eight clauses encode the master properties of the VCG mechanism: DSIC for agent zero, DSIC for agent one, truthful bidding as Nash equilibrium, the pivot identity linking payment to the second-highest bid, sigma conservation, and welfare optimality. The module sets the local setting as the single-item second-price auction with n agents, allocation to the highest bidder, and payments equal to the externality imposed on the displaced bidder. Upstream, sigma_conservation states that the total sigma in a closed system is conserved; if one agent gains sigma, another must lose it. The cost definitions from ObserverForcing and MultiplicativeRecognizerL4 supply the J-cost of recognition events that underpins the sigma ledger.
proof idea
The definition is a direct structural assembly that populates each field of VCGCert by reference to the module's sibling lemmas: dsic_agent_zero supplies the first DSIC clause, dsic_agent_one the second, truthful_is_nash the equilibrium property, pivot_identity the payment rule, sigma_conservation_truthful the conservation statement, and welfare_optimal_truthful the optimality clause.
why it matters
This definition supplies the inhabited master certificate that closes the VCG track in the Recognition Science framework, realizing the one-statement summary theorem printed in the module. It feeds the sigma-conservation and cost machinery from MoralDebt and ObserverForcing into a concrete mechanism, confirming that the auction respects the Recognition Composition Law through the pivot identity and welfare optimality. No open scaffolding remains in this module; the certificate stands as the terminal object for Track E10.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.