Integral Domain

n * m = 0 iff n = 0 or m = 0. tau-Idx has no zero divisors (integral domain property). Forward direction uses positive core closure.

Integral Domain

Summary

n * m = 0 iff n = 0 or m = 0. tau-Idx has no zero divisors (integral domain property). Forward direction uses positive core closure.

Statement

%
\label{prop:integral-domain}
For $\underline{n}, \underline{m} \in \tau\text{-Idx}$:
\[
    \underline{n} \times \underline{m} = \underline{0}
    \quad\Longleftrightarrow\quad
    \underline{n} = \underline{0}
    \;\text{ or }\;
    \underline{m} = \underline{0}.
\]
That is, $\tau$-Idx has no zero divisors.

Proof / Justification

($\Leftarrow$)
If $\underline{n} = \underline{0}$ or $\underline{m} = \underline{0}$,
then the product is $\underline{0}$
by the absorption property
(Proposition~\ref{prop:arithmetic-laws},
Chapter~\ref{ch:swap-add-mul}).

($\Rightarrow$)
If $\underline{n} > \underline{0}$ and $\underline{m} > \underline{0}$,
then $\underline{n} \times \underline{m} > \underline{0}$
by positive core closure
(Proposition~\ref{prop:positive-closed},
Chapter~\ref{ch:exp-tetration}).
Contrapositive: product zero implies a factor is zero.

Source Context

• Registry source: book-01.jsonl line 104
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part04/ch16-primes-divisibility.tex lines 163-174

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Denotation.Structural
• Name: Tau.Denotation.tauIdx_integral_domain

Dependencies

• Canonical: I.P16, I.D11

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.