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

目標與範圍

係數向量依 [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∈[γ,δ]。

逐步主鏈

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

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

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

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

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

(2,3)\in R\ ?

(2,3)\in R

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

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

f(2,1)

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

f(1,2)

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

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

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

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

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

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

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

\varphi(x)=x^2+3

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

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

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

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

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)

\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

局部子步與引理

2\in[-1,2]

-1\le 2\le 2

3\in[0,3]

0\le 3\le 3

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

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

逐步反向審查

• 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、反控制與修訂記錄）