描述統計：保留重數計算平均數、中位數、全距與眾數集合

目標與範圍

對觀測列 D=(4,10,1,3,8,1,6,3)，保留重複值，求觀測數 n、算術平均、中位數、全距與本輪約定的眾數集合；證明一般性質「最小值 ≤ 平均 ≤ 最大值」並用它核對；最後說明若先去重會得到不同（錯誤）的平均與中位數。

只處理非空有限的整數觀測列與 MKO 定義的四個摘要；完整證明平均數介於最小值與最大值之間。不處理樣本變異數、其他分位數或圖表，不從摘要推論母體、機率律或因果，也不否定其他教材「無眾數」的用語；不改動 canonical MKO 或英文 edition。

已知條件與符號

• numeric_evaluation
• finite_sum_rules
• frac_rules
• order_basics
• finite_counting_basics

• G1 — D=(4,10,1,3,8,1,6,3) 是原創合成的整數觀測列；它是列表，保留順序與重複值，不是去重集合（MKO 假設 a1、a2）。
• G2 — 眾數集合約定：所有出現次數達最大值的數，按遞增列出、每值一次（MKO 陳述與假設 a3）。
• G3 — 本題只作描述摘要，不假定 D 是某母體的獨立樣本（MKO 假設 a3）。

• D=(d_i)_{i=1}^{n} — 保留順序與重數的觀測列
• n — 觀測數
• \bar d — 算術平均
• s_{(k)} — 排序後第 k 個值
• f(v) — 值 v 在 D 中出現的次數
• m,\ M — 最小值與最大值

規則與來源

• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• 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。
• frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠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。
• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_descstat_def · cited — 給非空有限實數觀測列 D，算術平均為 Σdi/n；排序後奇數 n 的中位數是中央值，偶數 n 是中間兩值的平均；全距為最大值減最小值。本輪眾數集合約定為所有出現頻率達最大值的數，按遞增列出；各數均只出現一次時，全部不同觀測值都是此約定的頻率最大者。 · mko-descriptive-statistics
• perm_invariance · prerequisite — 重新排列有限列表的項不改變其和，也不改變每個值的出現次數（有限和的一般交換律，可由 add_assoc、add_comm 歸納得到）。
• L_mean_bounds · lemma — 對非空有限實數列 (d_i)_{i=1}^{n}，若 m≤d_i≤M 對每個 i 成立，則 m≤(Σd_i)/n≤M。

逐步主鏈

D=(d_i)_{i=1}^{n},\ n>0

\bar d=\tfrac{1}{n}\sum_{i=1}^{n}d_i,\ \tilde d,\ R=\max D-\min D,\ \operatorname{Mo}(D)

D=(4,10,1,3,8,1,6,3)

n=8>0

\sum_{i=1}^{8}d_i

4+10+1+3+8+1+6+3=36

\bar d=\tfrac{36}{8}

\bar d=\tfrac{9}{2}

(4,10,1,3,8,1,6,3)

(s_{(k)})_{k=1}^{8}=(1,1,3,3,4,6,8,10)

\tilde d,\ n=8\ \text{even}

\tilde d=\tfrac{s_{(4)}+s_{(5)}}{2}=\tfrac{3+4}{2}=\tfrac{7}{2}

R=\max D-\min D

R=10-1=9

f(v)\ \text{for } v\in\{1,3,4,6,8,10\}

f(1)=2,\ f(3)=2,\ f(4)=f(6)=f(8)=f(10)=1

\max_v f(v)=2

\operatorname{Mo}(D)=\{1,3\}

1\le d_i\le 10\ \text{for every } i

1\le \tfrac{9}{2}\le 10

\bar d=\tfrac{9}{2},\ \tilde d=\tfrac{7}{2}

\bar d\notin D,\ \tilde d\notin D

\{1,3,4,6,8,10\}\ \text{(deduplicated)}

\tfrac{32}{6}=\tfrac{16}{3}\neq\tfrac{9}{2},\quad \tfrac{4+6}{2}=5\neq\tfrac{7}{2}

\text{tasks of the goal}

n=8,\ \bar d=\tfrac{9}{2},\ \tilde d=\tfrac{7}{2},\ R=9,\ \operatorname{Mo}(D)=\{1,3\}

局部子步與引理

m\le d_i\ \text{for every } i

nm=\sum_{i=1}^{n}m\le\sum_{i=1}^{n}d_i

nm\le\sum_{i=1}^{n}d_i,\ n>0

m\le\tfrac{1}{n}\sum_{i=1}^{n}d_i=\bar d

d_i\le M\ \text{for every } i

\bar d\le M

逐步反向審查

