# Adding An Algebraic Law
Adding a law type expands the language used to define operation structure. A
law is a permanent semantic claim, so it must be formal, checkable, and
discriminating before it enters the registry.
## Required Definition
A proposed law must define:
- Formal statement using quantified variables and operation signatures.
- Verification strategy describing how the checker evaluates the law.
- At least one operation that satisfies the law.
- At least one operation that does not satisfy the law.
- Failure report shape, including the counterexample fields required to debug
a violation.
## Formal Statement
The statement must be precise enough to implement without interpretation. For
example, commutativity is:
```text
for all a, b in u32: f(a, b) = f(b, a)
```
Avoid prose-only definitions. If a law depends on another operation, constant,
ordering, bounds, or type-specific behavior, include that in the formal
statement.
## Verification Strategy
The strategy must say which input tuples are generated, which expressions are
evaluated, what equality or comparator is used, and what domains are required
for exhaustive and witnessed verification. It must also define how custom
parameters such as identity elements, bounds, or related operation IDs are
encoded in `AlgebraicLaw`.
## Positive Example
Every law needs at least one operation that satisfies it. The positive example
proves the law is useful for real registry entries and gives future readers a
concrete model. For example, `BitXor` satisfies self-inverse with result `0`.
## Negative Example
Every law needs at least one operation that does not satisfy it. The negative
example is critical because it proves the law discriminates. A property that
every operation satisfies does not help conformance. For example, `Sub` does
not satisfy commutativity because `Sub(5, 3) != Sub(3, 5)`.
## Stability
Once accepted, the law meaning is permanent. Future changes may improve the
checker or add better counterexample shrinking, but they may not redefine the
law. If a better incompatible property is needed, add a new law with a new
name.