You've got your definition of an $\infty$-loop space wrong. An $\infty$-loop space is a space admitting all deloopings (strictly speaking, equipped with a specific choice of them). An n-fold delooping of an n-fold loop space is by definition an $(n-1)$-connected basepointed space, so in your sequence each $Y_i$ must be $(i-1)$-connected, unlike the case of general spectra.

putting on my constructivist hat Well if you define a function over the naturals by its values for odd and even numbers, then you must prove that this indeed defines a function for all $n:\mathbb N$. Some people can even claim this way that there are discontinuous functions $\mathbb R \to \mathbb R$!

I don't understand why do you drop out the disjoint loops. Looks like you proved that those 2 morphisms are inverse up to multiplication by $\mathrm{dim}\, X$, which is not invertible in general.

Constant sheaves are the same as the colimit of a diagram that maps each object to the final object $1: \mathcal{E}$, since sheaffification commutes with colimits and constant presheaves are of this form. More geometrically, we have a unique geometric morphism $\mathcal E \xrightarrow{p} Set$ and the constant sheaves are object isomorphic to $p^* X$ for $X: Set$.

There is nothing deep or mysterious here, $c_m$ and $\mathrm{log}_4 B_m$ just have approximately equal Taylor expansions in $1/m$. Honestly, both functions are so elementary that some relation between them isn't surprising.

When you write $A/ \alpha$, what does it mean? Is it just the spectrum cofiber of $\mathrm S \xrightarrow{\alpha} A$? Because that can't be right, at the very least you must factor out all $\pi_0(A)\alpha$.

Morally the reason we consider torsion sheaves is that the Galois group itself is profinite, so it only really makes sense to consider its cohomology with finite coefficients. Many related results illustrate this. The most basic is that the comparison theorem between topological and etale cohomology of proper complex varieties is only valid if we consider torsion coefficients. Functorially, considering homotopy types up to isomorphisms in finite cohomology is equivalent to profinite homotopy theory, and the profinite homotopy type of complex variety is functorial wrt Galois action.

@SaalHardali You take a $G$-equivariant sheaf on $X$ and a $G^{op} \times H$-equivariant sheaf on $X\times Y$, take their total spaces (which are $G$ and $G^{op}\times H$ sets respectively), factor their product by the diagonal action of $G$ and consider the projection to $Y$, getting an object in $Sh_H(Y)$. More geometrically you can describe it in Fourier-Mukai style: pull $F:Sh_G(X)$ back to $X\times Y$, multiply it by the kernel and push forward along $X\times Y \to Y$, which amounts to taking fiberwise coinvariants of $G$ action.

@SaalHardali Everything that I described is perfectly explicit and generalizes your construction for the point. Note also that your description also works exclusively for colimit-preserving functors (e.g. right adjoint to restriction of scalars isn't included). What exactly is your question?