# 多變數實函數：二變數二次多項式的係數次序、宣告定義域、切片與點值

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-multivariable-real-function/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-multivariable-real-function-01 · production-20261019-adopted-96



## 目標與範圍

係數向量依 [1,x,y,x²,xy,y²] 次序為 c=(1,−2,3,1,2,−1)，宣告定義域為閉矩形 R=[−1,2]×[0,3]。(1) 寫出 f 並確認 f:R→ℝ 是函數；(2) 分別核對 x、y 邊界，判定 (2,3)、(3,1)、(0,−1) 是否在 R 中；(3) 計算 f(2,1) 與 f(1,2)，並證明交換 x、y 係數得到的 g 是不同的函數；(4) 求 y=1 的 x-切片，並說明給定的 y=1 切片與指定四個點值各自都不足以決定 f。

只處理 G1、G2 指定的二變數整數係數二次多項式切片與閉矩形定義域（MKO 假設 a1、a2）。不宣稱連續、可微或向量值；不證明多項式恆等定理或任何點集對二次多項式的唯一決定性。不改動 canonical MKO 或其英文 edition。





## 已知條件與符號


- function_def
- cartesian_product_def
- order_basics
- distributive
- numeric_evaluation


- G1 — 係數次序固定為 [1,x,y,x²,xy,y²]；f 的係數向量是 c=(1,−2,3,1,2,−1)（MKO 假設 a1：六個整數係數）。
- G2 — 宣告定義域 R=[−1,2]×[0,3]，第一坐標為 x、第二坐標為 y；對應域 ℝ（MKO 假設 a2：只核明示閉矩形）。
- G3 — 比較函數（同一定義域 R）：g 的係數 (1,3,−2,−1,2,1)；h 的係數 (1,−2,2,1,2,0)；k 的係數 (1,−3,3,2,2,−1)。


- c=(c_0,c_1,c_2,c_3,c_4,c_5) — 依 [1,x,y,x²,xy,y²] 次序的係數
- f(x,y) — 由 c=(1,−2,3,1,2,−1) 給出的函數
- R=[-1,2]\times[0,3] — 宣告的閉矩形定義域
- g — 交換 x、y 係數後的函數
- \varphi(x)=f(x,1) — y=1 的 x-切片
- h,\ k — 與 f 在切片或有限點上一致的比較函數





## 規則與來源


- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- mko_mvf_def · cited — 本條目先限二變數實多項式 f:ℝ²→ℝ 的明示切片，係數依 [1,x,y,x²,xy,y²] 固定次序。函數資格需明示定義域與座標角色；本輪不自動宣稱連續、可微或向量值。 · mko-multivariable-real-function
- p_interval_def · prerequisite — 閉區間與閉矩形：u∈[α,β] ⇔ α≤u≤β；(x,y)∈[α,β]×[γ,δ] ⇔ x∈[α,β] 且 y∈[γ,δ]。





## 逐步主鏈

S01 · definition操作前

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

操作後

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

條件：無

規則：mko_mvf_def · 依賴：mko_mvf_def, G1

葉節點依據：mko_mvf_def + def_unfold

MKO 固定係數次序 [1,x,y,x²,xy,y²]：第 0 個係數乘 1，第 1 個乘 x，第 2 個乘 y，第 3 個乘 x²，第 4 個乘 xy，第 5 個乘 y²。只有次序固定，係數向量才能精確重算出函數（MKO 段落 0）。



S02 · equivalent操作前

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

操作後

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

條件：無

規則：eq_replace · 依賴：S01, G1

葉節點依據：eq_replace + mul_one

把 c_0=1、c_1=−2、c_2=3、c_3=1、c_4=2、c_5=−1 依次代入 S01 的通式。係數 1 的項寫成 x²，係數 −1 的項寫成 −y²。



S03 · implies操作前

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

操作後

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

條件：無

規則：function_def · 依賴：S02, G2, function_def

葉節點依據：function_def + numeric_evaluation

函數資格需要三件事：宣告的定義域 R、對應域 ℝ、以及每個 (x,y)∈R 恰好一個值。對實數 x、y，式子只用加、減、乘，結果是唯一確定的實數，所以每點恰有一個值。坐標角色由 G2 固定：第一坐標代入 x，第二坐標代入 y。



S04 · equivalent操作前

