Base tau^1

The base of the tau^3 fibration: the two-dimensional space tau^1 = {(D, A)} where A is a tau-prime and prime factors of D are strictly less than A. Carries the radial and address coordinates.

Base tau^1

Summary

The base of the tau^3 fibration: the two-dimensional space tau^1 = {(D, A)} where A is a tau-prime and prime factors of D are strictly less than A. Carries the radial and address coordinates.

Statement

%
\label{def:base-tau1}
The \textbf{base} of the $\tau^3$ fibration is
the two-dimensional space
\[
    \tau^1
    \;:=\;
    \bigl\{\, (D, A) \;:\;
    D \in \mathbb{N}_{\geq 1},\;
    A \in \mathbb{P}_\tau,\;
    \text{prime factors of } D \text{ are } < A
    \,\bigr\},
\]
where $\mathbb{P}_\tau$ denotes the internal primes
of $\tau$-Idx
(Book~I, Part~III).

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: I.D17

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.