A computable model of ℚ(√2)

The quadratic field ℚ(√2) as pairs (a, b) ↔ a + b√2, with fully computable field operations and decidable equality, so that order conditions of Runge–Kutta schemes with √2 in their coefficients (the EES(2,7;x) family of arXiv:2507.21006, Section 8) can be machine-checked by native_decide.

structure BSeries.Qsqrt2 : Type

The quadratic field ℚ(√2) as pairs (a, b) ↔ a + b√2.

• a : ℚ
• b : ℚ

theorem BSeries.Qsqrt2.ext {x y : Qsqrt2} (a : x.a = y.a) (b : x.b = y.b) : x = y

theorem BSeries.Qsqrt2.ext_iff {x y : Qsqrt2} : x = y ↔ x.a = y.a ∧ x.b = y.b

@[implicit_reducible]

instance BSeries.instDecidableEqQsqrt2 : DecidableEq Qsqrt2

Equations

• BSeries.instDecidableEqQsqrt2 = BSeries.instDecidableEqQsqrt2.decEq

def BSeries.instDecidableEqQsqrt2.decEq (x✝ x✝¹ : Qsqrt2) : Decidable (x✝ = x✝¹)

Equations

• BSeries.instDecidableEqQsqrt2.decEq { a := a, b := a_1 } { a := b, b := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance BSeries.Qsqrt2.instZero : Zero Qsqrt2

Equations

• BSeries.Qsqrt2.instZero = { zero := { a := 0, b := 0 } }

@[implicit_reducible]

instance BSeries.Qsqrt2.instOne : One Qsqrt2

Equations

• BSeries.Qsqrt2.instOne = { one := { a := 1, b := 0 } }

@[implicit_reducible]

instance BSeries.Qsqrt2.instAdd : Add Qsqrt2

Equations

• BSeries.Qsqrt2.instAdd = { add := fun (x y : BSeries.Qsqrt2) => { a := x.a + y.a, b := x.b + y.b } }

@[implicit_reducible]

instance BSeries.Qsqrt2.instNeg : Neg Qsqrt2

Equations

• BSeries.Qsqrt2.instNeg = { neg := fun (x : BSeries.Qsqrt2) => { a := -x.a, b := -x.b } }

@[implicit_reducible]

instance BSeries.Qsqrt2.instMul : Mul Qsqrt2

Equations

• BSeries.Qsqrt2.instMul = { mul := fun (x y : BSeries.Qsqrt2) => { a := x.a * y.a + 2 * x.b * y.b, b := x.a * y.b + x.b * y.a } }

@[implicit_reducible]

instance BSeries.Qsqrt2.instInv : Inv Qsqrt2

Equations

• BSeries.Qsqrt2.instInv = { inv := fun (x : BSeries.Qsqrt2) => { a := x.a / (x.a ^ 2 - 2 * x.b ^ 2), b := -x.b / (x.a ^ 2 - 2 * x.b ^ 2) } }

@[simp]

theorem BSeries.Qsqrt2.zero_a : a 0 = 0

@[simp]

theorem BSeries.Qsqrt2.zero_b : b 0 = 0

@[simp]

theorem BSeries.Qsqrt2.one_a : a 1 = 1

@[simp]

theorem BSeries.Qsqrt2.one_b : b 1 = 0

@[simp]

theorem BSeries.Qsqrt2.add_a (x y : Qsqrt2) : (x + y).a = x.a + y.a

@[simp]

theorem BSeries.Qsqrt2.add_b (x y : Qsqrt2) : (x + y).b = x.b + y.b

@[simp]

theorem BSeries.Qsqrt2.neg_a (x : Qsqrt2) : (-x).a = -x.a

@[simp]

theorem BSeries.Qsqrt2.neg_b (x : Qsqrt2) : (-x).b = -x.b

@[simp]

theorem BSeries.Qsqrt2.mul_a (x y : Qsqrt2) : (x * y).a = x.a * y.a + 2 * x.b * y.b

@[simp]

theorem BSeries.Qsqrt2.mul_b (x y : Qsqrt2) : (x * y).b = x.a * y.b + x.b * y.a

@[simp]

theorem BSeries.Qsqrt2.inv_a (x : Qsqrt2) : x⁻¹.a = x.a / (x.a ^ 2 - 2 * x.b ^ 2)

@[simp]

theorem BSeries.Qsqrt2.inv_b (x : Qsqrt2) : x⁻¹.b = -x.b / (x.a ^ 2 - 2 * x.b ^ 2)

theorem BSeries.Qsqrt2.sq_ne_two (q : ℚ) : q ^ 2 ≠ 2

No rational square root of two.

theorem BSeries.Qsqrt2.norm_ne_zero {x : Qsqrt2} (hx : x ≠ 0) : x.a ^ 2 - 2 * x.b ^ 2 ≠ 0

The field norm a² - 2b² vanishes only at zero.

@[implicit_reducible]

instance BSeries.Qsqrt2.field : Field Qsqrt2

Equations

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

theorem BSeries.Qsqrt2.natCast_def (n : ℕ) : ↑n = { a := ↑n, b := 0 }

instance BSeries.Qsqrt2.instCharZero : CharZero Qsqrt2

@[implicit_reducible]

instance BSeries.Qsqrt2.instInvertibleOfNat : Invertible 2

Equations

• BSeries.Qsqrt2.instInvertibleOfNat = invertibleOfNonzero BSeries.Qsqrt2.instInvertibleOfNat._proof_2

def BSeries.Qsqrt2.sqrt2 : Qsqrt2

The square root of two.

Equations

• BSeries.Qsqrt2.sqrt2 = { a := 0, b := 1 }

@[simp]

theorem BSeries.Qsqrt2.sqrt2_mul_self : sqrt2 * sqrt2 = 2