Fox–Neuwirth prime configuration model

This file records existence of the concrete compact Fox–Neuwirth model constructed in CellAtlas, with its free prime-symmetry action and equivariant map to labelled configurations.

The signed cellular cycle, orientation comparison, and nonzero orbit count are not postulated here. They provide the finite model used by the obstruction argument.

theorem NRR.primeConfigurationModel_exists_of_prime {p : ℕ} (hp : Nat.Prime p) : ∃ (M : PrimeConfigurationModel hp), M = foxNeuwirthTopCellModel hp

Public existence statement for the concrete compact model.