Canonical Ladder Theorem

The enrichment ladder E₀ ⊊ E₁ ⊊ E₂ ⊊ E₃ is (i) non-empty at each level, (ii) strictly increasing, (iii) saturating at E₃, (iv) the unique maximal enrichment chain for Category τ. It is the organising result of Book III and the architectural blueprint for the entire series.

Canonical Ladder Theorem

Summary

The enrichment ladder E₀ ⊊ E₁ ⊊ E₂ ⊊ E₃ is (i) non-empty at each level, (ii) strictly increasing, (iii) saturating at E₃, (iv) the unique maximal enrichment chain for Category τ. It is the organising result of Book III and the architectural blueprint for the entire series.

Statement

%
\label{thm:canonical-ladder}
The self-enrichment of Category~$\tau$
via the enrichment functor~$\mathcal{F}_E$
produces a chain of four layers
\[
    E_0 \;\subsetneq\; E_1 \;\subsetneq\; E_2 \;\subsetneq\; E_3
\]
satisfying:
\begin{enumerate}
    \item[\textup{(i)}] \textbf{Non-emptiness.}
          Each $E_k$ is non-empty: $\lvert \Obj(E_k) \rvert \geq 1$
          and $E_k$ admits non-identity morphisms.
    \item[\textup{(ii)}] \textbf{Strict increase.}
          Each inclusion is proper:
          $E_k \setminus E_{k-1} \neq \varnothing$
          for $k = 1, 2, 3$.
    \item[\textup{(iii)}] \textbf{Saturation.}
          $\mathcal{F}_E(E_3) = E_3$.
    \item[\textup{(iv)}] \textbf{Uniqueness.}
          If $E_0' \subsetneq E_1' \subsetneq \cdots \subsetneq E_m'$
          is any maximal enrichment chain
          for Category~$\tau$
          satisfying~\textup{(i)--(iii)},
          then $m = 3$ and $E_k' \cong E_k$
          for all~$k$.
\end{enumerate}

Proof / Justification

No immediate manuscript proof block was extracted in this pilot run.

Source Context

• Registry source: book-03.jsonl line 20
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part01/ch08-the-canonical-ladder-theorem.tex lines 99-127

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Enrichment.CanonicalLadder
• Name: canonical_ladder_8_3

Dependencies

• Canonical: III.T01, III.T02, III.T03

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.