# Mathematical representation: deciding whether words, a formula, tables and ordered pairs represent the same function [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-mathematical-representation/) 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-mathematical-representation-01 · production-20261019-adopted-96 ## Goal and scope Fix the object f:D→ℤ with D={0,1,2,3} and f(x)=2x−1. Decide: the words 'double the input, then subtract 1' correspond to 2x−1; the table T1={(0,−1),(1,1),(2,3),(3,5)} represents f; the set of ordered pairs is the graph of f; the affine rule is recovered uniquely from the two rows (1,1) and (3,5); the table T2, with (3,5) replaced by (3,6), represents neither f nor any affine rule; T3, with a repeated input, is not a function table; g(x)=2x−1 defined on ℤ is not the same function as f; and a table supplies no values at unlisted points. The worked exercises use integer-coefficient affine rules and completely listed finite tables or ordered pairs (MKO assumption a1); the auxiliary two-point affine lemma is stated for real coefficients and real coordinates; every check is made on the listed domain only, and unlisted points and the appearance of a graph supply no values (assumption a2). General semantics of diagrams and a fuller typed semantic bridge are not treated; the canonical MKO and its English edition are not changed. ## Givens and symbols - function_def - cartesian_product_def - set_extensionality - mul_inverse_nonzero - quantifier_negation - G1 — Object: f:D→ℤ with D={0,1,2,3} and f(x)=2x−1. - G2 — Interpretation rule: a table row (x,y) means 'the output at input x is y'. A table represents f exactly when its inputs are the elements of D, each appearing once, and every row satisfies y=f(x). - G3 — Verbal representation W: 'double the input, then subtract 1'. - G4 — T1={(0,−1),(1,1),(2,3),(3,5)}; T2={(0,−1),(1,1),(2,3),(3,6)}; T3=(0,−1),(1,1),(1,2),(2,3),(3,5) (input 1 appears twice). - G5 — g:ℤ→ℤ, g(x)=2x−1. - D=\{0,1,2,3\} — the domain of f - f(x)=2x-1 — the symbolic representation - T_1,\ T_2,\ T_3 — the three tables or lists of pairs to be checked - \Gamma_f — the graph of f, {(x,f(x)) ∣ x∈D} - g — the same formula on the domain ℤ ## Rules and sources - 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. - cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d. - set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements. - 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. - quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x). - 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. - def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements. - set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x). - 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. - distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu. - 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. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - mko_repr · cited — The same mathematical object can be represented in words, symbols, tables, ordered pairs or diagrams. To determine whether representations correspond, first fix the object, domain, scale and interpretation rules; visual resemblance alone does not establish equivalence. · mko-mathematical-representation - mko_repr_notes · cited — A table lists specified inputs and outputs, while a formula gives a rule of computation; they form an explicit semantic bridge only on a common domain with every row matching. Two points determine a non-vertical affine rule, but their x-coordinates must first be checked to differ; repeated inputs with different outputs do not form a function table. A picture can support understanding, but pixel positions, a visual sense of straightness or unlabelled scales cannot replace explicit data. · mko-mathematical-representation - L_two_point · lemma — For real coordinates, if x₁≠x₂ then exactly one real-coefficient affine rule y=ax+b passes through (x₁,y₁) and (x₂,y₂), namely a=(y₂−y₁)/(x₂−x₁) and b=y₁−a·x₁. ## Main derivation S01 · definitionBefore \text{several representations} After \text{object }f:D\to\mathbb{Z},\ D=\{0,1,2,3\},\ \text{row }(x,y)\ \text{means}\ f(x)=y Conditions: none Rule: mko_repr · Uses: G1, G2, mko_repr Leaf basis: mko_repr + def_intro By the MKO, the object, domain and interpretation rules must be fixed before deciding any correspondence. The object is f from G1, the domain is four integers, and the reading of tables is given by G2. Every later decision compares against these fixed settings, not appearances. S02 · equivalentBefore W:\ \text{double the input, then subtract 1} After x\mapsto 2x-1 Conditions: none Rule: def_unfold · Uses: G3, G1 Leaf basis: def_unfold Follow the order of operations in the words: doubling first gives 2x, then subtracting 1 gives 2x−1. The order matters: 'subtract 1, then double' is 2(x−1)=2x−2, which gives −2 at x=0 instead of −1. S03 · equivalentBefore f(0),f(1),f(2),f(3) After -1,\ 1,\ 3,\ 5 Conditions: none Rule: numeric_evaluation · Uses: G1 Leaf basis: numeric_evaluation Compute at the four points of the domain: 2·0−1=−1, 2·1−1=1, 2·2−1=3, 2·3−1=5. S04 · impliesBefore \text{inputs of }T_1:\ 0,1,2,3 After \text{each }x\in D\ \text{appears exactly once in }T_1 Conditions: none Rule: function_def · Uses: G4, G1, function_def Leaf basis: function_def + finite_counting_basics The inputs of T1 are 0, 1, 2, 3, exactly the four elements of D, each once. So T1 gives each x∈D exactly one output and defines a function on D (call it h₁). S05 · impliesBefore h_1(x)\ \text{vs}\ f(x)\ \text{for }x\in D After h_1=f\ \text{(}T_1\ \text{represents }f\text{)} Conditions: \text{same domain }D Rule: function_def · Uses: S03, S04, G2, mko_repr_notes Leaf basis: function_def + numeric_evaluation Compare row by row: (0,−1) with f(0)=−1, (1,1) with f(1)=1, (2,3) with f(2)=3, (3,5) with f(3)=5; all four rows match. h₁ and f have the same domain D and the same value at every point, so by the definition of equality of functions h₁=f. This is the MKO's explicit semantic bridge: a common domain with every row matching. S06 · equivalentBefore \Gamma_f=\{(x,f(x))\mid x\in D\} After \Gamma_f=\{(0,-1),(1,1),(2,3),(3,5)\}=T_1 Conditions: none Rule: set_builder · Uses: S03, G1, G4 Leaf basis: set_builder + set_extensionality Ordered-pair representation: the graph of f is the set of all (x,f(x)); by S03 it lists four pairs, exactly the rows of T1, so as sets Γ_f=T1. S07 · impliesBefore (x_1,y_1),(x_2,y_2),\ x_1\neq x_2 After a=\frac{y_2-y_1}{x_2-x_1},\ b=y_1-a\,x_1\ \text{(unique)} Conditions: x_1\neq x_2 Rule: L_two_point · Uses: L_two_point Leaf basis: mul_inverse_nonzero + eq_congruence By Lemma L_two_point (uniqueness and existence proved in S07.1 and S07.2): two points with different x-coordinates determine exactly one affine rule. S08 · impliesBefore (1,1),(3,5)\in T_1,\ 1\neq 3 After a=\tfrac{5-1}{3-1}=2,\ b=1-2=-1;\ \text{rows }(0,-1),(2,3)\ \text{also satisfy }y=2x-1 Conditions: 1\neq 3 Rule: L_two_point · Uses: S07, G4, S03 Leaf basis: L_two_point + numeric_evaluation First confirm that the x-coordinates differ, 1≠3; then the lemma gives a=4/2=2 and b=1−2·1=−1, recovering y=2x−1. Two points only determine a candidate rule; the remaining rows (0,−1) and (2,3) must still be checked: 2·0−1=−1 and 2·2−1=3, both match. S09 · impliesBefore T_2\ \text{row }(3,6),\ f(3)=5 After T_2\ \text{does not represent }f\ \text{nor any affine rule} Conditions: none Rule: quantifier_negation · Uses: G4, S03, S07 Leaf basis: quantifier_negation + L_two_point + numeric_evaluation The row of T2 at x=3 is 6, but f(3)=5; one mismatching row negates 'every row matches', so T2 does not represent f. Further, any affine rule representing T2 would pass through (0,−1) and (1,1) (with 0≠1), so by L_two_point it could only be y=2x−1, which gives 5≠6 at x=3; hence no affine rule represents T2. Matching the first three rows is not enough. S10 · impliesBefore T_3\ni(1,1),(1,2) After T_3\ \text{is not a function table} Conditions: 1\neq 2 Rule: function_def · Uses: G4, function_def, mko_repr_notes Leaf basis: function_def A function assigns exactly one output to each input. In T3 the input 1 is paired with both 1 and 2, and 1≠2, so T3 is not a function table and cannot represent f or any function. It is also the case where L_two_point does not apply because the two points share an x-coordinate (a vertical arrangement): the slope through (1,1) and (1,2) would need division by 0. S11 · impliesBefore g:\mathbb{Z}\to\mathbb{Z},\ f:D\to\mathbb{Z} After g\neq f,\ \ g|_D=f Conditions: D\neq\mathbb{Z} Rule: function_def · Uses: G1, G5, function_def Leaf basis: function_def + set_extensionality g and f use the same formula but have different domains (ℤ and D), so by the definition of equality of functions they are not the same function; for example g(4)=7 is defined while 4∉D. Restricting g to D gives the same value as f at every point, so g|_D=f. This is why the MKO requires fixing the domain first. S12 · impliesBefore x=4,\ x=\tfrac{1}{2} After \text{no value supplied: }4,\tfrac{1}{2}\notin D Conditions: none Rule: mko_repr_notes · Uses: G1, G4, mko_repr_notes Leaf basis: mko_repr_notes + function_def T1 lists only the four points of D. f(4) is undefined because 4∉D, and 1/2 is not in D either. If the four points are plotted they look collinear, and the line passes through (1/2,0), but by MKO assumption a2 the appearance of a graph and unlisted points supply no values, so f(1/2)=0 cannot be claimed. S13 · impliesBefore \text{decisions} After W,\ 2x-1,\ T_1,\ \Gamma_f\ \text{represent }f;\ T_2,\ T_3,\ g\ \text{do not} Conditions: none Rule: and_intro_elim · Uses: S02, S05, S06, S08, S09, S10, S11, S12 Leaf basis: and_intro_elim Combine the decisions: with the object, domain and interpretation rule fixed, the words W, the formula 2x−1, the table T1 and the pair set Γ_f all represent f; the rows (1,1) and (3,5) recover the rule uniquely; T2 represents neither f nor any affine rule; T3 is not a function table; g differs from f in its domain; unlisted points have no values. ## Substeps and lemmas S07.1 · impliesBefore a x_1+b=y_1,\ a x_2+b=y_2 After a(x_2-x_1)=y_2-y_1\ \Rightarrow\ a=\frac{y_2-y_1}{x_2-x_1},\ b=y_1-a\,x_1 Conditions: x_2-x_1\neq 0 Rule: mul_inverse_nonzero · Uses: mul_inverse_nonzero, eq_congruence Leaf basis: mul_inverse_nonzero + eq_congruence + distributive Uniqueness: if y=ax+b passes through both points, subtracting the equations eliminates b and gives a(x₂−x₁)=y₂−y₁. Since x₂−x₁≠0, multiplying by 1/(x₂−x₁) gives the only possible a, and the first equation gives b=y₁−a·x₁. If x₁=x₂ this would divide by 0 and the argument fails. S07.2 · impliesBefore a=\frac{y_2-y_1}{x_2-x_1},\ b=y_1-a\,x_1 After a x_1+b=y_1,\ a x_2+b=y_2 Conditions: x_2-x_1\neq 0 Rule: eq_replace · Uses: S07.1 Leaf basis: eq_replace + distributive + mul_inverse_nonzero Existence: substituting back, a x₁+b=a x₁+y₁−a x₁=y₁, and a x₂+b=y₁+a(x₂−x₁)=y₁+(y₂−y₁)=y₂ (the identity multiplied through by x₂−x₁ is N9). So the rule does pass through both points. S07.1 and S07.2 together prove Lemma L_two_point. ## Reverse audits - S13 · sufficient_goal_reduction · S02, S05, S06, S08, S09, S10, S11, S12, and_intro_elim — Goal G: the determinations in the goal. Sufficient condition H: the listed steps, each already proved (H⇒G by conjunction introduction). H is derived forwards from the givens; G is never used as a premise. - S12 · premise_audit · mko_repr_notes, function_def — It needs only that these points are outside the domain; the conclusion is 'no data', not 'the value is some number'. - S11 · premise_audit · function_def, set_extensionality — Different domains suffice for the functions to differ; an identical formula cannot fix that. - S10 · premise_audit · function_def, mko_repr_notes — It needs only one input paired with two different outputs; if a repeated row had the same output, it would merely be a duplicate row, a separate matter. - S09 · premise_audit · S03, L_two_point, quantifier_negation — Negating the universal statement needs one counterexample; 'no affine rule' uses the uniqueness part of the lemma. - S08 · premise_audit · L_two_point, numeric_evaluation — It needs x₁≠x₂; checking the other rows is necessary, because the affine rule is determined by two points and other rows may fail to lie on it (S09). - S07.2 · premise_audit · eq_replace, distributive, mul_inverse_nonzero — It needs a(x₂−x₁)=y₂−y₁, which follows from the definition of a and x₂−x₁≠0. - S07.1 · premise_audit · mul_inverse_nonzero, eq_congruence, distributive — This step proves only 'if one exists, it is unique'; existence is checked separately in S07.2. - S07 · premise_audit · L_two_point — It depends on the lemma, whose hypothesis x₁≠x₂ cannot be dropped. - S06 · inverse_equivalence · set_builder, set_extensionality, cartesian_product_def — Both sides have the same elements, so the set equality holds both ways. - S05 · premise_audit · S03, S04, function_def, mko_repr_notes — It needs all four rows to match; checking only some rows would not give equality of functions (see T2 in S09). - S04 · premise_audit · function_def, G4 — It needs both 'covers D' and 'no repetition'; checking only one of them does not give a function. - S03 · inverse_equivalence · numeric_evaluation — Exact integer computation, the same both ways. - S02 · inverse_equivalence · def_unfold — Reading 2x−1 back into words: multiply by 2, then subtract 1, which is exactly W; both directions describe the same procedure. - S01 · premise_audit · G1, G2, mko_repr — This step only fixes the settings and derives no new fact. ## Error controls and negative controls Looking the same is not being equivalentOne misconception named by the MKO: when T2 is plotted, (3,6) is only one unit above the line and the four points look almost collinear. But correspondence is decided row by row: f(3)=5≠6 (S09). Pixel positions and a visual sense of straightness cannot replace explicit data. Domains and repeated inputs cannot be ignoredAnother misconception named by the MKO: g(x)=2x−1 on ℤ has the same formula as f but a different domain, so it is a different function (S11); in T3 the input 1 has two outputs, so it is not a function table (S10). Before deciding, check the domain and that each input appears once. Two points give a candidate; the other rows must still be checkedRecovering an affine rule from two rows needs different x-coordinates (S07.1 divides by x₂−x₁). The recovered rule is only a candidate: the other rows of T1 are checked and match (S08), while the fourth row of T2 does not (S09). - T2 represents f because three of its four rows match and the plot is almost a straight line → reject — Representation needs every row to match; f(3)=5≠6 (S09). - g:ℤ→ℤ with g(x)=2x−1 is the same function as f → reject — The domains differ; for example g(4)=7 is defined while 4∉D (S11). - Every row of T3 is an ordered pair, so T3 is a function table → reject — The input 1 is paired with two outputs, 1 and 2 (S10). - From T1, f(1/2)=0, because the points lie on a line → reject — 1/2∉D, and unlisted points and the appearance of a graph supply no values (S12). - The words 'double the input, then subtract 1' describe 2(x−1) → reject — 2(x−1) subtracts first and then doubles; at x=0 it gives −2, while W gives −1 (S02). ## Result and limitations With f:D→ℤ (D={0,1,2,3}, f(x)=2x−1) and the reading 'a row (x,y) means f(x)=y' fixed: the words 'double the input, then subtract 1', the formula 2x−1, the table T1 and the pair set {(0,−1),(1,1),(2,3),(3,5)} all represent f; from (1,1) and (3,5) (with 1≠3) the rule y=2x−1 is recovered uniquely, and the other rows are checked separately and match. T2 has value 6≠5 at x=3, so it does not represent f, and by two-point uniqueness it represents no affine rule; in T3 the input 1 has two outputs, so it is not a function table; g:ℤ→ℤ differs from f because the domains differ; the table supplies no value at x=4 or x=1/2. - The diagram representation is discussed only in the error controls and S12, without a formal correspondence between coordinate scales and pixels; a fuller typed semantic bridge belongs to the MKO's formal next step. ## Verification and source binding 11 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: c57160d6a5d2e6e5cf54e5bc2ba0141c674852fb5e67bc4370040368f3ac58c2 - original source SHA-256: 9a638a2170e8b0d8bd35dbc76a4458dca4722cbd6f58352d5b1d907fd8f30ae8 - 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-mathematical-representation-01.json)