# Multivariable real-valued function: coefficient order, declared domain, slices and point values of a bivariate quadratic

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-multivariable-real-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-multivariable-real-function-01 · production-20261019-adopted-96



## Goal and scope

The coefficient vector in the order [1,x,y,x²,xy,y²] is c=(1,−2,3,1,2,−1), and the declared domain is the closed rectangle R=[−1,2]×[0,3]. (1) Write f and confirm that f:R→ℝ is a function; (2) check the x and y bounds separately to decide whether (2,3), (3,1), (0,−1) lie in R; (3) compute f(2,1) and f(1,2), and prove that g, obtained by swapping the x and y coefficients, is a different function; (4) find the x-slice at y=1 and show that neither the given y=1 slice nor the four specified point values determine f.

Treats only the bivariate integer-coefficient quadratic slice and the closed rectangular domain given by G1 and G2 (MKO assumptions a1, a2). Continuity, differentiability and vector values are not asserted; neither the polynomial identity theorem nor the unisolvence of any point set for quadratics is proved. The canonical MKO and its English edition are not changed.





## Givens and symbols


- function_def
- cartesian_product_def
- order_basics
- distributive
- numeric_evaluation


- G1 — The coefficient order is fixed as [1,x,y,x²,xy,y²]; the coefficient vector of f is c=(1,−2,3,1,2,−1) (MKO assumption a1: six integer coefficients).
- G2 — Declared domain R=[−1,2]×[0,3], first coordinate x and second coordinate y; codomain ℝ (MKO assumption a2: only the explicitly declared closed rectangle is checked).
- G3 — Comparison functions (same domain R): g with coefficients (1,3,−2,−1,2,1); h with coefficients (1,−2,2,1,2,0); k with coefficients (1,−3,3,2,2,−1).


- c=(c_0,c_1,c_2,c_3,c_4,c_5) — coefficients in the order [1,x,y,x²,xy,y²]
- f(x,y) — the function given by c=(1,−2,3,1,2,−1)
- R=[-1,2]\times[0,3] — the declared closed rectangular domain
- g — the function with x and y coefficients swapped
- \varphi(x)=f(x,1) — the x-slice at y=1
- h,\ k — comparison functions agreeing with f on a slice or at finitely many points





## 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.
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- 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.
- 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.
- mul_one · prerequisite — Multiplicative identity: 1·u=u.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬Q.
- power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
- 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.
- add_comm · prerequisite — Commutativity of addition: u+v=v+u.
- mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- mko_mvf_def · cited — This entry restricts attention to explicit slices of bivariate real polynomials f:ℝ²→ℝ, with coefficients ordered as [1,x,y,x²,x*y,y²]. Function qualification requires a declared domain and coordinate roles; continuity, differentiability and vector-valued codomains are not automatically asserted. · mko-multivariable-real-function
- p_interval_def · prerequisite — Closed intervals and rectangles: u∈[α,β] ⇔ α≤u≤β; (x,y)∈[α,β]×[γ,δ] ⇔ x∈[α,β] and y∈[γ,δ].





## Main derivation

S01 · definitionBefore

c=(c_0,c_1,c_2,c_3,c_4,c_5)

After

f(x,y)=c_0+c_1x+c_2y+c_3x^2+c_4xy+c_5y^2

Conditions: none

Rule: mko_mvf_def · Uses: mko_mvf_def, G1

Leaf basis: mko_mvf_def + def_unfold

The MKO fixes the coefficient order [1,x,y,x²,xy,y²]: coefficient 0 multiplies 1, coefficient 1 multiplies x, coefficient 2 multiplies y, coefficient 3 multiplies x², coefficient 4 multiplies xy, coefficient 5 multiplies y². Only with a fixed order can the coefficient vector reproduce the function exactly (MKO paragraph 0).



S02 · equivalentBefore

c=(1,-2,3,1,2,-1)

After

f(x,y)=1-2x+3y+x^2+2xy-y^2

Conditions: none

Rule: eq_replace · Uses: S01, G1

Leaf basis: eq_replace + mul_one

Substitute c_0=1, c_1=−2, c_2=3, c_3=1, c_4=2, c_5=−1 in order into the general form of S01. The term with coefficient 1 is written x², the one with coefficient −1 is written −y².



S03 · impliesBefore

f(x,y)=1-2x+3y+x^2+2xy-y^2,\ (x,y)\in R

After

f:R\to\mathbb{R}\ \text{is a function}

Conditions: none

Rule: function_def · Uses: S02, G2, function_def

Leaf basis: function_def + numeric_evaluation

