Accepting exactly half of a successful phase

The menu guarantee permits a fixed-size acceptance step: choose exactly ceil(active/2) clean requests. Their recovery lines avoid all occupied points and are pairwise disjoint, while exactly floor(active/2) requests remain. The existential selection here specifies the semantic obligation of the circuit's first-clean-request selection pass.

theorem Algebraic.MassProduction.Nonuniform.HalfClean.existsHalfSelection {capacity active : ℕ} {K : Type u_1} {V : Type u_2} [Field K] [Finite K] [AddCommGroup V] [Module K V] (state : PhaseState V (Projectivization K V) capacity active) (candidate : Fin active → Projectivization K V) (successful : HalfClean state candidate) : ∃ (accepted : Finset (Fin active)), accepted.card = (active + 1) / 2 ∧ acceptedᶜ.card = active / 2 ∧ (∀ index ∈ accepted, Disjoint (puncturedLine (state.2 index) (candidate index)) (phaseOccupied state)) ∧ (↑accepted).Pairwise fun (left right : Fin active) => Disjoint (puncturedLine (state.2 left) (candidate left)) (puncturedLine (state.2 right) (candidate right))

A successful candidate has an exactly half-sized clean subset with disjoint recovery lines and a fixed-size complement.