以全稱封閉認證過原點直線

目標與範圍

U={(x,2x):x∈R}是R²子空間，仿射平移U+(0,1)不是。

R²中齊次直線、零空間、全空間及明示反例；不用有限抽樣證正例。

已知條件與符號

• calc
• subspace_def

• G1 — V=R²，U={(x,y):y−2x=0}，採通常向量加法與所有實純量。

• U — 齊次直線
• \lambda — 任意實純量

規則與來源

• calc · prerequisite — 假設通常實數域與座標向量運算、矩陣乘法、線性獨立及生成的定義；所用消去均為可逆初等列運算。
• mko_definition · cited — 本輪只處理R²中的零空間、全空間、過原點直線與明示有限反例。正例使用齊次線性方程或span的全稱代數證書；有限抽樣通過不足以證子空間。 · mko-vector-subspace
• subspace_def · prerequisite — 實向量空間V的子集U若含零且對加法及每個實純量封閉，則在限制運算下為子空間；其餘向量法則由V繼承。

逐步主鏈

(x,y)\in U

y=2x\iff(x,y)=x(1,2)

0\in\mathbb R

(0,0)=0(1,2)\in U

u=a(1,2),\ v=b(1,2),\quad a,b\in\mathbb R

u+v=(a+b)(1,2)\in U

u=a(1,2),\quad\lambda\in\mathbb R

\lambda u=(\lambda a)(1,2)\in U

0\in U,\quad U+U\subseteq U,\quad\mathbb R U\subseteq U

U\le\mathbb R^2

Z=\{(0,0)\},\quad V=\mathbb R^2

Z+Z=Z,\ \lambda Z\subseteq Z;\quad V+V\subseteq V,\ \lambda V\subseteq V

A=\{(x,y):y=2x+1\}

(0,0)\notin A

B=\{(x,0):x\in\mathbb R\}\cup\{(0,y):y\in\mathbb R\}

(1,0),(0,1)\in B,\quad(1,1)\notin B

局部子步與引理

本稿無局部子步。

逐步反向審查

• S08 · premise_audit · G1, S03 — 一個明示反例足以否證全稱封閉；有限正例不足以證明。
• S07 · premise_audit · G1, S02 — (0,1)在A但0·(0,1)不在A，也給直接純量封閉反例。
• S06 · premise_audit · G1 — 兩者皆含零，但這裡也另核加法與全部純量。
• S05 · premise_audit · G1, S02, S03, S04 — 證書固定通常運算；不同運算不能沿用。
• S04 · premise_audit · G1, S01 — λ無任何有界或整數限制，只核λ=2不夠。
• S03 · premise_audit · G1, S01 — a、b全稱量化，不能以兩個數值例子替代。
• S02 · premise_audit · G1, S01 — 含零只是必要條件，還未證封閉。
• S01 · inverse_equivalence · G1 — 反代x(1,2)給2x−2x=0，兩方向成立。

錯誤控制與反例

全稱純量

必須對每個λ∈R證封閉，不能只核整數。

齊次性

y−2x=0含零；常數換成1便是不同仿射集合。

• y=2x+1的直線也是子空間。 → reject — 不含(0,0)。
• 含零且對整數倍封閉就夠。 → reject — Z²對加法及整數倍封閉，但(1/2)(1,0)不在Z²。
• 兩個子空間的聯集必是子空間。 → reject — 兩座標軸的聯集不含(1,0)+(0,1)=(1,1)。

結論與限制

U={(x,2x):x∈R}是R²子空間，仿射平移U+(0,1)不是。

驗證及來源綁定

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

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: 866398e5461531188f4557b3cabd302424ab3b6911d677de331ab220569bbdb6
• original source SHA-256: 866398e5461531188f4557b3cabd302424ab3b6911d677de331ab220569bbdb6
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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