• S13 · sufficient_goal_reduction · S02, S04, S06, S07, S09, S10, S12 — 目標 G：題目要求的各摘要與核對。足夠條件 H：S02 到 S12 的結論；H⇒G 只用合取。H 由 G1 到 G3 正向推出，沒有把 G 當作前提。
• S12 · premise_audit · S04, S06, numeric_evaluation — 反例只需要一組具體數字（N12 到 N14）；它說明去重一般不保持平均與中位數。
• S11 · premise_audit · S04, S06, divides_def — 只宣稱這兩個摘要不在 D 中；不宣稱平均或中位數一般不能是觀測值。
• S10.3 · premise_audit · S10.1, S10.2, order_basics — 同樣需要逐項上界與 n>0。
• S10.2 · premise_audit · S10.1, order_basics, mul_inverse_nonzero — 必須 n>0：乘負數會反向，n=0 時平均無定義。
• S10.1 · premise_audit · finite_sum_rules, order_basics, nat_induction — 需要每一項都滿足 m≤d_i；只要有一項小於 m，結論可能失敗。不宣稱反向。
• S10 · premise_audit · L_mean_bounds, S07 — 引理需要 n>0 與逐項的上下界；不宣稱反向，即落在 [1,10] 的數不一定是平均。
• S09 · premise_audit · S08, G2, mko_descstat_def — 需要完整的頻率表；只看第一個達到最大頻率的值會漏掉 3。
• S08 · premise_audit · finite_counting_basics, S02 — 頻率總和等於 n 是必要核對（N8）；不宣稱頻率表能還原原本的順序。
• S07 · inverse_equivalence · mko_descstat_def, numeric_evaluation — 精確計算（N7），雙向成立。
• S06 · inverse_equivalence · mko_descstat_def, numeric_evaluation — 依定義展開後是精確計算（N6），雙向成立；位置必須取自排序後的列表。
• S05 · premise_audit · perm_invariance, finite_counting_basics — 需要的是每個值的出現次數相同（N5、N8）；排序後的列表一般不等於原列表，所以只宣稱「同一組觀測」，不宣稱兩列表相等。
• S04 · inverse_equivalence · frac_rules, numeric_evaluation — 反向：分子分母同乘 4 回到 36/8；需要 8≠0 與 4≠0。
• S03 · inverse_equivalence · finite_sum_rules, numeric_evaluation — 精確整數計算（N1），可獨立重算，雙向成立。
• S02 · premise_audit · G1, finite_counting_basics — 計的是列表位置，不是不同值；這正是 MKO 假設 a1 的要求。
• S01 · premise_audit · G1, G2, mko_descstat_def — 此步只寫出定義，不推出新事實；n>0 是平均有定義的前提。

錯誤控制與反例

不要先去重

MKO 的誤解之一是先去重再算。去重後平均變成 16/3、中位數變成 5（S12），都不是 D 的摘要。重複值是資料的一部分：兩個 1 表示有兩筆觀測等於 1。

並列的最大頻率都要列入

1 與 3 都出現 2 次，眾數集合是 {1,3}，不是 {1}。若所有值都只出現一次，依本輪約定全部不同值都在眾數集合中；其他教材可能稱為「無眾數」，這是用語慣例不同，不是矛盾（MKO 假設 a3）。

中位數要在排序後取

未排序的 D 第 4、5 項是 3 與 8，平均 11/2，這不是中位數。必須先排序得 (1,1,3,3,4,6,8,10)，再取第 4、5 項 3 與 4，得 7/2（S06）。

• 中位數是 D 的第 4、5 項的平均 (3+8)/2=11/2 → reject — 中位數要在排序後取；排序後第 4、5 項是 3 與 4，中位數 7/2。
• 平均是 (1+3+4+6+8+10)/6=16/3 → reject — 這是去重後的平均；保留重數得 36/8=9/2。
• 眾數集合是 {1} → reject — 3 也出現 2 次，達到最大頻率；眾數集合是 {1,3}。
• D 的平均是 9/2，所以產生 D 的母體平均也是 9/2 → reject — 描述摘要只描述 D，本題沒有母體或抽樣模型（MKO 假設 a3）。

結論與限制

對 D=(4,10,1,3,8,1,6,3)：n=8，平均 36/8=9/2，排序後中位數 (3+4)/2=7/2，全距 10−1=9，眾數集合 {1,3}；且 1≤9/2≤10。若先去重會誤得平均 16/3、中位數 5。這些摘要只描述 D，不構成任何母體推論。

• perm_invariance（有限和的一般交換律與排序保留頻率）作為前提使用，未在本稿證明。
• 樣本變異數、其他分位數、圖表與機率矩不在本稿範圍；描述摘要與機率期望的型別區別保留給後續切片。
• MKO 的 formal next（有限列表求和、排序中位與頻數最大集合的橋接）未做。

驗證及來源綁定

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

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

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