Documentation

Transfer.Examples.ZModPolyDecide

decide_zmod_poly: deciding univariate polynomial identities over ZMod m #

ZModDecide.decide_zmod decides a ground ZMod m equation — every leaf a numeral — by bounded integer-residue computation. This module lifts that to a ∀ x : ZMod m polynomial identity p x = q x, where p/q are built from the variable x, +, -, *, ^, neg, and ZMod m numerals.

The mathematics is the seqpoly change of representation (HexSeqPoly): a polynomial is a dense coefficient list (HexPoly = List ℤ), evaluation is Horner form (evalC), and two Horner polynomials agree at every point of ZMod m once their coefficient lists are congruent mod m (evalC_congr_of_dvd). The variable is carried symbolically through the whole expression tree by the coefficient homomorphism lemmas evalC_cAdd / cScale / cMul / cPow, proved once over a generic commutative ring.

Boundedness #

denoteC reduces % m after every coefficient operation (cAddMod, cMulMod, cPowMod, …), so a coefficient is at most m² transiently and < m between steps. A degree-d identity produces two lists of about d + 1 coefficients, each below m; the closing divisibility check runs on those small integers. Unreduced convolution — repeated cMul inside cPow — would grow a coefficient's bit width additively per multiply, the blow-up that makes ring and native_decide over ZMod m diverge on a high-degree identity.

Main results #

Scope #

The integer-coefficient Horner evaluator (the seqpoly read-out) #

source
def Transfer.ZModPolyDecide.evalC {R : Type u_1} [CommRing R] :
List ℤ → R → R

Horner evaluation of an integer-coefficient list (low degree first) at x : R, coefficients cast in through Int.cast. This is the List ℤ (HexPoly) representation of a polynomial read out over R.