Specifying a function requires three things: the declared domain R, the codomain ℝ, and exactly one value at each (x,y)∈R. For real x, y the expression uses only addition, subtraction and multiplication, so its value is a uniquely determined real number, and each point has exactly one value. Coordinate roles are fixed by G2: the first coordinate is substituted for x, the second for y.



S04 · equivalentBefore

(2,3)\in R\ ?

After

(2,3)\in R

Conditions: none

Rule: p_interval_def · Uses: G2, p_interval_def

Leaf basis: p_interval_def + and_intro_elim

By the definition of a closed rectangle, (2,3)∈R ⇔ 2∈[−1,2] and 3∈[0,3]. The two conditions are checked separately in S04.1 and S04.2 and both hold; note that both coordinates sit exactly on the boundary, and closed intervals include their endpoints.



S05 · impliesBefore

(3,1),\ (0,-1)

After

(3,1)\notin R\ (3>2),\quad (0,-1)\notin R\ (-1<0)

Conditions: none

Rule: p_interval_def · Uses: G2, p_interval_def, S03

Leaf basis: p_interval_def + de_morgan_logic + order_basics

(3,1): y=1∈[0,3] passes, but x=3>2 fails the x bound. (0,−1): x=0∈[−1,2] passes, but y=−1<0 fails the y bound. Neither point is in R; each fails in only one coordinate, so a check of only one coordinate is bound to miss one of them. The polynomial expression still evaluates to 12 at (3,1), but that is not a value of the declared function f:R→ℝ.



S06 · equivalentBefore

f(2,1)

After

1-4+3+4+4-1=7

Conditions: (2,1)\in R

Rule: numeric_evaluation · Uses: S02, S03

Leaf basis: numeric_evaluation + eq_replace

(2,1)∈R (−1≤2≤2, 0≤1≤3). Substituting x=2, y=1 and computing term by term (S06.1) gives a total of 7 (N1).



S07 · equivalentBefore

f(1,2)

After

1-2+6+1+4-4=6

Conditions: (1,2)\in R

Rule: numeric_evaluation · Uses: S02, S03

Leaf basis: numeric_evaluation + eq_replace

(1,2)∈R (−1≤1≤2, 0≤2≤3). Substituting x=1, y=2: 1, −2, 6, 1, 2·1·2=4, −4, which total 6 (N2).



S08 · impliesBefore

f(2,1)=7,\ f(1,2)=6

After

f(2,1)\neq f(1,2)

Conditions: none

Rule: numeric_evaluation · Uses: S06, S07

Leaf basis: numeric_evaluation

The same two numbers 1 and 2 in different coordinate positions give different values. So the coordinate roles (which is x and which is y) are part of the data of the function and cannot be swapped at will.



S09 · equivalentBefore

g(x,y)=1+3x-2y-x^2+2xy+y^2

After

g(x,y)=f(y,x)\quad\text{when }(x,y)\in R\ \land\ (y,x)\in R

Conditions: (x,y)\in R; (y,x)\in R

Rule: eq_congruence · Uses: S01, G3

Leaf basis: add_comm + mul_comm + eq_congruence

The function g, still with domain R, is obtained by swapping c_1↔c_2 and c_3↔c_5 while keeping c_4 fixed. Swapping the variables in the polynomial expressions and rearranging gives the same expression. However, g(x,y)=f(y,x) is valid only when both (x,y) and (y,x) lie in R. The points (2,1) and (1,2) used here satisfy this condition. N3 checks the polynomial-expression identity, not values of f outside its domain.



S10 · impliesBefore

g(2,1)=f(1,2)=6,\ f(2,1)=7

After

g\neq f\ \text{as functions on}\ R

Conditions: (2,1)\in R

Rule: function_def · Uses: S09, S06, S07, function_def

Leaf basis: function_def + numeric_evaluation

By S09, g(2,1)=f(1,2)=6 (N4 computes 6 directly as well), while f(2,1)=7. Equal functions must agree at every point of the domain; they differ at (2,1)∈R, so g≠f. This is the misconception named by the MKO: swapping the x and y coefficients changes the function.



S11 · equivalentBefore

\varphi(x)=f(x,1),\ x\in[-1,2]

After

\varphi(x)=x^2+3

Conditions: y=1\in[0,3]

Rule: eq_congruence · Uses: S02, G2

Leaf basis: eq_congruence + add_inverse + add_comm

Fix y=1 (which lies in [0,3]) and let x vary in [−1,2]: f(x,1)=1−2x+3+x²+2x−1=x²+3, with −2x and 2x cancelling (N5 is an identity). This is a single-variable function, the slice of f along one horizontal line.



S12 · impliesBefore

h(x,y)=1-2x+2y+x^2+2xy

