A computable field of rational functions

CRatFunc K is the fraction field of the computable polynomial ring CPoly K, realised as a quotient of numerator/denominator pairs by the cross-multiplication relation. All field operations and equality are computable, so identities of rational functions in a generic parameter X can be verified by native_decide.

Sums and products reduce their result by an unverified polynomial gcd whose defining equations are checked by a decidable guard (CRatFunc.reducePair), so the reduction requires no gcd correctness theory while keeping intermediate degrees small.

This is the engine behind the symbolic verification of the parametric EES(2,5;x) and EES(2,7;x) order conditions (arXiv:2507.21006, Section 8; arXiv:2509.20599, Theorems E.1–E.2): instantiating a family at x := X : CRatFunc ℚ proves its order conditions at the generic parameter, i.e. as identities of rational functions.

instance BSeries.instNontrivialCPoly {K : Type u} [Field K] [DecidableEq K] : Nontrivial (CPoly K)

@[reducible, inline]

abbrev BSeries.PreRatFunc (K : Type u) [Field K] [DecidableEq K] : Type u

Fraction representatives: a numerator and a nonzero denominator.

Equations

• BSeries.PreRatFunc K = (BSeries.CPoly K × { q : BSeries.CPoly K // q ≠ 0 })

@[implicit_reducible]

instance BSeries.ratFuncSetoid (K : Type u) [Field K] [DecidableEq K] : Setoid (PreRatFunc K)

The cross-multiplication equivalence on fraction representatives.

Equations

• BSeries.ratFuncSetoid K = { r := fun (a b : BSeries.PreRatFunc K) => a.1 * ↑b.2 = b.1 * ↑a.2, iseqv := ⋯ }

@[reducible]

def BSeries.CRatFunc (K : Type u) [Field K] [DecidableEq K] : Type u

The computable field of rational functions over K.

Equations

• BSeries.CRatFunc K = Quotient (BSeries.ratFuncSetoid K)

def BSeries.CRatFunc.mk {K : Type u} [Field K] [DecidableEq K] (p q : CPoly K) (hq : q ≠ 0) : CRatFunc K

Build a rational function from a raw representative pair.

Equations

• BSeries.CRatFunc.mk p q hq = ⟦(p, ⟨q, hq⟩)⟧

theorem BSeries.CRatFunc.mk_eq_mk {K : Type u} [Field K] [DecidableEq K] {p₁ q₁ p₂ q₂ : CPoly K} {h₁ : q₁ ≠ 0} {h₂ : q₂ ≠ 0} : mk p₁ q₁ h₁ = mk p₂ q₂ h₂ ↔ p₁ * q₂ = p₂ * q₁

@[implicit_reducible]

instance BSeries.CRatFunc.instDecidableEq {K : Type u} [Field K] [DecidableEq K] : DecidableEq (CRatFunc K)

Equations

• x.instDecidableEq y = Quotient.recOnSubsingleton₂ x y fun (a b : BSeries.PreRatFunc K) => decidable_of_iff (a.1 * ↑b.2 = b.1 * ↑a.2) ⋯

@[implicit_reducible]

instance BSeries.CRatFunc.instZero {K : Type u} [Field K] [DecidableEq K] : Zero (CRatFunc K)

Equations

• BSeries.CRatFunc.instZero = { zero := BSeries.CRatFunc.mk 0 1 ⋯ }

@[implicit_reducible]

instance BSeries.CRatFunc.instOne {K : Type u} [Field K] [DecidableEq K] : One (CRatFunc K)

Equations

• BSeries.CRatFunc.instOne = { one := BSeries.CRatFunc.mk 1 1 ⋯ }

Reduction by a runtime-checked gcd

def BSeries.CRatFunc.reducePair {K : Type u} [Field K] [DecidableEq K] (a : PreRatFunc K) : PreRatFunc K

Cancel the (unverified) gcd of numerator and denominator; the guard checks the defining equations of the division, so the result represents the same fraction with no gcd correctness theory required.

Equations

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

theorem BSeries.CRatFunc.reducePair_equiv {K : Type u} [Field K] [DecidableEq K] (a : PreRatFunc K) : reducePair a ≈ a

Arithmetic

def BSeries.CRatFunc.addPair {K : Type u} [Field K] [DecidableEq K] (a b : PreRatFunc K) : PreRatFunc K

Raw sum of representatives.

Equations

• BSeries.CRatFunc.addPair a b = (a.1 * ↑b.2 + b.1 * ↑a.2, ⟨↑a.2 * ↑b.2, ⋯⟩)

def BSeries.CRatFunc.mulPair {K : Type u} [Field K] [DecidableEq K] (a b : PreRatFunc K) : PreRatFunc K

Raw product of representatives.

Equations

• BSeries.CRatFunc.mulPair a b = (a.1 * b.1, ⟨↑a.2 * ↑b.2, ⋯⟩)

def BSeries.CRatFunc.negPair {K : Type u} [Field K] [DecidableEq K] (a : PreRatFunc K) : PreRatFunc K

Raw negation of a representative.

Equations

• BSeries.CRatFunc.negPair a = (-a.1, a.2)

@[implicit_reducible]

instance BSeries.CRatFunc.instAdd {K : Type u} [Field K] [DecidableEq K] : Add (CRatFunc K)

Equations

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

@[implicit_reducible]

instance BSeries.CRatFunc.instMul {K : Type u} [Field K] [DecidableEq K] : Mul (CRatFunc K)

Equations

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

@[implicit_reducible]

instance BSeries.CRatFunc.instNeg {K : Type u} [Field K] [DecidableEq K] : Neg (CRatFunc K)

Equations

• BSeries.CRatFunc.instNeg = { neg := fun (x : BSeries.CRatFunc K) => Quotient.liftOn x (fun (a : BSeries.PreRatFunc K) => ⟦BSeries.CRatFunc.negPair a⟧) ⋯ }

theorem BSeries.CRatFunc.mk_eq_zero {K : Type u} [Field K] [DecidableEq K] {p q : CPoly K} {hq : q ≠ 0} : mk p q hq = 0 ↔ p = 0

A fraction is zero iff its numerator is zero.

@[implicit_reducible]

instance BSeries.CRatFunc.instInv {K : Type u} [Field K] [DecidableEq K] : Inv (CRatFunc K)

Equations

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

theorem BSeries.CRatFunc.inv_mk {K : Type u} [Field K] [DecidableEq K] {p q : CPoly K} (hq : q ≠ 0) (hp : p ≠ 0) : (mk p q hq)⁻¹ = mk q p hp

@[implicit_reducible]

instance BSeries.CRatFunc.field {K : Type u} [Field K] [DecidableEq K] : Field (CRatFunc K)

The field structure: all axioms are cross-multiplication identities in the computable polynomial domain CPoly K.

Equations

• BSeries.CRatFunc.field = Field.ofMinimalAxioms (BSeries.CRatFunc K) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def BSeries.CRatFunc.X {K : Type u} [Field K] [DecidableEq K] : CRatFunc K

The generic parameter.

Equations

• BSeries.CRatFunc.X = BSeries.CRatFunc.mk BSeries.CPoly.X 1 ⋯

def BSeries.CRatFunc.C {K : Type u} [Field K] [DecidableEq K] (c : K) : CRatFunc K

Embed a constant.

Equations

• BSeries.CRatFunc.C c = BSeries.CRatFunc.mk (BSeries.CPoly.C c) 1 ⋯

def BSeries.CRatFunc.ofPoly {K : Type u} [Field K] [DecidableEq K] : CPoly K →+* CRatFunc K

The embedding of polynomials, as a ring homomorphism.

Equations

• BSeries.CRatFunc.ofPoly = { toFun := fun (p : BSeries.CPoly K) => BSeries.CRatFunc.mk p 1 ⋯, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem BSeries.CRatFunc.ofPoly_injective {K : Type u} [Field K] [DecidableEq K] : Function.Injective ⇑ofPoly

instance BSeries.CRatFunc.instCharZeroCPoly {K : Type u} [Field K] [DecidableEq K] [CharZero K] : CharZero (CPoly K)

instance BSeries.CRatFunc.instCharZero {K : Type u} [Field K] [DecidableEq K] [CharZero K] : CharZero (CRatFunc K)

@[implicit_reducible]

instance BSeries.CRatFunc.instInvertibleOfNatOfCharZero {K : Type u} [Field K] [DecidableEq K] [CharZero K] : Invertible 2

Equations

• BSeries.CRatFunc.instInvertibleOfNatOfCharZero = invertibleOfNonzero ⋯