P-partition uniqueness for posets of height two

The P-partition generating series for weak order-preserving maps determines every finite naturally labeled poset of height at most two whose comparability graph has matching number at most three, among all finite naturally labeled posets. A Greene shape with r parts of size two and k parts of size one guarantees uniqueness exactly when r is at most three. The reconstruction counts flags of ideals whose successive blocks have unique extrema, recovers neighborhood multiplicities when one side has at most three vertices, and compares three-vertex covers in the remaining cases. The reconstruction theorem and the positive shape guarantee have formal proofs checked in Lean. The negative direction is due to Liu and Weselcouch, and their construction has also been checked in Lean.