After

h=f+(y^2-y),\ \ h(x,1)=f(x,1)=x^2+3

Conditions: none

Rule: eq_congruence · Uses: S11, G3

Leaf basis: eq_congruence + distributive + add_inverse

h differs from f by y²−y (N6 is an identity: 3y−y=2y and −y²+y²=0). At y=1, y²−y=0, so the y=1 slice of h is exactly that of f, namely x²+3 (N7 is an identity).



S13 · impliesBefore

h(0,2),\ f(0,2)

After

h(0,2)=5\neq 3=f(0,2)

Conditions: (0,2)\in R

Rule: function_def · Uses: S12, function_def

Leaf basis: function_def + numeric_evaluation

(0,2)∈R. h(0,2)=1+4=5 and f(0,2)=1+6−4=3 (N8, N9); the difference 2 is exactly y²−y at y=2. So h≠f although their y=1 slices are identical: one slice does not determine the whole function (MKO paragraph 2).



S14 · impliesBefore

k=f+(x^2-x)

After

k=f\ \text{at}\ (0,0),(1,0),(0,1),(1,1),\ \ k(2,0)=3\neq 1=f(2,0)

Conditions: (2,0)\in R

Rule: function_def · Uses: S02, G3, function_def

Leaf basis: function_def + numeric_evaluation + distributive

k differs from f by x²−x (N10 is an identity). For x∈{0,1}, x²−x=0 (N12 is only a finite check at these two points), so k and f agree at the four grid points (f takes the values 1, 0, 3, 4 there). But at (2,0)∈R, k(2,0)=3 while f(2,0)=1 (N13, N14). Thus agreement at these four specified points does not imply that the two functions are equal.



S15 · impliesBefore

\text{S03 to S14}

After

f=(c,R,\text{coordinate roles});\ \text{the }y=1\text{ slice and the four listed point values each fail to determine }f

Conditions: none

Rule: and_intro_elim · Uses: S03, S05, S10, S13, S14

Leaf basis: and_intro_elim

Summary: f is determined jointly by the coefficient vector in its fixed order, the declared domain R and the coordinate roles (S03); membership needs separate x and y checks (S04, S05); swapping coefficients gives a different function g (S10); neither the given y=1 slice (S13) nor the four specified point values (S14) determine f.







## Substeps and lemmas

S04.1 · equivalentBefore

2\in[-1,2]

After

-1\le 2\le 2

Conditions: none

Rule: p_interval_def · Uses: S04

Leaf basis: p_interval_def + order_basics

x bound: −1≤2 holds and 2≤2 holds (with equality). So x=2 lies in [−1,2].



S04.2 · equivalentBefore

3\in[0,3]

After

0\le 3\le 3

Conditions: none

Rule: p_interval_def · Uses: S04

Leaf basis: p_interval_def + order_basics

y bound: 0≤3 holds and 3≤3 holds. So y=3 lies in [0,3], (2,3)∈R, and f(2,3)=1−4+9+4+12−9=13 (N11) is a value of f.



S06.1 · equivalentBefore

1,\ -2x,\ 3y,\ x^2,\ 2xy,\ -y^2\ \text{at}\ (2,1)

After

1,\ -4,\ 3,\ 4,\ 4,\ -1

Conditions: none

Rule: numeric_evaluation · Uses: S02

Leaf basis: numeric_evaluation + power_laws

Term by term in coefficient order: constant 1; −2x=−4; 3y=3; x²=4; 2xy=2·2·1=4; −y²=−1. Listing the terms one by one prevents substituting x and y into the wrong places.







## Reverse audits


