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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-bisection-method/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-bisection-method-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

\text{bisection with supplied sign data}

After

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

Conditions: none

Rule: mko_bisect · Uses: G1, G2, G3, mko_bisect

Leaf basis: mko_bisect + def_intro

Fix the algorithm and its input data. By the MKO, each step chooses a half using only the explicit endpoint and midpoint signs; this is merely a bracket-data update. The guide keeps two things apart: S02 to S12 concern the algorithm itself (trace, invariant, width, termination), and only S13 and S14 address whether a root exists.



S02 · impliesBefore

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

After

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

Conditions: none

Rule: and_intro_elim · Uses: G1, G3

Leaf basis: and_intro_elim + numeric_evaluation

A valid input needs two things: an ordered interval (1<2) and opposite endpoint signs (− and +). Both are supplied by G1. Cross-check: f(1)=1−2=−1<0 and f(2)=4−2=2>0 (N1, N2), agreeing with the supplied signs. Equal endpoint signs violate this algorithm's opposite-sign input contract, so its proved invariant update cannot be used directly. This does not rule out finding an opposite-sign subinterval after obtaining a new midpoint sign.



S03 · impliesBefore

[a_0,b_0]=[1,2]

After

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

Conditions: a_0<b_0

Rule: L_mid · Uses: S02, G3

Leaf basis: L_mid + numeric_evaluation

Step 1 takes the midpoint m1=(1+2)/2=3/2. By Lemma L_mid the midpoint lies strictly between the ends, and the two halves [1,3/2] and [3/2,2] have equal width 1/2.



S04 · impliesBefore

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

After

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

Conditions: s(m)\neq 0

Rule: L_half · Uses: G3, case_analysis

Leaf basis: case_analysis + and_intro_elim

Prove Lemma L_half: as long as the midpoint sign is not 0, the signs determine uniquely which half to keep. This makes 'keep the half with opposite endpoint signs' well defined at every step. Three sub-steps: two cases, plus the check that the cases cover every possibility.



S05 · impliesBefore

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

After

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

Conditions: s(\tfrac{3}{2})\neq 0

Rule: L_half · Uses: S03, S04, G2

Leaf basis: L_half + numeric_evaluation

The supplied sign is s(3/2)=+=s(2), so by S04.2 keep [1,3/2], whose endpoint signs are − and +. Cross-check: f(3/2)=9/4−2=1/4>0 (N4).



S06 · impliesBefore

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

After

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

Conditions: s(\tfrac{5}{4})\neq 0

Rule: L_half · Uses: S05, S04, G2, L_mid

Leaf basis: L_half + L_mid + numeric_evaluation

m2=(1+3/2)/2=5/4 (N5). The supplied sign is s(5/4)=−=s(1), so by S04.1 keep [5/4,3/2]. Cross-check: f(5/4)=25/16−2=−7/16<0 (N6).



S07 · impliesBefore

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

After

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

Conditions: s(\tfrac{11}{8})\neq 0

Rule: L_half · Uses: S06, S04, G2, L_mid

Leaf basis: L_half + L_mid + numeric_evaluation

m3=(5/4+3/2)/2=11/8 (N7). The supplied sign is s(11/8)=−=s(5/4), so keep [11/8,3/2]. Cross-check: f(11/8)=121/64−2=−7/64<0 (N8).



S08 · impliesBefore

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

After

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

Conditions: s(\tfrac{23}{16})\neq 0

Rule: L_half · Uses: S07, S04, G2, L_mid

Leaf basis: L_half + L_mid + numeric_evaluation

m4=(11/8+3/2)/2=23/16 (N9). The supplied sign is s(23/16)=+=s(3/2), so keep [11/8,23/16]. Cross-check: f(23/16)=529/256−2=17/256>0 (N10). No step observed f(m)=0, so there was no early stop; by G3 the run ends after step 4.



S09 · impliesBefore

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

After

\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)

Conditions: none

Rule: nat_induction · Uses: S02, S03.1, S04, nat_induction

Leaf basis: nat_induction + L_mid + L_half

Invariant I(n): a_n<b_n, s(a_n)=− and s(b_n)=+. The base I(0) holds by S02. Induction step: if I(n) holds and s(m)≠0, the new interval is [a_n,m] or [m,b_n]; L_mid gives a_n<m<b_n, so the new interval is still ordered and lies inside the old one; in both cases of L_half the kept half has sign − at its left end and + at its right end (in S04.1 the new left end m has the sign − of a_n; in S04.2 the new right end m has the sign + of b_n). So I(n+1) holds. The trace S05 to S08 agrees with this invariant.



S10 · impliesBefore

w_0=b_0-a_0=1

After

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

Conditions: \text{no early stop}

Rule: L_width · Uses: S03.1, S09

Leaf basis: nat_induction + L_mid + power_laws

Prove Lemma L_width: each effective halving halves the width, so after n steps the width is w0/2^n. This is a purely geometric fact, independent of f. Two sub-steps form the induction.



S11 · impliesBefore

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

After

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

Conditions: none

Rule: L_mid · Uses: S08, S10

Leaf basis: L_mid + abs_rules + numeric_evaluation

The final bracket has width 1/16. Its midpoint is m5=(11/8+23/16)/2=45/32 (N16); by L_mid every point of the bracket is within (1/16)/2=1/32 of m5. This is a statement about interval geometry, about any point that lies in the bracket; it does not say that such a root exists.



S12 · impliesBefore

\tau>0

After

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

Conditions: \tau>0

Rule: archimedean · Uses: S10, archimedean, nat_induction

