hex

13.4. What the fields say🔗

The three propositional fields are the isolation contract, stated in aeval form so they read uniformly across the coefficient rings. Project unique_root at an index for the existence-and-uniqueness statement of that interval; simp [x4roots] computes the interval endpoints to their literal values, turning it into a self-contained theorem about x⁴ − 2:

open Hex Polynomial /-- One real root of `x⁴ − 2` in `(0, 4]`. -/ theorem root_pos : ∃! x : ℝ, x ^ 4 - 2 = 0 ∧ (0 : ℝ) < x ∧ x ≤ 4 := ⊢ ∃! x, x ^ 4 - 2 = 0 ∧ 0 < x ∧ x ≤ 4 All goals completed! 🐙

The covers field runs the other way: every real root lies in one of the intervals, so listing them is a complete case analysis of the roots. Here it proves that x⁴ − 2 has no real root outside the two intervals:

open Hex Polynomial theorem roots_complete (x : ℝ) (hx : x ^ 4 - 2 = 0) : (-4 < x ∧ x ≤ 0) ∨ (0 < x ∧ x ≤ 4) := x:ℝhx:x ^ 4 - 2 = 0⊢ -4 < x ∧ x ≤ 0 ∨ 0 < x ∧ x ≤ 4 x:ℝhx:x ^ 4 - 2 = 0i:Fin 2hlo:↑x4roots.intervals[i].1 < xhhi:x ≤ ↑x4roots.intervals[i].2⊢ -4 < x ∧ x ≤ 0 ∨ 0 < x ∧ x ≤ 4 x:ℝhx:x ^ 4 - 2 = 0i:Fin 2hlo:↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[i].1 < xhhi:x ≤ ↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[i].2⊢ -4 < x ∧ x ≤ 0 ∨ 0 < x ∧ x ≤ 4 x:ℝhx:x ^ 4 - 2 = 0hlo:↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨0, ⋯⟩].1 < xhhi:x ≤ ↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨0, ⋯⟩].2⊢ -4 < x ∧ x ≤ 0 ∨ 0 < x ∧ x ≤ 4x:ℝhx:x ^ 4 - 2 = 0hlo:↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨1, ⋯⟩].1 < xhhi:x ≤ ↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨1, ⋯⟩].2⊢ -4 < x ∧ x ≤ 0 ∨ 0 < x ∧ x ≤ 4 x:ℝhx:x ^ 4 - 2 = 0hlo:↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨0, ⋯⟩].1 < xhhi:x ≤ ↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨0, ⋯⟩].2⊢ -4 < x ∧ x ≤ 0 ∨ 0 < x ∧ x ≤ 4 exact .inl ⟨x:ℝhx:x ^ 4 - 2 = 0hlo:↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨0, ⋯⟩].1 < xhhi:x ≤ ↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨0, ⋯⟩].2⊢ -4 < x All goals completed! 🐙, x:ℝhx:x ^ 4 - 2 = 0hlo:↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨0, ⋯⟩].1 < xhhi:x ≤ ↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨0, ⋯⟩].2⊢ x ≤ 0 All goals completed! 🐙⟩ x:ℝhx:x ^ 4 - 2 = 0hlo:↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨1, ⋯⟩].1 < xhhi:x ≤ ↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨1, ⋯⟩].2⊢ -4 < x ∧ x ≤ 0 ∨ 0 < x ∧ x ≤ 4 exact .inr ⟨x:ℝhx:x ^ 4 - 2 = 0hlo:↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨1, ⋯⟩].1 < xhhi:x ≤ ↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨1, ⋯⟩].2⊢ 0 < x All goals completed! 🐙, x:ℝhx:x ^ 4 - 2 = 0hlo:↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨1, ⋯⟩].1 < xhhi:x ≤ ↑(IsolatedRealRoots.congrRoots x4roots._proof_2 (IsolatedRealRoots.ofCertPretty #v[{ interval := { lower := Dyadic.ofInt (-4), upper := Dyadic.ofInt 0, lt := x4roots._proof_3 }, count_one := x4roots._proof_4 }, { interval := { lower := Dyadic.ofInt 0, upper := Dyadic.ofInt 4, lt := x4roots._proof_5 }, count_one := x4roots._proof_6 }] #v[(↑(-4), ↑0), (↑0, ↑4)] x4roots._proof_9 x4roots._proof_10 x4roots._proof_11 x4roots._proof_12 x4roots._proof_13 x4roots._proof_15)).intervals[(fun i => i) ⟨1, ⋯⟩].2⊢ x ≤ 4 All goals completed! 🐙⟩

The ordered field says the intervals are sorted and pairwise disjoint. Because the intervals are half-open, this is what makes the index count n equal to the number of distinct real roots, and it gives disjointness as a one-liner:

open Hex Polynomial example : (x4roots.intervals[0]).2 ≤ (x4roots.intervals[1]).1 := ⊢ x4roots.intervals[0].2 ≤ x4roots.intervals[1].1 simpa using x4roots.ordered 0 1 (⊢ 0 < 1 All goals completed! 🐙)

The whole structure unpacks with obtain, so the fields can be named and fed to later tactics however a proof needs them:

open Hex Polynomial example : True := ⊢ True ivals:Vector (ℚ × ℚ) 2uniq:∀ (i : Fin 2), ∃! x, (aeval x) (X ^ 4 - 2) = 0 ∧ ↑ivals[i].1 < x ∧ x ≤ ↑ivals[i].2cov:∀ (x : ℝ), (aeval x) (X ^ 4 - 2) = 0 → ∃ i, ↑ivals[i].1 < x ∧ x ≤ ↑ivals[i].2ord:∀ (i j : Fin 2), i < j → ivals[i].2 ≤ ivals[j].1⊢ True All goals completed! 🐙