實內積空間：以 Sylvester 條件為 ℝ² 上的矩陣形式作全稱正定證書

目標與範圍

設 M 為第一行 (2,1)、第二行 (1,3) 的整數對稱矩陣，⟨x,y⟩_M=xᵀMy（x,y∈ℝ²）。（一）分別證明 ⟨·,·⟩_M 雙線性、對稱、正定，所以是 ℝ² 上的內積；正定性以 2×2 Sylvester 條件（完整證明其充分與必要方向）作全稱證書。（二）判定 N（行 (1,2),(2,1)）、P（行 (1,1),(1,1)）、R（行 (2,1),(0,3)）給出的形式為何不是內積。

在 MKO 的範圍內工作：矩陣與向量完整明示，候選矩陣為 2×2 整數矩陣（假設 a1）；正定性以首主子式與行行式的精確條件核對，不由有限個向量樣本建立（假設 a2）。雙線性、對稱、正定是三個分開的責任。不處理內積誘導範數（下一節點）或完備性，不處理 n>2 的 Sylvester 判準，不改動 canonical MKO 或英文 edition。

已知條件與符號

• matrix_product_def
• distributive
• square_nonneg
• order_basics
• numeric_evaluation

• G1 — V=ℝ²，向量 x=(x₁,x₂) 視為列向量，運算逐坐標進行。
• G2 — M 的列為 (2,1) 與 (1,3)；⟨x,y⟩_M=xᵀMy。
• G3 — 對照矩陣：N 的列為 (1,2),(2,1)；P 的列為 (1,1),(1,1)；R 的列為 (2,1),(0,3)；各自定義 ⟨x,y⟩=xᵀ(矩陣)y。

• M=\begin{pmatrix}2&1\\1&3\end{pmatrix} — 候選對稱整數矩陣
• \langle x,y\rangle_M=x^{T}My — 由 M 定義的雙線性形式
• q(x)=\langle x,x\rangle_M — 對應的二次型
• \begin{pmatrix}a&b\\b&c\end{pmatrix} — 一般 2×2 實對稱矩陣，q(x)=ax_1^2+2bx_1x_2+cx_2^2
• a,\ ac-b^2 — 首主子式與行行式
• N,P,R — 三個對照矩陣

規則與來源

• 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。
• square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
• 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。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• 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。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
• power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• mko_ips_def · cited — 在同一實向量空間上，內積須對兩槽雙線性、對稱，且對每個非零向量 x 都有 ⟨x,x⟩>0。本輪對 ℝ² 使用整係數對稱矩陣及 Sylvester 條件作全稱正定證書。 · mko-real-inner-product-space
• mko_bilinear_def · cited — B:V×V→ℝ 為雙線性，若固定任一輸入後，另一輸入上的映射皆為線性；整係數矩陣公式 B(x,y)=xᵀAy 作全稱座標證書。 · mko-real-bilinear-form
• L_sylvester_suff · lemma — 對實數 a,b,c，若 a>0 且 ac−b²>0，則 q(x)=ax₁²+2bx₁x₂+cx₂² 對每個 x≠0 都大於 0。
• L_sylvester_nec · lemma — 對實數 a,b,c，若 q(x)=ax₁²+2bx₁x₂+cx₂² 對每個 x≠0 都大於 0，則 a>0 且 ac−b²>0。

逐步主鏈

\langle\cdot,\cdot\rangle_M\ \text{inner product on}\ \mathbb{R}^2

\text{bilinear}\ \land\ \text{symmetric}\ \land\ \forall x\neq0:\ \langle x,x\rangle_M>0

\langle x,y\rangle_M=x^{T}My

\langle x,y\rangle_M=2x_1y_1+x_1y_2+x_2y_1+3x_2y_2

\langle\alpha x+\beta z,\ y\rangle_M

\alpha\langle x,y\rangle_M+\beta\langle z,y\rangle_M

\langle x,\ \alpha y+\beta w\rangle_M

\alpha\langle x,y\rangle_M+\beta\langle x,w\rangle_M

\langle y,x\rangle_M=2y_1x_1+y_1x_2+y_2x_1+3y_2x_2

\langle y,x\rangle_M=\langle x,y\rangle_M\ \ (\forall x,y)