(2,3)\in R\ ?

操作後

(2,3)\in R

條件：無

規則：p_interval_def · 依賴：G2, p_interval_def

葉節點依據：p_interval_def + and_intro_elim

依閉矩形的定義，(2,3)∈R ⇔ 2∈[−1,2] 且 3∈[0,3]。兩個條件分別在 S04.1、S04.2 核對，都成立；注意兩個坐標都正好落在邊界上，閉區間包含端點。



S05 · implies操作前

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

操作後

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

條件：無

規則：p_interval_def · 依賴：G2, p_interval_def, S03

葉節點依據：p_interval_def + de_morgan_logic + order_basics

(3,1)：y=1∈[0,3] 通過，但 x=3>2，x 邊界失敗。(0,−1)：x=0∈[−1,2] 通過，但 y=−1<0，y 邊界失敗。兩點都不在 R 中；每點都只有一個坐標失敗，所以只核一個坐標的檢查必定會漏掉其中之一。多項式式子在 (3,1) 仍可算出 12，但那不是宣告函數 f:R→ℝ 的值。



S06 · equivalent操作前

f(2,1)

操作後

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

條件：(2,1)\in R

規則：numeric_evaluation · 依賴：S02, S03

葉節點依據：numeric_evaluation + eq_replace

(2,1)∈R（−1≤2≤2、0≤1≤3）。代入 x=2、y=1，逐項計算見 S06.1，和為 7（N1）。



S07 · equivalent操作前

f(1,2)

操作後

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

條件：(1,2)\in R

規則：numeric_evaluation · 依賴：S02, S03

葉節點依據：numeric_evaluation + eq_replace

(1,2)∈R（−1≤1≤2、0≤2≤3）。代入 x=1、y=2：1、−2、6、1、2·1·2=4、−4，和為 6（N2）。



S08 · implies操作前

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

操作後

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

條件：無

規則：numeric_evaluation · 依賴：S06, S07

葉節點依據：numeric_evaluation

同樣兩個數 1 與 2，放在不同坐標位置得到不同值。所以坐標角色（哪個是 x、哪個是 y）是函數資料的一部分，不能隨意交換。



S09 · equivalent操作前

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

操作後

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

條件：(x,y)\in R; (y,x)\in R

規則：eq_congruence · 依賴：S01, G3

葉節點依據：add_comm + mul_comm + eq_congruence

g 是交換係數 c_1↔c_2、c_3↔c_5（c_4 不變）所得、仍以 R 為定義域的函數。交換兩個多項式式子的 x、y 並重排會得到相同式子；但僅當 (x,y)∈R 且 (y,x)∈R 時，才可寫 g(x,y)=f(y,x)。本題 (2,1) 與 (1,2) 均符合；N3 核對多項式式子的恆等，不把域外求值當作 f 的值。



S10 · implies操作前

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

操作後

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

條件：(2,1)\in R

規則：function_def · 依賴：S09, S06, S07, function_def

葉節點依據：function_def + numeric_evaluation

由 S09，g(2,1)=f(1,2)=6（N4 直接計算也得 6），而 f(2,1)=7。兩個函數相等需要在定義域每一點都同值；(2,1)∈R 上值不同，所以 g≠f。這正是 MKO 指出的誤解：交換 x 與 y 的係數會改變函數。



S11 · equivalent操作前

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

操作後

\varphi(x)=x^2+3

條件：y=1\in[0,3]

規則：eq_congruence · 依賴：S02, G2

葉節點依據：eq_congruence + add_inverse + add_comm

固定 y=1（在 [0,3] 中），x 在 [−1,2] 中變動：f(x,1)=1−2x+3+x²+2x−1=x²+3，−2x 與 2x 相消（N5 為恆等式）。這是一個單變數函數，是 f 在一條水平線上的切片。



S12 · implies操作前

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

操作後

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

條件：無

規則：eq_congruence · 依賴：S11, G3

葉節點依據：eq_congruence + distributive + add_inverse

h 與 f 的差是 y²−y（N6 為恆等式：3y−y=2y，−y²+y²=0）。y=1 時 y²−y=0，所以 h 的 y=1 切片與 f 的完全相同，都是 x²+3（N7 為恆等式）。



S13 · implies操作前

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

操作後

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

條件：(0,2)\in R

規則：function_def · 依賴：S12, function_def

