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

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-vector-subspace/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-vector-subspace-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

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繼承。





## 逐步主鏈

S01 · equivalent操作前

(x,y)\in U

操作後

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

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

解齊次方程得到完整參數化，不是只找到若干點。



S02 · implies操作前

0\in\mathbb R

操作後

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

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

取參數0證含零向量，因而非空。



S03 · implies操作前

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

操作後

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

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

任意兩元素之和仍為同一生成向量的實倍數。



S04 · implies操作前

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

操作後

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

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

任意實純量乘法保持參數化，包含非整數與負純量。



S05 · implies操作前

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

操作後

U\le\mathbb R^2

條件：無

規則：subspace_def · 依賴：G1, S02, S03, S04

葉節點依據：subspace_def

三項責任均以全稱代數完成，故U為子空間；其餘向量法則由R²限制。



S06 · implies操作前

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

操作後

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

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

零空間只有零，閉性直接成立；全空間因實數和積仍實也封閉。



S07 · implies操作前

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

操作後

(0,0)\notin A

條件：無

規則：calc · 依賴：G1, S02

葉節點依據：calc

仿射平移直線不含零，立刻否證子空間。



S08 · implies操作前

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

條件：無

規則：calc · 依賴：G1, S03

葉節點依據：calc

兩座標軸聯集雖含零且各軸封閉，聯集不對加法封閉。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-vector-subspace-01.json)