# A polynomial bracket and an exact intermediate value

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

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-intermediate-value-theorem-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Find value zero for f(x)=x^2-1 on [0,2], retaining endpoint and nonuniqueness boundaries.

A full polynomial certificate and exact witness, not a finite-bisection convergence claim.





## Givens and symbols


- algebra
- polynomial
- IVT


- G1 — f(x)=x^2-1, a=0,b=2, target y=0.


- y — target value
- c — witness allowing endpoints





## Rules and sources


- mko_definition · cited — Fix a<b, the entire interval domain and a continuous polynomial certificate. The target y must lie inclusively between f(a) and f(b), in either orientation. Exact families supply c∈[a,b] with f(c)=y and retain endpoint roots. IVT gives existence, not uniqueness, a rational closed form or convergence of finitely many bisection steps. An explicit discontinuous step can change sign without taking the target value, and finite samples do not prove continuity. · mko-intermediate-value-theorem
- algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities.
- polynomial · prerequisite — Real polynomials are continuous and differentiate termwise: the derivative of x^k is k*x^(k-1), and constants differentiate to zero.
- IVT · prerequisite — If a<b and f is continuous throughout [a,b], every y between its endpoint values inclusively and in either orientation equals f(c) for some c in [a,b].





## Main derivation

S01 · impliesBefore

a=0,\ b=2

After

a<b,\quad[a,b]=[0,2]\text{ is the full domain interval}

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

Fix the whole closed interval rather than substituting a discrete point set.



S02 · impliesBefore

f(x)=x^2-1

After

f\text{ continuous at every point of }[0,2]

Conditions: none

Rule: polynomial · Uses: G1, S01

Leaf basis: polynomial

The complete polynomial guarantees continuity on the whole closed interval, not apparent smoothness of samples.



S03 · impliesBefore

f(0)=0^2-1,\quad f(2)=2^2-1

After

f(0)=-1\le0\le3=f(2)

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

Exactly verify the target lies between the endpoint values.



S04 · theorem_applicationBefore

f\text{ continuous on }[0,2],\quad-1\le0\le3

After

\exists c\in[0,2]:f(c)=0

Conditions: none

Rule: IVT · Uses: S01, S02, S03

Leaf basis: IVT

The explicitly qualified IVT gives existence only, not uniqueness or a rational formula.



S05 · impliesBefore

c=1

After

0<1<2,\quad f(1)=1^2-1=0

Conditions: none

Rule: algebra · Uses: G1, S04

Leaf basis: algebra

This polynomial additionally has an exact rational witness, with interval membership and equality checked independently.



S06 · impliesBefore

[a,b]=[1,2],\quad y=0

After

c=a=1\text{ is a valid endpoint witness}

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

IVT permits c at an endpoint, unlike the strict-interior MVT obligation.



S07 · impliesBefore

g(x)=x^3-x\text{ on }[-2,2]

After

g(-2)=-6,\ g(2)=6,\quad g(-1)=g(0)=g(1)=0

Conditions: none

Rule: polynomial · Uses: G1

Leaf basis: polynomial

Another continuous bracketed example has three distinct roots, protecting the nonuniqueness boundary.



S08 · impliesBefore

s(x)=\begin{cases}-1&x<0\\1&x\ge0\end{cases}\quad\text{on }[-1,1]

After

s(-1)<0<s(1),\quad0\notin s([-1,1])

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

A discontinuous jump changes sign without taking zero, so continuity cannot be omitted.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1 — Continuity fails at zero, while the endpoint bracket itself genuinely holds.
- S07 · premise_audit · G1 — This does not assert three roots for the original f on [0,2]; the examples are distinct.
- S06 · premise_audit · G1 — The separate branch still satisfies a<b and f(1)=y.
- S05 · premise_audit · G1, S04 — One rational root does not give rational formulas for every IVT problem.
- S04 · premise_audit · S01, S02, S03 — Every premise is supplied; endpoint sign change alone does not give the conclusion.
- S03 · premise_audit · G1 — Bracketing is inclusive, allowing endpoint equality.
- S02 · premise_audit · G1, S01 — The universal range of continuity is explicit.
- S01 · premise_audit · G1 — The degenerate a=b case is outside this application.





## Error controls and negative controls

Separate premisesCheck the full interval, continuity and bracket separately.

Finite algorithmsFinite bisection gives a bracket or approximation, not automatically an infinite convergence proof.


- Sign change gives a root even without continuity. → reject — The jump at S08 never takes zero.
- An IVT witness must lie strictly inside. → reject — The endpoint at S06 already equals the target.
- Existence guarantees uniqueness. → reject — The three roots at S07 refute it.





## Result and limitations

The main witness is c=1; IVT guarantees existence only, permits endpoints and need not give uniqueness.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 374944ef5526713f1c77728586ee43f3af567de157b811fc6e0370d3635c1ff7
- original source SHA-256: 374944ef5526713f1c77728586ee43f3af567de157b811fc6e0370d3635c1ff7
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-intermediate-value-theorem-01.json)