Numerical Verification for Example 7.7 using Dyadic Rationals

This file connects the rigorous dyadic interval arithmetic verification to the abstract existence theorem from Example_7_7.lean.

Structure

1. Dyadic utilities: invAtPrec for division with precision control
2. Interval bounds: Dyadic enclosures for √3, ā₀, ā₁, ā₂, and derived quantities
3. Concrete instantiation: Definition of example_sol and example_A using Rat values
4. Connection lemmas: Proofs that abstract bounds ≤ dyadic upper bounds
5. Main theorem: example_7_7_existence applying existence_theorem

Mathematical Setup

For λ₀ = 1/3, ν = 1/4, N = 2:

• ā₀ = √(1/3) = √3/3
• ā₁ = 1/(2ā₀) = √3/2
• ā₂ = -ā₁²/(2ā₀) = -3√3/8

We verify p(r₀) < 0 for r₀ ≈ 0.1 using interval arithmetic.

def Dyadic.invAtPrec (x : Dyadic) (prec : ℤ) : Dyadic

Inverts a dyadic number at a given (maximum) precision. Returns the greatest dyadic with precision ≤ prec that is ≤ 1/x.

Equations

• Dyadic.zero.invAtPrec prec = Dyadic.zero
• x.invAtPrec prec = x.toRat.inv.toDyadic prec

Rational Computation

All numerical verification in ℚ, cast to ℝ only for the abstract theorem.

def RationalVerification.prec : ℤ

Precision for dyadic 1/3 approximation

Equations

• RationalVerification.prec = 60

Input values (all ℚ)

def RationalVerification.ā₀ : ℚ

Equations

• RationalVerification.ā₀ = (Dyadic.ofIntWithPrec 649519052838327 50).toRat

def RationalVerification.ā₁ : ℚ

Equations

• RationalVerification.ā₁ = (Dyadic.ofIntWithPrec 974278579257490 50).toRat

def RationalVerification.ā₂ : ℚ

Equations

• RationalVerification.ā₂ = -(Dyadic.ofIntWithPrec 730893789193589 50).toRat

def RationalVerification.A₀₀ : ℚ

Equations

• RationalVerification.A₀₀ = (Dyadic.ofIntWithPrec 974278579257490 50).toRat

def RationalVerification.A₁₀ : ℚ

Equations

• RationalVerification.A₁₀ = -(Dyadic.ofIntWithPrec 1461417868886235 50).toRat

def RationalVerification.A₂₀ : ℚ

Equations

• RationalVerification.A₂₀ = (Dyadic.ofIntWithPrec 3288190204494028 50).toRat

def RationalVerification.lam0 : ℚ

Equations

• RationalVerification.lam0 = (Dyadic.invAtPrec 3 RationalVerification.prec).toRat

def RationalVerification.ν : ℚ

Equations

• RationalVerification.ν = 1 / 4

def RationalVerification.r0 : ℚ

Equations

• RationalVerification.r0 = (Dyadic.ofIntWithPrec 102 10).toRat

F(ā) computation

def RationalVerification.F₀ : ℚ

Equations

• RationalVerification.F₀ = RationalVerification.ā₀ * RationalVerification.ā₀ - RationalVerification.lam0

def RationalVerification.F₁ : ℚ

Equations

• RationalVerification.F₁ = 2 * RationalVerification.ā₀ * RationalVerification.ā₁ - 1

def RationalVerification.F₂ : ℚ

Equations

• RationalVerification.F₂ = RationalVerification.ā₁ * RationalVerification.ā₁ + 2 * RationalVerification.ā₀ * RationalVerification.ā₂

A·F(ā) computation

def RationalVerification.AF₀ : ℚ

Equations

• RationalVerification.AF₀ = RationalVerification.A₀₀ * RationalVerification.F₀

def RationalVerification.AF₁ : ℚ

Equations

• RationalVerification.AF₁ = RationalVerification.A₁₀ * RationalVerification.F₀ + RationalVerification.A₀₀ * RationalVerification.F₁

def RationalVerification.AF₂ : ℚ

Equations

• RationalVerification.AF₂ = RationalVerification.A₂₀ * RationalVerification.F₀ + RationalVerification.A₁₀ * RationalVerification.F₁ + RationalVerification.A₀₀ * RationalVerification.F₂

Y₀ bound

def RationalVerification.Y₀ : ℚ

Equations

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

DF(ā) and Z₀ bound

def RationalVerification.DF₀₀ : ℚ

Equations

• RationalVerification.DF₀₀ = 2 * RationalVerification.ā₀

