%
\label{thm:linearity-census}
Of TauLib's 77~modules (${\approx}\,15{,}900$~lines):
\begin{enumerate}[\normalfont(i)]
    \item 74~modules $(96.1\%)$ use no classical axioms
          and are fully constructive within CIC.
    \item 2~modules use \texttt{Classical.em},
          both applied to decidable predicates,
          both eliminable
          (Proposition~\ref{prop:em-eliminable}, I.P38).
    \item 1~module uses the \texttt{funext} tactic,
          which invokes a CIC kernel axiom,
          not a classical commitment.
\end{enumerate}
Conclusion: Book~I's Lean~4 formalization
is compatible with the $!$-free fragment of linear logic
at the object level,
in the sense that classical excluded middle ---
the propositional expression of free contraction ---
is never essentially used.

Items~(i)--(iii) are the empirical result
of the audit described in
Sections~\ref{sec:ch70-protocol}--\ref{sec:ch70-census}.
The eliminability claim in item~(ii)
is Proposition~\ref{prop:em-eliminable}.
The kernel-axiom classification in item~(iii)
follows from the fact that \texttt{funext}
is a Lean~4 kernel axiom
(Remark~\ref{rem:kernel-not-violation}).

For the conclusion:
the $!$-free fragment of linear logic
prohibits free contraction
(Theorem~\ref{thm:diagonal-linear}, I.T37).
At the propositional level,
classical excluded middle $A \lor \neg A$
yields contraction ---
from $A \lor \neg A$ and two copies of a hypothesis,
one can route through both branches.
Since no theorem in TauLib
\emph{essentially} depends on
\texttt{Classical.em}
(the two sites are eliminable),
no theorem requires the contraction
that excluded middle provides.
The formalization operates within the $!$-free fragment.