Hyperfactorization Theorem

HINGE THEOREM 1: Every x in Obj(tau) has a unique canonical NF via three critical lemmas (tetration injectivity, no-tie determinism, strict remainder descent). Provable in ZFC.

Hyperfactorization Theorem

Summary

HINGE THEOREM 1: Every x in Obj(tau) has a unique canonical NF via three critical lemmas (tetration injectivity, no-tie determinism, strict remainder descent). Provable in ZFC.

Statement

%
\label{thm:hyperfactorization}
For every $X \in \tau\text{-Idx}$ with $X \geq \underline{2}$,
the decomposition
\[
    \boxed{X
    \;=\;
    ((\underline{A} \uparrow\uparrow \underline{C})^{\underline{B}})
    \cdot \underline{D}}
\]
with
\begin{enumerate}
    \item[(i)] $\underline{A} \in \mathbb{P}_\tau$
          (prime),
    \item[(ii)] $\underline{B} \geq \underline{1}$,
          $\underline{C} \geq \underline{1}$,
    \item[(iii)] $\underline{D} \geq \underline{1}$,
          and if $\underline{D} > \underline{1}$,
          all prime factors of $\underline{D}$
          are strictly less than $\underline{A}$,
\end{enumerate}
exists and is \textbf{unique}.
That is, if
$((\underline{A'} \uparrow\uparrow \underline{C'})
^{\underline{B'}}) \cdot \underline{D'} = X$
also satisfies (i)--(iii), then
$\underline{A'} = \underline{A}$,
$\underline{B'} = \underline{B}$,
$\underline{C'} = \underline{C}$,
$\underline{D'} = \underline{D}$.

Proof / Justification

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

Source Context

• Registry source: book-01.jsonl line 34
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part05/ch24-hyperfactorization.tex lines 42-73

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Coordinates.Hyperfact
• Name: Tau.Coordinates.hyperfact_check

Dependencies

• Canonical: I.P05, I.L03, I.L04, I.D17

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.