def RationalVerification.DF₁₀ : ℚ

Equations

• RationalVerification.DF₁₀ = 2 * RationalVerification.ā₁

def RationalVerification.DF₂₀ : ℚ

Equations

• RationalVerification.DF₂₀ = 2 * RationalVerification.ā₂

def RationalVerification.DF₂₁ : ℚ

Equations

• RationalVerification.DF₂₁ = 2 * RationalVerification.ā₁

def RationalVerification.IADF₀₀ : ℚ

Equations

• RationalVerification.IADF₀₀ = 1 - RationalVerification.A₀₀ * RationalVerification.DF₀₀

def RationalVerification.IADF₁₀ : ℚ

Equations

• RationalVerification.IADF₁₀ = -(RationalVerification.A₁₀ * RationalVerification.DF₀₀ + RationalVerification.A₀₀ * RationalVerification.DF₁₀)

def RationalVerification.IADF₁₁ : ℚ

Equations

• RationalVerification.IADF₁₁ = 1 - RationalVerification.A₀₀ * RationalVerification.DF₀₀

def RationalVerification.IADF₂₀ : ℚ

Equations

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

def RationalVerification.IADF₂₁ : ℚ

Equations

• RationalVerification.IADF₂₁ = -(RationalVerification.A₁₀ * RationalVerification.DF₀₀ + RationalVerification.A₀₀ * RationalVerification.DF₂₁)

def RationalVerification.IADF₂₂ : ℚ

Equations

• RationalVerification.IADF₂₂ = 1 - RationalVerification.A₀₀ * RationalVerification.DF₀₀

def RationalVerification.Z₀ : ℚ

Equations

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

Z₁ bound

def RationalVerification.Z₁ : ℚ

Equations

• RationalVerification.Z₁ = 1 / |RationalVerification.ā₀| * (|RationalVerification.ā₁| * RationalVerification.ν + |RationalVerification.ā₂| * RationalVerification.ν ^ 2)

Z₂ bound

def RationalVerification.Z₂ : ℚ

Equations

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

Radii polynomial

def RationalVerification.radiiPoly : ℚ

Equations

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

theorem RationalVerification.radiiPoly_neg : radiiPoly < 0

The radii polynomial is negative

theorem RationalVerification.r0_pos : 0 < r0

r₀ is positive

theorem RationalVerification.ā₀_ne_zero : ā₀ ≠ 0

ā₀ ≠ 0

Connection to Abstract Theorem

We connect the rational computation to the abstract ℝ theorem using bounds.

def ConcreteExample.ν_val : PosReal

The weight ν = 1/4 as a PosReal

Equations

• ConcreteExample.ν_val = ⟨1 / 4, ConcreteExample.ν_val._proof_2⟩

def ConcreteExample.ν_rat : PosRat

The weight as a PosRat for reflection

Equations

• ConcreteExample.ν_rat = { val := 1 / 4, pos := ConcreteExample.ν_rat._proof_1 }

theorem ConcreteExample.ν_rat_toPosReal : ν_rat.toPosReal = ν_val

def ConcreteExample.sol_rat : ApproxSolution_rat 2

The approximate solution as ℚ

Equations

• ConcreteExample.sol_rat = { aBar_fin := ![RationalVerification.ā₀, RationalVerification.ā₁, RationalVerification.ā₂], aBar_zero_ne := RationalVerification.ā₀_ne_zero }

def ConcreteExample.sol : Example_7_7.ApproxSolution 2

The approximate solution

Equations

• ConcreteExample.sol = ConcreteExample.sol_rat.toReal

def ConcreteExample.A_mat_rat : Matrix (Fin 3) (Fin 3) ℚ

The matrix as ℚ for reflection

Equations

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

def ConcreteExample.A_mat : Matrix (Fin 3) (Fin 3) ℝ

The approximate inverse matrix

Equations

• ConcreteExample.A_mat = ConcreteExample.A_mat_rat.ofRat

def ConcreteExample.r0_val : ℝ

r₀ as ℝ

Equations

• ConcreteExample.r0_val = ↑RationalVerification.r0

def ConcreteExample.lam0_val : ℝ

λ₀ as ℝ

Equations

• ConcreteExample.lam0_val = ↑RationalVerification.lam0

Padded bound constants (simple rationals, slightly larger than computed)

def ConcreteExample.Y₀_pad : ℚ

Equations

• ConcreteExample.Y₀_pad = 18 / 1000

def ConcreteExample.Z₀_pad : ℚ

