Sum Zero Iff Both Zero

n + m = 0 iff n = 0 and m = 0. Contrapositive: if either summand is positive, the sum is positive.

Sum Zero Iff Both Zero

Summary

n + m = 0 iff n = 0 and m = 0. Contrapositive: if either summand is positive, the sum is positive.

Statement

%
\label{prop:sum-zero-iff}
For $\underline{n}, \underline{m} \in \tau\text{-Idx}$:
\[
    \underline{n} + \underline{m} = \underline{0}
    \quad\Longleftrightarrow\quad
    \underline{n} = \underline{0}
    \;\text{ and }\;
    \underline{m} = \underline{0}.
\]

Proof / Justification

($\Leftarrow$)
If both are zero, then
$\underline{0} + \underline{0} = \rho^0(\underline{0}) = \underline{0}$.

($\Rightarrow$)
Suppose $\underline{n} + \underline{m} = \underline{0}$.
By definition, $\underline{n} + \underline{m}
= \rho^m(\rho^n(\alpha)) = \rho^{n+m}(\alpha) = \underline{n+m}$.
If $n > 0$ or $m > 0$, then $n + m > 0$,
so $\underline{n+m} = \rho^{n+m}(\alpha) \neq \alpha = \underline{0}$
(by $\KAxiom{4}$: each application of $\rho$ advances
depth by exactly~$1$).
Contradiction.

Source Context

• Registry source: book-01.jsonl line 96
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part03/ch11-swap-add-mul.tex lines 257-267

Lean / Formalization Notes

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

Dependencies

• Canonical: I.D10

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.