- S15 · premise_audit · S03, S10, S13, S14 — Only conjoins conclusions already proved; there is no new inference.
- S14 · premise_audit · function_def, numeric_evaluation — This only refutes 'these four points determine f'; whether some other special point set determines a function within the class of quadratics is not discussed, and no such result is claimed.
- S13 · premise_audit · function_def, numeric_evaluation — One point of the domain suffices to refute h=f.
- S12 · premise_audit · eq_congruence, distributive — Agreement is claimed only on the line y=1; agreement at other y is not claimed, and S13 shows it fails.
- S11 · inverse_equivalence · eq_congruence, add_inverse — The simplification uses only additive inverses and collecting like terms, so it holds both ways.
- S10 · premise_audit · function_def, S09 — Refuting equality of functions needs one point, which must lie in the declared domain; (2,1) is in R.
- S09 · inverse_equivalence · add_comm, mul_comm — Only commutativity of addition and multiplication is used to rearrange terms, so it holds both ways.
- S08 · premise_audit · S06, S07 — Only claims that the values at this pair of points differ; it does not claim that f differs at every swapped pair (for example f(0,0)=f(0,0)).
- S07 · inverse_equivalence · numeric_evaluation — Exact integer evaluation; recomputed by N2.
- S06.1 · inverse_equivalence · numeric_evaluation, power_laws — Each term is a definite integer product, so it holds both ways.
- S06 · inverse_equivalence · numeric_evaluation — Exact integer evaluation, both sides the same number; recomputed by N1.
- S05 · premise_audit · p_interval_def, order_basics — A conjunction is refuted by one failing condition; here an x failure and a y failure are shown separately.
- S04.2 · inverse_equivalence · p_interval_def, order_basics — The same interval definition as S04.1, applied to the second coordinate and the y-interval.
- S04.1 · inverse_equivalence · p_interval_def, order_basics — The interval definition is two-way; using the open interval (−1,2) by mistake would wrongly exclude x=2.
- S04 · inverse_equivalence · p_interval_def, and_intro_elim — Membership in the rectangle is the conjunction of two interval conditions, two-way; both must be checked (MKO paragraph 1).
- S03 · premise_audit · function_def, G2 — The polynomial expression can be evaluated on all of ℝ², but the domain of this function is the declared R (MKO assumption a2); this step asserts neither continuity nor differentiability.
- S02 · inverse_equivalence · eq_replace, S01 — Backward: reading off the coefficients of 1, x, y, x², xy, y² in order recovers (1,−2,3,1,2,−1).
- S01 · premise_audit · mko_mvf_def — This step only fixes how the vector is read; reading the same numbers in another order gives a different function (see S09, S10).





## Error controls and negative controls

Swapping the x and y coefficientsThe first misconception named by the MKO is swapping the x and y coefficients. The coefficient vector must be read in the order [1,x,y,x²,xy,y²]; read as [1,y,x,y²,xy,x²], the same numbers give g; the identity g(x,y)=f(y,x) holds when both (x,y) and (y,x) lie in R, and g(2,1)=6≠7=f(2,1). Substitution must also respect the coordinate roles: the first coordinate goes to x, the second to y (which is why S06.1 lists the terms one by one).

A few point values cannot establish global equivalenceThe second misconception named by the MKO is using a few point values to claim global equivalence, continuity or differentiability. The function k of S14 agrees with f at (0,0), (1,0), (0,1), (1,1) but differs at (2,0); the function h of S13 agrees with f on the whole slice y=1 but differs at (0,2). Checking these four points is insufficient for global equality. With a known polynomial-degree bound, a suitable sufficiently large finite point set can decide an identity; that criterion is not used here.

Check both coordinates of a rectangular domainFor (0,−1), x=0 lies in [−1,2], so checking only x would wrongly put it in R; for (3,1), y=1 lies in [0,3], so checking only y would also err. Also R is a closed rectangle, so boundary points such as (2,3) belong to R.


- f(2,1)=f(1,2), because the same two numbers are used → reject — f(2,1)=7 while f(1,2)=6 (S06, S07).
- k and f agree at (0,0), (1,0), (0,1), (1,1), so k=f → reject — k(2,0)=3≠1=f(2,0), and (2,0)∈R (S14).
- f(3,1)=12 is a value of the declared function f:R→ℝ → reject — (3,1)∉R because x=3>2 (S05); being able to evaluate the expression does not put the point in the domain.
- The y=1 slice x²+3 determines f → reject — h has the same y=1 slice, but h(0,2)=5≠3=f(0,2) (S12, S13).





## Result and limitations

f(x,y)=1−2x+3y+x²+2xy−y² is a function on the declared domain R=[−1,2]×[0,3]; (2,3)∈R (f=13), while (3,1) (x>2) and (0,−1) (y<0) are not in R. f(2,1)=7 and f(1,2)=6; the coefficient-swapped g has g(2,1)=f(1,2)=6 at these valid swapped points, so g≠f. The y=1 slice is x²+3, but h has the same slice with h(0,2)=5≠3=f(0,2); k agrees with f at four grid points yet k(2,0)=3≠1=f(2,0).


- This guide does not assert that f is continuous or differentiable; partial derivatives and the gradient belong to a later entry (the MKO's formal next).
- N12 is only a finite check at the two points x∈{0,1}, not an identity; the guide uses it precisely to show that agreement at these four grid points is insufficient for global equality.





## Verification and source binding

15 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 896db668ee991856b4a5f03263420b664073e8a89c748e47bac90da89b7ed88b
- original source SHA-256: 896db668ee991856b4a5f03263420b664073e8a89c748e47bac90da89b7ed88b
- 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-multivariable-real-function-01.json)