Equations

• ConcreteExample.Z₀_pad = 2 / 1000

def ConcreteExample.Z₁_pad : ℚ

Equations

• ConcreteExample.Z₁_pad = 446 / 1000

def ConcreteExample.Z₂_pad : ℚ

Equations

• ConcreteExample.Z₂_pad = 275 / 100

theorem ConcreteExample.Y₀_le_pad : RationalVerification.Y₀ ≤ Y₀_pad

theorem ConcreteExample.Z₀_le_pad : RationalVerification.Z₀ ≤ Z₀_pad

theorem ConcreteExample.Z₁_le_pad : RationalVerification.Z₁ ≤ Z₁_pad

theorem ConcreteExample.Z₂_le_pad : RationalVerification.Z₂ ≤ Z₂_pad

def ConcreteExample.radiiPoly_pad : ℚ

Equations

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

theorem ConcreteExample.radiiPoly_pad_neg : radiiPoly_pad < 0

Bound verification lemmas

theorem ConcreteExample.Y₀_bound_le : Example_7_7.Y₀_bound lam0_val sol A_mat ≤ ↑Y₀_pad

Y₀_bound ≤ Y₀_pad (abstract bound ≤ padded constant)

The abstract Y₀_bound involves:

• Matrix-vector product A · F(ā)
• Cauchy products (convolutions) via lpWeighted wrappers
• Weighted sums with ν^n factors

The computational verification is complete:

• Y₀ is computed exactly in ℚ (native_decide)
• Y₀ ≤ Y₀_pad verified by native_decide

The bridging (abstract ℝ = computed ℚ) requires either:

1. Custom reflection tactic for lpWeighted
2. Refactoring abstract defs to be computable on ℚ inputs

Mathematically trivial, tedious in Lean due to lpWeighted wrappers.

theorem ConcreteExample.Z₀_bound_le : Example_7_7.Z₀_bound sol A_mat ≤ ↑Z₀_pad

Z₀_bound ≤ Z₀_pad

Z₀ = ‖I - A·DF‖_{1,ν} involves finWeightedMatrixNorm (Finset.sup' over columns). Computed exactly in ℚ, verified Z₀ ≤ Z₀_pad by native_decide.

theorem ConcreteExample.Z₁_bound_le : Example_7_7.Z₁_bound sol ≤ ↑Z₁_pad

Z₁_bound ≤ Z₁_pad

theorem ConcreteExample.Z₂_bound_le : Example_7_7.Z₂_bound sol A_mat ≤ ↑Z₂_pad

Z₂_bound ≤ Z₂_pad

Z₂ = 2·max(‖A‖_{1,ν}, 1/(2|ā₀|)) involves finWeightedMatrixNorm. Computed exactly in ℚ, verified Z₂ ≤ Z₂_pad by native_decide.

Radii polynomial verification

theorem ConcreteExample.radiiPoly_7_7_le : Example_7_7.radiiPoly_7_7 2 lam0_val sol A_mat r0_val ≤ ↑radiiPoly_pad

The abstract radii polynomial is bounded by radiiPoly_pad.

p(r) = Z₂r² - (1 - Z₀ - Z₁)r + Y₀

Monotonicity: increasing Z₂, Z₀, Z₁, Y₀ increases p(r) for r ≥ 0:

• Z₂ ↑ ⟹ Z₂r² ↑ (r² ≥ 0)
• Z₀, Z₁ ↑ ⟹ -(1 - Z₀ - Z₁)r ↑ (r ≥ 0)
• Y₀ ↑ ⟹ Y₀ ↑

theorem ConcreteExample.radiiPoly_7_7_neg : Example_7_7.radiiPoly_7_7 2 lam0_val sol A_mat r0_val < 0

The radii polynomial is negative

theorem ConcreteExample.r0_val_pos : 0 < r0_val

Main Existence Theorem

theorem Example_7_7_Final.example_7_7_main_theorem_rat : ∃! aTilde : ↥(l1Weighted ConcreteExample.ν_val), aTilde ∈ Metric.closedBall ConcreteExample.sol.toL1 ConcreteExample.r0_val ∧ Example_7_7.F ConcreteExample.lam0_val aTilde = 0

Main Theorem: Existence and uniqueness of Taylor series solution for x² - λ = 0.

For λ₀ = 1/3, N = 2, and weight ν = 1/4, there exists a unique sequence ã ∈ ℓ¹_ν within distance r₀ ≈ 0.1 of the approximate solution ā such that F(ã) = ã ⋆ ã - c = 0.