Unconditional AAK theorem from the affine-pullback stable collar

The exact relative stable-collar construction supplies the stable homotopy-invariance input required by the refined S6 route. This module provides the final adapter and exports the arbitrary- n fair-partition theorem without a theorem-provider argument.

theorem NRR.AAK.avvakumov_akopyan_karasev (K : Geometry.ConvexBody Geometry.Plane) (n : ℕ) : 0 < n → ∃ (P : ConvexPartition K n), P.IsFair

Unconditional arbitrary-n Akopyan--Avvakumov--Karasev theorem obtained from the concrete affine-pullback collar, Route B perturbation, finite Stokes comparison, and the stable refined S6 obstruction.

theorem NRR.avvakumov_akopyan_karasev (K : Geometry.ConvexBody Geometry.Plane) (n : ℕ) : 0 < n → ∃ (P : ConvexPartition K n), P.IsFair

Canonical top-level public theorem. The conditional theorem-provider form is available as avvakumov_akopyan_karasev_of_primeRefinement.

theorem NRR.avvakumov_akopyan_karasev_affinePullback (K : Geometry.ConvexBody Geometry.Plane) (n : ℕ) : 0 < n → ∃ (P : ConvexPartition K n), P.IsFair

Route-specific alias for the unconditional affine-pullback proof.