q(x)=\langle x,x\rangle_M

q(x)=2x_1^2+2x_1x_2+3x_2^2=ax_1^2+2bx_1x_2+cx_2^2\ \ (a,b,c)=(2,1,3)

a=2>0,\ \ ac-b^2=6-1=5>0

\forall x\neq0:\ q(x)>0

2\,q(x)=2(2x_1^2+2x_1x_2+3x_2^2)

2\,q(x)=(2x_1+x_2)^2+5x_2^2

\text{S03},\ \text{S04},\ \text{S05},\ \text{S07}

\langle\cdot,\cdot\rangle_M\ \text{is an inner product};\ (\mathbb{R}^2,\langle\cdot,\cdot\rangle_M)\ \text{real inner-product space}

e_1=(1,0),\ e_2=(0,1),\ x=(1,-1)

\langle e_1,e_2\rangle_M=1,\ q(e_1)=2,\ q(e_2)=3,\ q(1,-1)=2-2+3=3

\forall x\neq0:\ ax_1^2+2bx_1x_2+cx_2^2>0

a>0\ \land\ ac-b^2>0

N:\ a=1,\ b=2,\ c=1,\ ac-b^2=1-4=-3<0

q_N(-2,1)=4-8+1=-3<0\ \Rightarrow\ \langle\cdot,\cdot\rangle_N\ \text{not an inner product}

P:\ a=b=c=1,\ ac-b^2=0

q_P(x)=(x_1+x_2)^2\ge0,\ q_P(1,-1)=0\ \Rightarrow\ \text{semi-definite, not an inner product}

R=\begin{pmatrix}2&1\\0&3\end{pmatrix}

\langle e_1,e_2\rangle_R=R_{12}=1\neq 0=R_{21}=\langle e_2,e_1\rangle_R\ \Rightarrow\ \text{not symmetric}

\text{S09},\ \text{S12},\ \text{S13},\ \text{S14}

M\ \text{inner product};\ N\ \text{indefinite};\ P\ \text{semi-definite};\ R\ \text{not symmetric}

局部子步與引理

a\,q(x)=a(ax_1^2+2bx_1x_2+cx_2^2)

a\,q(x)=(ax_1+bx_2)^2+(ac-b^2)x_2^2

a>0,\ ac-b^2>0,\ a\,q(x)=(ax_1+bx_2)^2+(ac-b^2)x_2^2

a\,q(x)\ge 0\ \Rightarrow\ q(x)\ge 0

q(x)=0

x_2=0\ \land\ x_1=0,\ \text{so}\ x\neq0\Rightarrow q(x)>0

x=e_1=(1,0)\neq0

q(e_1)=a>0

x=(-b,a)\neq0

q(-b,a)=ab^2-2ab^2+ca^2=a(ac-b^2)>0\ \Rightarrow\ ac-b^2>0

逐步反向審查

