hex

35.3. HexReflect: shared algebraic reflection🔗

35.3.1. Introduction🔗

HexReflect turns a batch of commutative-ring expressions into Hex.MvPoly values over one sealed variable environment and proves that the conversion preserves interpretation. It is the only Hex library that imports Lean.Meta.Sym.Arith: Lean canonicalizes expressions, classifies their algebraic structure, and recognizes the fixed ring language, while this library owns the atom environment, the conversion to executable values, the interpretation proofs, provider selection, conditions, and resource accounting. Symbolic frontends such as the planned matrix tactics consume the session and result records defined here rather than parsing expressions themselves.

The computational library is Mathlib-free and depends on HexMvPoly and HexBasic. HexReflectMathlib, described in the correspondence section, states the conversion theorem for Mathlib's multivariate polynomials.

35.3.2. Sessions and batches🔗

A session belongs to one tactic invocation or one programmatic batch. The standalone runner enters SymM.run exactly once; every operation is written over any monad that lifts SymM and carries the session state, so a richer caller can run the same operations without a nested run.

🔗def
Hex.Reflect.ReflectM (α : Type) : Type
Hex.Reflect.ReflectM (α : Type) : Type

The standalone session monad.

🔗def
Hex.Reflect.run {α : Type} (x : Hex.Reflect.ReflectM α)
  (cfg : Hex.Reflect.Config := { }) : Lean.MetaM α
Hex.Reflect.run {α : Type}
  (x : Hex.Reflect.ReflectM α)
  (cfg : Hex.Reflect.Config := { }) :
  Lean.MetaM α

Run a standalone session, entering SymM.run exactly once.

A batch has two phases. While the environment is growing, every input is canonicalized, classified, and reified with the current Lean reifier; an otherwise unrecognized subexpression becomes one atom, and repeated canonical atoms receive the same identifier. Sealing fixes the size n, and every conversion after that point is against the same Fin n.

🔗def
Hex.Reflect.reifyCommRing {m : Type → Type} [Monad m]
  [MonadLiftT Lean.Meta.Sym.SymM m] [MonadLiftT Lean.MetaM m]
  [MonadStateOf Hex.Reflect.State m] [Lean.MonadError m]
  (input : Lean.Expr) :
  m (Hex.Reflect.ProviderOutcome Hex.Reflect.ReifiedRing)
Hex.Reflect.reifyCommRing
  {m : Type → Type} [Monad m]
  [MonadLiftT Lean.Meta.Sym.SymM m]
  [MonadLiftT Lean.MetaM m]
  [MonadStateOf Hex.Reflect.State m]
  [Lean.MonadError m]
  (input : Lean.Expr) :
  m
    (Hex.Reflect.ProviderOutcome
      Hex.Reflect.ReifiedRing)

Reify one commutative-ring input, allocating atoms in the growing environment.

🔗def
Hex.Reflect.reifyCommSemiring {m : Type → Type} [Monad m]
  [MonadLiftT Lean.Meta.Sym.SymM m] [MonadLiftT Lean.MetaM m]
  [MonadStateOf Hex.Reflect.State m] [Lean.MonadError m]
  (input : Lean.Expr) :
  m (Hex.Reflect.ProviderOutcome Hex.Reflect.ReifiedSemiring)
Hex.Reflect.reifyCommSemiring
  {m : Type → Type} [Monad m]
  [MonadLiftT Lean.Meta.Sym.SymM m]
  [MonadLiftT Lean.MetaM m]
  [MonadStateOf Hex.Reflect.State m]
  [Lean.MonadError m]
  (input : Lean.Expr) :
  m
    (Hex.Reflect.ProviderOutcome
      Hex.Reflect.ReifiedSemiring)

Reify one commutative-semiring input, allocating atoms in the growing environment.

🔗def
Hex.Reflect.sealAtoms {m : Type → Type} [Monad m]
  [MonadStateOf Hex.Reflect.State m] : m Hex.Reflect.Sealed
