@BryanShih For a), you are right, and this comes from the following observation : the homotopy groups of S^0/p are p^2-torsion (this can be seen two ways: either use the long exact sequence of the cofiber sequence S^0 -> S^0 -> S^0/p, or prove directly that p^2 is nullhomotopic on S^0/p )

because of this, and because \tau_{\leq n}S^0/p is an iterated extension of its homotopy groups, it is an iterated extension of Eilenberg-MacLane spectra of finitely generated p^2-torsion abelian groups - it therefore suffices to show the result for these

but now if A is p^2-torsion, then pA -> A -> A/pA is a fiber sequence with both pA and A/pA F_p-modules, so direct sums of F_p's, and so we're done

(you are right in the beginning, but are wrong that the homotopy groups of S^0/p aren't in there ;) )

For b) : the short exact sequence from above translates into a fiber sequence of classifying spaces, now a fiber sequence F -> E -> BG can be interpreted as an action of G on F with homotopy orbits E; this is essentially the straightening-unstraightening equivalence

namely, the functor colim : Fun(BG,Spaces) -> Spaces refines to a functor Fun(BG,Spaces) -> Spaces/BG (if you have a functor F, you have a morphims F -> pt which induces a morphism colim F -> colim pt = BG), and straightening-unstraightening (in the case of left or right fibrations) says that this refined functor is an equivalence, and the inverse is given by "take the fiber over the point"

more precisely (there is an even stronger statement than what I'm about to say but...) if you compose the inverse functor Spaces/BG -> Fun(BG,Spaces) with the evaluation at the point of BG, you get the functor "fiber over that point": Spaces/BG -> Spaces

(preserves homotopy colimits)

And finally for c), I guess it's because the functor described in 4.23 is the composite of the forgetful Ring^{nu,h} -> Ab with the Eilenberg-MacLane functor, and lemma 4.24 shows that the latter is Latt-pseudocoherent, and the former is corepresented by R{x}^+ which is in the D of interest