Lean4: 宇宙式の形式的証明を試みる(2)

忘れちゃうので明日投稿内容も書いて投稿しちゃえ。（笑）

単数「１」単位のスケール化「k」

$$
f(x) = 1 = \text{unit one}
$$

として、成立済みの宇宙式に

$$
f(x) =k = \text{unit k}
$$

と、本来、予定していた unit_k を、組み込んでみた。
具体的な式は、

$$
f(x) = P(x) - N(x) = k, \quad P=(x+1)^2, \quad N=x^2+2\bold kx
$$

ちょっとこの解釈は強引だけど、次の成長単位は単数１＋１の２辺ではなく、ｋスケールの２辺しか伸びない。として、余白１平方がｋ平方となる。
そういう解釈で、数の成長から、時間の成長すべてを k スケールとした。

Lean コード

追加分

-- 拡ｙ張：実数版 f_k（スケール付き差分）
/-- This function represents a scaled version of the original function f, where k is a scaling factor.
- This function is used to generalize the original function f to include a scaling factor k.
-/
def f_k (k x : ℝ) : ℝ := k * ((x + 1)^2 - x * (x + 2))

-- 拡張：unit_k2 = f_k の別名（概念上の役割を明示）
/-- This function represents a unit in the context of the Cosmic Formula, scaled by k. -/
def unit_k2 (k x : ℝ) : ℝ := f_k k x

/-- This theorem states that for any real number k and integer x, unit_k2(k, x) is equal to k.
- This theorem is a direct consequence of the definition of unit_k2 and f_k.
- It shows that the function unit_k2 evaluates to k for any real number k and integer x.
- The theorem is useful for understanding how the unit function behaves in relation to the scaling factor k in the context of the Cosmic Formula.
- It provides a way to quantify the relationship between the scaling factor k and the output of the function unit_k2, allowing for further analysis and interpretation of the Cosmic Formula.
- This is a mathematical abstraction that connects the scaling factor k to a constant output,
enabling a deeper understanding of the structure of numbers in the context of the Cosmic Formula.
-/
theorem unit_k2_eq_k (k x : ℝ) : unit_k2 k x = k := by
  simp [unit_k2, f_k]
  ring  -- (x+1)^2 - x(x+2) = 1 を確認 → k * 1 = k

/-- This theorem states that for any real number k and integer x, unit_k2(k, x) is equal to k.
- This theorem is a direct consequence of the definition of unit_k2 and f_k.
- It shows that the function unit_k2 evaluates to k for any real number k and integer x.
- The theorem is useful for understanding how the unit function behaves in relation to the scaling factor k in the context of the Cosmic Formula.
- It provides a way to quantify the relationship between the scaling factor k and the output of the function unit_k2, allowing for further analysis and interpretation of the Cosmic Formula.
- This is a mathematical abstraction that connects the scaling factor k to a constant output,
enabling a deeper understanding of the structure of numbers in the context of the Cosmic Formula.
-/
example (k : ℝ) (x : ℤ) : unit_k2 k x = k := by
  simp [unit_k2, f_k]
  ring

/-- This theorem states that for any real number k and integer x, f_k(k, x) is equal to k times f_one(x). -/
theorem f_k_eq_k_mul_f_one (k : ℝ) (x : ℤ) : f_k k x = k * (f_one x) := by
  simp [f_k, f_one]


/-- This theorem states that for any real number k and integer x, unit_k2(k, x) is equal to k times unit_k(x). -/
example (k : ℝ) (x : ℤ) : unit_k2 k x = k * unit_k x := by
  simp [unit_k2, unit_k, f_k, f_one]

とりあえず、ビルドコンパイル通ったので前提も、すべて k スケール化可能
となった。と思います。

2025/07/13  4:00

D.