ZFC internalizes the extensional results of choice but not the exteriority of selection as such. A choice function is a set of ordered pairs; the operative distinction-making in virtue of which one element rather than another is taken up is not among them. This paper names the structural trace of that reduction ρ and advances the ρ Thesis: every extensional formalization reduces an operative act to its extensional output, and this reduction is irreducible — any attempt to formalize the act produces a new extensional artifact whose own enactment generates a new remainder. The thesis is not a new axiom within ZFC but a meta-theoretic marker of the structural cost of extensional closure. Structural resonances with Gödelian incompleteness and Cohen's forcing are noted.
Han Qin (Sun,) studied this question.