# 用一致性求完整像空間

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

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

derivation-mko-linear-map-image-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

im T=span{(1,2)}；(3,6)在像內，(0,1)不在像內。

精確2×2線性系統的全實數像，不以有限輸入清單當range。





## 已知條件與符號


- calc


- G1 — T:R²→R²，A=[[1,2],[2,4]]，c₁=(1,2)，c₂=(2,4)。


- c_1,c_2 — 矩陣columns
- u,v — 任意目標座標





## 規則與來源

本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。


- calc · prerequisite — 假設通常實數域與座標向量運算、矩陣乘法、線性獨立及生成的定義；所用消去均為可逆初等列運算。
- mko_definition · cited — 本輪用精確 2×2 矩陣與 symbolic column-span certificate。membership 以 Ax=y 的精確一致性判定；bounded fiber 只提供 witness 或 bounded nonexistence，不可證全 R² 非 membership。像（image，亦常稱 range）不得與宣告陪域（codomain）或有限抽樣的輸出清單混同。 · mko-linear-map-image





## 逐步主鏈

S01 · implies操作前

A\binom{x}{y}

操作後

x\binom{1}{2}+y\binom{2}{4}

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

矩陣輸出為columns的任意實線性組合，因此像包含於column span。



S02 · implies操作前

z=xc_1+yc_2

操作後

z=T(x,y)\Rightarrow\operatorname{span}\{c_1,c_2\}\subseteq\operatorname{im}T

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

任何column線性組合都由同一係數作輸入得到，證反向包含。



S03 · implies操作前

c_2=2c_1

操作後

T(x,y)=(x+2y)c_1

條件：無

規則：calc · 依賴：G1, S01, S02

葉節點依據：calc

兩columns成比例，把任意輸出縮成單一參數s=x+2y。



S04 · implies操作前

s\in\mathbb R

操作後

T(s,0)=(s,2s),\quad\operatorname{im}T=\{(s,2s):s\in\mathbb R\}

條件：無

規則：mko_definition · 依賴：G1, S03

葉節點依據：mko_definition

明示全稱前像證每個此形向量都可到達。



S05 · equivalent操作前

A\binom{x}{y}=\binom{u}{v}

操作後

x+2y=u,\quad 2x+4y=v\iff v=2u

條件：無

規則：calc · 依賴：G1, S01, S04

葉節點依據：calc

第二方程減兩倍第一方程得必要條件；若v=2u則x=u,y=0給解，亦充分。



S06 · implies操作前

(u,v)=(3,6)

操作後

6=2\cdot3,\quad T(3,0)=(3,6)

條件：無

規則：calc · 依賴：G1, S05

葉節點依據：calc

一致性成立且有精確前像(3,0)，認證membership。



S07 · implies操作前

(u,v)=(0,1)

操作後

1\ne2\cdot0\Rightarrow(0,1)\notin\operatorname{im}T

條件：無

規則：calc · 依賴：G1, S05

葉節點依據：calc

全實數一致性失敗，故真非membership，不僅是某盒內無解。



S08 · implies操作前

|x|,|y|\le1,\quad x,y\in\mathbb Z

操作後

-3\le x+2y\le3,\quad(100,200)=T(100,0)\in\operatorname{im}T

條件：無

規則：calc · 依賴：G1, S04, S05

葉節點依據：calc

小盒漏掉(100,200)，但它仍有全域前像，示範搜尋界線。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S04, S05 — bounded無解不能代替S05的符號判準。
- S07 · premise_audit · G1, S05 — 矛盾1=0排除所有實輸入。
- S06 · premise_audit · G1, S05 — 前像非唯一；加任意t(−2,1)仍輸出(3,6)。
- S05 · inverse_equivalence · G1, S01, S04 — 兩方向均證，並非有限搜尋未命中的推斷。
- S04 · premise_audit · G1, S03 — 像只是R²內直線，不等於宣告codomain R²。
- S03 · premise_audit · G1, S01, S02 — s可任意實數，因可選x=s,y=0。
- S02 · premise_audit · G1, S01 — 兩包含合起來才得完整像，而非下界。
- S01 · premise_audit · G1 — 係數x、y可取全部實數，不能只看columns本身。





## 錯誤控制與反例

像與陪域以Ax=y一致性分類，不由T:R²→R²猜滿射。

盒界線有限搜尋否定只適用已宣告輸入盒。


- codomain R²等於image。 → reject — (0,1)不滿足v=2u。
- 兩個columns便是全部像元素。 → reject — 任意實倍數s(1,2)都是輸出，例如(3,6)。
- 小盒找不到(100,200)表示非membership。 → reject — (100,0)是明示全域前像。





## 結論與限制

im T=span{(1,2)}；(3,6)在像內，(0,1)不在像內。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: b01b892b391c388da6d5e1fa97da0a688e710e364c061e305952d03b4ff25546
- original source SHA-256: 841d6adb1aa0065b3f001c0945ad4d8276511c210c6df28756fc85df02fed2aa
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-linear-map-image-01.json)