Fibered Product tau^3

Fibered Product tau^3

Fibered Product tau^3

Summary

Fibered Product tau^3

Statement

%
\label{def:fibered-product-tau3}
The \textbf{fibered product} is the space
\[
    \tau^3
    \;:=\;
    \tau^1 \times_f T^2
    \;=\;
    \bigl\{\, (D, A, B, C) \;:\;
    (D, A) \in \tau^1,\;
    (B, C) \in T^2_{(D,A)}
    \,\bigr\},
\]
where $T^2_{(D,A)}$ denotes the fiber over the base point $(D, A)$:
the set of exponent-tetration pairs $(B, C)$
that are $\tau$-admissible at that base point.
The projection
\[
    \mathrm{pr} \colon \tau^3 \to \tau^1,
    \qquad
    (D, A, B, C) \;\mapsto\; (D, A)
\]
forgets the fiber coordinates,
retaining only the multiplicative skeleton.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 13
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part01/ch06-tau3-fibration.tex lines 228-253

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Interior.Tau3Fibration
• Name: Tau.BookII.Interior.Tau3

Dependencies

• Canonical: II.D05, II.D06, II.D02

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.