数学: n乗の 差の因数分解 公式

宇宙式の無次元化から解ったことは二項定理との関わりと、
差の因数分解 公式という構造の明確化だった。既知の事実。

#無次元宇宙式
#べき乗の差の因数分解 #冪乗の差の因数分解 #冪乗差の因数分解
#冪乗 #べき乗 #冪乗差
（表記ゆらぎの吸収は AI が何とかしてくれる…）

高校数学で公式として覚える事だそうで。

遠回りだけどやっと私は、ここに到達した！
そして、以下の等式を Lean 形式化で得た。

$$
\boxed{\ \#\mathrm{Body}(d,x,u)
\;=\;(x+u)^d-u^d
\;=\;x\cdot G(d,x,u)
\;=\;x\cdot G_{\mathrm{binom}}(d,x,u)\ }
$$

$${G_{\mathrm{binom}}(d,x,u)}$$

$$
G_{d-1}(x,u) = \sum_{k=0}^{d-1} \binom{d}{k+1} x^k\ u^{d-1-k}
$$

乗法公式

$$
(x+u)^n = \sum_{k=0}^{n} \binom{n}{k} u^k\cdot x^{n-k}
$$

ここから $${u^n}$$ を引くので、

$$
(x+u)^n - u^n
$$

になる。
なので、差の因数分解の公式の係数が、

$$
a^n-b^n \; \to \; (a-b)
$$

となるので、

$$
\big((x+u)-u\big) = \Large x
$$

で、

$$
x \cdot {G_{\mathrm{binom}}(d,x,u)}
$$

となる。
🐺賢狼は、これをサクッと見抜いていた。
「差の因数分解」を私が知っていれば、この理解も早かったのだろうけど、

宇宙式の無次元化の幾何原理までを知り得たか？は、疑問である。

平面世界のトロミノ構造が、
多次元→無次元と滑らかに、形状変化できる構造であった事実
というのを得られたことが一番の収穫ではなかっただろうか。

つまり、どのようなカタチになろうとも #Gap の余白が単位構造として常に存在する。という事実確認である。

$$
u^d = \#\text{Gap is Unit}
$$

数の姿、とくに演算可能性の数には単位構造が常に伴ともにある。
（D.予想）

