Concept guide
With the ascending coefficient lists f=[2,0,1] and g=[1,3] (that is f(x)=2+x² and g(x)=1+3x): first prove from the definition of the derivative the differentiation formula for polynomials of degree at most three; then find (fg)' and (f∘g)' along two independent routes, differentiating the expansion and applying the product and chain rules, and confirm they agree at every x; also check the sum and scalar rules, expose the errors f'g', a missing inner derivative, an outer derivative at the wrong point and reversed coefficient reading, and evaluate at x=1.
Differentiating polynomial sums, products, and compositions
derivation-mko-derivative-rules-01
Concept guide
For f=[3,−4,6] (f(x)=3−4x+6x²): prove from the definition the derivative formula for polynomials of degree at most four; build the representative antiderivative F0=[0,3,−2,2] and verify F0'=f; prove that F0+C is an antiderivative for every real C and that, among polynomials with at most five coefficients, every antiderivative is F0+C; check the candidates G=[7,3,−2,2] (accept), H=[0,3,−4,2] (reject) and K=[0,3,−3,8/3] (reject although it matches at two test points); evaluate F0(2)+C with C=−5; and explain why an antiderivative is not an inverse function.
Polynomial antiderivatives and the choice of constant
derivation-mko-antiderivative-01
Concept guide
Let f(x)=x²−4, a=0, b=3. (1) Using only the Riemann definition (the common limit of all valid tagged-partition sums as the mesh tends to zero) and the premise that f is integrable, find I(f,0,3) as the limit of the N-piece left sums L_N; (2) recompute it independently with the moment formula listed in this MKO and compare; (3) find the reversed integral I(f,3,0); (4) use N=3 and N=50 to show that a finite left sum is not the integral, and explain why the signed integral is not a nonnegative area.
Signed polynomial definite integrals on finite intervals
derivation-mko-definite-integral-01
Concept guide
Let f:ℝ→ℝ be continuous on all of ℝ, a∈ℝ, and G(x)=∫_a^x f(t)dt an oriented integral. (1) Prove that G is differentiable at every point with G′(x)=f(x); (2) if F:ℝ→ℝ is differentiable with F′=f, prove ∫_a^b f(t)dt=F(b)−F(a) for arbitrary real a, b; (3) with f(t)=6t²−2t+1 and the candidate F(x)=2x³−x²+x+1/2, compute ∫_2^{−1} f(t)dt, and explain why G(2)=0 does not give G′(2)=0 and why bounds coinciding at x=0 do not give a zero derivative.
Fundamental theorem of calculus: continuity and oriented endpoints
derivation-mko-fundamental-theorem-calculus-01
Concept guide
Let G=(V,E) with V={1,2,3,4,5,6} and E={{1,2},{2,3},{2,4},{4,5},{4,6}}. (1) Prove from the MKO's definition that G is a tree (V nonempty, connected, no simple cycle); (2) list its leaves; (3) find the path from 3 to 6 and prove it is unique; (4) add the edge {3,6}, write the simple cycle it creates and prove it is the only simple cycle; (5) contrast: a triangle plus an isolated vertex has |E|=|V|−1 but is not a tree; a single vertex without edges is a tree with no leaf.
Nonempty finite trees: connectivity, cycles, and unique paths
derivation-mko-tree-01
Concept guide
Let X={a,b,c} with a, b, c distinct. (1) Prove that τ₁={∅,{a},{a,b},X} is a topology on X, covering all 16 subfamilies (including the empty one); (2) prove that τ₂={∅,{a},{b},X} is not a topology, and say which checks it does pass; (3) compare τ₁ with the indiscrete and discrete topologies; (4) on ℕ, prove that τ_fin={finite subsets of ℕ}∪{ℕ} is closed under pairwise unions and finite intersections but is not a topology.
Topological space
derivation-mko-topological-space-01
Concept guide
From the MKO's definition (a∣b ⇔ there is a natural k with b=a·k): (1) prove 6∣84; (2) prove 6∤87; (3) prove 4∤10, although 10/4=5/2 is a number; (4) prove that every a divides 0; (5) prove 0∣b ⇔ b=0, and explain why the witness for 0∣0 is not unique and why 0∤5; (6) prove that for a>0 there is at most one witness (and when a∣b that existing witness is unique); (7) prove reflexivity and transitivity of divisibility, and from 3∣6 and 6∣84 find a witness for 3∣84.
Natural-number divisibility
derivation-mko-natural-divisibility-01
Concept guide
From the MKO's divisibility characterization (d∣a, d∣b, and every common divisor c divides d): (1) prove that at most one d satisfies it; (2) prove that each step of Euclid's algorithm preserves the set of common divisors and that the algorithm stops, use it to compute gcd(84,36)=12, and verify directly that 12 satisfies the characterization; (3) explain why the common divisor 6 is not the gcd; (4) compute gcd(8,15)=1 and explain that 8 and 15 are coprime although neither is prime; (5) treat the zero cases gcd(0,1)=1, gcd(0,6)=6 and gcd(0,0)=0.
Greatest common divisor and coprimality
derivation-mko-gcd-coprime-01
Concept guide
From the MKO's definition (p is prime ⇔ 2≤p and every natural divisor d of p satisfies d=1 or d=p): (1) explain why 0 and 1 are not prime; (2) prove that 2 is prime; (3) prove that 91 is composite with the witness 7, and show that testing only 2, 3, 5 misjudges it; (4) prove 'if n=dk with d, k≥2 then min(d,k)²≤n', and use it to prove that 97 is prime by checking only 2 to 9; (5) prove that 2 is the only even prime.
Prime natural number
derivation-mko-prime-number-01
Concept guide
From the MKO's definition (n>0, a≡b (mod n) ⇔ a mod n=b mod n): (1) decide 100≡23 (mod 7); (2) prove that this is equivalent to the witness form 'there are naturals k, l with a+nk=b+nl', and give witnesses for 100 and 23; (3) explain why congruence is an equivalence relation; (4) prove that addition and multiplication preserve congruence, and from 15≡1 (mod 7) obtain 115≡24 and 1500≡23 (mod 7); (5) use 2·3≡2·0 (mod 6) to show that a common factor cannot be cancelled unconditionally; (6) explain why different moduli cannot be chained, and why the modulus 0 is excluded.
Natural-number congruence modulo a positive modulus
derivation-mko-modular-congruence-01
Concept guide
Take the input set X={0,1,2,3,4,5,6,7,8,9}, the specification P(x): 'x is prime', and the yes-instance set Y={x∈X ∣ P(x)}. In the explicit while-program model W, prove that the trial-division procedure D1 terminates on every x∈X and that D1(x)=true exactly when x∈Y, so D1 is a decider for (X,Y); then show that D2, which halts only on yes-instances, and D3, which tests only parity, are not deciders.
Decision problem
derivation-mko-decision-problem-01
Concept guide
Take the source string s: `∀ (a b : Nat), a ≤ b → a < b + 1` as a teaching object and, in an environment E that is fixed explicitly but never executed, explain layer by layer: its bound variables and their types, its hypothesis and conclusion, the core term S that elaboration would have to produce if it succeeded, why S would have type Prop, and what a proof term would have to establish; then give an informal proof of its mathematical content and contrast it with s′: `∀ (a : Nat), a - 1 < a` (a Prop, but false) and s″: `∀ (a : Int), a - 1 < a` (true). Lean is not run at any point, and nothing here claims that any text parses, elaborates, compiles or is proved by Lean.
Formal statements in a proof assistant
derivation-mko-lean-formal-statement-01
Concept guide
Let X={1,2,3,4} and τ={∅,{1},{1,2},{3,4},{1,3,4},X}. First verify that τ is a topology on X, then list all closed sets and sort the sixteen subsets of X into four classes: clopen, open only, closed only, and neither; finally prove that in every topological space ∅ and X are clopen, and that the union of two closed sets is closed.
Open and closed sets
derivation-mko-open-closed-set-01
Concept guide
Let X={1,2,3,4} and τ={∅,{1},{1,2},{3,4},{1,3,4},X}. Decide whether N1={1,2,3} and N2={2,3,4} are neighborhoods of the point 2; prove that in a finite topology the neighborhoods of x are exactly the subsets containing O_x (the intersection of all open sets containing x), and use this to list all neighborhoods of the points 1, 2, 3 and 4; prove that neighborhoods are closed upwards; and show that the verdict for the same set can change under the discrete topology.
Neighborhood
derivation-mko-neighborhood-01
Concept guide
Let X={1,2,3} with τX={∅,{1},{1,2},X}, and Y={a,b} with τY={∅,{a},Y}. For three maps given by complete tables, f (1↦a, 2↦a, 3↦b), g (1↦a, 2↦b, 3↦a) and c (everything ↦b), decide continuity by the preimage condition and decide whether each is an open map; prove that a composite of continuous maps is continuous and check it with q:Y→Z; finally count all continuous maps X→Y.
Continuous maps between topological spaces
derivation-mko-topological-continuity-01
Concept guide
Given the finite model (S,Init,Step,Halt) with S={s0,s1,s2,s3,s4,s5,s6}, Init={s0}, Halt={s3} and raw edge data {(s0,s1),(s0,s2),(s1,s3),(s1,s5),(s2,s4),(s4,s2),(s3,s6)}: truncate edges out of halt states as the MKO requires, compute the reachable set by fixpoint iteration, identify halt states, stuck states and reachable cycles, exhibit legal halting, stuck and infinite executions, rule out three illegal traces, and explain why depth-bounded exploration that has not exhausted the reachable graph cannot certify termination of all maximal executions merely from the absence of an observed counterexample.
Abstract computational model
derivation-mko-computational-model-01
Concept guide
In a finite-state model M whose states are the six permutations of (1,2,3), with initial state (3,2,1), each step may nondeterministically swap any adjacent inverted pair, and Halt={(1,2,3)}. With the postcondition 'increasing, and a rearrangement of the input', prove partial correctness, termination and total correctness of M, using the ranking function inv (the number of inversions) to show every execution takes at most 3 steps and every maximal execution stops in Halt. Then use the variant M′ (any adjacent pair may be swapped) to show that one successful path and partial correctness do not give total correctness, and the variant M″ (a wrong halting condition) to show that termination does not give correctness.
Algorithm correctness
derivation-mko-algorithm-correctness-01
Concept guide
Let the cost function be f(n)=3n²+5n+2 (n starting at 0), with comparison functions g(n)=n² and h(n)=n. With explicit full-tail witnesses prove f∈O(g) (c=10, N=1) and f∈Ω(g) (c=3, N=0), hence f∈Θ(g); show that N=0 cannot work for O, that c=3 cannot work for O, and that another witness c=4, N=6 also works; then prove f∉O(h), so f∈Ω(h) but f∉Θ(h).
Asymptotic resource bounds
derivation-mko-asymptotic-resource-bound-01
Concept guide
In an explicit synthetic small propositional type system ST (matching MKO assumption a2), with distinct propositional atoms P and Q: explain part by part what each piece of the term t=λh:P∧Q. ⟨snd h, fst h⟩ establishes and what type it has, derive the judgment ⊢ t : P∧Q→Q∧P, and explain why the type of t matches the proposition S=P∧Q→Q∧P; then prove that the similar-looking t′=λh:P∧Q. ⟨fst h, snd h⟩ is not a proof term for S. Finally separate three things: a typing derivation in ST, acceptance by the Lean kernel, and a saved proof-term receipt.
Proof term
derivation-mko-lean-proof-term-01
Concept guide
State space X={0,1,2,3,4,5,6}, update map T(x)=(3x+1) mod 7. From x_0=0 compute the orbit given by x_(n+1)=T(x_n), prove x_(n+6)=x_n for every natural number n and use it to find x_2026; enumerate the fixed points completely; decide that A={0,1,2,4,5,6} is forward invariant while B={0,1} is not, and prove that the orbit from 0 never reaches the fixed point.
Discrete-time dynamical system
derivation-mko-discrete-dynamical-system-01
Concept guide
On the interval I=ℝ consider the ordinary differential equation y″−2y′+y=x²−4x+2. (1) Determine its order; (2) check that y₁(x)=x² is a solution on all of ℝ (its residual is identically zero); (3) prove that y₂(x)=x²+x has residual x−2, which vanishes only at x=2, so it is not a solution on ℝ; (4) check the initial values y(0)=0, y′(0)=0 and, citing the existence and uniqueness theorem for second-order linear equations with its hypotheses, conclude that y₁ is the unique solution of this initial value problem; (5) show that without initial values the solution is not unique.
Ordinary differential equation
derivation-mko-ordinary-differential-equation-01
Concept guide
Using exact rationals: compute the absolute and relative error of the approximation a=33/100 to the reference x=1/3; decide whether a is within the tolerances τ₁=1/250, τ₂=1/400 and τ₃=1/300 (τ₃ is the endpoint case); prove |a−x|≤τ ⇔ x−τ≤a≤x+τ; compare the errors after scaling by 1000; explain why relative error is undefined for a zero reference and why an error value alone does not reveal the source of the error.
Numerical approximation and error
derivation-mko-numerical-approximation-error-01
Concept guide
The candidate set C={0,1,2}² has nine points, the constraint is x+2y≥3 and the objective is f(x,y)=x+y. Minimize with a scan algorithm that first decides feasibility and then compares values one by one, and prove the result with an invariant: optimal value m=2, argmin={(0,2),(1,1)} (a tie of two); explain why (0,0) and (2,0) are excluded although their objective values do not exceed 2; find the maximum; and show that under the same constraint over the real nonnegative quadrant, the minimum is 3/2, attained at (0,3/2), which is not in the declared finite candidate set.
Optimization problem
derivation-mko-optimization-problem-01
Concept guide
With integer exponent vectors d(Q)=(a,b,c) over the base dimensions L, M, T: compute the dimensions of speed, acceleration and two energy expressions; decide that ½mv²=mgh is dimensionally consistent, that v=2gh is not and cannot be repaired by a pure-number constant, and that v²=4gh is consistent but wrong in the constant-acceleration model; decide that m+v cannot be added; solve E=C·m^α v^β for α=1 and β=2; and explain that equal dimensions do not mean equal unit conversion factors.
Dimensional analysis
derivation-mko-dimensional-analysis-01