# The Partition Principle does not imply Choice

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The Partition Principle does not imply Choice](../../preprints/The-Partition-Principle-does-not-imply-Choice-September-24-2026/partition-principle-without-choice.pdf)

## Scope

The Partition Principle says that every surjection admits an injection in the reverse direction. The formalization proves the relative-consistency implication: if ZF is consistent, then so is ZF with the Partition Principle, Choice for ordinal-indexed families, and failure of the Axiom of Choice.

The linked model-construction result also constructs a transitive model of the Partition Principle without Choice from an externally countable transitive ground model satisfying the stated axioms, including Choice, and containing an internal strongly inaccessible cardinal. The paper's stronger transitive-model preservation assertions are outside that selected construction.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Partition Principle without Choice from a ground model | [PartitionPrinciple.lean](../ComparatorChallenges/PartitionPrinciple.lean) |
| Relative consistency of the Partition Principle with ordinal Choice and failure of Choice | [PartitionConsistency.lean](../ComparatorChallenges/PartitionConsistency.lean) |