Primorial Thinness

A subset K is primordially thin at stage k if it occupies fewer than k-1 of the first k CRT positions (leaving >= 2 free directions). The tau-analog of codimension >= 2. Empty set is globally thin.

Primorial Thinness

Summary

A subset K is primordially thin at stage k if it occupies fewer than k-1 of the first k CRT positions (leaving >= 2 free directions). The tau-analog of codimension >= 2. Empty set is globally thin.

Statement

%
\label{def:primorial-thinness}
A subset $K \subseteq \mathbb{L}$
(Theorem~\ref{thm:algebraic-lemniscate}, I.D18)
is \textbf{primordially thin} if for every $d \geq 1$,
the projection $K_d := \{t \bmod M_d : t \in K\}$
misses at least two independent CRT directions:
\[
    \boxed{%
    K \text{ is thin}
    \quad:\Longleftrightarrow\quad
    \forall\, d \geq 1,\;
    \exists\, k_1 \neq k_2 \leq d:\;
    K_d \text{ misses the } k_1\text{-th and }
    k_2\text{-th CRT directions.}}
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 151
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part16/ch61-thinness.tex lines 93-110

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Holomorphy.Thinness
• Name: Tau.Holomorphy.PrimoriallyThin

Dependencies

• Canonical: I.D29

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.