Bisection: four bracket updates, the invariant and the separate proof obligation for root existence

Goal and scope

For f(x)=x²−2, start from [1,2] with the supplied endpoint signs f(1)<0 and f(2)>0, run four bisection steps with the supplied midpoint signs and trace the brackets; prove that 'opposite endpoint signs and a<b' is an invariant, that the width after n steps is 1/2^n, and that, in an extended run with every needed sign available and effective updates, a width-based stopping rule terminates after finitely many steps; then show that the bracket data alone do not prove a root exists, and separately cite the intermediate value theorem to conclude, for the continuous f, that the final bracket contains a root.

Works inside the MKO's scope: endpoint and midpoint signs are supplied directly by the problem (assumption a1), and the algorithm only updates bracket data; the width bound w/2^n is a geometric halving result, not a proof that a root exists (assumption a2). Root existence is handled as a separate proof obligation with the cited intermediate value theorem (citation_verified) and continuity of polynomials. Floating-point error, comparisons of convergence speed and other root-finding methods are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• order_basics
• frac_rules
• power_laws
• nat_induction
• archimedean
• case_analysis
• numeric_evaluation

• G1 — f(x)=x²−2. Initial bracket [a0,b0]=[1,2], with supplied endpoint signs s(1)=− and s(2)=+.
• G2 — Supplied midpoint signs: s(3/2)=+, s(5/4)=−, s(11/8)=− and s(23/16)=+. These are data supplied by the problem (MKO assumption a1); the guide cross-checks them by exact rational evaluation of f, not by reading a graph.
• G3 — Algorithm (MKO): given [a,b] with a<b and opposite endpoint signs, take m=(a+b)/2; if f(m)=0 has been observed, stop at m; otherwise keep the half whose endpoint signs are opposite. Here four steps are run unless the algorithm stops earlier.
• G4 — For the separate root-existence step: f is a polynomial and hence continuous on ℝ.

• [a_n,b_n] — the bracket after step n
• m_n — the midpoint (a_{n-1}+b_{n-1})/2 of step n
• s(x) — the supplied sign of f(x), one of −, 0, +
• w_n=b_n-a_n — the width after step n
• \tau — the tolerance of a width-based stopping rule

Rules and sources

• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
• archimedean · prerequisite — Archimedean property: for every real x there is a natural number n>x; hence for every ε>0 there is n with 1/n<ε.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• mko_bisect · cited — Given an ordered interval [a,b] and supplied endpoint sign-bracket data, take m=(a+b)/2 at each step. If f(m)=0 has been observed, stop at m; otherwise retain the half whose endpoint signs are opposite. Without separately applying an intermediate value theorem, this is a bracket-data update and does not itself prove root existence. · mko-bisection-method
• ivt · cited — Intermediate value theorem (sign form): if f is continuous on [a,b] and f(a)<0<f(b), then there is some x∈[a,b] with f(x)=0. · OpenStax, Calculus Volume 1, Section 2.4, Intermediate Value Theorem
• poly_continuous · prerequisite — Polynomial functions are continuous everywhere on ℝ, hence on every closed interval.
• L_mid · lemma — If a<b and m=(a+b)/2, then a<m<b and m−a=b−m=(b−a)/2.
• L_half · lemma — If one of s(a), s(b) is − and the other +, and s(m)≠0, then exactly one of [a,m] and [m,b] has opposite endpoint signs.
• L_width · lemma — Without an early stop, after n effective halvings b_n−a_n=(b_0−a_0)/2^n.

Main derivation

\text{bisection with supplied sign data}

[a_0,b_0]=[1,2],\ m_{n}=\tfrac{a_{n-1}+b_{n-1}}{2}

[1,2],\ s(1)=-,\ s(2)=+

\text{valid input: } 1<2,\ \text{opposite endpoint signs}

[a_0,b_0]=[1,2]

m_1=\tfrac{1+2}{2}=\tfrac{3}{2},\ 1<\tfrac{3}{2}<2

\{s(a),s(b)\}=\{-,+\},\ s(m)\neq 0

\text{exactly one of }[a,m],\ [m,b]\ \text{has opposite endpoint signs}

[1,2],\ s(\tfrac{3}{2})=+

[a_1,b_1]=[1,\tfrac{3}{2}]

[1,\tfrac{3}{2}],\ m_2=\tfrac{5}{4},\ s(\tfrac{5}{4})=-

[a_2,b_2]=[\tfrac{5}{4},\tfrac{3}{2}]

[\tfrac{5}{4},\tfrac{3}{2}],\ m_3=\tfrac{11}{8},\ s(\tfrac{11}{8})=-

