As Stated

Case record · Matching and social choice

Stability and strategy-proofness for matching with constraints: A necessary and sufficient condition

No defect was found in Theorems 1 or 2 within the stated audit scope. This is not a proof that the theorems are correct.

  • Findings2 claims
  • Updated6 November 2026 · version 1.0
  • AuthorsNot contacted

2 claims investigated in this paper

1Theorem 1Theorem · main resultNo defect foundDeep auditfull source check
2Theorem 2Theorem · main resultNo defect foundDeep auditfull source check

Claim 1 of 2 · theorem · main result · p. 771

Theorem 1

No defect found

No counterexample or nontrivial proof gap survived the recorded audit of the hierarchy direction.

Theorem 1. If the region family is a hierarchy, there exists a mechanism that is stable and strategy-proof for doctors.

Assumptions
finite doctors and hospitals with strict doctor rankings; responsive hospital preferences and regional quotas; admissible substitutable regional quasi-choice preferences; a fixed region family containing singleton and grand regions
Scope of the claim
The mechanism must work across the paper's admitted regional caps, regional preferences and agent preference profiles for the fixed doctor, hospital and region sets.

This record reports an unsuccessful attempt to find a defect within the stated scope. It is not a proof that the result is correct.

What was tested

The audit reconstructed the hierarchy mechanism and checked archived finite suites covering 4,284 hierarchical markets, 1,638,144 outcomes and 59,927,040 unilateral-deviation checks, with zero recorded failures. The proof logic and theorem quantifiers were also reviewed against the published version.

Limits

The finite search is selective and does not prove unrestricted sufficiency. The publication review reconciled the archived counts and source logic but did not rerun all 59,927,040 deviation checks.

Source

Full check, pp. 769–772. The stability definition, mechanism quantifiers and Theorem 1 were checked on rendered pages of the published version.

Evidence rerun

Partial. The archived package integrity and reported counts were reconciled; the full historical computation was not rerun during publication review.

Claim 2 of 2 · theorem · main result · p. 772

Theorem 2

No defect found

No counterexample or nontrivial proof gap survived the recorded audit of the non-hierarchy impossibility direction.

Theorem 2. If the region family is not a hierarchy, no mechanism is stable and strategy-proof for doctors across the paper's admitted domain.

Assumptions
finite doctors and hospitals with strict doctor rankings; responsive hospital preferences and regional quotas; admissible substitutable regional quasi-choice preferences; a fixed region family containing singleton and grand regions
Scope of the claim
The impossibility concerns one mechanism required to work across the full admitted domain for the fixed doctor, hospital and region sets; it is not a claim that every fixed non-hierarchical profile is itself impossible.

This record reports an unsuccessful attempt to find a defect within the stated scope. It is not a proof that the result is correct.

What was tested

The audit checked the paper's decisive three-profile non-hierarchy example: at the baseline there are two stable matchings, and whichever one a putative stable mechanism selects, one doctor can misreport so that the other becomes uniquely stable and is strictly better under that doctor's true ranking. An exact certificate, a separate finite stability checker and a full 576-report stable-selection model corroborate the case split.

Limits

The theorem is about a mechanism over the full admitted domain, not impossibility for every fixed non-hierarchical profile. The finite certificate supports the decisive construction but does not by itself prove every step of the general theorem.

Source

Full check, pp. 772–774, 787–788. Theorem 2, the three-profile example and the general non-hierarchy proof were checked on rendered pages of the published version.

Evidence rerun

Partial. The archived exact certificate and model outputs were reconciled and the logical case split was rechecked; the entire historical computation was not rerun during publication review.

Authors and corrections

Authors
The authors were not contacted; author notification is not a publication requirement.
Correction
None published.

History

  1. October 2026Deep audit completed: no defect found within the recorded scope
  2. 31 October 2026Full published-version source check completed
  3. 6 November 2026Record version 1.0 approved for release

Versions

  1. Version 1.06 November 2026First release.

Released versions are never edited; each keeps its own address.

Use of AI in this case

AI systems were used in the historical audit and in later review. The record distinguishes AI and computational evidence from human verification and does not treat AI agreement as human confirmation.