Hex.Reflect.sealAtoms {m : Type → Type}
  [Monad m]
  [MonadStateOf Hex.Reflect.State m] :
  m Hex.Reflect.Sealed

Seal the environment at its current size. Sealing an already sealed environment returns the same sealed identity.

🔗def
Hex.Reflect.reflectRingBatch (inputs : Array Lean.Expr)
  (order : Hex.Reflect.MonoOrder := Hex.Reflect.MonoOrder.grevlex)
  (cfg : Hex.Reflect.Config := { }) :
  Lean.MetaM (Hex.Reflect.ProviderOutcome Hex.Reflect.RingBatch)
Hex.Reflect.reflectRingBatch
  (inputs : Array Lean.Expr)
  (order : Hex.Reflect.MonoOrder :=
    Hex.Reflect.MonoOrder.grevlex)
  (cfg : Hex.Reflect.Config := { }) :
  Lean.MetaM
    (Hex.Reflect.ProviderOutcome
      Hex.Reflect.RingBatch)

The standalone batch runner.

A matrix frontend passes all entries as one batch: calling the single-expression runner once per entry would number equal atoms differently and make polynomial matrix operations meaningless.

🔗def
Hex.Reflect.reflectRing (input : Lean.Expr)
  (order : Hex.Reflect.MonoOrder := Hex.Reflect.MonoOrder.grevlex)
  (cfg : Hex.Reflect.Config := { }) :
  Lean.MetaM (Hex.Reflect.ProviderOutcome Hex.Reflect.RingEntry)
Hex.Reflect.reflectRing
  (input : Lean.Expr)
  (order : Hex.Reflect.MonoOrder :=
    Hex.Reflect.MonoOrder.grevlex)
  (cfg : Hex.Reflect.Config := { }) :
  Lean.MetaM
    (Hex.Reflect.ProviderOutcome
      Hex.Reflect.RingEntry)

The standalone single-expression runner. A matrix frontend must not call this once per entry; it passes all entries to reflectRingBatch.

35.3.3. Conversion and its proof🔗

The conversion consumes the reflected value directly. It normalizes with Expr.toPoly, or with Expr.toPolyC when Lean supplies characteristic evidence, translates each ordered variable and exponent to an exponent vector, maps every integer coefficient through the selected coefficient provider, and builds the polynomial with Hex.MvPoly.ofTerms under the requested comparator. Every variable bound is checked.

🔗def
Hex.Reflect.convertTerms? (n : ℕ) (char? : Option ℕ)
  (e : Hex.Reflect.RingExpr) : Option (List (Hex.Mono n × ℤ))
Hex.Reflect.convertTerms? (n : ℕ)
  (char? : Option ℕ)
  (e : Hex.Reflect.RingExpr) :
  Option (List (Hex.Mono n × ℤ))

The term list of a reflected expression over a sealed environment of size n.

