Affine and degree-one functions: finding m and b from two points, and deciding degree, zero and linearity

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

f:\mathbb{R}\to\mathbb{R}

f(x)=mx+b;\ m\neq0\Rightarrow\deg f=1;\ m=0\Rightarrow f\ \text{constant}

f(x_2)-f(x_1)

m(x_2-x_1)

f(3)-f(1)=m(3-1)

0-4=2m,\ \text{i.e.}\ -4=2m

-4=2m

m=\frac{-4}{2}=-2

f(1)=4:\ -2\cdot 1+b=4

b=4+2=6

m=-2,\ b=6

f(x)=-2x+6,\quad f(3)=-6+6=0

f(x)=-2x+6

b=f(0)=6,\quad f(x+1)-f(x)=m=-2

m=-2

m\neq 0\Rightarrow f\ \text{has degree one}

f(x)=0:\ -2x+6=0

x=\frac{-6}{-2}=3=-\frac{b}{m}

f(0)=6

f\ \text{is not}\ \mathbb{R}\text{-linear}

\forall x\in\mathbb{R}:\ mx+b=nx+c

m=n\ \land\ b=c

f(2)=-4+6=2=k(2)

f\neq k\quad((-2,6)\neq(1,0))

g(x)=0x+5,\ h(x)=0x+0

g\ \text{has no zero};\ \text{every real is a zero of}\ h;\ \text{neither has degree one}

f,\ k,\ g,\ h

f(x)=-2x+6:\ \deg 1,\ \text{zero}\ 3,\ \text{not linear};\ f\neq k;\ g,h\ \text{constant}

Substeps and lemmas

(mx_2+b)-(mx_1+b)

mx_2-mx_1=m(x_2-x_1)

T\ \mathbb{R}\text{-linear}

T(0)=T(0\cdot 0)=0\cdot T(0)=0

\forall x:\ mx+b=nx+c

b=c\ (x=0),\quad m+b=n+c\ (x=1)\ \Rightarrow\ m=n

m=n\ \land\ b=c

\forall x:\ mx+b=nx+c

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 function

The 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 sense

The 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 everywhere

S03 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)