How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Nonlinear equations and Newton methods — Examples
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Countability and Uncountability
- Determinants of Matrices over a Commutative Ring
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Metric Spaces
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Nonlinear equations and Newton methods
- Order, Zorn's Lemma, and the Axiom of Choice
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Fundamental Theorems of Calculus
- The Inverse and Implicit Function Theorems
- The Riemann Integral: Definition and Integrability
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
These computations contrast fixed-point residual stopping with nonlinear-root stopping, verify the local Newton error recurrence at a simple root, and show reduced order at a double root. They also exhibit a singular starting Jacobian outside the stated local neighborhood and calculate how a frozen inverse differs from the updated-Jacobian Newton map.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Fixed points, local Newton behavior, and failure boundaries
Example
The examples use exact arithmetic. The first is a fixed-point iteration on the complete metric space with distance . The remaining examples concern the square residual or the double-root residual .
Facts & Assumptions
Given: The fixed-point algorithm and the exact-Jacobian finite-budget Newton algorithm; the cited Banach and local Newton results; and the positive square root .
Fixed-point iteration with a residual stop and finite budget: the map is iterated from ; at each iterate the procedure checks before the finite update-budget status.
and for with the Euclidean metric are complete, componentwise from the Cauchy criterion in : with distance is complete.
A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point: a contraction of a nonempty complete metric space into itself has one fixed point, and its iterates from every starting point converge to it.
The a priori bound and the a posteriori bound : for a contraction with constant , the iterate error is bounded by .
Newton correction for a square vector residual: an invertible linear map and residual have a unique correction solving ; a noninvertible map returns the singular-jacobian status.
Finite-budget Newton for a square vector residual: an exact-Jacobian update applies the correction and sets when the trial is in .
Updated-Jacobian Newton has local quadratic convergence at a simple root: if a simple root has a Lipschitz Jacobian and a uniform local inverse bound, sufficiently close exact Newton iterates satisfy a quadratic error estimate and remain local.
Newton maps are uniform contractions near a point with invertible derivative: for a fixed , the map is a contraction on a small ball about ; this is a fixed-inverse map.
Square roots exist: a unique with ; the positives are : the positive square root exists uniquely and satisfies and .
Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric: a metric is a real-valued function satisfying separation, symmetry, and the triangle inequality.
Squaring is monotone on the nonnegatives: squaring is strictly increasing on nonnegative reals.
Verification
Given: on ; with root ; and with root .
The distance is a metric by [F11], and with it is complete by [F2]. This metric space is nonempty because , as is a field by [F11]. For all , , so is a contraction with factor . Its fixed-point equation gives , and [F3] gives convergence of the iterates from every .
The recurrence gives by induction. Hence , which tends to zero by [F5]; the finite-budget algorithm therefore meets any if allowed enough updates. For and , no finite iterate meets the test, so a finite budget returns iteration-budget-exhausted. Also [F4] gives , agreeing with the exact formula.
For , [F6] solves , so the exact Newton update in [F7] is . Direct subtraction using [F10] gives . If , then and . Thus the ball of radius is invariant and the error decreases at least linearly by a factor , with the sharper quadratic bound .
At , and the fixed-inverse map from [F9] with is . Starting at , it gives and . Updated-Jacobian Newton uses the [F6] correction at , where , and gives . Since , the fixed-inverse and updated-Jacobian maps differ; [F9] does not itself assert a Newton convergence theorem.
The start lies in the radius- ball of step 1.3 because , which follows from and [F12]. Iteration gives by [F5]. Also ; since , we have and hence , so the residual tends to zero and any positive tolerance is eventually met if the update budget is large enough.
For the double-root residual and any , [F6] and [F7] give the Newton formula , so for . Iterating gives by [F5]. Suppose a local quadratic bound held on some radius , so for every and some finite . Since , it would require for every such . If , choose ; if , choose any . Either choice contradicts the required inequality. Unlike the simple-root bound in step 1.3, , so the simple-root hypothesis in [F8] fails.
For , the start lies outside the radius- ball of step 1.3 because . At , and , so [F6] returns the singular-jacobian status before any update, despite the two exact roots .