🔗def
Hex.Reflect.ofIntTerms {n : ℕ} {C : Type} [Zero C] [Add C] [BEq C]
  [LawfulBEq C] {cmp : Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (ofInt : ℤ → C)
  (ts : List (Hex.Mono n × ℤ)) : Hex.MvPoly n C cmp
Hex.Reflect.ofIntTerms {n : ℕ} {C : Type}
  [Zero C] [Add C] [BEq C] [LawfulBEq C]
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  (ofInt : ℤ → C)
  (ts : List (Hex.Mono n × ℤ)) :
  Hex.MvPoly n C cmp

Build the polynomial from integer-coefficient terms through a coefficient map, merging monomials that became equal and dropping coefficients mapped to zero.

🔗def
Hex.Reflect.convert {m : Type → Type} [Monad m]
  [MonadLiftT Lean.Meta.Sym.SymM m] [MonadLiftT Lean.MetaM m]
  [MonadStateOf Hex.Reflect.State m] [Lean.MonadError m]
  (r : Hex.Reflect.ReifiedRing) (s : Hex.Reflect.Sealed)
  (order : Hex.Reflect.MonoOrder)
  (provider? : Option Hex.Reflect.CoeffProvider := none) :
  m (Hex.Reflect.ProviderOutcome Hex.Reflect.Conversion)
Hex.Reflect.convert {m : Type → Type}
  [Monad m]
  [MonadLiftT Lean.Meta.Sym.SymM m]
  [MonadLiftT Lean.MetaM m]
  [MonadStateOf Hex.Reflect.State m]
  [Lean.MonadError m]
  (r : Hex.Reflect.ReifiedRing)
  (s : Hex.Reflect.Sealed)
  (order : Hex.Reflect.MonoOrder)
  (provider? :
    Option Hex.Reflect.CoeffProvider :=
    none) :
  m
    (Hex.Reflect.ProviderOutcome
      Hex.Reflect.Conversion)

Convert a reified ring input against a sealed environment under the requested order. An explicit coefficient provider is validated against the classified ring and included in the conversion cache key; it does not alter registered provider selection or its cache.

The value-level soundness theorem is proved from the public Lean.Grind.CommRing denotation theorems and the evaluation laws of Hex.MvPoly.

🔗theorem
Hex.Reflect.eval₂_convertTerms.{u} {α : Type u} {n : ℕ} {C : Type}
  [Zero C] [Add C] [BEq C] [LawfulBEq C]
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {ofInt : ℤ → C} {interp : C → α}
  [Lean.Grind.CommRing α] (laws : Hex.Reflect.CoeffLaws ofInt interp)
  (ctx : Lean.RArray α) (x : Fin n → α)
  (hx : ∀ (i : Fin n), x i = ctx.get ↑i) {e : Hex.Reflect.RingExpr}
  {ts : List (Hex.Mono n × ℤ)}
  (h : Hex.Reflect.convertTerms? n none e = some ts) :
  Hex.MvPoly.eval₂ interp x (Hex.Reflect.ofIntTerms ofInt ts) =
    Lean.Grind.CommRing.Expr.denote ctx e
Hex.Reflect.eval₂_convertTerms.{u}
  {α : Type u} {n : ℕ} {C : Type} [Zero C]
  [Add C] [BEq C] [LawfulBEq C]
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {ofInt : ℤ → C} {interp : C → α}
  [Lean.Grind.CommRing α]
  (laws :
    Hex.Reflect.CoeffLaws ofInt interp)
  (ctx : Lean.RArray α) (x : Fin n → α)
  (hx : ∀ (i : Fin n), x i = ctx.get ↑i)
  {e : Hex.Reflect.RingExpr}
  {ts : List (Hex.Mono n × ℤ)}
  (h :
    Hex.Reflect.convertTerms? n none e =
      some ts) :
  Hex.MvPoly.eval₂ interp x
      (Hex.Reflect.ofIntTerms ofInt ts) =
    Lean.Grind.CommRing.Expr.denote ctx e

Conversion without characteristic evidence commutes with interpretation.

🔗theorem
Hex.Reflect.eval₂_convertTermsC.{u} {α : Type u} {n : ℕ} {C : Type}
  [Zero C] [Add C] [BEq C] [LawfulBEq C]
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {ofInt : ℤ → C} {interp : C → α}
  [Lean.Grind.CommRing α] {c : ℕ} [Lean.Grind.IsCharP α c]
  (laws : Hex.Reflect.CoeffLaws ofInt interp) (ctx : Lean.RArray α)
  (x : Fin n → α) (hx : ∀ (i : Fin n), x i = ctx.get ↑i)
  {e : Hex.Reflect.RingExpr} {ts : List (Hex.Mono n × ℤ)}
  (h : Hex.Reflect.convertTerms? n (some c) e = some ts) :
  Hex.MvPoly.eval₂ interp x (Hex.Reflect.ofIntTerms ofInt ts) =
    Lean.Grind.CommRing.Expr.denote ctx e
Hex.Reflect.eval₂_convertTermsC.{u}
  {α : Type u} {n : ℕ} {C : Type} [Zero C]
  [Add C] [BEq C] [LawfulBEq C]
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {ofInt : ℤ → C} {interp : C → α}
  [Lean.Grind.CommRing α] {c : ℕ}
  [Lean.Grind.IsCharP α c]
  (laws :
    Hex.Reflect.CoeffLaws ofInt interp)
  (ctx : Lean.RArray α) (x : Fin n → α)
  (hx : ∀ (i : Fin n), x i = ctx.get ↑i)
  {e : Hex.Reflect.RingExpr}
  {ts : List (Hex.Mono n × ℤ)}
  (h :
    Hex.Reflect.convertTerms? n (some c)
        e =
      some ts) :
  Hex.MvPoly.eval₂ interp x
      (Hex.Reflect.ofIntTerms ofInt ts) =
    Lean.Grind.CommRing.Expr.denote ctx e

Conversion modulo the characteristic commutes with interpretation.

The Meta proof returned to a caller applies these theorems to the quoted reflected syntax, sealed context, and term list. The equality between the pure conversion and the quoted term list is left to reduction of concrete reflected data, and the result is related to the caller's source by definitional equality. No symbolic evaluation is decided by the kernel.

🔗def
Hex.Reflect.Conversion.mkProof {m : Type → Type} [Monad m]
  [MonadLiftT Lean.Meta.Sym.SymM m] [MonadLiftT Lean.MetaM m]
  [MonadStateOf Hex.Reflect.State m] [Lean.MonadError m]
  (c : Hex.Reflect.Conversion) (input : Lean.Expr)
  (cfg : Hex.Reflect.Config := { }) :
  m (Hex.Reflect.ProviderOutcome Hex.Reflect.EqualityResult)
Hex.Reflect.Conversion.mkProof
  {m : Type → Type} [Monad m]
  [MonadLiftT Lean.Meta.Sym.SymM m]
  [MonadLiftT Lean.MetaM m]
  [MonadStateOf Hex.Reflect.State m]
  [Lean.MonadError m]
  (c : Hex.Reflect.Conversion)
  (input : Lean.Expr)
  (cfg : Hex.Reflect.Config := { }) :
  m
    (Hex.Reflect.ProviderOutcome
      Hex.Reflect.EqualityResult)

Assemble the interpretation proof of a conversion. The proof applies the general soundness theorem to the quoted reflected syntax, sealed context, and term list; the equality between the pure conversion and the quoted term list is left to reduction of concrete reflected data; and the result is related to the canonical source and to the caller's instantiated source by definitional equality.

🔗structure
Hex.Reflect.EqualityResult : Type
Hex.Reflect.EqualityResult : Type

An unconditional equality between a source expression and its result.

Constructor

Hex.Reflect.EqualityResult.mk

Fields

source : Lean.Expr

The caller's instantiated source expression.

value : Lean.Expr

The quoted result value.

interpretation : Lean.Expr

The interpretation of the value in the source carrier, the left-hand side of proof.

proof : Lean.Expr

A proof of interpretation = source.

atoms : Array Lean.Expr

The sealed atom environment, as presentation data and valuation.

35.3.4. Providers, conditions, and budgets🔗

A provider supplies executable operations together with the theorems needed to interpret them. Registration is separate from Lean.Meta.Sym.Arith recognition: it can change which verified computation handles a request, but it cannot change the source grammar or atom allocation.

🔗structure
Hex.Reflect.Registration : Type
Hex.Reflect.Registration : Type

A Meta registration. recognize inspects the canonical carrier and its exact instances and reports one of the four provider outcomes: notApplicable when the provider does not recognize the request, declined when it recognizes the request but cannot satisfy a stated condition, success with evidence, or failure when its own data is malformed.

Constructor

Hex.Reflect.Registration.mk

Fields

id : Hex.Reflect.ProviderId

Stable provider identity for diagnostics and condition provenance.

capability : Hex.Reflect.Capability

The capability this registration supplies.

priority : ℕ

Higher priorities are consulted first.

recognize : Hex.Reflect.CarrierRequest → Lean.Meta.Sym.SymM (Hex.Reflect.ProviderOutcome Hex.Reflect.Evidence)

Recognize the classified carrier with its exact instances.

🔗structure
Hex.Reflect.CoeffLaws.{u} {C : Type} {α : Type u} [Zero C] [Add C]
  [Lean.Grind.Ring α] (ofInt : ℤ → C) (interp : C → α) : Prop
Hex.Reflect.CoeffLaws.{u} {C : Type}
  {α : Type u} [Zero C] [Add C]
  [Lean.Grind.Ring α] (ofInt : ℤ → C)
  (interp : C → α) : Prop

The laws a coefficient interpretation must satisfy for Hex.MvPoly.eval₂ to agree with the Grind denotation: the map from reflected integer coefficients agrees with the integer cast, and the interpretation is additive and fixes zero.

Constructor

Hex.Reflect.CoeffLaws.mk.{u}

Fields

interp_ofInt : ∀ (k : ℤ), interp (ofInt k) = ↑k

The coefficient map followed by the interpretation is the integer cast.

interp_zero : interp 0 = 0

The interpretation fixes zero.

interp_add : ∀ (a b : C), interp (a + b) = interp a + interp b

The interpretation is additive.

🔗inductive type
Hex.Reflect.ProviderOutcome (α : Type) : Type
Hex.Reflect.ProviderOutcome (α : Type) :
  Type

The four outcomes of provider selection or of an expensive request.

Constructors

Hex.Reflect.ProviderOutcome.notApplicable {α : Type} :
  Hex.Reflect.ProviderOutcome α

The provider does not recognize this request; dispatch may continue.

Hex.Reflect.ProviderOutcome.declined {α : Type}
  (reason : Hex.Reflect.Decline)
  (usage : Hex.Reflect.BudgetUsage) :
  Hex.Reflect.ProviderOutcome α

The request is recognized but a stated condition or budget cannot be satisfied.

Hex.Reflect.ProviderOutcome.success {α : Type} (value : α)
  (usage : Hex.Reflect.BudgetUsage) :
  Hex.Reflect.ProviderOutcome α

Checked data together with the budget it consumed.

Hex.Reflect.ProviderOutcome.failure {α : Type}
  (error : Hex.Reflect.Failure) :
  Hex.Reflect.ProviderOutcome α

Malformed registration, quoted value, or evidence; reported immediately.

🔗inductive type
Hex.Reflect.Decline : Type
Hex.Reflect.Decline : Type

Why a recognized request could not be satisfied.

Constructors

Hex.Reflect.Decline.unsupportedView
  (requested : Hex.Reflect.RequestedView) (found : String) :
  Hex.Reflect.Decline

The carrier has an algebraic structure, but not the requested one.

Hex.Reflect.Decline.unsupportedCarrier
  (carrier : Lean.Expr) : Hex.Reflect.Decline

The carrier has no recognized algebraic structure.

Hex.Reflect.Decline.unresolvedMetavariable
  (source : Lean.Expr) : Hex.Reflect.Decline

A relevant metavariable remains unassigned.

Hex.Reflect.Decline.missingCapability
  (capability : Hex.Reflect.Capability)
  (carrier : Lean.Expr) : Hex.Reflect.Decline

No registered provider supplies the capability for this carrier.

Hex.Reflect.Decline.ambiguousProvider
  (capability : Hex.Reflect.Capability)
  (candidates : Array Hex.Reflect.ProviderId) :
  Hex.Reflect.Decline

Several providers of equal priority recognize the request.

Hex.Reflect.Decline.unsupportedSourceType
  (type : Lean.Expr) : Hex.Reflect.Decline

The source type is outside the supported translations.

Hex.Reflect.Decline.providerCondition
  (provider : Hex.Reflect.ProviderId) (reason : String) :
  Hex.Reflect.Decline

A recognizing provider cannot satisfy a required condition.

Hex.Reflect.Decline.budgetExhausted
  (info : Hex.Reflect.BudgetExhausted) : Hex.Reflect.Decline

A budget dimension would be exceeded.

Hex.Reflect.Decline.mixedCarriers
  (first second : Lean.Expr) : Hex.Reflect.Decline

A proof-producing batch mixes two carriers.

🔗inductive type
Hex.Reflect.Failure : Type
Hex.Reflect.Failure : Type

Malformed registration, evidence, or generated data.

Constructors

Hex.Reflect.Failure.invalidProviderEvidence
  (provider : Hex.Reflect.ProviderId) (message : String) :
  Hex.Reflect.Failure

A provider's registration, quoted value, or evidence is malformed.

Hex.Reflect.Failure.variableOutOfRange (var size : ℕ) :
  Hex.Reflect.Failure

A reflected variable identifier is outside the sealed environment.

Hex.Reflect.Failure.illTypedProof (message : String) :
  Hex.Reflect.Failure

A generated proof does not type-check.

Hex.Reflect.Failure.internal (message : String) :
  Hex.Reflect.Failure

An invariant of the session was violated.

Conditions record the propositions a result depends on, together with their provenance. Deduplication uses provenance and canonical proposition identity and preserves the first occurrence, so side-goal order is deterministic.

🔗structure
Hex.Reflect.Condition : Type
Hex.Reflect.Condition : Type

A proposition a result depends on, together with its provenance.

Constructor

Hex.Reflect.Condition.mk

Fields

proposition : Lean.Expr

The canonical proposition the result depends on.

provider : Lean.Name

The provider that introduced the condition.

source : Lean.Expr

The source subexpression the condition concerns.

operation : String

The operation that introduced the condition.

reason : String

Why the operation needs the condition.

🔗def
Hex.Reflect.dischargeConditions (cs : Array Hex.Reflect.Condition)
  (policy : Hex.Reflect.ConditionPolicy := { }) :
  Lean.MetaM
    (Array (Hex.Reflect.Condition × Lean.Expr) ×
      Array Hex.Reflect.Condition)
Hex.Reflect.dischargeConditions
  (cs : Array Hex.Reflect.Condition)
  (policy : Hex.Reflect.ConditionPolicy :=
    { }) :
  Lean.MetaM
    (Array
        (Hex.Reflect.Condition ×
          Lean.Expr) ×
      Array Hex.Reflect.Condition)

Try to discharge conditions by definitional equality with a local hypothesis, then by the configured normalizers. Unresolved conditions are returned rather than turned into goals.

Budgets bound every dimension of a request independently. Exhaustion is a decline that reports the dimension, limit, consumed amount, and requested increment.

🔗structure
Hex.Reflect.Budget : Type
Hex.Reflect.Budget : Type

Per-dimension amounts, used both for limits and for consumed usage.

Constructor

Hex.Reflect.Budget.mk

Fields

sourceNodes : ℕ

Source syntax nodes and batch entries.

atoms : ℕ

Atoms in the growing environment.

reflectedNodes : ℕ

Reflected syntax nodes.

exponent : ℕ

Literal exponent size.

terms : ℕ

Converted monomials and polynomial terms.

coefficientBits : ℕ

Coefficient size in bits.

proofNodes : ℕ

Proof-reconstruction nodes and quoted expression size.

🔗structure
Hex.Reflect.BudgetExhausted : Type
Hex.Reflect.BudgetExhausted : Type

The report returned when a request exceeds one budget dimension.

Constructor

Hex.Reflect.BudgetExhausted.mk

Fields

dimension : Hex.Reflect.BudgetDimension

The exceeded dimension.

limit : ℕ

The limit of that dimension.

consumed : ℕ

The amount consumed before the request.

requested : ℕ

The requested increment.

35.3.5. Mathlib correspondence🔗

HexReflectMathlib records the coefficient interpretation of a reflected batch as a Mathlib ring homomorphism, translates Mathlib characteristic evidence into the Grind form used by characteristic-aware normalization, and states the conversion theorem for MvPolynomial (Fin n) R through HexMvPolyMathlib.equiv.

🔗theorem
HexReflectMathlib.coeffLaws_ofRingHom.{u} {R : Type u} [CommRing R]
  {C : Type} [Ring C] (f : C →+* R) (ofInt : ℤ → C)
  (h : ∀ (k : ℤ), f (ofInt k) = ↑k) : Hex.Reflect.CoeffLaws ofInt ⇑f
HexReflectMathlib.coeffLaws_ofRingHom.{u}
  {R : Type u} [CommRing R] {C : Type}
  [Ring C] (f : C →+* R) (ofInt : ℤ → C)
  (h : ∀ (k : ℤ), f (ofInt k) = ↑k) :
  Hex.Reflect.CoeffLaws ofInt ⇑f

A Mathlib ring homomorphism from a coefficient ring that agrees with the integer cast on reflected coefficients satisfies the coefficient laws.

🔗theorem
HexReflectMathlib.isCharP_of_charP.{u} {R : Type u} [CommRing R] (p : ℕ)
  [CharP R p] : Lean.Grind.IsCharP R p
HexReflectMathlib.isCharP_of_charP.{u}
  {R : Type u} [CommRing R] (p : ℕ)
  [CharP R p] : Lean.Grind.IsCharP R p

Mathlib characteristic evidence gives the Grind form used by Expr.toPolyC. This helper is a theorem, not a global instance. Importing Mathlib.Algebra.CharP.Basic separately supplies a global bridge for cancellative semirings, so frontends may already obtain characteristic evidence through instance search. This theorem also permits supplying the Mathlib ring's exact characteristic instance explicitly.

🔗theorem
HexReflectMathlib.eval₂_equiv_ofIntTerms.{u} {R : Type u} [CommRing R]
  {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] (ctx : Lean.RArray R) {e : Hex.Reflect.RingExpr}
  {ts : List (Hex.Mono n × ℤ)}
  (h : Hex.Reflect.convertTerms? n none e = some ts) :
  MvPolynomial.eval₂ (Int.castRingHom R)
      (Hex.Reflect.ctxValuation ctx n)
      (HexMvPolyMathlib.equiv (Hex.Reflect.ofIntTerms id ts)) =
    Lean.Grind.CommRing.Expr.denote ctx e
HexReflectMathlib.eval₂_equiv_ofIntTerms.{u}
  {R : Type u} [CommRing R] {n : ℕ}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  (ctx : Lean.RArray R)
  {e : Hex.Reflect.RingExpr}
  {ts : List (Hex.Mono n × ℤ)}
  (h :
    Hex.Reflect.convertTerms? n none e =
      some ts) :
  MvPolynomial.eval₂ (Int.castRingHom R)
      (Hex.Reflect.ctxValuation ctx n)
      (HexMvPolyMathlib.equiv
        (Hex.Reflect.ofIntTerms id ts)) =
    Lean.Grind.CommRing.Expr.denote ctx e

The integer specialization of eval₂_equiv_ringHom_ofIntTerms.

🔗theorem
HexReflectMathlib.aeval_algEquiv_ofIntTerms.{u} {R : Type u}
  [CommRing R] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (ctx : Lean.RArray R)
  {e : Hex.Reflect.RingExpr} {ts : List (Hex.Mono n × ℤ)}
  (h : Hex.Reflect.convertTerms? n none e = some ts) :
  (MvPolynomial.aeval (Hex.Reflect.ctxValuation ctx n))
      (HexMvPolyMathlib.algEquiv (Hex.Reflect.ofIntTerms id ts)) =
    Lean.Grind.CommRing.Expr.denote ctx e
HexReflectMathlib.aeval_algEquiv_ofIntTerms.{u}
  {R : Type u} [CommRing R] {n : ℕ}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  (ctx : Lean.RArray R)
  {e : Hex.Reflect.RingExpr}
  {ts : List (Hex.Mono n × ℤ)}
  (h :
    Hex.Reflect.convertTerms? n none e =
      some ts) :
  (MvPolynomial.aeval
        (Hex.Reflect.ctxValuation ctx n))
      (HexMvPolyMathlib.algEquiv
        (Hex.Reflect.ofIntTerms id ts)) =
    Lean.Grind.CommRing.Expr.denote ctx e

The algebra form: with ℤ acting through algebraMap, the transported converted polynomial evaluates by MvPolynomial.aeval.