Registry · Theorem I.T17 established formalized

I.T17 — Multiplicative Cancellation iff Positive

CLIMAX: Multiplicative cancellation holds for n iff n > 0. Zero is the unique obstruction. One locus, one guard, maximal universality everywhere else.

Book I Part 3 Ch. 15

Dependency Graph

Depends on (3)

I.P17 I.T16 I.P19

Lean Formalization

Module: TauLib.BookI.Denotation.Structural

Symbol: Tau.Denotation.tauIdx_mul_cancel_exactly_pos