%
\label{thm:fibration-structure}
The fibered product $\tau^3 = \tau^1 \times_f T^2$
is a fibration over $\tau^1$:
\begin{enumerate}
    \item \textbf{Projection.}
          The map $\mathrm{pr} \colon \tau^3 \to \tau^1$
          is surjective:
          every base point admits at least one fiber point
          (the trivial exponent tower $B = 1, C = 0$).
    \item \textbf{Fiber variation.}
          The fiber $T^2_{(D,A)}$ depends on the base point $(D,A)$:
          different primes $A$ yield different admissible ranges
          for $(B,C)$.
    \item \textbf{Non-triviality.}
          The fibration is not a product bundle:
          there is no global trivialization
          $\tau^3 \cong \tau^1 \times T^2$
          because the peel-order constraint
          couples the base coordinates
          and the admissibility conditions
          vary across base points.
    \item \textbf{Faithfulness.}
          The fibered product is faithful to the ABCD chart:
          the map
          $\Phi \colon \mathrm{Obj}(\tau) \to \tau^3$
          given by $X \mapsto (D(X), A(X), B(X), C(X))$
          is injective
          (by hyperfactorization, I.T04).
\end{enumerate}

[Proof sketch]
Surjectivity of $\mathrm{pr}$:
for any $(D, A) \in \tau^1$,
the object $D \cdot A$ has ABCD coordinates
$(D, A, 1, 0)$, so $(1, 0) \in T^2_{(D,A)}$.
Fiber variation:
if $A = p_1$ (the smallest prime),
then $D = 1$ necessarily (no smaller primes exist),
and the exponent range for $B$ is unrestricted;
if $A = p_k$ for large $k$,
then $D$ can be a product of $k-1$ smaller primes,
and the interaction between $D$ and $A$
constrains the admissible tetration heights.
Non-triviality:
suppose a global trivialization existed.
Then for every base point $(D, A)$,
the fiber would be the same space $T^2_0$.
But the constraint ``prime factors of $D < A$''
means that the admissible objects
over $(1, p_1)$ are different in kind
from those over $(p_1 \cdot p_2, p_3)$---the
fiber geometry depends essentially on the base.
Faithfulness is the Hyperfactorization Theorem (I.T04).