Formalize regular Myerson optimality under explicit assumptions

[ma-yuxuan]

Closes #13

Summary

• formalize the regular Myerson optimality endpoint for MSZ 12.59 under explicit analytic assumptions
• add the reserve second-price specialization for MSZ 12.61 under common reserve assumptions
• modularize the analytic assumption interfaces around environment, candidate/profile-split, reserve-candidate, interim measurability, and a.e. uniqueness packages
• update the Myerson knowledge nodes to document the completed conditional endpoints and future-work boundary

Validation

• lake build EconCSLib.MechanismDesign.Auction.OptimalSingleItem
• lake build EconCSLib.MechanismDesign.Auction.RegularMyersonReserveSecondPrice
• python scripts\check_knowledge_references.py docs\knowledge
• D:\FYP\mdblueprint\.venv\Scripts\mdblueprint-check.exe docs\knowledge --lean-root .

Notes

This PR intentionally keeps primitive analytic discharge, uniform distribution examples, nonzero seller value, boundary tie-sharing variants, and non-regular ironing as follow-up work.

[zhanquen]

Restructure maxBid and argmaxBid

maxBid and argmaxBid are tools based on the hypothesis "b : I -> R", which is a specialisation of single-parameter mechanism.
Define SingleParameterAuction first, then define the above tools as its methods.

BidExcluding

Bid excluding, i.e. bidProfileWithout_i should be an abstract structure in MechanismDesign, as it is helpful for the properties including DsIC.
Check what a bidProfile is, then define on it bidProfileWithout_i. The maxBidExcluding is then defined.

[zhanquen]

This hierarchy should be helpful

[zhanquen]

Restructure firstly AuctionBasic.lean