# Radius, endpoints and complete coefficient laws

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-power-series-radius-of-convergence/)

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-power-series-radius-of-convergence-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Find R for geometric coefficients 2^n, and exhibit endpoint and zero/infinity boundaries.

A radius certificate uses a full coefficient law; a finite prefix is insufficient.





## Givens and symbols


- algebra
- epsilon
- geom
- harmonic_boundaries


- G1 — The main series is sum over n≥0 of 2^n*(x-1)^n; also consider endpoint coefficients 2^n/(n+1).


- R — radius allowing zero or infinity
- r — full geometric ratio





## Rules and sources

Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged.


- mko_definition · cited — For sum over n≥0 of a_n*(x−c)^n, R may be0, finite positive or infinity. Distance less than R gives absolute convergence and distance greater than R gives divergence; equality cannot be decided from R alone. This slice declares geometric coefficients q^n, endpoint coefficients R^(−n)/(n+1)^p, and two complete laws sharing zeros at every index 0≤n≤N before distinct scaled geometric tails. A ratio test needs its relevant limit and is not a general definition. A finite coefficient prefix cannot determine a general radius, and a bounded-real-only supremum rule must not exclude0 or infinity. · mko-power-series-radius-of-convergence
- algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities.
- epsilon · prerequisite — Convergence requires for every positive epsilon an integer N controlling every n≥N by a strict error bound; use the Archimedean property of the reals.
- geom · prerequisite — The finite geometric sum is (1-r^(N+1))/(1-r) for r≠1; for |r|<1 its remainder vanishes, while for |r|≥1 its terms do not tend to zero.
- harmonic_boundaries · prerequisite — Harmonic dyadic blocks each contribute at least 1/2 and diverge; alternating-harmonic parity partial sums bracket a common limit.





## Main derivation

S01 · equivalentBefore

2^n(x-1)^n

After

r^n,\quad r=2(x-1)

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

The full power series becomes geometric with center fixed at 1.



S02 · impliesBefore

|x-1|<1/2

After

|r|<1\Longrightarrow\sum_{n\ge0}|r|^n<\infty

Conditions: none

Rule: geom · Uses: S01

Leaf basis: geom

The finite-sum formula and vanishing remainder prove absolute convergence inside.



S03 · impliesBefore

|x-1|>1/2

After

|r|>1\Longrightarrow r^n\not\to0

Conditions: none

Rule: geom · Uses: S01

Leaf basis: geom

Outside, terms fail to vanish, so the series diverges; thus R=1/2.



S04 · impliesBefore

x=1+1/2\text{ or }1-1/2

After

r=1\text{ or }-1;\quad r^n\not\to0

Conditions: none

Rule: algebra · Uses: S01, S02, S03

Leaf basis: algebra

Both endpoints of the main geometric family diverge, separately checked by the term condition rather than radius alone.



S05 · impliesBefore

a_n=2^n/(n+1),\quad x=1\pm1/2

After

\sum1/(n+1)\text{ diverges};\quad\sum(-1)^n/(n+1)\text{ converges conditionally}

Conditions: none

Rule: harmonic_boundaries · Uses: G1

Leaf basis: harmonic_boundaries

For this same-radius law the interior is geometrically dominated and exterior ratios eventually exceed one; endpoints instead give divergence on one side and conditional convergence on the other.



S06 · impliesBefore

a_n=n!,\quad x\ne0\text{ about center }0

After

|(a_{n+1}x^{n+1})/(a_nx^n)|=(n+1)|x|\ge2\text{ eventually};\quad R=0

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

For any nonzero x, the magnitudes of successive terms eventually grow by at least a factor of 2 and cannot tend to zero; at the center only the initial term remains.



S07 · impliesBefore

a_n=1/n!,\quad x\in\mathbb R\text{ fixed}

After

|x|/(n+1)\le1/2\text{ eventually};\quad R=\infty

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

Choose an integer N>2|x|; the tail is dominated by a ratio-1/2 geometric tail, giving absolute convergence at every x.



S08 · impliesBefore

a_n=b_n=0\ (0\le n\le N);\quad a_n=2^{n-N-1},\ b_n=3^{n-N-1}\ (n>N)

After

R_a=1/2,\quad R_b=1/3\text{ despite the same finite prefix}

Conditions: none

Rule: geom · Uses: G1

Leaf basis: geom

Two full laws share the entire finite prefix but have different geometric tail rates; a finite power factor does not alter convergence away from the center.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1 — The different radii come from declared infinite tails, not guessed future coefficients.
- S07 · premise_audit · G1 — After fixing x, N may depend on x; this suffices for an infinite convergence radius.
- S06 · premise_audit · G1 — R=0 is a legitimate boundary, not excluded by a bounded-real supremum convention.
- S05 · premise_audit · G1 — The endpoints use separate harmonic and alternating certificates.
- S04 · premise_audit · S01, S02, S03 — These endpoint statuses are not extrapolated to every series with the same radius.
- S03 · premise_audit · S01 — Divergence uses the necessary term condition, not the sign of a formula's denominator.
- S02 · premise_audit · S01 — The interior uses absolute values, not positive r alone.
- S01 · inverse_equivalence · G1 — Combine the coefficient and shifted power without losing the center.





## Error controls and negative controls

Endpoints separatelyInterior/exterior rules do not settle equality; prove endpoints independently.

Whole lawThe coefficient law must cover every n.


- |x-c|=R guarantees absolute convergence. → reject — The main geometric endpoints have nonvanishing terms.
- A missing ratio limit means no convergence radius exists. → reject — For a_n=1+(-1)^n/2, adjacent ratios alternate between 1/3 and 3 and have no limit. Yet 1/2≤a_n≤3/2 gives geometric domination for |x|<1 and nonvanishing terms for |x|>1, so the radius is one.
- The first N coefficients uniquely determine radius. → reject — S08 supplies full laws with the same prefix and different radii.





## Result and limitations

The main radius is 1/2 with both endpoints divergent; endpoint behavior varies at the same radius, zero/infinity are valid, and finite prefixes do not determine R.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: b1b6d270c26519919c71c61c0d056e80a89da34835bc561d38bb1032610e97fc
- original source SHA-256: b7e224751e7201b56434d747ff1921e9b689113df97dd8d49367655f50ab91d8
- 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-power-series-radius-of-convergence-01.json)