dm³ 103 · Week 4 — Milestone V — Mechanising Σ Numerically

dm³ 103 · Week 04 · Milestone

Milestone V — Mechanising Σ Numerically

Course: dm³ 103 · Milestone · Source: Numerical methods + Lean interval arithmetic

Since \(\Sigma\) has no closed radical form, a Lean proof about it can’t simply rfl or ring its way to a value the way Theorem C.1 did with \(c^*=3\). What’s provable instead: existence and uniqueness of a real root in a bracketing interval, via the intermediate value theorem, plus a numerical bound tight enough to be useful — e.g. \(1.965<\Sigma<1.967\), provably, using interval arithmetic rather than an approximate floating-point claim.

Milestone task

Evaluate \(f(x)=x^5-x^4-x^3-x^2-x-1\) at \(x=1.965\) and \(x=1.967\) by hand, confirm a sign change (IVT gives existence), and confirm \(f\) is strictly increasing on this interval (derivative positivity gives uniqueness there). Write the bracketing argument as a real proof sketch, then compare it structurally to Cardano’s exact-value derivation from 102 — both are legitimate proofs of different kinds of claims (interval containment vs. exact closed form) about roots of polynomials.

This week’s content is grounded directly in the AXLE/Book 3/5 sources cited above — no material in this page depends on the external, unverified source removed from dm³ 102.

-- dm³ 103 · Week 04 · Milestone V — Σ via bracketing, not radicals

def f (x : ℝ) : ℝ := x^5 - x^4 - x^3 - x^2 - x - 1

-- Milestone: confirm f(1.965) < 0 < f(1.967) by hand (IVT ⟹ root exists)
-- and f is strictly increasing on [1.965, 1.967] (derivative > 0 ⟹ unique)
-- Different proof SHAPE than Cardano — interval containment, not
-- closed radical form. Both are legitimate; neither is "less proved."
example : True := trivial

← Week 3 ↑ dm³ 103 Course Week 5 →