Universal Additive Cancellation

n + a = n + b implies a = b. Additive cancellation is UNIVERSAL: no positivity guard needed. Follows from rho-injectivity.

Universal Additive Cancellation

Summary

n + a = n + b implies a = b. Additive cancellation is UNIVERSAL: no positivity guard needed. Follows from rho-injectivity.

Statement

%
\label{prop:add-cancel-universal}
% Depends: I.D08 (addition)
For all $\underline{n}, \underline{a}, \underline{b} \in \tau\text{-Idx}$:
\[
    \underline{n} + \underline{a} = \underline{n} + \underline{b}
    \quad\Longrightarrow\quad
    \underline{a} = \underline{b}.
\]
Additive cancellation holds without any positivity guard.

Proof / Justification

Recall that $\underline{n} + \underline{a} = \rho^a(\underline{n})$
(Definition~\ref{def:idx-add}).
If $\rho^a(\underline{n}) = \rho^b(\underline{n})$,
then both sides have seed $\alpha$
and respective depths $n + a$ and $n + b$.
Equality of depths gives $n + a = n + b$,
hence $a = b$, hence $\underline{a} = \underline{b}$.
Right cancellation follows symmetrically by commutativity.

Source Context

• Registry source: book-01.jsonl line 100
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part03/ch15-denotational-order.tex lines 200-210

Lean / Formalization Notes

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

Dependencies

• Canonical: I.D10, I.P02

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.