structure HexPolyTheory.Literal.Recognized : Type

The evaluated coefficients and the proof identifying the user's expression.

• coefficients : List ℚ
• proof : Lean.Expr

def HexPolyTheory.Literal.blockProof (xs : List ℚ) (block : Lean.Expr) : Lean.MetaM Lean.Expr

Integer cross products identify a compiled coefficient list with a block.

Equations

• One or more equations did not get rendered due to their size.

def HexPolyTheory.Literal.encode (a : Recognized) : Lean.MetaM (Lean.Expr × Lean.Expr)

Encode coefficients in compiled code; only cross products enter the proof.

Equations

• One or more equations did not get rendered due to their size.

def HexPolyTheory.Literal.finish (raw : Lean.Expr) (xs : List ℚ) (proof : Lean.Expr) : Lean.MetaM Recognized

Finish an adapter step without reducing rational coefficient arithmetic.

Equations

• One or more equations did not get rendered due to their size.

def HexPolyTheory.Literal.binary (a b : Recognized) (op theoremName listOp : Lean.Name) (xs : List ℚ) : Lean.MetaM Recognized

Combine two identified literals through integer coefficient operations.

Equations

• One or more equations did not get rendered due to their size.

def HexPolyTheory.Literal.subLists (xs ys : List ℚ) : List ℚ

Ascending coefficients of a subtraction, used only in adapter identities.

Equations

• HexPolyTheory.Literal.subLists xs ys = HexPolyTheory.addLists xs (HexPolyTheory.scaleList (-1) ys)

partial def HexPolyTheory.Literal.parse (e : Lean.Expr) (fuel : ℕ := 64) : Lean.MetaM Recognized

Recognize the rational polynomial fragment with bounded unfolding and closed powers. Each recursive step supplies its algebraic identification.

def HexPolyTheory.Literal.recognize (p : Lean.Expr) : Lean.MetaM Recognized

Identify an expression with ascending coefficients. The consumer includes this proof in its one auxiliary theorem; there is no adapter kernel precheck.

Equations

• One or more equations did not get rendered due to their size.