• S15 · sufficient_goal_reduction · S09, S12, S13, S14, and_intro_elim — 目標是四項判定的合取；各項由所行步驟正向證得，H⇒G 由合取引入。
• S14 · premise_audit · quantifier_negation, matrix_product_def — 一對反例否定全稱對稱性（N9）。
• S13 · premise_audit · S11, contrapositive, numeric_evaluation — 見證 (1,−1)≠0 而 q_P=0（N8）。
• S12 · premise_audit · S11, contrapositive, numeric_evaluation — 一個負值見證就否定正定（N7）；不需要行舉其他向量。
• S11.2 · premise_audit · S11.1, forall_elim, order_basics — 需要 S11.1 的 a>0，才能保證 (−b,a)≠0 並除以 a。
• S11.1 · premise_audit · forall_elim, mul_zero — 只用正定假設的一個特例。
• S11 · premise_audit · L_sylvester_nec — 與 S07 合起來給出等價；本步只用必要方向。
• S10 · premise_audit · S02, numeric_evaluation — 可由 N5 重算；有限個值不能取代 S07 的全稱證書（見錯誤控制）。
• S09 · sufficient_goal_reduction · S01, S03, S04, S05, S07, and_intro_elim — 目標 G：內積。足夠條件 H：三項責任；H⇒G 由 S01。H 由 G2 正向證得，沒有用到 G，也沒有用到向量樣本。
• S08 · inverse_equivalence · S07.1, numeric_evaluation — 多項式恆等式（N4），雙向成立。
• S07.3 · premise_audit · zero_product, square_nonneg, contrapositive — 「非負數之和為 0 ⇒ 各項為 0」與零積性質；兩個嚴格條件都用到。
• S07.2 · premise_audit · square_nonneg, order_basics — 需要 a>0 才能除以 a 而不翻轉不等號；不宣稱反向。
• S07.1 · inverse_equivalence · distributive, power_laws — 多項式恆等式，兩邊同值。
• S07 · premise_audit · S06, L_sylvester_suff, numeric_evaluation — 需要兩個嚴格不等式；若 ac−b²=0（見 S13）結論就不成立。
• S06 · premise_audit · S02, def_intro — 只命名與合併同類項；之後的正定判斷都在 q 上進行。
• S05 · premise_audit · mul_comm, G2 — 條件 M_{12}=M_{21} 不可省略：S14 的 R 違反它，形式就不對稱（N2 以恆等式核對本步）。
• S04 · inverse_equivalence · distributive, mul_assoc, mul_comm — 恆等式，雙向成立。
• S03 · inverse_equivalence · distributive, mul_assoc, mul_comm — 所用都是實數恆等式，兩邊同值，雙向成立。
• S02 · inverse_equivalence · matrix_product_def, distributive — 展開是恆等式；反向把四項重組回 xᵀMy，兩邊同值。
• S01 · premise_audit · mko_ips_def — 只展開定義，不推出新事實。

錯誤控制與反例

對稱雙線性或半正定都不夠

MKO 指出的誤解是把對稱雙線性形式或半正定形式直接叫內積。N 與 P 都對稱雙線性；N 在 (1,−1) 取負值，P 在非零的 (1,−1) 取 0。內積要求每個非零向量嚴格為正。

向量樣本不證正定

N 的二次型在 (1,0)、(0,1)、(1,1) 的值是 1、1、6，全為正，抽樣會誤判為正定；但 q_N(1,−1)=−2。正定必須由全稱證書建立：配方恆等式加 Sylvester 條件（S07）。

對角元為正不夠

N 的對角元 1、1 都為正，只滿足第一個條件 a>0；行行式 ac−b²=−3 才揭露它不正定。2×2 時兩個條件缺一不可（S11 證明兩者都是必要的）。

• N 的二次型在 (1,0)、(0,1)、(1,1) 都為正，所以 ⟨·,·⟩_N 是內積 → reject — q_N(1,−1)=1−4+1=−2<0。
• P 對稱且 q_P≥0，所以 ⟨·,·⟩_P 是內積 → reject — q_P(1,−1)=0 而 (1,−1)≠0，只是半正定。
• xᵀRy 雙線性且對角元為正，所以是內積 → reject — ⟨e₁,e₂⟩_R=1 但 ⟨e₂,e₁⟩_R=0，不對稱。
• 對角元都為正的 2×2 對稱矩陣必定正定 → reject — N 的對角元為 1、1，但行行式 −3，q_N(−2,1)=−3。

結論與限制

⟨x,y⟩_M=2x₁y₁+x₁y₂+x₂y₁+3x₂y₂ 對兩槽雙線性、對稱，且 2q(x)=(2x₁+x₂)²+5x₂² 只在 x=0 時為 0，Sylvester 條件 a=2>0、ac−b²=5>0 給出全稱正定證書，所以 (ℝ²,⟨·,·⟩_M) 是實內積空間。對 2×2 對稱矩陣，Sylvester 條件是正定的充要條件。N（行行式 −3，q_N(−2,1)=−3）、P（行行式 0，q_P(1,−1)=0）、R（不對稱）都不給出內積。

• MKO 提醒內積空間不自動完備；ℝ² 本身是完備的，但本稿不處理完備性或 Hilbert 空間。
• Sylvester 判準只對 2×2 完整證明；n×n 的一般形式不在本稿範圍內。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: d02e546e2588353f6bbb496de2a5d6006b38b2adc1288620b1b7141c8175932f
• original source SHA-256: b8b97eaec9185806e2d7a87378d14b180297a8ad4a22308761b5db72c6a6627c
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）