Arithmetic Laws

tau-Idx with index addition and multiplication forms a commutative semiring: commutativity, associativity, distributivity, identity elements.

Arithmetic Laws

Summary

tau-Idx with index addition and multiplication forms a commutative semiring: commutativity, associativity, distributivity, identity elements.

Statement

%
\label{prop:arithmetic-laws}
The structure $(\tau\text{-Idx}, +, \times, \underline{0}, \underline{1})$
is a commutative semiring:
\begin{itemize}
    \item $(\tau\text{-Idx}, +, \underline{0})$
          is a commutative monoid.
    \item $(\tau\text{-Idx}, \times, \underline{1})$
          is a commutative monoid.
    \item Multiplication distributes over addition.
    \item $\underline{0} \times \underline{n} = \underline{0}$
          (absorption).
\end{itemize}

Proof / Justification

Follows from
Propositions~\ref{prop:add-properties} and~\ref{prop:mul-properties}.

Source Context

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

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Denotation.Arithmetic
• Name: Tau.Denotation.arithmetic_laws

Dependencies

• Canonical: I.D10, I.D11

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.