葉節點依據：function_def + numeric_evaluation

(0,2)∈R。h(0,2)=1+4=5，f(0,2)=1+6−4=3（N8、N9），差 2 正是 y²−y 在 y=2 的值。所以 h≠f，雖然它們的 y=1 切片相同：單一切片不能決定完整函數（MKO 段落 2）。



S14 · implies操作前

k=f+(x^2-x)

操作後

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

條件：(2,0)\in R

規則：function_def · 依賴：S02, G3, function_def

葉節點依據：function_def + numeric_evaluation + distributive

k 與 f 的差是 x²−x（N10 為恆等式）。x∈{0,1} 時 x²−x=0（N12 只是這兩點的有限核對），所以 k 與 f 在四個格點上值相同（f 的值依次為 1、0、3、4）。但在 (2,0)∈R，k(2,0)=3 而 f(2,0)=1（N13、N14）。所以在本題指定四點的值相同，不足以推出兩個函數相等。



S15 · implies操作前

\text{S03 to S14}

操作後

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

條件：無

規則：and_intro_elim · 依賴：S03, S05, S10, S13, S14

葉節點依據：and_intro_elim

總結：f 由固定次序的係數向量、宣告定義域 R 與坐標角色共同決定（S03）；成員資格要分開核 x、y（S04、S05）；交換係數得到不同函數 g（S10）；給定的 y=1 切片（S13）與指定四個點值（S14）各自不足以決定 f。







## 局部子步與引理

S04.1 · equivalent操作前

2\in[-1,2]

操作後

-1\le 2\le 2

條件：無

規則：p_interval_def · 依賴：S04

葉節點依據：p_interval_def + order_basics

x 邊界：−1≤2 成立，2≤2 成立（等號）。所以 x=2 在 [−1,2] 中。



S04.2 · equivalent操作前

3\in[0,3]

操作後

0\le 3\le 3

條件：無

規則：p_interval_def · 依賴：S04

葉節點依據：p_interval_def + order_basics

y 邊界：0≤3 成立，3≤3 成立。所以 y=3 在 [0,3] 中，(2,3)∈R，f(2,3)=1−4+9+4+12−9=13（N11）是 f 的一個值。



S06.1 · equivalent操作前

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

操作後

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

條件：無

規則：numeric_evaluation · 依賴：S02

葉節點依據：numeric_evaluation + power_laws

依係數次序逐項：常數 1；−2x=−4；3y=3；x²=4；2xy=2·2·1=4；−y²=−1。逐項列出可以避免把 x、y 代錯位置。







## 逐步反向審查


- S15 · premise_audit · S03, S10, S13, S14 — 只合取已證結論，沒有新推論。
- S14 · premise_audit · function_def, numeric_evaluation — 這裡只否定「這四個點足以決定 f」；不討論是否有其他特殊點集能在二次多項式類中決定函數，本稿不宣稱任何這類結果。
- S13 · premise_audit · function_def, numeric_evaluation — 一個定義域內的點就足以否定 h=f。
- S12 · premise_audit · eq_congruence, distributive — 只宣稱在 y=1 這條線上一致；其他 y 值上的一致性不宣稱，S13 正好顯示它失敗。
- S11 · inverse_equivalence · eq_congruence, add_inverse — 化簡只用加法反元素與合併同類項，雙向成立。
- S10 · premise_audit · function_def, S09 — 否定函數相等只需一個點；該點必須在宣告定義域內，(2,1) 在 R 中。
- S09 · inverse_equivalence · add_comm, mul_comm — 只用到加法與乘法交換律重排各項，雙向成立。
- S08 · premise_audit · S06, S07 — 只宣稱這一對點的值不同；不宣稱 f 在每一對交換點上都不同（例如 f(0,0)=f(0,0)）。
- S07 · inverse_equivalence · numeric_evaluation — 精確整數求值；可由 N2 重算。
- S06.1 · inverse_equivalence · numeric_evaluation, power_laws — 每項都是確定的整數乘積，雙向成立。
- S06 · inverse_equivalence · numeric_evaluation — 精確整數求值，兩邊是同一個數；可由 N1 重算。
- S05 · premise_audit · p_interval_def, order_basics — 否定合取只需一個條件失敗；這裡分別示範 x 失敗與 y 失敗。
- S04.2 · inverse_equivalence · p_interval_def, order_basics — 與 S04.1 相同的區間定義，用在第二坐標與 y 的區間上。
- S04.1 · inverse_equivalence · p_interval_def, order_basics — 區間定義雙向成立；若誤用開區間 (−1,2)，x=2 會被錯誤排除。
- S04 · inverse_equivalence · p_interval_def, and_intro_elim — 矩形成員資格是兩個區間條件的合取，雙向成立；兩個條件都要核（MKO 段落 1）。
- S03 · premise_audit · function_def, G2 — 多項式式子在整個 ℝ² 上都能求值，但這裡的函數定義域是宣告的 R（MKO 假設 a2）；本步不宣稱連續或可微。
- S02 · inverse_equivalence · eq_replace, S01 — 反向：依次讀出 1、x、y、x²、xy、y² 的係數，回到 (1,−2,3,1,2,−1)。
- S01 · premise_audit · mko_mvf_def — 這一步只規定讀法；同一組數字換一種次序讀，會得到不同的函數（見 S09、S10）。





