Reference · Natural numbers

rainbow.math.nat.ring-reflect-sound

Natural numberssrc/rainbow/math/nat/ring_reflect_sound.clj0 definitions, 8 theorems

Unconditional, native soundness of the nat reflection normalizer. All polynomial lemmas quantify over arbitrary Pol, without an ordering or nonzero-coefficient assumption. Host helpers only assemble proof terms; every supporting lemma and each of the seven interface theorems is checked. A derived identity theorem packages their use for compact instance proofs.

Depends onmath.nat.ring-reflectmath.nat.semiring

ring/eval-pol-mk-px :
  (env : ℕ → ℕ) (p : ring/Pol) (i : ℕ) (q : ring/Pol)
  → ring/eval-pol env (ring/mk-px p i q) = ring/eval-pol env (ring/px p i q)

ring/eval-pol-add :
  (env : ℕ → ℕ) (p right : ring/Pol)
  → ring/eval-pol env (ring/pol-add p right) = algebra/nat-add (ring/eval-pol env p) (ring/eval-pol env right)

ring/eval-pol-scale :
  (env : ℕ → ℕ) (k : ℕ) (r : ring/Pol)
  → ring/eval-pol env (ring/pol-scale k r) = nat/multiply k (ring/eval-pol env r)

ring/eval-pol-mul-var :
  (env : ℕ → ℕ) (i : ℕ) (r : ring/Pol)
  → ring/eval-pol env (ring/pol-mul-var i r) = nat/multiply (ring/eval-pol env r) (env i)

ring/eval-pol-mul :
  (env : ℕ → ℕ) (p q : ring/Pol)
  → ring/eval-pol env (ring/pol-mul p q) = nat/multiply (ring/eval-pol env p) (ring/eval-pol env q)

ring/sound :
  (env : ℕ → ℕ) (e : ring/Expr)
  → ring/denote env e = ring/eval-pol env (ring/normalize e)

ring/pol-equal-sound :
  (p right : ring/Pol)
  (h₁ : ring/pol-equal p right = data/true)
  → p = right

ring/identity-sound :
  (env : ℕ → ℕ) (left right : ring/Expr)
  (checked : ring/pol-equal (ring/normalize left) (ring/normalize right) = data/true)
  → ring/denote env left = ring/denote env right