Choice and smallness ledger for the initial-object lemma, GAFT, and SAFT

The initial-object construction in A complete locally small category with a jointly weakly initial set has an initial object, without class-indexed choice forms a limit of a supplied small full subcategory and uses one existential witness for each fixed target. It does not choose arrows simultaneously over all targets.

The objectwise theorems General adjoint functor theorem, objectwise initial-object form and Special adjoint functor theorem, objectwise form with explicit intersection smallness or preservation data produce an initial comma object for one fixed ambient object. Their functor forms require a supplied family of those comma objects so that no proper-class selection is hidden in assembling the adjoint. Both SAFT branches require the functor to preserve all small limits, which is what makes the comma category complete; neither branch replaces that hypothesis. On top of it, the chosen-well-powered branch supplies representative sets for subobjects, while the direct branch assumes the relevant class intersections and their preservation explicitly, so that it never treats a proper class as a small diagram.