Equations
Instances For
    source
    def Transfer.ZModPolyDecide.cAdd :
    List ℤ → List ℤ → List ℤ

    Coefficient-wise addition.

    Equations
    Instances For
      source
      def Transfer.ZModPolyDecide.cScale (a : ℤ) :
      List ℤ → List ℤ

      Scalar multiplication of a coefficient list.

      Equations
      Instances For
        source
        def Transfer.ZModPolyDecide.cMul :
        List ℤ → List ℤ → List ℤ

        Coefficient-wise (convolution) product.

        Equations
        Instances For
          source
          def Transfer.ZModPolyDecide.cSub (p q : List ℤ) :
          List ℤ

          Coefficient-wise subtraction.

          Equations
          Instances For
            source
            def Transfer.ZModPolyDecide.cReduce (m : ℤ) (l : List ℤ) :
            List ℤ

            Reduce every coefficient mod m, keeping each entry in [0, m).

            Equations
            Instances For
              source
              @[simp]
              theorem Transfer.ZModPolyDecide.evalC_nil {R : Type u_1} [CommRing R] (x : R) :
              evalC [] x = 0
              source
              @[simp]
              theorem Transfer.ZModPolyDecide.evalC_cons {R : Type u_1} [CommRing R] (c : ℤ) (cs : List ℤ) (x : R) :
              evalC (c :: cs) x = ↑c + x * evalC cs x

              Coefficient homomorphism lemmas — proved once, generically over R #

              source
              theorem Transfer.ZModPolyDecide.evalC_cAdd {R : Type u_1} [CommRing R] (p q : List ℤ) (x : R) :
              evalC (cAdd p q) x = evalC p x + evalC q x
              source
              theorem Transfer.ZModPolyDecide.evalC_cScale {R : Type u_1} [CommRing R] (a : ℤ) (q : List ℤ) (x : R) :
              evalC (cScale a q) x = ↑a * evalC q x
              source
              theorem Transfer.ZModPolyDecide.evalC_cMul {R : Type u_1} [CommRing R] (p q : List ℤ) (x : R) :
              evalC (cMul p q) x = evalC p x * evalC q x
              source
              theorem Transfer.ZModPolyDecide.evalC_cSub {R : Type u_1} [CommRing R] (p q : List ℤ) (x : R) :
              evalC (cSub p q) x = evalC p x - evalC q x
              source
              theorem Transfer.ZModPolyDecide.evalC_cReduce (m : ℕ) (l : List ℤ) (x : ZMod m) :
              evalC (cReduce (↑m) l) x = evalC l x

              Reducing coefficients mod m leaves the value over ZMod m unchanged (ZMod.intCast_mod), lifted over the list.

              The decision step over ZMod m #

              source
              theorem Transfer.ZModPolyDecide.evalC_eq_zero_of_all {m : ℕ} (ds : List ℤ) (h : ∀ c ∈ ds, ↑c = 0) (x : ZMod m) :
              evalC ds x = 0

              A coefficient list all of whose entries reduce to 0 in ZMod m evaluates to 0 at every point.

              source
              theorem Transfer.ZModPolyDecide.evalC_congr_of_dvd {m : ℕ} (p q : List ℤ) (h : ∀ c ∈ cSub p q, ↑m ∣ c) (x : ZMod m) :
              evalC p x = evalC q x

              Two Horner polynomials are equal at every point of ZMod m once every coefficient of their difference cSub p q is divisible by m — a decidable integer predicate. This is HexDecide.residueMulReal's eq_transfer_backward step lifted from a single binop to a whole polynomial.

              The bounded coefficient operations (% m after every step) #

              source
              def Transfer.ZModPolyDecide.cAddMod (m : ℤ) (p q : List ℤ) :
              List ℤ

              Coefficient-wise addition, reduced mod m.

              Equations
              Instances For
                source
                def Transfer.ZModPolyDecide.cSubMod (m : ℤ) (p q : List ℤ) :
                List ℤ

                Coefficient-wise subtraction, reduced mod m.

                Equations
                Instances For
                  source
                  def Transfer.ZModPolyDecide.cMulMod (m : ℤ) (p q : List ℤ) :
                  List ℤ

                  Convolution product, reduced mod m.

                  Equations
                  Instances For
                    source
                    def Transfer.ZModPolyDecide.cNegMod (m : ℤ) (p : List ℤ) :
                    List ℤ

                    Coefficient-wise negation, reduced mod m.

                    Equations
                    Instances For
                      source
                      def Transfer.ZModPolyDecide.cPowMod (m : ℤ) (p : List ℤ) :
                      ℕ → List ℤ

                      Power by repeated reduced multiplication, so coefficients stay < m.

                      Equations
                      Instances For
                        source
                        theorem Transfer.ZModPolyDecide.evalC_cAddMod (m : ℕ) (p q : List ℤ) (x : ZMod m) :
                        evalC (cAddMod (↑m) p q) x = evalC p x + evalC q x
                        source
                        theorem Transfer.ZModPolyDecide.evalC_cSubMod (m : ℕ) (p q : List ℤ) (x : ZMod m) :
                        evalC (cSubMod (↑m) p q) x = evalC p x - evalC q x
                        source
                        theorem Transfer.ZModPolyDecide.evalC_cMulMod (m : ℕ) (p q : List ℤ) (x : ZMod m) :
                        evalC (cMulMod (↑m) p q) x = evalC p x * evalC q x
                        source
                        theorem Transfer.ZModPolyDecide.evalC_cNegMod (m : ℕ) (p : List ℤ) (x : ZMod m) :
                        evalC (cNegMod (↑m) p) x = -evalC p x
                        source
                        theorem Transfer.ZModPolyDecide.evalC_cPowMod (m : ℕ) (p : List ℤ) (n : ℕ) (x : ZMod m) :
                        evalC (cPowMod (↑m) p n) x = evalC p x ^ n

                        The polynomial-expression front #

                        source
                        inductive Transfer.ZModPolyDecide.PolyExpr :
                        Type

                        Univariate polynomial expressions over ZMod m: a variable leaf, integer- numeral constants, and the ring operations.

                        Instances For
                          source
                          def Transfer.ZModPolyDecide.instReprPolyExpr.repr :
                          PolyExpr → ℕ → Std.Format
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[instance_reducible]
                            instance Transfer.ZModPolyDecide.instReprPolyExpr :
                            Repr PolyExpr
                            Equations
                            source
                            def Transfer.ZModPolyDecide.PolyExpr.denoteA (m : ℕ) :
                            PolyExpr → ZMod m → ZMod m

                            The abstract meaning of a PolyExpr as a function ZMod m → ZMod m.

                            Equations
                            Instances For
                              source
                              def Transfer.ZModPolyDecide.PolyExpr.denoteC (m : ℤ) :
                              PolyExpr → Param.HexPoly

                              The bounded coefficient-list normalizer: the polynomial's dense coefficient list (HexPoly), reduced mod m after every operation.

                              Equations
                              Instances For
                                source
                                theorem Transfer.ZModPolyDecide.PolyExpr.denoteC_correct (m : ℕ) (e : PolyExpr) (x : ZMod m) :
                                denoteA m e x = evalC (denoteC (↑m) e) x

                                The refinement. The abstract value at x equals the Horner evaluation of the bounded coefficient list at x: the coefficient homomorphism lifted over the expression tree, with every reduction step invisible over ZMod m.

                                source
                                def Transfer.ZModPolyDecide.PolyExpr.allDvdB (m : ℤ) (l : List ℤ) :
                                Bool

                                The decidable coefficient-list divisibility check on the difference of the two normalized polynomials.

                                Equations
                                Instances For
                                  source
                                  theorem Transfer.ZModPolyDecide.PolyExpr.allDvdB_true {m : ℤ} {l : List ℤ} (h : allDvdB m l = true) (c : ℤ) :
                                  c ∈ l → m ∣ c
                                  source
                                  def Transfer.ZModPolyDecide.PolyExpr.polyCheck (m : ℤ) (e₁ e₂ : PolyExpr) :
                                  Bool

                                  The reflective coefficient check: every coefficient of the normalized difference is divisible by m.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    theorem Transfer.ZModPolyDecide.PolyExpr.decide_transfer_poly (m : ℕ) (e₁ e₂ : PolyExpr) (h : polyCheck (↑m) e₁ e₂ = true) (x : ZMod m) :
                                    denoteA m e₁ x = denoteA m e₂ x

                                    The backward transfer. When the coefficient check passes, the two abstract polynomials agree at every point of ZMod m. Underwritten by denoteC_correct and evalC_congr_of_dvd, so the decide on the reduced coefficients is proof, not trust.

                                    The decide_zmod_poly tactic #

                                    source
                                    partial def Transfer.ZModPolyDecide.reifyPoly (xvar : Lean.FVarId) (e : Lean.Expr) :
                                    Lean.MetaM Lean.Expr

                                    Reify a ZMod m expression into a PolyExpr, mapping the free variable xvar to PolyExpr.var. Fails on any leaf that is neither the variable nor a numeral.

                                    source
                                    def Transfer.ZModPolyDecide.tacticDecide_zmod_poly :
                                    Lean.ParserDescr

                                    Close a univariate polynomial identity ∀ x : ZMod m, p x = q x by bounded coefficient-list computation: introduce x, reify both sides into PolyExpr, then discharge via PolyExpr.decide_transfer_poly and a kernel decide on the reduced coefficient lists. Axiom-free (no Lean.ofReduceBool). Every leaf must be the variable or a numeral.

                                    Equations
                                    Instances For

                                      Examples #

                                      Axiom audit #

                                      source
                                      theorem Transfer.ZModPolyDecide.poly_example_audit (x : ZMod 7) :
                                      (x + 1) ^ 2 = x ^ 2 + 2 * x + 1