Reference · Natural numbers

rainbow.math.nat.ring-reflect

Natural numberssrc/rainbow/math/nat/ring_reflect.clj10 definitions, 0 theorems

Definitions for proving nat semiring identities BY REFLECTION. `rainbow.math.nat.ring` proves an identity by emitting a rewrite chain, and the chain grows super-linearly with the degree: (a+b+c)^3 takes 914,191 term nodes over nnrat. Reflection moves that work into one kernel computation instead. A goal is reified as a `ring/Expr`, both sides are normalized to Horner polynomials (`ring/Pol`) by `ring/normalize`, and `ring/pol-equal` compares the two normal forms; one soundness theorem, proved once, turns `pol-equal ... = true` into the equality of the original sides. The per-goal proof is then the size of the reified goal, and the kernel computes the normal forms (natively, on numeral literals). This module holds only the definitions. The soundness theorems (`ring/eval-pol-add`, `ring/eval-pol-mul`, `ring/sound`, `ring/pol-equal-sound`) are stated in WORKPLAN-2026-10-15-reflection.md and live in their own module. Normal form. `px p i q` denotes p * x_i + q. A polynomial is canonical when, in every `px p i q`, p is not `pc 0`, every index in p is >= i and every index in q is > i; `mk-px` keeps the first condition, and the operations keep the others when their inputs are canonical. Canonical forms of equal polynomials are equal, so `pol-equal` decides the identity. Soundness does not depend on canonicity: on any input the operations denote addition and multiplication, so a non-canonical input can make the tactic fail, never make it prove something false. Addition retains an equal-index px without testing its summed coefficient: canonical Nat coefficients cannot cancel. On non-canonical inputs this can retain a zero coefficient; the unconditional denotation law still holds. Native and axiom-free.

Depends onmath.logic.boolean-andmath.nat.linear-ordermath.linear.matrix.row-length-decidermath.finite.expectation

ring/is-zero-pc :
  (x₁ : ring/Pol)
  → data/Bool

ring/mk-px :
  (x₁ : ring/Pol) (x₂ : ℕ) (x₃ : ring/Pol)
  → ring/Pol

ring/eval-pol :
  (x₁ : ℕ → ℕ) (x₂ : ring/Pol)
  → ℕ

ring/pol-add :
  (x₁ x₂ : ring/Pol)
  → ring/Pol

ring/pol-scale :
  (x₁ : ℕ) (x₂ : ring/Pol)
  → ring/Pol

ring/pol-mul-var :
  (x₁ : ℕ) (x₂ : ring/Pol)
  → ring/Pol

ring/pol-mul :
  (x₁ x₂ : ring/Pol)
  → ring/Pol

ring/normalize :
  (x₁ : ring/Expr)
  → ring/Pol

ring/denote :
  (x₁ : ℕ → ℕ) (x₂ : ring/Expr)
  → ℕ

ring/pol-equal :
  (x₁ x₂ : ring/Pol)
  → data/Bool