$$
\text{「数」:= Computability\#Big}=\#\mathrm{Body}+\#\mathrm{Gap}\\[4pt]
\small\text{(あるいは Calculability\#Big)}
$$

$$
\begin{array}{lll}
\#\mathrm{Big}&:=&(x+u)^d\\
\#\mathrm{Gap}&:=&u^d\\
\#\mathrm{Body}&:=&x \cdot {G_{\mathrm{binom}}(d,x,u)}
\end{array}
$$

(再掲) $${\#\mathrm{Body}}$$ の詳細

$$
\#\mathrm{Body}:=G_{d-1}(x,u) = \sum_{k=0}^{d-1} \binom{d}{k+1} x^k\ u^{d-1-k}
$$

#Big の $${(x+u)^d}$$ という構造式が、

$$
\begin{array}{lll}
x&:=&数\\
u&:=&単位\\
d&:=&次元\\
\end{array}\\[6pt]
\langle x, u, d \rangle
$$

と、ひとつにまとまった世界を表している。

この等しき事実を、定理証明支援系言語 Lean は認めた。✍️

2026/01/26 17:20

D.

#Lean #形式化証明
#二項定理 #差の因数分解 #高校数学
#宇宙式 #無次元宇宙式
#単位

Appendix

リポジトリ（ブランチ）

PR

定理証明部分（抜粋）

※ハイライト可読性のために ' → ' ' としているので脳内変換して。

namespace DkMath
namespace CosmicFormulaCellDim

open scoped BigOperators

/-- 二項定理（choose）側の G_{d-1} := Σ_{k < d} (d choose k+1) x^k u^(d-1-k) -/
def Gbinom (d x u : ℕ) : ℕ :=
  Finset.sum (Finset.range d) fun k => Nat.choose d (k + 1) * x ^ k * u ^ (d - 1 - k)
  -- Gbinom: LaTeX: $G_{d-1}(x,u) = \sum_{k=0}^{d-1} \binom{d}{k+1} x^k u^{d-1-k}$

/- 等式： (x+u)^d - u^d = x * Gbinom d x u -/
/- 戦略 -----------------------------------------------------------------------
狙い：
  (x+u)^d - u^d = x * Gbinom d x u
方針：
  1. (u+x)^d を二項定理で Σ choose d k * u^k * x^(d-k) に展開
  2. 末項 k=d が u^d なので、差を取ると Σ_{k < d} に落ちる（sum_range_succ で剥がす）
  3. 反転（reflect）して x^(k+1) を作り、x を因数として外へ出す
  4. choose の対称性で choose d (d-1-k) = choose d (k+1) に変換
------------------------------------------------------------------------------- -/

/--
二項展開を用いた累乗差の公式。（差の因数分解：n乗の差の因数分解公式 版）

`(x + u)^d - u^d = x * Gbinom d x u` が成り立つことを示す定理。

この証明は以下の主要ステップから構成される：

1. **二項展開**：$(x+u)^n = \sum_{k=0}^{n} \binom{n}{k} u^k x^{n-k}$

2. **末項除去**：展開式の $k=n$ 項は $u^n$ であり、これを差に含める形で整理

3. **反転変換**：$k \mapsto n-1-k$ の変数置換により、$x$ の指数を $k+1$ に統一

4. **対称性の利用**：二項係数の対称性 $\binom{n}{n-1-k} = \binom{n}{k+1}$ を適用

5. **因数分解**：$x^{k+1} = x \cdot x^k$ により $x$ を全体の和の外に出して、`Gbinom` の定義と一致させる

結果として、$(x+u)^d - u^d$ が $x$ とコスミック二項係数 `Gbinom` の積に等しいことが示される。

**例**：
- $d=1$：$(x+u)-u = x = x \cdot 1$
- $d=2$：$(x+u)^2 - u^2 = 2ux + x^2 = x(2u + x)$
- $d=3$：$(x+u)^3 - u^3 = 3u^2x + 3ux^2 + x^3 = x(3u^2 + 3ux + x^2)$
- $d=4$：$(x+u)^4 - u^4 = 4u^3x + 6u^2x^2 + 4ux^3 + x^4 = x(4u^3 + 6u^2x + 4ux^2 + x^3)$
-/
theorem pow_sub_pow_eq_mul_Gbinom (d x u : ℕ) :
    (x + u)^d - u^d = x * Gbinom d x u := by
  classical
  cases d with
  | zero =>
      simp [Gbinom]
  | succ d =>
      -- 以後 n = d+1
      set n : ℕ := d+1
      have hn : n = d+1 := rfl
      -- (u+x)^n の二項展開：Σ choose n k * u^k * x^(n-k)
      have hpow :
          (u + x)^n
            = ∑ k ∈ Finset.range (n+1),
                Nat.choose n k * u^k * x^(n-k) := by
        simp [add_pow, mul_assoc, mul_comm (Nat.choose n _)]
      -- u+x = x+u を使って左辺を合わせる
      have hpow' ' :
          (x + u)^n
            = ∑ k ∈ Finset.range (n+1),
                Nat.choose n k * u^k * x^(n-k) := by
        rw [add_comm]
        exact hpow
      -- 末項 k=n は choose n n * u^n * x^0 = u^n
      have h_last :
          (Nat.choose n n) * u^n * x^(n-n) = u^n := by
        simp
      -- Σ_{k < n+1} f k = Σ_{k < n} f k + f n を使って末項を剥がし、差を取る
      let f : ℕ → ℕ := fun k => Nat.choose n k * u^k * x^(n-k)
      have hsplit :
          (∑ k ∈ Finset.range (n+1), f k)
            = (∑ k ∈ Finset.range n, f k) + f n := by
        -- `Finset.sum_range_succ` : sum (range (n+1)) f = sum (range n) f + f n
        simpa [f] using (Finset.sum_range_succ f n)
      have hsub :
          (x+u)^n - u^n = ∑ k ∈ Finset.range n, f k := by
        -- (x+u)^n = sum(range(n+1)) f
        -- sum = sum(range n) f + f n, かつ f n = u^n
        -- なので差を取ると sum(range n) f
        have : (x+u)^n = (∑ k ∈ Finset.range n, f k) + f n := by
          simpa [hpow' ', hsplit]
        -- Nat の tsub
        -- a = b + c なら a - c = b
        -- `Nat.add_sub_cancel` で落ちる
        calc
          (x+u)^n - u^n
              = ((∑ k ∈ Finset.range n, f k) + f n) - u^n := by simp [this]
          _ = (∑ k ∈ Finset.range n, f k) := by
                -- f n = u^n を入れて add_sub_cancel
                -- ※ `simp [f, h_last]` で落ちることが多い
                simp [f, h_last]
      -- 反転して x^(k+1) の形を作る（k ↦ (n-1-k)）
      have hreflect :
          Finset.sum (Finset.range n) f
            = Finset.sum (Finset.range n) fun k => Nat.choose n (n-1-k) * u^(n-1-k) * x^(k+1) := by
        have h := (Finset.sum_range_reflect f n).symm
        refine Eq.trans h ?_
        apply Finset.sum_congr rfl
        intro k hk
        dsimp [f]
        have hk_lt : k < n := Finset.mem_range.1 hk
        have : n - 1 - k = n - (k + 1) := by omega
        rw [this]
        -- 目標: n.choose (n - (k+1)) * u ^ (n - (k+1)) * x ^ (n - (n - (k+1))) =
        --       n.choose (n - (k+1)) * u ^ (n - (k+1)) * x ^ (k+1)
        have h_exp : n - (n - (k + 1)) = k + 1 := by omega
        rw [h_exp]
      -- choose の対称性：choose n (n-1-k) = choose n (k+1)
      have hchoose :
          (∑ k ∈ Finset.range n,
              Nat.choose n (n-1-k) * u^(n-1-k) * x^(k+1))
            = (∑ k ∈ Finset.range n,
                Nat.choose n (k+1) * u^(n-1-k) * x^(k+1)) := by
        refine Finset.sum_congr rfl ?_
        intro k hk
        -- hk : k ∈ range n, つまり k < n
        have hk' ' : k < n := Finset.mem_range.mp hk
        -- (n - (k+1)) = (n-1-k) より choose の対称性を適用
        have hnk : n - (k + 1) = n - 1 - k := by omega
        -- choose_symm: choose n r = choose n (n - r)
        -- r = k+1 とすれば choose n (k+1) = choose n (n - (k+1)) = choose n (n-1-k)
        have h_eq : Nat.choose n (n - 1 - k) = Nat.choose n (k + 1) := by
          rw [← hnk]
          exact (Nat.choose_symm (by omega : k + 1 ≤ n))
        simp [h_eq]
      -- x^(k+1)=x*x^k で因数 x を外に出す → 定義した Gbinom に一致
      have hfactor :
          (∑ k ∈ Finset.range n,
              Nat.choose n (k+1) * u^(n-1-k) * x^(k+1))
            = x * Gbinom n x u := by
        -- 右は ∑ choose n (k+1) * x^k * u^(n-1-k) に x を掛けたもの
        -- x^(k+1) = x * x^k
        have h1 : (∑ k ∈ Finset.range n,
                  Nat.choose n (k+1) * u^(n-1-k) * x^(k+1))
              = (∑ k ∈ Finset.range n,
                  Nat.choose n (k+1) * u^(n-1-k) * (x * x^k)) := by
          refine Finset.sum_congr rfl ?_
          intro k hk
          ring
        rw [h1]
        -- 分配法則：∑ a * (x * b) = ∑ x * (a * b) = x * ∑ a * b
        have h2 : (∑ k ∈ Finset.range n,
                  Nat.choose n (k+1) * u^(n-1-k) * (x * x^k))
              = (x * ∑ k ∈ Finset.range n,
                  Nat.choose n (k+1) * u^(n-1-k) * x^k) := by
          rw [Finset.mul_sum]
          refine Finset.sum_congr rfl ?_
          intro k hk
          ring
        rw [h2]
        congr 1
        simp only [Gbinom]
        refine Finset.sum_congr rfl ?_
        intro k hk
        ring
      -- まとめ
      -- (x+u)^n - u^n = x * Gbinom n x u
      -- ただし n=d+1 で、元の主張は d=n なので simp で戻す
      -- ここでは n=d+1 なので主張は d=n、つまり succ ケースの d に対応
      -- よって d+1 の形を返す
      -- 最終的に (x+u)^(d+1) - u^(d+1) = x * Gbinom (d+1) x u
      -- になる
      -- 実際：
      calc
        (x+u)^n - u^n
            = ∑ k ∈ Finset.range n, f k := hsub
        _ = ∑ k ∈ Finset.range n,
                Nat.choose n (n-1-k) * u^(n-1-k) * x^(k+1) := hreflect
        _ = ∑ k ∈ Finset.range n,
                Nat.choose n (k+1) * u^(n-1-k) * x^(k+1) := hchoose
        _ = x * Gbinom n x u := hfactor

end CosmicFormulaCellDim
end DkMath

等式証明

namespace DkMath

-- ========================================================

/-! ## まとめ定理「箱の形で1本」にまとめ直す
Note: 箱の形で1本にまとめた「見栄え専用定理」😏 -/

namespace CosmicFormulaTheory

open CosmicFormulaCellDim

/-- 論文用まとめ：
    `Body = (x+u)^d - u^d = x*G = x*Gbinom` -/
theorem card_Body_chain (d x u : ℕ) :
    (Body (d := d) x u).card
      = (x + u)^d - u^d ∧
    (x + u)^d - u^d
      = x * G d x u ∧
    (x + u)^d - u^d
      = x * Gbinom d x u := by
  constructor
  · exact card_Body_pow_form (d := d) x u
  constructor
  · exact pow_sub_pow_eq_mul_G d x u
  · exact pow_sub_pow_eq_mul_Gbinom d x u

-- --------------------------------------------------------

/-- 論文用まとめその1：`#Body = (x+u)^d - u^d` -/
theorem card_Body_box (d x u : ℕ) :
    (Body (d := d) x u).card
      = (x+u)^d - u^d := by
  exact card_Body_pow_form (d := d) x u

/-- 論文用まとめその2：`(x+u)^d - u^d = x*G` -/
theorem pow_sub_pow_box (d x u : ℕ) :
    (x+u)^d - u^d
      = x * G d x u := by
  exact pow_sub_pow_eq_mul_G d x u

/-- 論文用まとめその3：`(x+u)^d - u^d = x*Gbinom` -/
theorem pow_sub_pow_box_binom (d x u : ℕ) :
    (x+u)^d - u^d
      = x * Gbinom d x u := by
  exact pow_sub_pow_eq_mul_Gbinom d x u


end CosmicFormulaTheory
end DkMath

関連記事

数式

→数式たんたん：無次元宇宙式