%
\label{prop:boolean-recovery}
Let $\mathrm{val} : \mathrm{Prop}_\tau \to \mathrm{Truth4}$
be a Truth4 valuation,
and let $S \subseteq \mathrm{Prop}_\tau$
be a set of propositions.
Then the following are equivalent:
\begin{enumerate}
    \item \textbf{Boolean sufficiency.}
          For every $P \in S$,
          $\mathrm{val}(P) \in \{\mathsf{T}, \mathsf{F}\}$
          (no intermediate truth values occur).
    \item \textbf{Spectral decisiveness.}
          For every $P \in S$,
          the spectral decomposition
          of the predicate yields
          identical verdicts in both sectors:
          either both sectors confirm $P$
          and neither confirms $\lnot P$ (giving $\mathsf{T}$),
          or both sectors confirm $\lnot P$
          and neither confirms $P$ (giving $\mathsf{F}$).
    \item \textbf{Lossless collapse.}
          The forgetful map $f$ restricted to
          the image $\mathrm{val}(S)$
          is an \emph{isomorphism}:
          $f|_{\mathrm{val}(S)} : \mathrm{val}(S)
          \xrightarrow{\sim} \{f(v) : v \in \mathrm{val}(S)\}$.
          No information is lost
          by collapsing Truth4 to Bool on $S$.
    \item \textbf{Negation compatibility.}
          For every $P \in S$,
          $f(\lnot \mathrm{val}(P))
          = \lnot f(\mathrm{val}(P))$:
          negation commutes with the forgetful map.
\end{enumerate}
Under any (hence all) of these conditions,
the full logic on $S$
is captured by classical Boolean logic:
\[
    \boxed{%
    \mathrm{Truth4}|_S \;\cong\; \mathrm{Bool}|_S.}
\]

$(1) \Rightarrow (2)$:
If $\mathrm{val}(P) = \mathsf{T}$,
then by the definition of Truth4
(Definition~\ref{def:truth4}),
both the $B$-sector and the $C$-sector
confirm $P$ and neither confirms $\lnot P$.
If $\mathrm{val}(P) = \mathsf{F}$,
both sectors confirm $\lnot P$
and neither confirms $P$.
In both cases, the sectors agree ---
this is spectral decisiveness.

$(2) \Rightarrow (1)$:
Spectral decisiveness means
the two sectors never split:
they either both confirm ($\mathsf{T}$)
or both deny ($\mathsf{F}$).
The values $\mathsf{B}$ (both confirm and deny)
and $\mathsf{N}$ (neither confirms nor denies)
cannot arise under spectral decisiveness.
Therefore $\mathrm{val}(P) \in \{\mathsf{T}, \mathsf{F}\}$.

$(1) \Rightarrow (3)$:
If $\mathrm{val}(S) \subseteq \{\mathsf{T}, \mathsf{F}\}$,
then $f|_{\mathrm{val}(S)}$ is the identity map
(since $f(\mathsf{T}) = \mathsf{T}$
and $f(\mathsf{F}) = \mathsf{F}$),
which is trivially an isomorphism.

$(3) \Rightarrow (1)$:
If $\mathrm{val}(P) = \mathsf{B}$ for some $P \in S$,
then $f(\mathsf{B}) = \mathsf{T} = f(\mathsf{T})$,
so $f$ identifies $\mathsf{B}$ with $\mathsf{T}$:
it is not injective on $\mathrm{val}(S)$
(assuming $\mathsf{T}$ is also in the image),
contradicting the isomorphism property.
Similarly for $\mathsf{N}$.

$(1) \Rightarrow (4)$:
If $\mathrm{val}(P) = \mathsf{T}$,
then $f(\lnot \mathsf{T}) = f(\mathsf{F}) = \mathsf{F}
= \lnot \mathsf{T} = \lnot f(\mathsf{T})$.
If $\mathrm{val}(P) = \mathsf{F}$,
then $f(\lnot \mathsf{F}) = f(\mathsf{T}) = \mathsf{T}
= \lnot \mathsf{F} = \lnot f(\mathsf{F})$.
In both cases, negation commutes with $f$.

$(4) \Rightarrow (1)$:
Since $\lnot \mathsf{B} = \mathsf{N}$,
we have $f(\lnot \mathsf{B}) = f(\mathsf{N}) = \mathsf{F}$
and $\lnot f(\mathsf{B}) = \lnot \mathsf{T} = \mathsf{F}$:
negation commutes with $f$ at $\mathsf{B}$.
Similarly at $\mathsf{N}$.
\emph{Note:} since the forgetful map $f$
is a Boolean algebra homomorphism
(projection from $\mathbf{2} \times \mathbf{2}$ to $\mathbf{2}$),
negation compatibility holds universally
and condition~(4) is automatically satisfied.
The nontrivial equivalence is between
conditions~(1)--(3).