Leaf basis: archimedean + nat_induction + order_basics

Width index: provided every requested midpoint sign is available and updates can be performed effectively, with early stopping when a zero is observed, the rule 'stop when the width is ≤τ' terminates after finitely many steps for every τ>0. This is a conditional statement about an extended run; the exercise actually supplies only four midpoint signs. First, 2^n≥n+1 by induction: for n=0, 1≥1; if 2^n≥n+1, then 2^(n+1)=2·2^n≥2n+2≥n+2. Then by the Archimedean property choose a natural number N>1/τ, so 2^N≥N+1>1/τ and w_N=1/2^N<τ. N14 is a finite check for n=0 to 20; the proof itself is the induction above.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: case_analysis · Uses: G1, G2, S05, S06, S07, S08

Leaf basis: case_analysis + numeric_evaluation + exists_intro

Sign data alone do not prove a root. Take the step function g with g(x)=−1 for x<7/5 and g(x)=1 for x≥7/5. Compare 1, 2, 3/2, 5/4, 11/8 and 23/16 with 7/5: 1<7/5, 5/4<7/5 and 11/8<7/5, while the others are ≥7/5 (N17 to N20). So g has exactly the signs of G1 and G2 at these six points and the four steps produce exactly the same brackets, yet g takes only the values −1 and 1 and has no root. The algorithm sees only signs and cannot tell f from g; hence nothing in S02 to S12 by itself yields a root.



S14 · theorem_applicationBefore

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})

After

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

Conditions: f\ \text{continuous on}\ [a_4,b_4]; f(a_4)<0<f(b_4)

Rule: ivt · Uses: G4, poly_continuous, ivt, S07, S08, S11

Leaf basis: ivt + poly_continuous + numeric_evaluation

This is the separate proof obligation for root existence. f is a polynomial and continuous on [11/8,23/16] (G4); exact evaluation gives the endpoint values f(11/8)=−7/64<0 and f(23/16)=17/256>0 (N8, N10). Both hypotheses of the intermediate value theorem (cited, citation_verified) hold, so some c∈[11/8,23/16] has f(c)=0; and by S11, |c−45/32|≤1/32. This c is √2, though the guide does not need that name.



S15 · impliesBefore

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

After

[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}

Conditions: none

Rule: and_intro_elim · Uses: S08, S09, S10, S12, S13, S14

Leaf basis: and_intro_elim

Summary: the four-step trace gives [11/8,23/16] (S08), the invariant keeps opposite endpoint signs (S09), the width is 1/16 (S10), and a width rule always terminates (S12); all of these are properties of bracket data only (S13). That the interval contains a root is a different conclusion, coming from continuity and the intermediate value theorem (S14).







## Substeps and lemmas

S03.1 · impliesBefore

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

After

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

Conditions: a<b

Rule: order_basics · Uses: order_basics, frac_rules

Leaf basis: order_basics + frac_rules + distributive

m−a=(a+b)/2−2a/2=(b−a)/2 and b−m=2b/2−(a+b)/2=(b−a)/2 (N12 and N13 are degree-one polynomial identities). From a<b we get b−a>0, and multiplying by the positive number 1/2 keeps it positive, so m−a>0 and b−m>0, that is a<m<b. This proves Lemma L_mid.



S04.1 · impliesBefore

s(m)=s(a)

After

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

Conditions: s(a)\neq s(b)

Rule: def_unfold · Uses: G3

Leaf basis: def_unfold + eq_refl_symm_trans

If s(m)=s(a), then [a,m] has equal endpoint signs and cannot be kept; [m,b] has endpoint signs s(m)=s(a) and s(b), and s(a)≠s(b), so they are opposite and [m,b] is kept.



S04.2 · impliesBefore

s(m)=s(b)

After

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

Conditions: s(a)\neq s(b)

Rule: def_unfold · Uses: G3

Leaf basis: def_unfold + eq_refl_symm_trans

If s(m)=s(b), symmetrically [m,b] has equal signs, while [a,m] has endpoint signs s(a) and s(m)=s(b), which are opposite, so [a,m] is kept.



S04.3 · case_splitBefore

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

After

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

Conditions: s(m)\neq 0

Rule: case_analysis · Uses: S04.1, S04.2, case_analysis

Leaf basis: case_analysis + and_intro_elim

When s(m)≠0 it is either − or +; exactly one of s(a), s(b) is − and the other +, so s(m) equals exactly one of them. The two cases are exclusive and exhaustive, and with S04.1 and S04.2 exactly one half is kept. S04.1 to S04.3 prove Lemma L_half. If s(m)=0, the algorithm stops at m by G3 and this lemma is not used.



S10.1 · induction_baseBefore

n=0

After

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

Conditions: none

Rule: nat_induction · Uses: G1

Leaf basis: nat_induction + power_laws

Base: 2^0=1, so w0/2^0=w0.



S10.2 · induction_stepBefore

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

After

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

Conditions: \text{no early stop}

Rule: nat_induction · Uses: S10.1, S03.1, S04

Leaf basis: nat_induction + frac_rules + power_laws

The new interval is [a_n,m] or [m,b_n], and by S03.1 both have width (b_n−a_n)/2=w_n/2. With the induction hypothesis, w_(n+1)=w0/(2^n·2)=w0/2^(n+1). By induction this proves Lemma L_width. With w0=1 and n=4, w4=1/16, matching 23/16−11/8=1/16 (N11).







## 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 existsOne 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 errorThe 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 signsThe 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-bisection-method-01.json)