Does the Partition Principle imply the Axiom of Choice over ZF?

### What is the conjecture

> Does the Partition Principle imply the Axiom of Choice over ZF?

The **Partition Principle (PP)** states that whenever there is a surjection
`f : Y → X`, there is an injection `g : X → Y`. The Axiom of Choice implies PP because a choice
function for the fibers of `f` gives an injective right inverse. The converse is a longstanding open
question.

References:

- B. Banaschewski and G. H. Moore, [The dual Cantor-Bernstein theorem and the partition
principle](https://doi.org/10.1305/ndjfl/1093635502), *Notre Dame Journal of Formal Logic* 31(3),
1990.
- A. Karagila, [On the Partition Principle](https://karagila.org/2014/on-the-partition-principle/),
2014. This survey explicitly presents `PP → AC` as open and summarizes known partial results.

### Prerequisites needed

The intended formal statement is that every model of ZF and PP satisfies AC, namely
$\mathrm{ZF} + \mathrm{PP} \models \mathrm{AC}$.

Mathlib already provides generic first-order syntax, structures, satisfaction, and semantic
consequence in `Mathlib.ModelTheory`. What is currently missing is the first order ZFC axioms:

1. The ZFC axioms.
2. Formulas for set-coded functions, surjections, and injections.
3. PP sentence.
4. The conjecture.

The contribution structure would be:

```text
FormalConjecturesForMathlib/
└── SetTheory/
└── FirstOrderZFC.lean
FormalConjectures/
└── Paper/
└── PartitionPrinciple.lean
```

The final conjecture would look approximately like this:

```lean
import FormalConjecturesUtil

namespace PartitionPrinciple

open FirstOrder FirstOrder.Language

/--
Does the Partition Principle imply the Axiom of Choice over ZF?
-/
@[category research open, AMS 3]
theorem partition_principle_implies_axiom_of_choice :
(FirstOrderZFC.zf ∪ {FirstOrderZFC.partitionPrinciple}) ⊨ᵇ
FirstOrderZFC.axiomOfChoice := by
sorry

end PartitionPrinciple
```

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-03 Mathematical logic and foundations

### Choose either option

- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start by reading Mathlib.ModelTheory and the planned FormalConjecturesForMathlib/SetTheory/FirstOrderZFC.lean structure, then inspect the repository's existing formal conjecture patterns. Implement the listed ZFC axioms, formulas, Partition Principle sentence, and conjecture in PartitionPrinciple.lean. Done means the stated semantic-consequence theorem is represented with the requested imports and namespace.

Written by the indexing model from the issue text.