## 錯誤控制與反例

交換 x 與 y 係數MKO 指出的第一個誤解是交換 x 與 y 係數。係數向量必須依 [1,x,y,x²,xy,y²] 讀；若誤讀成 [1,y,x,y²,xy,x²]，同一組數字給出的是 g；當 (x,y)、(y,x) 均在 R 時有 g(x,y)=f(y,x)，而 g(2,1)=6≠7=f(2,1)。代入時也要依坐標角色：第一坐標代 x，第二坐標代 y（S06.1 逐項列出就是為此）。

幾個點值不能宣稱全域等價MKO 的第二個誤解是以幾個點值宣稱全域函數等價、連續或可微。S14 的 k 與 f 在 (0,0)、(1,0)、(0,1)、(1,1) 完全一致，卻在 (2,0) 不同；S13 的 h 與 f 的整條 y=1 切片一致，卻在 (0,2) 不同。本題指定四點的核對不足以保證全域相等；若另外知道多項式的次數上界，足夠且適當的有限點可判定恆等，本稿不使用該判準。

矩形定義域要分開核兩個坐標(0,−1) 的 x=0 在 [−1,2] 中，若只核 x 就會誤判它在 R 中；(3,1) 的 y=1 在 [0,3] 中，若只核 y 也會誤判。另外 R 是閉矩形，邊界點如 (2,3) 屬於 R。


- f(2,1)=f(1,2)，因為用的是同樣兩個數 → reject — f(2,1)=7 而 f(1,2)=6（S06、S07）。
- k 與 f 在 (0,0)、(1,0)、(0,1)、(1,1) 的值相同，所以 k=f → reject — k(2,0)=3≠1=f(2,0)，而 (2,0)∈R（S14）。
- f(3,1)=12 是宣告函數 f:R→ℝ 的一個值 → reject — (3,1)∉R，因為 x=3>2（S05）；式子可求值不等於該點在定義域中。
- y=1 的切片 x²+3 決定了 f → reject — h 有相同的 y=1 切片，但 h(0,2)=5≠3=f(0,2)（S12、S13）。





## 結論與限制

f(x,y)=1−2x+3y+x²+2xy−y² 在宣告定義域 R=[−1,2]×[0,3] 上是函數；(2,3)∈R（f=13），(3,1) 因 x>2、(0,−1) 因 y<0 不在 R 中。f(2,1)=7、f(1,2)=6；交換係數的 g 在合法的交換點上有 g(2,1)=f(1,2)=6，所以 g≠f。y=1 切片為 x²+3，但 h 有相同切片而 h(0,2)=5≠3=f(0,2)；k 與 f 在四個格點上相同而 k(2,0)=3≠1=f(2,0)。


- 本稿不宣稱 f 連續或可微；偏導數與梯度屬於後續條目（MKO 的 formal next）。
- N12 只是 x∈{0,1} 兩點的有限核對，不是恆等式；本稿正是用它說明在指定四個格點上一致不足以推出全域相等。





## 驗證及來源綁定

15 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 896db668ee991856b4a5f03263420b664073e8a89c748e47bac90da89b7ed88b
- original source SHA-256: 896db668ee991856b4a5f03263420b664073e8a89c748e47bac90da89b7ed88b
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-multivariable-real-function-01.json)