[a_3,b_3]=[\tfrac{11}{8},\tfrac{3}{2}]

[\tfrac{11}{8},\tfrac{3}{2}],\ m_4=\tfrac{23}{16},\ s(\tfrac{23}{16})=+

[a_4,b_4]=[\tfrac{11}{8},\tfrac{23}{16}]

a_0<b_0,\ s(a_0)=-,\ s(b_0)=+

\forall n\le 4:\ a_n<b_n,\ s(a_n)=-,\ s(b_n)=+,\ [a_{n}, b_{n}]\subseteq[a_{n-1},b_{n-1}]\ (n\geq 1)

w_0=b_0-a_0=1

w_n=\tfrac{1}{2^n}

[a_4,b_4]=[\tfrac{11}{8},\tfrac{23}{16}]

w_4=\tfrac{1}{16},\ m_5=\tfrac{45}{32},\ |x-m_5|\le\tfrac{1}{32}\ \ \forall x\in[a_4,b_4]

\tau>0

\exists N:\ \tfrac{1}{2^N}<\tau

g(x)=\begin{cases}-1 & x<\tfrac{7}{5}\\ 1 & x\ge\tfrac{7}{5}\end{cases}

g\ \text{gives the same signs and brackets, and}\ g(x)\neq 0\ \forall x

f\ \text{continuous on}\ [\tfrac{11}{8},\tfrac{23}{16}],\ f(\tfrac{11}{8})=-\tfrac{7}{64}<0<\tfrac{17}{256}=f(\tfrac{23}{16})

\exists c\in[\tfrac{11}{8},\tfrac{23}{16}]:\ f(c)=0,\ |c-\tfrac{45}{32}|\le\tfrac{1}{32}

\text{trace, invariant, width, termination, root duty}

[a_4,b_4]=[\tfrac{11}{8},\tfrac{23}{16}],\ w_4=\tfrac{1}{16},\ \text{root in}\ [a_4,b_4]\ \text{only via IVT}

Substeps and lemmas

a<b,\ m=\tfrac{a+b}{2}

m-a=b-m=\tfrac{b-a}{2}>0

s(m)=s(a)

[a,m]\ \text{same signs},\ [m,b]\ \text{opposite signs}

s(m)=s(b)

[a,m]\ \text{opposite signs},\ [m,b]\ \text{same signs}

s(m)\in\{-,+\},\ \{s(a),s(b)\}=\{-,+\}

s(m)=s(a)\ \veebar\ s(m)=s(b)

n=0

w_0=\tfrac{w_0}{2^0}

w_n=\tfrac{w_0}{2^n}

w_{n+1}=\tfrac{w_n}{2}=\tfrac{w_0}{2^{n+1}}

Reverse audits

• S15 · sufficient_goal_reduction · S08, S09, S10, S12, S13, S14 — Goal G: the trace result, invariant, width, termination and the root conclusion. Sufficient condition H: S08, S09, S10, S12 and S14 each hold, with S13 marking which conclusions cannot come from the data alone. H is derived forwards from the data, the lemmas and the cited theorem; G is never used as a premise.
• S14 · premise_audit · ivt, poly_continuous, G4, S11 — The theorem needs continuity and actual endpoint values of strictly opposite sign; both are supplied separately here rather than by the bracket updates. The g of S13 lacks continuity, so the same argument cannot be made for g.
• S13 · premise_audit · case_analysis, numeric_evaluation — One function with the same data and no root suffices to show that the data do not imply a root; g is discontinuous at 7/5, which is exactly what the hypothesis of the intermediate value theorem excludes.
• S12 · premise_audit · archimedean, nat_induction, S10 — It needs τ>0; with τ=0 the width never becomes ≤0 and the rule never fires. This is termination of the algorithm, not existence of a root.
• S11 · premise_audit · L_mid, S10 — Only the midpoint and the width are used; before the distance bound can be applied to a root, the root must separately be shown to lie in the interval.
• S10.2 · premise_audit · S03.1, power_laws, frac_rules — Both choices have the same width, so it does not matter which half was chosen.
• S10.1 · premise_audit · power_laws — Only a^0=1 is used.
• S10 · premise_audit · L_width, S03.1 — Only the position of the midpoint is needed; it is not claimed that the width bound is an error bound for a root (that needs a root actually in the interval, see S14).
• S09 · premise_audit · S02, L_mid, L_half, nat_induction — The induction step needs s(m)≠0; if s(m)=0 is observed, the algorithm stops and the invariant need not be extended. The invariant describes only sign data and interval positions; it does not include 'the interval contains a root'.
• S08 · premise_audit · L_half, L_mid, G2 — As in S06; the run ends because the step count fixed in G3 is reached.
• S07 · premise_audit · L_half, L_mid, G2 — As in S06.
• S06 · premise_audit · L_half, L_mid, G2 — As in S05: the midpoint is placed by L_mid and the half chosen by L_half.
• S05 · premise_audit · L_half, G2 — Only the supplied midpoint sign and the lemma are used; the exact value of f is a cross-check.
• S04.3 · premise_audit · case_analysis, S04.1, S04.2 — Proof by cases needs exhaustive cases; here the two cases exhaust the nonzero values of s(m).
• S04.2 · premise_audit · G3, def_unfold — Symmetric to S04.1.
• S04.1 · premise_audit · G3, def_unfold — Only transitivity of equal signs and s(a)≠s(b) are used.
• S04 · premise_audit · L_half, case_analysis — The lemma uses only sign data, not continuity of f or any function value; for the same reason it cannot yield the existence of a root.
• S03.1 · premise_audit · order_basics, frac_rules — It needs a<b; if a=b the midpoint equals the endpoints and there are no longer two nondegenerate halves.
• S03 · premise_audit · L_mid, S02 — It needs a0<b0 (S02); the lemma is proved in S03.1.
• S02 · premise_audit · G1, and_intro_elim — Validity is a conjunction of two conditions; the exact evaluation is only a cross-check, and the algorithm uses the supplied signs.
• S01 · premise_audit · G1, G2, G3, mko_bisect — This step only states the algorithm and the data and derives no new fact.

