# 實雙線性形式：以矩陣公式 x^T A y 分槽證明雙線性並精確求值 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-real-bilinear-form/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-real-bilinear-form-01 · production-20261019-adopted-96 ## 目標與範圍 設 A=[[1,2],[−1,3]]，B(x,y)=x^T A y（x、y∈ℝ²）。分別證明 B 對第一槽與第二槽都是線性的（雙線性）；對 x=(2,−1)、y=(1,4) 精確求 B(x,y)=7 與 B(y,x)=−20，說明雙線性不要求對稱；並證明黑箱函數 f(x,y)=x1y1+(x2³−x2)y2 雖通過若干加法樣本卻不是雙線性。 只在 MKO 的範圍內：具體數值核對使用整係數矩陣、相容維度與安全整數座標（假設 a1）；一般雙線性證書對任意實數座標與純量成立，固定實矩陣也可；矩陣展開是雙線性的全稱代數證書，有限樣本不足以證任意黑箱函數雙線性（假設 a2）。對稱、正定、非退化與內積資格只作對照，不在本稿證明。不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - matrix_product_def - distributive - finite_sum_rules - vector_space_axioms - linear_map_def - G1 — A=[[1,2],[−1,3]]，即 a11=1、a12=2、a21=−1、a22=3。x、y 視為 ℝ² 的列向量（2×1），B(x,y)=x^T A y。 - G2 — 例子：x=(2,−1)、y=(1,4)、x′=(1,1)、α=3、β=−2。 - G3 — 對照黑箱：f(x,y)=x1y1+(x2³−x2)y2。 - A=(a_{ij}) — 2×2 整係數矩陣 [[1,2],[−1,3]] - B(x,y)=x^{T}Ay — 由 A 給出的雙線性形式 - x,\ x',\ y,\ y' — ℝ² 中的向量 - \alpha,\ \beta — 實數係數 - f — 對照用的黑箱函數 ## 規則與來源 - matrix_product_def · prerequisite — 矩陣乘法：若 A 為 m×n、B 為 n×p，則 (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}。矩陣乘法一般不可交換。 - distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。 - finite_sum_rules · prerequisite — 有限和：Σ_{i=1}^{0} a_i=0、Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}；Σ(a_i+b_i)=Σa_i+Σb_i；Σ c·a_i=c·Σa_i。 - vector_space_axioms · prerequisite — 向量空間公理（實數或其他域 F 上）：加法成交換群；純量乘法滿足 a(u+v)=au+av、(a+b)u=au+bu、(ab)u=a(bu)、1u=u。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。 - mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。 - power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。 - mko_bilinear_def · cited — B:V乘V到R為雙線性，若固定任一輸入後，另一輸入上的映射皆為線性。本輪用整係數矩陣公式B(x,y)=x^T A y作全稱座標證書並精確求值。 · mko-real-bilinear-form - linear_map_def · prerequisite — 映射 L:ℝ²→ℝ 是線性的，若對所有 u、u′∈ℝ² 與 α、β∈ℝ，L(αu+βu′)=αL(u)+βL(u′)。 - L_slot2 · lemma — 對每個固定的 x∈ℝ²，y↦B(x,y)=Σ_iΣ_j x_i a_ij y_j 是線性的：B(x,αy+βy′)=αB(x,y)+βB(x,y′)。 ## 逐步主鏈 S01 · definition操作前 B\ \text{bilinear} 操作後 \forall y:\ x\mapsto B(x,y)\ \text{linear}\ \land\ \forall x:\ y\mapsto B(x,y)\ \text{linear} 條件：無 規則：mko_bilinear_def · 依賴：G1, linear_map_def 葉節點依據：mko_bilinear_def + def_unfold 依 MKO，雙線性有兩項分開的責任：固定第二輸入時第一槽線性，固定第一輸入時第二槽線性。兩項都要對所有向量與所有實數係數成立。 S02 · equivalent操作前 x^{T}Ay\ \ (1\times2)(2\times2)(2\times1) 操作後 B(x,y)=\sum_{i=1}^{2}\sum_{j=1}^{2}x_i\,a_{ij}\,y_j 條件：\text{dimensions compatible} 規則：matrix_product_def · 依賴：G1, matrix_product_def 葉節點依據：matrix_product_def + distributive + finite_sum_rules 維度相容：x^T 是 1×2、A 是 2×2、y 是 2×1，乘積是 1×1，即一個實數。用兩次矩陣乘法定義：(Ay)_i=Σ_j a_ij y_j，再 x^T(Ay)=Σ_i x_i (Ay)_i，合起來是雙重和。 S03 · equivalent操作前 \sum_{i,j}x_i\,a_{ij}\,y_j 操作後 x_1y_1+2x_1y_2-x_2y_1+3x_2y_2 條件：無 規則：finite_sum_rules · 依賴：S02, G1 葉節點依據：finite_sum_rules + numeric_evaluation 把四項 (i,j)=(1,1)、(1,2)、(2,1)、(2,2) 寫出並代入 a11=1、a12=2、a21=−1、a22=3。N1 以格點核對這個多線性恆等式。 S04 · equivalent操作前 B(\alpha x+\beta x',y) 操作後 \sum_{i,j}(\alpha x_i+\beta x'_i)\,a_{ij}\,y_j 條件：無 規則：vector_space_axioms · 依賴：S02, vector_space_axioms 葉節點依據：vector_space_axioms + eq_replace 第一槽：固定 y，任取 x、x′∈ℝ² 與 α、β∈ℝ。向量 αx+βx′ 的第 i 個座標是 αx_i+βx′_i（座標運算），代入 S02 的雙重和。 S05 · equivalent操作前 \sum_{i,j}(\alpha x_i+\beta x'_i)\,a_{ij}\,y_j 操作後 \sum_{i,j}\left(\alpha\,x_i a_{ij} y_j+\beta\,x'_i a_{ij} y_j\right) 條件：無 規則：distributive · 依賴：S04, distributive 葉節點依據：distributive + mul_assoc + mul_comm 每一項用分配律展開 (αx_i+βx′_i)a_ij y_j=αx_i a_ij y_j+βx′_i a_ij y_j。 S06 · equivalent操作前 \sum_{i,j}\left(\alpha\,x_i a_{ij} y_j+\beta\,x'_i a_{ij} y_j\right) 操作後 \alpha B(x,y)+\beta B(x',y) 條件：無 規則：finite_sum_rules · 依賴：S05, finite_sum_rules 葉節點依據：finite_sum_rules + eq_replace 有限和可拆成兩個和（Σ(a+b)=Σa+Σb），常數 α、β 可提出（Σca=cΣa），剩下的兩個和依 S02 分別是 B(x,y) 與 B(x′,y)。所以第一槽線性。N2 以格點核對這個恆等式。 S07 · theorem_application操作前 B(x,\alpha y+\beta y') 操作後 \alpha B(x,y)+\beta B(x,y') 條件：無 規則：L_slot2 · 依賴：S02 葉節點依據：L_slot2 第二槽要另外證明（引理 L_slot2，S07.1 到 S07.3）：A 不對稱，所以不能把第一槽的結論「交換 x、y」搬過來。 S08 · implies操作前 \text{slot 1 linear (S06)},\ \text{slot 2 linear (S07)} 操作後 B\ \text{is a bilinear form on}\ \mathbb{R}^2 條件：無 規則：forall_intro · 依賴：S01, S06, S07 葉節點依據：forall_intro + and_intro_elim + mko_bilinear_def S04 到 S07 中 x、x′、y、y′、α、β 都是任意取的，沒有額外假設，依全稱推廣兩槽對所有輸入都線性，所以 B 雙線性。論證只用到 a_ij 是固定的數，所以固定 m×n 實矩陣在相容的 ℝᵐ×ℝⁿ 上都給雙線性映射；若稱為同一 ℝⁿ 上的雙線性形式，矩陣取 n×n。本題是 n=2 的方形情形。 S09 · implies操作前 B(x,y)=x^{T}(Ay),\ x=(2,-1),\ y=(1,4) 操作後 B(x,y)=7 條件：無 規則：matrix_product_def · 依賴：S02, G1, G2 葉節點依據：matrix_product_def + numeric_evaluation 先算 Ay（S09.1），再與 x 作內積式的乘法（S09.2）。 S10 · implies操作前 B(y,x)=y^{T}(Ax),\ Ax=(1\cdot2+2\cdot(-1),\ -1\cdot2+3\cdot(-1)) 操作後 Ax=(0,-5),\ B(y,x)=1\cdot0+4\cdot(-5)=-20 條件：無 規則：matrix_product_def · 依賴：S02, G1, G2 葉節點依據：matrix_product_def + numeric_evaluation 交換兩個輸入：Ax=(2−2,−2−3)=(0,−5)，y^T(Ax)=1·0+4·(−5)=−20。 S11 · implies操作前 B(x,y)=7,\ B(y,x)=-20 操作後 B\ \text{bilinear but not symmetric} 條件：無 規則：numeric_evaluation · 依賴：S08, S09, S10 葉節點依據：numeric_evaluation + quantifier_negation 7≠−20，所以 B 不對稱；但 S08 已證 B 雙線性。對稱是額外條件，不是雙線性的一部分；內積還要求對稱與正定，所以 B 不是內積。 S12 · implies操作前 \alpha x+\beta x'=(4,-5) 操作後 B((4,-5),y)=-19=3\cdot7+(-2)\cdot20 條件：無 規則：numeric_evaluation · 依賴：S06, S09, G2 葉節點依據：numeric_evaluation + matrix_product_def αx+βx′=(3·2−2·1, 3·(−1)−2·1)=(4,−5)。用 Ay=(9,11)：B((4,−5),y)=36−55=−19；B(x′,y)=9+11=20，αB(x,y)+βB(x′,y)=21−40=−19。這個實例與 S06 一致，但只是例子，不是證明。 S13 · implies操作前 x=x'=(0,1),\ y=(0,1) 操作後 f(x+x',y)=6\neq0=f(x,y)+f(x',y) 條件：無 規則：contradiction · 依賴：G3, linear_map_def 葉節點依據：contradiction + quantifier_negation + numeric_evaluation f((0,2),(0,1))=0+(8−2)·1=6，而 f((0,1),(0,1))=0+(1−1)·1=0，兩者相加為 0。取 α=β=1，第一槽的線性失敗，所以 f 不是雙線性。 S14 · implies操作前 x_2,\ x'_2,\ x_2+x'_2\in\{-1,0,1\} 操作後 f(x+x',y)=f(x,y)+f(x',y)\ \text{on these samples} 條件：無 規則：numeric_evaluation · 依賴：G3, S13 葉節點依據：numeric_evaluation + power_laws 當 t∈{−1,0,1} 時 t³−t=0，所以只要 x2、x′2 與 x2+x′2 都在 {−1,0,1}，f 在這些輸入上等於 x1y1，可加性樣本全部通過（例如 x=(1,1)、x′=(2,−1)）。但 S13 已證 f 不是雙線性：通過有限樣本不能證明黑箱函數雙線性，必須有像 S04 到 S07 那樣的全稱證書。 ## 局部子步與引理 S07.1 · equivalent操作前 B(x,\alpha y+\beta y') 操作後 \sum_{i,j}x_i\,a_{ij}\,(\alpha y_j+\beta y'_j) 條件：無 規則：vector_space_axioms · 依賴：S02, vector_space_axioms 葉節點依據：vector_space_axioms + eq_replace 固定 x，αy+βy′ 的第 j 個座標是 αy_j+βy′_j，代入雙重和。 S07.2 · equivalent操作前 \sum_{i,j}x_i\,a_{ij}\,(\alpha y_j+\beta y'_j) 操作後 \sum_{i,j}\left(\alpha\,x_i a_{ij} y_j+\beta\,x_i a_{ij} y'_j\right) 條件：無 規則：distributive · 依賴：S07.1, distributive 葉節點依據：distributive + mul_comm + mul_assoc 每一項用分配律展開，常數 α、β 移到前面（乘法交換與結合）。 S07.3 · equivalent操作前 \sum_{i,j}\left(\alpha\,x_i a_{ij} y_j+\beta\,x_i a_{ij} y'_j\right) 操作後 \alpha B(x,y)+\beta B(x,y') 條件：無 規則：finite_sum_rules · 依賴：S07.2, finite_sum_rules 葉節點依據：finite_sum_rules + eq_replace 拆成兩個和並提出常數，依 S02 得 αB(x,y)+βB(x,y′)。S07.1 到 S07.3 合起來證得引理 L_slot2。N3 以格點核對。 S09.1 · equivalent操作前 Ay=\begin{pmatrix}1&2\\-1&3\end{pmatrix}\begin{pmatrix}1\\4\end{pmatrix} 操作後 \begin{pmatrix}9\\11\end{pmatrix} 條件：無 規則：matrix_product_def · 依賴：G1, G2 葉節點依據：matrix_product_def + numeric_evaluation (Ay)_1=1·1+2·4=9，(Ay)_2=(−1)·1+3·4=11。 S09.2 · equivalent操作前 x^{T}(Ay)=(2,-1)\begin{pmatrix}9\\11\end{pmatrix} 操作後 2\cdot9+(-1)\cdot11=7 條件：無 規則：matrix_product_def · 依賴：S09.1, G2 葉節點依據：matrix_product_def + numeric_evaluation 2·9+(−1)·11=18−11=7。 ## 逐步反向審查 - S14 · premise_audit · G3, S13 — 此步只說明樣本通過；結論「不是雙線性」來自 S13。 - S13 · premise_audit · G3, contradiction, linear_map_def — 線性是全稱命題，一個反例就否證。 - S12 · premise_audit · S06, numeric_evaluation — 一般結論來自 S06；此步只核一個實例（N9）。 - S11 · premise_audit · S08, S09, S10 — 一個不等的值對就否證對稱（全稱命題）；雙線性不受影響。 - S10 · premise_audit · matrix_product_def, numeric_evaluation — 精確整數計算（N7）。 - S09.2 · inverse_equivalence · matrix_product_def, numeric_evaluation — 兩邊是同一個數。 - S09.1 · inverse_equivalence · matrix_product_def, numeric_evaluation — 兩邊是同一個向量。 - S09 · premise_audit · S02, matrix_product_def — 精確整數計算，可用 S03 的展開式交叉核對（N13）。 - S08 · sufficient_goal_reduction · S01, S06, S07, forall_intro — 目標 G：B 雙線性。足夠條件 H：兩槽各自線性；H⇒G 由 S01。H 由 S04 到 S07 正向證成，是全稱代數證書，不是樣本。 - S07.3 · inverse_equivalence · finite_sum_rules — 拆和與提出常數可倒推；此子步不使用 L_slot2。 - S07.2 · inverse_equivalence · distributive, mul_comm — 展開與因式分解互逆；此子步不使用 L_slot2。 - S07.1 · inverse_equivalence · vector_space_axioms, matrix_product_def — 代入同一向量的座標，雙向成立；此子步不使用 L_slot2。 - S07 · premise_audit · S02, L_slot2 — 只需 S02 的雙重和表示與引理。 - S06 · inverse_equivalence · finite_sum_rules — 拆和與提出常數都可倒推，雙向成立。 - S05 · inverse_equivalence · distributive — 展開與因式分解互逆，雙向成立。 - S04 · inverse_equivalence · vector_space_axioms, matrix_product_def — 代入同一個向量的座標，兩邊相等，雙向成立。 - S03 · inverse_equivalence · finite_sum_rules — 有限和的逐項展開是等值改寫，雙向成立。 - S02 · inverse_equivalence · matrix_product_def, distributive — 兩式是同一個數的兩種寫法，雙向成立。 - S01 · premise_audit · mko_bilinear_def, linear_map_def — 此步只展開定義，兩槽之後分開核（S04 到 S06、S07）。 ## 錯誤控制與反例 對稱不是雙線性MKO 指出的誤解是只核 B(x,y)=B(y,x) 就宣稱雙線性或內積。g(x,y)=(x1y1)² 對稱，但 g(2e1,e1)=4≠2=2g(e1,e1)，不是雙線性。反過來，本稿的 B 雙線性卻不對稱（7≠−20）。B(x,x)=x1²+x1x2+3x2²=(x1+x2/2)²+(11/4)x2² 對 x≠0 為正，但因不對稱仍不是內積。 兩個槽分開核；雙線性不是對 (x,y) 線性A 不對稱，所以第二槽不能由第一槽交換得到（S07 另證）。雙線性也不是 B(x+x′,y+y′)=B(x,y)+B(x′,y′)：正確展開還有交叉項 B(x,y′)+B(x′,y)。例如 x=x′=y=y′=e1：B(2e1,2e1)=4，而 B(e1,e1)+B(e1,e1)=2。 黑箱樣本不足f 在所有 x2、x′2、x2+x′2∈{−1,0,1} 的樣本上都通過可加性（S14），卻在 (0,1)+(0,1) 失敗（S13）。MKO 假設 a2：矩陣展開是全稱證書，有限樣本不能證任意黑箱函數雙線性。 - g(x,y)=(x1y1)² 對稱，所以是雙線性形式 → reject — g(2e1,e1)=4，而 2g(e1,e1)=2。 - 因為 B(x,y)=7≠−20=B(y,x)，所以 x^T A y 不是雙線性形式 → reject — 雙線性不要求對稱；S04 到 S08 已證 B 雙線性。 - 雙線性表示 B(x+x′,y+y′)=B(x,y)+B(x′,y′) → reject — x=x′=y=y′=e1 時左邊 4、右邊 2；漏了交叉項。 - f 通過了 x=(1,1)、x′=(2,−1) 等多組可加性測試，所以 f 雙線性 → reject — f((0,2),(0,1))=6，而 f((0,1),(0,1))+f((0,1),(0,1))=0。 ## 結論與限制 B(x,y)=x^T A y=x1y1+2x1y2−x2y1+3x2y2 對第一槽與第二槽分別線性（全稱代數證書），所以是雙線性形式；固定實矩陣在相容的兩個座標空間上皆給雙線性映射，同一空間上的形式使用方形矩陣。B(x,y)=7、B(y,x)=−20，B 雙線性但不對稱，也不是內積。黑箱 f(x,y)=x1y1+(x2³−x2)y2 在 x2∈{−1,0,1} 的樣本上看似可加，但 f((0,2),(0,1))=6≠0，不是雙線性。 - 錯誤控制中 B(x,x) 的配方式由 N14 以多項式恆等式核對；本稿不處理正定性或內積的一般理論。 - N2、N3 是每個變數的次數分別至多 1（總次數可大於 1）的多線性恆等式格點核對，決定該恆等式；N9 只是一個實例。 ## 驗證及來源綁定 15 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: e1078dee19a7ff2ca3fc623044adf902aaf5c6edb8681d13aaaa972aa31c4f49 - original source SHA-256: 1412fb7e13e4018d6967accecdadadcf60832aad360e17ead14a7174bc1399a7 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-real-bilinear-form-01.json)