# Affine and degree-one functions: finding m and b from two points, and deciding degree, zero and linearity [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-linear-function/) 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-linear-function-01 · production-20261019-adopted-96 ## Goal and scope The graph of the affine function f:ℝ→ℝ, f(x)=mx+b, passes through (1,4) and (3,0). Find m and b; decide whether f has degree one, find its zero, and decide whether f is an ℝ-linear map in the sense of linear algebra. Then prove that two affine functions are equal on ℝ exactly when their slopes and intercepts agree, and use it to explain why f(2)=k(2) (with k(x)=x) does not give f=k; finally treat the two degenerate examples with m=0, g(x)=5 and h(x)=0. Within the MKO's scope: domain and codomain are both ℝ, and m, b are real constants. The two-point slope is used only when x_1≠x_2, and a comparison at one input asserts only that the outputs there agree. Multivariable affine maps and other fields are not discussed; the canonical MKO and its English edition are not changed. ## Givens and symbols - distributive - eq_congruence - mul_inverse_nonzero - function_def - numeric_evaluation - G1 — f:ℝ→ℝ with f(x)=mx+b and real constants m, b (MKO assumption a1). It has degree one when m≠0 and is constant when m=0; an ℝ-linear map in linear algebra additionally requires additivity and homogeneity. - G2 — The graph of f passes through (1,4) and (3,0), that is, f(1)=4 and f(3)=0. - G3 — Functions for comparison: k(x)=x, g(x)=0·x+5 and h(x)=0·x+0, all ℝ→ℝ. - f(x)=mx+b — an affine function with slope m and intercept b - (x_1,y_1),\ (x_2,y_2) — two points on the graph - k(x)=x — a function for comparison - g(x)=5,\ h(x)=0 — two degenerate examples with m=0 ## Rules and sources - distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu. - eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule. - mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined. - function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable. - add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v). - add_comm · prerequisite — Commutativity of addition: u+v=v+u. - add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w). - forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds. - eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true. - two_nonzero · prerequisite — In the reals 0<1, hence 0<1+1=2, so 2≠0. - contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q. - mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0. - mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ). - iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold. - forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain. - case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - mko_affine · cited — For m,b∈R, the function f:R→R defined by f(x)=mx+b is affine. If m≠0 its polynomial degree is one; if m=0 it is constant. An R-linear map in linear algebra additionally requires b=0, and must be distinguished from the elementary textbook term linear function. · mko-linear-function - linear_map_def · prerequisite — T:ℝ→ℝ is an ℝ-linear map when T(u+v)=T(u)+T(v) and T(cu)=cT(u) for all reals u, v, c. - L_diff · lemma — For affine f(x)=mx+b and all reals x_1, x_2: f(x_2)−f(x_1)=m(x_2−x_1). - L_lin_zero · lemma — Every ℝ-linear map T has T(0)=0. - L_affine_eq · lemma — For reals m, b, n, c: (mx+b=nx+c for every x∈ℝ) if and only if (m=n and b=c). ## Main derivation S01 · definitionBefore f:\mathbb{R}\to\mathbb{R} After f(x)=mx+b;\ m\neq0\Rightarrow\deg f=1;\ m=0\Rightarrow f\ \text{constant} Conditions: m,b\in\mathbb{R} Rule: mko_affine · Uses: G1 Leaf basis: mko_affine + def_intro By the MKO, every function of the form mx+b is affine; only those with m≠0 have degree one, and those with m=0 are constant. A linear map in linear algebra is a separate notion requiring additivity and homogeneity (linear_map_def), and the MKO notes that it additionally needs b=0. The three names must not be mixed up. S02 · equivalentBefore f(x_2)-f(x_1) After m(x_2-x_1) Conditions: none Rule: L_diff · Uses: S01 Leaf basis: distributive + add_inverse + add_comm By Lemma L_diff, the difference of outputs of an affine function is the slope times the difference of inputs; the intercept b cancels in the subtraction. The proof is S02.1. S03 · theorem_applicationBefore f(3)-f(1)=m(3-1) After 0-4=2m,\ \text{i.e.}\ -4=2m Conditions: x_1=1\neq 3=x_2 Rule: forall_elim · Uses: G2, S02 Leaf basis: forall_elim + eq_replace + numeric_evaluation Take x_1=1 and x_2=3 in L_diff and substitute f(1)=4 and f(3)=0: 0−4=m(3−1), that is −4=2m. The two inputs differ (1≠3), so 3−1=2≠0 and the next step may divide. S04 · equivalentBefore -4=2m After m=\frac{-4}{2}=-2 Conditions: 2\neq 0 Rule: mul_inverse_nonzero · Uses: S03, mul_inverse_nonzero Leaf basis: mul_inverse_nonzero + eq_congruence + two_nonzero + numeric_evaluation Since 2≠0, multiplying both sides by 1/2 gives m=−4/2=−2. This is the two-point slope formula m=(y_2−y_1)/(x_2−x_1)=(0−4)/(3−1). S05 · equivalentBefore f(1)=4:\ -2\cdot 1+b=4 After b=4+2=6 Conditions: none Rule: eq_congruence · Uses: G2, S04 Leaf basis: eq_congruence + add_inverse + numeric_evaluation Substitute m=−2 and f(1)=4 into f(x)=mx+b: −2·1+b=4. Adding 2 to both sides gives b=6. S06 · impliesBefore m=-2,\ b=6 After f(x)=-2x+6,\quad f(3)=-6+6=0 Conditions: none Rule: eq_replace · Uses: S04, S05, G2 Leaf basis: eq_replace + numeric_evaluation So f(x)=−2x+6. Check the second point: f(3)=−2·3+6=0, consistent with G2, and f(1)=−2+6=4 as well. Every move in S03 to S05 was an equivalence or followed directly from the data, so this is the only affine function through the two points. S07 · impliesBefore f(x)=-2x+6 After b=f(0)=6,\quad f(x+1)-f(x)=m=-2 Conditions: none Rule: forall_elim · Uses: S06, S02 Leaf basis: forall_elim + numeric_evaluation Following MKO para0: b=f(0)=−2·0+6=6; taking x_2=x_1+1 in L_diff gives f(x+1)−f(x)=m·1=−2, so each unit increase of the input lowers the output by 2. S08 · impliesBefore m=-2 After m\neq 0\Rightarrow f\ \text{has degree one} Conditions: m\neq 0 Rule: mko_affine · Uses: S01, S04 Leaf basis: mko_affine + numeric_evaluation m=−2≠0, so by the MKO f has polynomial degree one and is a degree-one function. If m were 0 it would not be degree one, even though it is written as mx+b (see S13). S09 · equivalentBefore f(x)=0:\ -2x+6=0 After x=\frac{-6}{-2}=3=-\frac{b}{m} Conditions: m=-2\neq 0 Rule: mul_inverse_nonzero · Uses: S06, mul_inverse_nonzero Leaf basis: mul_inverse_nonzero + eq_congruence + numeric_evaluation Subtract 6 from both sides of −2x+6=0 to get −2x=−6; since −2≠0, multiply both sides by −1/2 to get x=3. Every move is an equivalence, so the zero is unique and equals −b/m=−6/(−2)=3, in agreement with the point (3,0) of G2. S10 · impliesBefore f(0)=6 After f\ \text{is not}\ \mathbb{R}\text{-linear} Conditions: b=6\neq 0 Rule: contrapositive · Uses: S06, linear_map_def Leaf basis: L_lin_zero + contrapositive + numeric_evaluation By Lemma L_lin_zero, every ℝ-linear map sends 0 to 0 (proof in S10.1). Since f(0)=6≠0, the contrapositive shows that f is not ℝ-linear. Additivity also fails directly: f(1+1)=f(2)=2, but f(1)+f(1)=4+4=8. So an affine function with nonzero intercept is not a linear map in the sense of linear algebra. S11 · equivalentBefore \forall x\in\mathbb{R}:\ mx+b=nx+c After m=n\ \land\ b=c Conditions: none Rule: L_affine_eq · Uses: S01 Leaf basis: forall_elim + eq_congruence + iff_intro By Lemma L_affine_eq, two affine functions are equal on all of ℝ exactly when their slopes and intercepts both agree (MKO para2). The two directions are proved in S11.1 and S11.2. S12 · impliesBefore f(2)=-4+6=2=k(2) After f\neq k\quad((-2,6)\neq(1,0)) Conditions: none Rule: L_affine_eq · Uses: S06, S11, G3 Leaf basis: L_affine_eq + contrapositive + numeric_evaluation f(2)=−2·2+6=2 and k(2)=2, so the outputs at input 2 agree; this is a fact about one input only (MKO assumption a2). f has (m,b)=(−2,6) and k has (m,b)=(1,0); the slopes differ, so by S11 f and k are not equal on ℝ; for example f(0)=6≠0=k(0). S13 · case_splitBefore g(x)=0x+5,\ h(x)=0x+0 After g\ \text{has no zero};\ \text{every real is a zero of}\ h;\ \text{neither has degree one} Conditions: m=0 Rule: case_analysis · Uses: G3, S01, linear_map_def Leaf basis: case_analysis + mul_zero + linear_map_def With m=0 the zeros split into two cases. g: for every x, g(x)=0·x+5=5≠0, so there is no zero. h: h(x)=0 for every x, so every real is a zero. Both are affine (constant) functions, but m=0, so neither has degree one. Moreover h satisfies h(u+v)=0=h(u)+h(v) and h(cu)=0=c·h(u), so it is ℝ-linear; g is not, since g(0)=5≠0. S14 · impliesBefore f,\ k,\ g,\ h After f(x)=-2x+6:\ \deg 1,\ \text{zero}\ 3,\ \text{not linear};\ f\neq k;\ g,h\ \text{constant} Conditions: none Rule: and_intro_elim · Uses: S06, S08, S09, S10, S12, S13 Leaf basis: and_intro_elim Summary: f(x)=−2x+6 is an affine function of degree one with unique zero 3, but it is not ℝ-linear; f and k agree only at input 2 and are not equal; g and h are constant functions, g with no zero and h zero everywhere. ## Substeps and lemmas S02.1 · equivalentBefore (mx_2+b)-(mx_1+b) After mx_2-mx_1=m(x_2-x_1) Conditions: none Rule: distributive · Uses: distributive, add_inverse Leaf basis: distributive + add_inverse + add_comm + add_assoc Expand the subtraction: (mx_2+b)−(mx_1+b)=mx_2+b−mx_1−b; b−b=0 leaves mx_2−mx_1, and distributivity takes out m to give m(x_2−x_1). This proves Lemma L_diff. S10.1 · impliesBefore T\ \mathbb{R}\text{-linear} After T(0)=T(0\cdot 0)=0\cdot T(0)=0 Conditions: none Rule: linear_map_def · Uses: linear_map_def, mul_zero Leaf basis: linear_map_def + mul_zero + mul_comm 0=0·0, so homogeneity with c=0 and u=0 gives T(0)=T(0·0)=0·T(0), which is 0 by u·0=0. This proves Lemma L_lin_zero. S11.1 · impliesBefore \forall x:\ mx+b=nx+c After b=c\ (x=0),\quad m+b=n+c\ (x=1)\ \Rightarrow\ m=n Conditions: none Rule: forall_elim · Uses: forall_elim, eq_congruence Leaf basis: forall_elim + eq_congruence + add_inverse The equation holds for every x; x=0 gives b=c, and x=1 gives m+b=n+c, and subtracting b (=c) from both sides gives m=n. This is the ⇒ direction. Note that two different inputs are needed; an equation at one input is not enough. S11.2 · impliesBefore m=n\ \land\ b=c After \forall x:\ mx+b=nx+c Conditions: none Rule: eq_replace · Uses: eq_replace Leaf basis: eq_replace + forall_intro If m=n and b=c, replacing m by n and b by c for an arbitrary x gives mx+b=nx+c; since x was arbitrary, it holds for every x by forall_intro. This is the ⇐ direction. S11.1 and S11.2 together prove Lemma L_affine_eq. ## Reverse audits - S14 · sufficient_goal_reduction · S06, S08, S09, S10, S12, S13, and_intro_elim — Goal G: all the stated conclusions. Sufficient condition H: the separate conclusions of S06 to S13; H⇒G is just conjunction. H is proved forwards from the data; G is never used as a premise. - S13 · premise_audit · S01, case_analysis, linear_map_def, mul_zero — The case m=0 splits by whether b is zero, which covers every possibility; the conclusions agree with MKO para1. - S12 · premise_audit · S11, S06, numeric_evaluation — It uses the contrapositive of the ⇒ direction of S11: different coefficients give different functions; agreement at one input (N9) does not give global equality. - S11.2 · premise_audit · eq_replace, forall_intro — Replacement of equals can be done for every x, with no side condition. - S11.1 · premise_audit · forall_elim, eq_congruence — The premise is that the equation holds for every x; if it held only at x=2, S12 shows the conclusion can fail. - S11 · inverse_equivalence · L_affine_eq — Both directions of the lemma are proved in the sub-steps, so it may be used as an equivalence. - S10.1 · premise_audit · linear_map_def, mul_zero — Uses only homogeneity and multiplication by zero; additivity is not needed. - S10 · premise_audit · L_lin_zero, contrapositive, linear_map_def — Only the contrapositive of 'linear ⇒ T(0)=0' is used; the converse 'T(0)=0 ⇒ linear' is not claimed for general functions. - S09 · inverse_equivalence · mul_inverse_nonzero, eq_congruence — Subtracting 6 and multiplying by −1/2 are both reversible, given m≠0; substituting back, −2·3+6=0 (N8). - S08 · premise_audit · S04, mko_affine — The test looks only at whether m is zero; the intercept b does not affect the degree. - S07 · premise_audit · S02, S06, forall_elim — Both readings are special cases of results already proved, with no extra premise (N7). - S06 · premise_audit · S04, S05, G2, numeric_evaluation — Checking the two points only confirms the arithmetic (N5, N6); uniqueness comes from the derivation in S03 to S05, not from these two substitutions. - S05 · inverse_equivalence · eq_congruence, add_inverse — Adding 2 and subtracting 2 undo each other; substituting back, −2+6=4. - S04 · inverse_equivalence · mul_inverse_nonzero, eq_congruence, two_nonzero — Multiplying by 1/2 and by 2 undo each other, given 2≠0; substituting back, 2·(−2)=−4. - S03 · premise_audit · G2, S02, forall_elim — It needs both points on the graph (G2); if x_1=x_2 the equation would read 0=0 and could not determine m (MKO assumption a2). - S02.1 · inverse_equivalence · distributive, add_inverse, add_comm — Every move is an identity of real numbers, valid both ways. - S02 · inverse_equivalence · L_diff — Both sides name the same real number for all x_1, x_2 (N1). - S01 · premise_audit · G1, mko_affine, linear_map_def — This step only states definitions and the classification; no new fact is derived. ## Error controls and negative controls Not every mx+b is a degree-one functionThe first error named in the MKO is to call every mx+b a degree-one function. Only m≠0 gives degree one (S08); g(x)=0·x+5, although written in the form mx+b, is a constant function with no zero (S13). Affine is not linear in the linear-algebra senseThe second error named in the MKO is to treat an affine function with nonzero intercept as a linear map of linear algebra. A linear map must have T(0)=0 (S10.1), but f(0)=6; additivity fails too: f(2)=2≠8=f(1)+f(1) (S10). The elementary 'linear function' and the linear-algebra 'linear map' are different notions. The two-point slope needs x_1≠x_2; equality at one input is not equality everywhereS03 and S04 may divide by x_2−x_1 because 1≠3. If two points share the first coordinate, say (2,1) and (2,5), then (5−1)/(2−2) is undefined, and no function ℝ→ℝ takes both values 1 and 5 at 2. On the other hand, f(2)=k(2) says only that the outputs at input 2 agree; equality everywhere needs equal slopes and equal intercepts (S11, S12). - g(x)=5 is a degree-one function because it can be written as 0·x+5 → reject — m=0, so g is a constant function: affine, but not of degree one. - f(x)=−2x+6 is an ℝ-linear map → reject — f(0)=6≠0; moreover f(1+1)=2≠8=f(1)+f(1). - The affine function through (2,1) and (2,5) has slope (5−1)/(2−2) → reject — With x_1=x_2 the slope formula divides by zero; and no function ℝ→ℝ takes both 1 and 5 at 2. - f(2)=k(2)=2, so f=k → reject — Equality at one input does not give equality everywhere: f(0)=6≠0=k(0), and the slopes −2≠1. ## Result and limitations From (1,4) and (3,0), m=(0−4)/(3−1)=−2 and b=6, so f(x)=−2x+6. Since m≠0, f has degree one with unique zero −b/m=3; but f(0)=6≠0, so f is not ℝ-linear. Two affine functions are equal on ℝ exactly when their slopes and intercepts agree, so f(2)=k(2)=2 does not give f=k. With m=0, g(x)=5 has no zero and h(x)=0 vanishes everywhere, and neither has degree one. - This guide handles only affine functions ℝ→ℝ; multivariable affine maps and linear maps on general vector spaces are out of scope. - N1 is a degree-type grid check (degree at most one in each variable) supporting the algebraic identity L_diff; the lemma's proof is S02.1. ## Verification and source binding 15 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: fb722ebaf4dc7b60839292d104faf6dc837ca15a0a3ed5015f7c9c626d96a85a - original source SHA-256: fb722ebaf4dc7b60839292d104faf6dc837ca15a0a3ed5015f7c9c626d96a85a - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-linear-function-01.json)