Error controls and negative controls

Opposite signs alone do not prove a root exists

One mistake named by the MKO is to skip the intermediate value theorem and declare a root on seeing opposite signs. The step function g of S13 has the same signs as f at every point used and produces the same brackets, yet has no root. A root needs continuity plus the intermediate value theorem (S14), a proof obligation separate from the bracket updates.

Width is not function-value error

The other mistake named by the MKO. The final width 1/16 bounds only distances in the x-direction (and only once the root is known to lie in the interval). The function h(x)=100(x²−2) has exactly the same signs and brackets, but h(11/8)=−175/16, about 10.9 in absolute value (N15), far larger than 1/16. The width bound and the size of |f(x)| are different things.

Choose the half by endpoint signs

The step most easily done wrong is keeping the wrong half: when s(m) equals s(a), keep [m,b], not [a,m] (S04.1). The check is whether the kept interval has one negative and one positive end; the invariant of S09 requires − at the left end and + at the right.

• f(1)<0<f(2), so the bisection method itself proves that [1,2] contains a root → reject — The step function g has the same endpoint and midpoint signs and no root (S13); a root needs continuity and the intermediate value theorem separately.
• The final bracket width 1/16 alone guarantees |h(45/32)|≤1/16 for every function h giving the same sign data. → reject — Width controls distances in x, not function values in general. Take h(x)=100(x²−2), which gives the same signs and brackets but at the same midpoint has |h(45/32)|=575/256>1/16. The original f happens to satisfy |f(45/32)|=23/1024≤1/16; that numerical fact is not guaranteed by width alone.
• s(3/2)=+, so keep [3/2,2] → reject — Both ends of [3/2,2] are +; the half with opposite signs is [1,3/2] (S05).
• Starting from [1,2] with supplied signs s(1)=+ and s(2)=+, bisection can still proceed normally → reject — Equal endpoint signs violate this algorithm's opposite-sign input contract (S02), so the bracket invariant cannot be invoked directly. This does not claim that no opposite-sign subinterval could be found with additional sign information.

Result and limitations

Starting from [1,2] with the supplied signs +, −, −, +, four bisection steps give the brackets [1,3/2], [5/4,3/2], [11/8,3/2] and [11/8,23/16], of width 1/16=1/2⁴; opposite endpoint signs form an invariant, and a width rule terminates for every τ>0. These bracket data alone do not prove a root (the step function g gives the same data and has no root); separately, continuity of polynomials and the intermediate value theorem show that f(x)=x²−2 has a root c in [11/8,23/16], with |c−45/32|≤1/32.

• The intermediate value theorem is used by citation (citation_verified) and not proved here; continuity of polynomials is a prerequisite.
• N14 is a finite check for n=0 to 20; the proof that 2^n≥n+1 for all n is the induction in S12; N12 and N13 are grid checks of degree-one polynomial identities.

Verification and source binding

21 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: fc6815b2e34c1a498109d7c25fa634c56e668faddafc9d05c16b74cc9206e49d
• original source SHA-256: 6785e2b4757cf8bcdb04bf8c2e24e02150a9f5d955df275d9ba4228ece867aaa
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)