實雙線性形式：以矩陣公式 x^T A y 分槽證明雙線性並精確求值

目標與範圍

設 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′)。

逐步主鏈

B\ \text{bilinear}

\forall y:\ x\mapsto B(x,y)\ \text{linear}\ \land\ \forall x:\ y\mapsto B(x,y)\ \text{linear}

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

\sum_{i,j}x_i\,a_{ij}\,y_j

x_1y_1+2x_1y_2-x_2y_1+3x_2y_2

B(\alpha x+\beta x',y)

\sum_{i,j}(\alpha x_i+\beta x'_i)\,a_{ij}\,y_j

\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)

\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)

B(x,\alpha y+\beta y')

\alpha B(x,y)+\beta B(x,y')

\text{slot 1 linear (S06)},\ \text{slot 2 linear (S07)}

B\ \text{is a bilinear form on}\ \mathbb{R}^2

B(x,y)=x^{T}(Ay),\ x=(2,-1),\ y=(1,4)

B(x,y)=7

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

B(x,y)=7,\ B(y,x)=-20

B\ \text{bilinear but not symmetric}

\alpha x+\beta x'=(4,-5)

B((4,-5),y)=-19=3\cdot7+(-2)\cdot20

x=x'=(0,1),\ y=(0,1)

f(x+x',y)=6\neq0=f(x,y)+f(x',y)

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}

局部子步與引理

B(x,\alpha y+\beta y')

\sum_{i,j}x_i\,a_{ij}\,(\alpha y_j+\beta y'_j)

\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)

\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')

Ay=\begin{pmatrix}1&2\\-1&3\end{pmatrix}\begin{pmatrix}1\\4\end{pmatrix}

\begin{pmatrix}9\\11\end{pmatrix}

x^{T}(Ay)=(2,-1)\begin{pmatrix}9\\11\end{pmatrix}

2\cdot9+(-1)\cdot11=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、反控制與修訂記錄）