Conceptual map
- V-02.01Legality of an implication
- V-02.02Fixed and random objects
- V-02.03Changing ranges
- V-02.04Decomposed conclusions
- V-02.05Proof validity and claim truth
1. Each implication carries domains and quantifiers
A proof audit asks which objects are fixed, which vary, where each expression is defined, and whether the conclusion uses the same quantifier order as its premise.
Write an arrow as \((A,D,Q)\Rightarrow C\): assumptions, domains, quantifiers, and conclusion. Common changes include pointwise to uniform, almost sure to everywhere, fixed index to selected index, local to global, finite horizon to infinite horizon, and equality at an interior point to equality on a boundary. The proof is complete only if every change is licensed by a theorem whose hypotheses are present.
For each proof step, record the input statements, output statement, rule or cited result, object types, exceptional set, and dependencies. A step marked “algebra” still records nonzero denominators, operator domains, and any interchange of limit, expectation, derivative, or optimization.
2. Pointwise convergence does not control moving peaks
On [0,1], define \(f_{n}(x)=n x(1-x)^{n}\). For each fixed \(x\), the sequence converges to zero: at the endpoints this is immediate, and for \(0<x<1\) the exponential decay dominates \(n\). Differentiation shows the maximum occurs at \(x_{n}=1/(n+1)\), with value
Thus pointwise convergence to zero does not imply uniform convergence or convergence of suprema to zero. At \(n=10\) and 100, the maxima are approximately 0.350494 and 0.366051.
If \(f_{n}\) converges uniformly to \(f\) on a set \(D\) and \(f_{n}(x)\le0\) for all \(x\in D\) and every \(n\), then \(f(x)\le0\) for every \(x\in D\).
Proof. If \(f(x^{*})=\delta>0\) at some point, uniform convergence gives \(\lvert f_{n}(x^{*})-f(x^{*})\rvert<\delta/2\) for all large \(n\). Then \(f_{n}(x^{*})>\delta/2\), contradicting the assumed inequality. ∎
3. Narrow the conclusion at the first unsupported arrow
Suppose a theorem claims existence, uniqueness, continuity, and identification. Its existence argument may be valid while uniqueness uses strict convexity absent at a parameter boundary. The audit should preserve existence and mark only the dependent conclusions as unsupported. A dependency graph prevents an error in one branch from invalidating unrelated results.
Fixed and random objects require the same care. A probability statement established for every predetermined index does not automatically apply to an index selected from the realized data. Conditioning can repair some arguments, but only when the conditional law and measurable selection are specified.
4. Null sets, boundaries, and interchanges need separate gates
An equality holding outside a measure-zero set supplies no value at a particular point that may lie in that set. A version, continuity argument, or one-sided limit must define the boundary value.
Division requires a nonzero denominator. Matrix inversion requires the declared square map to be bijective on its spaces. Differentiation under an integral needs domination or another interchange theorem. Expectation limits need uniform integrability or suitable domination beyond convergence in probability. Infinite-horizon conclusions need tail control. Equality constraints can reduce dimension, while active inequalities replace unconstrained gradients by tangent-cone conditions. Disconnected domains block path-integration arguments across components.
5. Implementation, exercises, and sources
Number the proof sentences, parse each into premises and conclusion, and add explicit domains. Mark theorem invocations and compare every hypothesis with the assumption ledger. Search for quantifier changes and operators with restricted domains. When a step fails, compute the smallest downstream claim set and test whether a local repair, added assumption, or narrowed conclusion closes the gap.
Download the volume verification script →Exercises
- Derive the maximizer and limit in (1).
- Give an almost-surely convergent sequence whose expectations fail to converge.
- Audit the step \(A^{-1}Ax=x\) when \(A\) is a rectangular matrix.
Partial solutions
1. Differentiate the logarithm on (0,1); the stationary condition is \(1/x-n/(1-x)=0\). 2. On (0,1), let \(X_{n}=n1\{U\le1/n\}\); it converges almost surely to zero for continuous \(U\), while its expectation is one. 3. A two-sided inverse generally does not exist; a left inverse only recovers \(x\) when \(A\) has full column rank and dimensions are compatible.
- Walter Rudin, Principles of Mathematical Analysis, chapters on sequences of functions.Pointwise and uniform convergence.
- Patrick Billingsley, Probability and Measure, sections on modes of convergence and integration.Almost-sure limits and expectation interchange.
- R. Tyrrell Rockafellar and Roger J-B Wets, Variational Analysis, sections on constrained first-order conditions.Boundary and tangent-cone arguments.
6. Audit checkpoint
Object types, domains, quantifier order, fixed versus selected indices, exceptional sets, boundary values, denominator and inverse conditions, convergence mode, domination or uniform integrability, derivative and expectation interchanges, active constraints, connected components, time horizon, terminal condition, and the exact downstream claims depending on each arrow.
7. Scope boundary
The chapter presents manual proof-audit methods. Machine-checked type theory and formalization in theorem provers require separate syntax and libraries.