Mul Cancel Fails at Zero

0 * 1 = 0 * 2 but 1 != 2. Multiplicative left-cancellation fails when the cancelled factor is zero.

Mul Cancel Fails at Zero

Summary

0 * 1 = 0 * 2 but 1 != 2. Multiplicative left-cancellation fails when the cancelled factor is zero.

Statement

%
\label{thm:mul-cancel-fails-zero}
% Depends: I.D09 (multiplication), I.P06 (zero vacuous)
$\underline{0} \times \underline{1} = \underline{0} \times \underline{2}$,
yet $\underline{1} \neq \underline{2}$.
That is, multiplicative left-cancellation fails when the
cancelled factor is $\underline{0}$.

Proof / Justification

By absorption (Proposition~\ref{prop:zero-vacuous}\,(4)):
$\underline{0} \times \underline{1}
 = \underline{0}
 = \underline{0} \times \underline{2}$.
Yet $\underline{1} = \langle\alpha, 1\rangle
     \neq \langle\alpha, 2\rangle = \underline{2}$.

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: I.D11, I.P18

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.