5 · Inside the Normal Form

Prerequisites: 4 · Differentiation.

Every proven so far rested on one claim: two terms compile to the same node. This tutorial opens that node up. The representation turns out to be the one you already met in tutorial 2, with one part removed.

Constants first

zelph> .import math
zelph+> <x> ~ polyring
(:needsring <x>) ⇐ (<x> ~ polyring)
zelph+> ? :topoly $( 7 )
Answer: (:topoly &7) = (pos zint &7)
zelph+> ? :topoly $( -7 )
Answer: (:topoly $( neg(&7) )) = (neg zint &7)

A constant polynomial takes the form of a signed integer term, either (pos zint N) or (neg zint N), where N represents a natural numeral from the substrate currently in use. No additional mechanisms are required: pos, neg, and zint are plain atoms, and the pair functions as a fact node just like any other. The expression (pos zint &7) carries an explicit sign since it is the coefficient form within the polynomial layer. Beyond this layer, a nonnegative integer is simply the natural numeral – 7 is expressed as &7 – and a zint term serves exclusively to denote a negative value.

The integer layer, integer-arithmetic, serves as a façade. It owns no recursion; each of its rules delegates the magnitude work to the natural module by asserting ordinary +, -, * and cmp facts. What it buys is totality – the gap tutorial 2 left open. math has already imported it; importing it again, as the first line below does, is harmless and merely indicates that the module is skipped:

zelph+> .import integer-arithmetic
zelph+> ? &3 - &5
zelph+> ? (pos zint &3) - (pos zint &5)
Answer: ((pos zint &3) - (pos zint &5)) = (neg zint &2)
zelph+> ? &2 + (neg zint &5)
Answer: (&2 + (neg zint &5)) = (neg zint &3)
zelph+> ? (neg zint &2) - (neg zint &5)
Answer: ((neg zint &2) - (neg zint &5)) = &3

The natural subtraction remains partial – nothing was patched. A second set of rules identifies signed operands (either two zint terms or a natural numeral paired with a negative one) and routes them to the signed implementation, whereas the natural rules yield no outcome in that context. An explicit (pos zint N) remains valid when placed alongside another zint term (when adjacent to a natural numeral, it derives nothing), and responses follow the same convention: a nonnegative outcome is expressed as a natural numeral, while only a negative value is represented as a zint term.

One variable

zelph+> ? :topoly $( x )
Answer: (:topoly x) = (x poly <(pos zint &0) (pos zint &1)>)
zelph+> ? :topoly $( 3*x^2 - 5 )
Answer: (:topoly $( &3 * x ^ &2 - &5 )) = (x poly <(neg zint &5) (pos zint &0) (pos zint &3)>)

A non-constant polynomial with main variable V is (V poly L), where L is a cons list of coefficients — least significant first, so the V⁰ coefficient is the outermost cell. Read the second answer: ⟨−5, 0, 3⟩ is −5 + 0·x + 3·x².

Least-significant-first is the same orientation as the digits of &42, and that is not a coincidence. A number in base b is a polynomial evaluated at b. The rules that add two coefficient lists in polynomial.zph are literally the digit recursion of common-arithmetic.zph with the carry removed — that is the whole difference between ℤ[x] and base-b arithmetic.

Two invariants

Collapse. A polynomial that happens to be constant in V is stored as its constant coefficient directly, never as (V poly (C cons nil)). So a canonical coefficient list always has length ≥ 2.

No trailing zero. The last element — the leading coefficient — is never the zero polynomial. Inner zeros are value-relevant and kept, which is why ⟨−5, 0, 3⟩ keeps its middle cell.

Together these give the property everything depends on: one polynomial, one node. The zero polynomial at every nesting level is the single node (pos zint &0). Which is why cancellation just happens:

zelph+> ? :topoly $( x - x )
Answer: (:topoly (x - x)) = (pos zint &0)
zelph+> ? :topoly $( (x + 1) - (1 + x) )
Answer: (:topoly $( x + &1 - (&1 + x) )) = (pos zint &0)

symbolic-minus converts X - X into &0 as well, yet it compares nodes rather than polynomials: :simplify transforms (x - x) into &0 and maintains (x + &1) - (&1 + x) unaltered, since its operands simplify to two distinct terms. Eliminating terms that are equal as polynomials falls outside the responsibility of a local rewrite – this is precisely what the canonical form built here achieves.

Several variables

Coefficients are themselves polynomials, in strictly inner variables:

zelph+> <x y> ~ polyring
(:needsring <x y>) ⇐ (<x y> ~ polyring)
zelph+> ? :topoly $( x*y )
Answer: (:topoly (x * y)) = (x poly <(pos zint &0) (y poly <(pos zint &0) (pos zint &1)>)>)

Outer variable x; the x⁰ coefficient is 0, the x¹ coefficient is the polynomial y. So this is 0 + (y)·x = xy.

A larger one:

zelph+> ? :topoly $( (x+y)^2 )
Answer: (:topoly ((x + y) ^ &2)) = (x poly <(y poly <(pos zint &0) (pos zint &0) (pos zint &1)>) (y poly <(pos zint &0) (pos zint &2)>) (pos zint &1)>)

Three x-coefficients: y², 2y, 1. That is y² + 2yx + x². The tag x on the outer list and y on the inner ones is what keeps the representation unambiguous — without it, the list for y as a constant-in-x polynomial would be node-identical to the list for x, and node identity would stop meaning equality.

Variable order

The nesting order is declared, and it is what <x y> ~ polyring was for. The rules in math.zph walk the list and emit, for each adjacent pair, a fact x pouter y — "x is strictly outer than y". Transitivity is provided by the polynomial layer, so adjacent pairs suffice.

Change the declaration and the normal form changes with it:

zelph+> <x y> ~ polyring
zelph> ? :topoly $( y*x )
Answer: (:topoly (y * x)) = (x poly <(pos zint &0) (y poly <(pos zint &0) (pos zint &1)>)>)

In a fresh session that declares the opposite order:

zelph> .import math
zelph+> <y x> ~ polyring
(:needsring <y x>) ⇐ (<y x> ~ polyring)
zelph+> ? :topoly $( y*x )
Answer: (:topoly (y * x)) = (y poly <(pos zint &0) (x poly <(pos zint &0) (pos zint &1)>)>)

Same polynomial, two normal forms — which is fine, because within one session the order is fixed and the form is unique. What is not optional is that the order be a strict total order on the variables in use. Declaring both x pouter y and y pouter x would break single-valuedness, and the polynomial layer reports such a pair as a contradiction, naming both conflicting facts. Two composites with no declared order derive nothing at all — partiality by absence, once again.

The operations

The data layer offers five, each exposed under = in the standard idiom:

(P padd Q) = R      addition
(:pneg P) = R       negation
(P psub Q) = R      subtraction, via pneg + padd
(P pmul Q) = R      multiplication
(P ppow N) = R      exponentiation, N a natural numeral

They are worth a look because of what is not in them. Addition of two polynomials in the same main variable is elementwise list addition — the digit recursion minus the carry — followed by a strip stage that removes trailing zeros and re-collapses. Multiplication is schoolbook: split off the head coefficient, multiply the tail, shift by consing a zero onto the front, and delegate the accumulation back to padd. Exponentiation is the naive recursion with pmul in place of *.

There is no clever algorithm here. What makes it fast enough for the Jacobian case study is the engine: hash-consing means every repeated subterm is computed once and shared, and every intermediate is memoised as a fact for the rest of the session.

Why this is a proof

Assemble the pieces:

• every canonical polynomial is a unique node (the two invariants plus the variable tag),
• every compilation produces a canonical result (leaves are canonical, and the operations preserve canonicity),
• so equality of polynomials is identity of nodes.

Which is why the identity rule in topoly.zph is one line and contains no comparison:

(A ≡ B, (:topoly A) = P, (:topoly B) = P) => ((A ≡ B) = proven)

Unification does the work. Both conditions mention the same variable P; it binds only if both compilations landed on the identical node.

Exercises

1. Compute ? :topoly $( (x+y)^3 ) and read the four coefficients off the answer. Check them against the binomial theorem.
2. ? :topoly $( (x - y) * (x + y) ) and ? :topoly $( x^2 - y^2 ) — the same node. Confirm it with zelph/exists rather than by eye.
3. Why is (V poly (C cons nil)) never produced? Construct a term whose compilation would build it if the collapse invariant were dropped, and say which later comparison would then fail.
4. Declare c ~ symconst alongside <x> ~ polyring and compile $( c*x ). What sort does the polynomial layer give c — and why does it need to appear in the pouter order like any variable?

Next

6 · Refuting the Jacobian Conjecture runs the whole stack — digits, integers, terms, derivatives, normal forms — on a result from July 2026.