Theory map: the object, the guarantee, and the boundary
On this page
Use this section as a retrieval aid after the corresponding teaching, not as a replacement for it. For each row, be able to give a fresh example, state the assumptions, and explain why a tempting stronger conclusion does not follow. A formula without a domain and a program without a contract are both incomplete specifications.
Mathematical guarantees and the computing ideas they support#
| Idea and location | What is established | What is not established |
|---|---|---|
| Function/domain: M02, W01 | One accepted input maps to one output; expression substitution replaces the entire input. | Equal simplified formulas need not have identical domains. |
| Derivative: M08–M11, W01 | When the limit exists, a local linear rate describes first-order output change. | A derivative is not the function value or the line intercept. Continuity alone does not imply differentiability. |
| Mean Value Theorem: M13 | Continuity on a closed interval and differentiability inside yield a point matching the secant slope. | A corner, jump, or missing endpoint can defeat the hypotheses. The theorem does not identify the point constructively in every problem. |
| FTC: M16–M17 | Under the stated regularity, accumulation and antiderivatives are linked. | A symbolically plausible primitive does not remove an improper singularity or justify exchanging limits. |
| Convergence: M26–M30 | A specified sequence of partial sums approaches a finite limit under a valid test. | Terms tending to zero alone do not prove series convergence; conditional convergence is not absolute convergence. |
| Taylor error: M30 | A valid remainder hypothesis bounds approximation on the stated interval. | A small last printed coefficient is not a universal error bound; a series may fail at an endpoint. |
| Gradient/Jacobian: M36–M37, W04 | Differentiability yields a linear local map with explicit input/output dimensions. | Existing partial derivatives alone need not establish total differentiability. A step in raw coordinate units is not scale-invariant. |
| Change of variables: M41 | With a suitable map and multiplicity control, the absolute Jacobian adjusts scalar volume. | Dropping the Jacobian or ignoring noninjective coverage changes the integral. Orientation rules differ for flux forms. |
| Boundary theorems: M43–M46 | Domain regularity, field conditions, and matching orientation link interior derivatives with boundary integrals. | Zero curl on a punctured domain alone does not prove a global potential. Singularities cannot be silently integrated through. |
| Least squares: A02, G05 | Full column rank gives a unique Euclidean least-squares minimizer with residual orthogonal to the column space. | Small residual does not imply small coefficient uncertainty in an ill-conditioned problem. Normal equations need not be the best numerical algorithm. |
| Probability/inference: A03–A04, G04 | A conditional model, sampling assumptions, and an estimator support a precisely scoped uncertainty statement. | A confidence interval is not a guarantee about a fixed parameter in one realized interval; a seed does not make sampling assumptions true. |
| Numerical stability: A05–A06, W05 | An analyzed scheme controls specific error behavior within a stated parameter regime. | Stable does not mean exact; conserved energy does not establish correct phase or physical-model adequacy. |
Computational guarantees and their prerequisites#
| Idea and location | What is established | What is not established |
|---|---|---|
| Loop invariant: C04–C05, G01 | Initialization, preservation, and exit connect an iterative program to a postcondition. | Partial correctness alone does not prove termination; integer overflow can invalidate the chosen model. |
| Induction/recursion: C02, C05, GP1 | A base case and justified smaller structures support a result over recursively built objects. | Testing the base case and a few recursive inputs is not an inductive proof. |
| DAG recurrence: C07–C08, W02 | A topological order supplies completed dependencies and permits negative edge weights without cycles. | A cyclic graph does not inherit the one-pass proof. Dijkstra’s nonnegative-edge hypothesis is a different premise. |
| Amortized analysis: C06, W02 | A sequence-level bound distributes occasional expensive work over many operations. | It does not bound one frame’s pause or establish a millisecond latency target. |
| Lifetime/ownership: C03, W03 | Valid owners and aliases keep designated objects alive through access. | The same-looking address or successful read does not prove lifetime validity. |
| Synchronization: C10, J05, W03 | A correct happens-before and ownership argument supports valid concurrent access under the language model. | Atomic work allocation is not automatically payload publication. Stress tests do not exhaust schedules. |
| Transactions: C11, J03, GP2 | A chosen transaction groups local effects under the database’s documented isolation and durability assumptions. | Local atomicity is not global exactly-once delivery or power-loss certification. |
| Protocol/retry identity: C12–C13, G08 | Framing handles byte-stream boundaries; persistent matching IDs permit controlled replay semantics. | TCP receipt is not application commit; a timeout does not mean the effect did not happen. |
| Type safety: C15, G02, GP1 | A defined type system and its metatheory rule out a specified class of execution errors. | Well-typed code can compute the wrong business result, exceed resources, or violate unstated requirements. |
| Finite equivalence: W07 | Reachability in a bounded product automaton decides equivalence for those complete finite machines. | It is not an equivalence decider for every general-purpose program. |
| Optimization/certificates: G03, G05 | Feasibility plus a matching valid bound can certify an optimum in the stated problem. | A feasible heuristic output and a fast run are not automatically optimality evidence. |
| ML evaluation: G12–G15, GP2 | Properly separated data and a frozen policy support an empirical result on the defined held-out unit. | High accuracy does not establish calibration, causal effect, fair impacts, or performance on another population. |
An integrated vocabulary for your error log#
Definition fixes what an object or term means. Identity is an equality holding on a stated domain. Theorem is a conclusion derived from hypotheses. Approximation is a replacement whose error must be interpreted. Implementation choice is one way to realize a specification. Empirical observation is a measured result under recorded conditions. Hypothesis is a claim proposed for investigation. Do not use the visual authority of a displayed equation to blur these categories.
Invariant is a property preserved across a specified transition. Variant is a decreasing well-founded measure used to prove termination. Precondition restricts starting inputs or states. Postcondition describes permitted outcomes after completion. Certificate is evidence that a checker can validate for a particular claim. Oracle in testing is a source of expected behavior, which itself can be wrong or share implementation assumptions.
Conditioning concerns how the mathematical answer changes when problem data changes. Stability concerns error introduced or amplified by an algorithm under a specified analysis. Residual measures how closely a candidate satisfies equations or predictions; it need not be the same as error in the desired unknown. Bias and variance are statistical properties relative to a model and repeated-sampling interpretation, not labels for every discrepancy.
Atomicity concerns indivisibility of an operation or all-or-nothing transactional effect. Isolation concerns interactions between transactions under a particular policy. Linearizability places completed concurrent operations consistently within their invocation/response intervals. Idempotency means repetition has a specified no-additional-effect property; it must name which state and identity are repeated. Availability and durability need explicit failure and progress assumptions.
Training loss measures an objective on fitting data. Validation supports model or policy selection. Test evaluation estimates a frozen choice on held-out data under a defined sampling/deployment question. Leakage lets unavailable or held-out information influence fitting or selection. Calibration concerns agreement of predicted probabilities with outcome frequencies in an appropriate population; it is not identical to ranking or accuracy.
How to use a failure to select the next lesson#
When a result is wrong, identify the first unsupported transition rather than rereading a whole subject. Wrong domain or object: return to notation and representation. Correct setup but incorrect manipulation: repair the algebra or state trace. Correct operations applied under a false premise: revisit method selection and hypotheses. Correct ideal proof but failing code: examine bounds, types, lifetimes, error paths, and implementation invariants. Passing code with weak performance claims: repair the experiment. Good local metrics with poor deployed outcomes: reconsider data availability, distribution, policy, and human context.
A learning milestone is not “I finished a chapter.” It is “I can solve a new problem, explain why the method applies, identify a failure case, and verify the result using a different route.” Repeat that standard at increasing scope: a substitution, a loop, a data structure, a service, a model, and finally an independently defended engineering investigation. That is the connection running through this entire book.