宇宙式: Lean4 コード

Lean4 コード

leanprover/lean4:v4.22.0-rc3
✅️ build pass.

live: Lean 4 web

ブラウザで直接確認できます

コードの解説

CosmicFormula.lean

2025/07/12 15:33 version.

-- CosmicFormula/CosmicFormula.lean
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Sqrt
import Mathlib.Tactic.Ring
import Mathlib.RingTheory.Int.Basic

/-- Cosmic Formula in Lean

N+1=(P+1)^2

P is prime product of primes
N is natural number

f(x) = (x+1)^2 - x(x+2) = 1

This is a simple proof that N = P * P + 2 * P

P = (x+1)^2
N = x^2+2*x = x(x+2)
P is the square of the sum of a prime product structure and a unit scale.
N is the sum of a square and two sides.

Cosmic Formula states that for any integer x, P(x) = N(x) + 1.
This is a generalization of the formula to all integers.

This file contains the definitions and proofs related to the Cosmic Formula.
It includes the definitions of P, N, and their relationships, as well as examples and theorems that demonstrate the properties of these functions.
-/

def P (p : ℤ) : ℤ := (p + 1)^2         -- P is the square of the sum of a prime product structure and a unit scale.
def N (n : ℤ) : ℤ := n^2 + 2*n         -- N is the sum of a square and two sides
def N_plus_two (n : ℤ) : ℤ := n*(n+2)  -- N_plus_two is another way to express N as the product of n and (n + 2)

/-- This will show that P(x) = N(x) + 1 holds for all integers x -/
example (x : ℤ) : P x = N x + 1 := by
  simp [P, N]       -- Simplify the definitions of P and N
  ring              -- Use the ring tactic to simplify the equation
  -- The ring tactic automatically handles the algebraic manipulation in the context of a commutative

/-- This theorem states that for any integer n, N(n) is equal to N_plus_two(n) -/
theorem N_eq_N_plus_two (n : ℤ) : N n = N_plus_two n := by
  simp [N, N_plus_two]    -- Simplify the definitions of N and N_plus_two
  ring
  -- This shows that both definitions of N are equivalent

#check P -- Check the type of P
#check N -- Check the type of N
#check N_plus_two -- Check the type of N_plus_two

/-- The formula states that for any integer x, the expression evaluates to 1.
- f(x) is a commonly known identity that always returns 1.
- This is a mathematical abstraction that connects the integer x to a constant output, allowing for further analysis and interpretation of the Cosmic Formula.
- The function f is defined as the difference between the square of (x + 1) and the product of x and (x + 2).
- This definition is used to relate the integer x to a constant output in the context of the Cosmic Formula.
- It provides a way to quantify the relationship between the integer x and the constant output, allowing for further analysis and interpretation of the Cosmic Formula.
- This is a mathematical abstraction that connects the integer x to a constant output, enabling a deeper understanding of the structure of numbers in the context of the Cosmic Formula.
-/
def f_one (x : ℤ) : ℤ := (x + 1)^2 - x * (x + 2)  -- original definition of f

/-- This theorem states that for any integer x, f(x) is equal to 1.
- This theorem is a direct consequence of the definition of f.
- It shows that the function f always evaluates to 1 for any integer input.
- The theorem is useful for understanding the behavior of the function f in the context of the Cosmic Formula.
- It provides a way to quantify the relationship between the integer input and the output of the function f.
- This is a mathematical abstraction that connects the integer input to a constant output, allowing for further analysis and interpretation of the Cosmic Formula.
-/
example (x:ℤ) : f_one x = 1 := by
  simp [f_one]
  ring

#check f_one -- Check the type of f

/-- This theorem states that for any integer x, f(x) is equal to 1.
- This theorem is a direct consequence of the definition of f.
- It shows that the function f always evaluates to 1 for any integer input.
- The theorem is useful for understanding the behavior of the function f in the context of the Cosmic Formula.
- It provides a way to quantify the relationship between the integer input and the output of the function f.
- This is a mathematical abstraction that connects the integer input to a constant output, allowing for further analysis and interpretation of the Cosmic Formula.
-/
theorem f_eq_one (x : ℤ) : f_one x = 1 := by
  simp [f_one]  -- Simplify the definition of f
  ring          -- Use the ring tactic to simplify the equation
  -- This shows that f always evaluates to 1 for any integer input

/-- This function represents a unit in the context of the Cosmic Formula. -/
def unit_k (x : ℤ) : ℤ := f_one x  -- original definition of unit

/-- This theorem states that for any integer x, unit(x) is equal to 1.
- This theorem is a direct consequence of the definition of unit.
- It shows that the function unit always evaluates to 1 for any integer input.
- The theorem is useful for understanding the behavior of the function unit in the context of the Cosmic Formula.
- It provides a way to quantify the relationship between the integer input and the output of the function unit.
- This is a mathematical abstraction that connects the integer input to a constant output, allowing for further analysis and interpretation of the Cosmic Formula.
- The theorem is useful for understanding how the unit function behaves in relation to the Cosmic Formula.
- It provides a way to quantify the relationship between the integer input and the output of the function unit, allowing for further analysis and interpretation of the Cosmic Formula.
-/
theorem unit_eq_one (x : ℤ) : unit_k x = 1 := by
  simp [unit_k, f_one]
  ring

/-- This theorem states that for any integer x, unit(x) is equal to f(x).
- This theorem is a direct consequence of the definition of unit.
- It shows that the function unit always evaluates to f for any integer input.
- The theorem is useful for understanding the relationship between the function unit and the function f in the context of the Cosmic Formula.
- It provides a way to quantify the relationship between these two functions, allowing for further analysis and interpretation of the Cosmic Formula.
- This is a mathematical abstraction that connects the integer input to the output of the function f, enabling a deeper understanding of the structure of numbers in the context of the Cosmic Formula.
-/
theorem unit_eq_f (x : ℤ) : unit_k x = f_one x := by
  simp [unit_k]

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

#check unit_k -- Check the type of unit
#check unit_eq_one -- Check the type of unit_eq_one

/-- T is defined as the progression of time, which is defined as t + f(t). -/
def T (t : ℤ) : ℤ := t + unit_k t

/-- This theorem states that for any integer t, T(t) is equal to t plus f(t). -/
theorem T_eq_t_plus_f (t : ℤ) : T t = t + unit_k t := by
  simp [T, unit_k]

#check T -- Check the type of T
#check T_eq_t_plus_f -- Check the type of T_eq_t_plus_f

/-- Space is defined as the square of the sum of an integer p and the function f applied to p.
- This definition is used to relate the integer p to a spatial dimension in the Cosmic Formula.
- This is a mathematical abstraction that connects the integer p to a spatial dimension, allowing for a geometric interpretation of the Cosmic Formula.
-/
def Space (p : ℤ) : ℤ := (p + unit_k p)^2

/-- Num is defined as the difference between Space and f, representing a numerical value derived from the Cosmic Formula.
- This definition is used to calculate a numerical value based on the spatial dimension and the function f.
- It provides a way to quantify the relationship between the spatial dimension and the function f in the context of the Cosmic Formula.
- This is a mathematical abstraction that connects the spatial dimension and the function f to a numerical value, allowing for further analysis and interpretation of the Cosmic Formula.
-/
def Num (p : ℤ) : ℤ := Space p - unit_k p

/-- This theorem states that for any integer p, Num(p) is equal to Space(p) minus f(p).
- This theorem is a direct consequence of the definitions of Num, Space, and f.
- It shows the relationship between these three functions in the context of the Cosmic Formula.
- The theorem is useful for understanding how the numerical value derived from the Cosmic Formula relates to the spatial dimension and the function f.
- It provides a way to quantify the relationship between these three components, allowing for further analysis and interpretation of the Cosmic Formula.
-/
theorem num_eq_space_minus_f (p : ℤ) : Num p = Space p - unit_k p := by
  simp [Num, Space, unit_k]  -- Simplify the definitions of Num, Space, and unit

/-- This theorem states that for any integer x, f(x) is equal to 1.
- This theorem is a direct consequence of the definition of f.
- It shows that the function f always evaluates to 1 for any integer input.
- The theorem is useful for understanding the behavior of the function f in the context of the Cosmic Formula.
- It provides a way to quantify the relationship between the integer input and the output of the function f.
- This is a mathematical abstraction that connects the integer input to a constant output, allowing for further analysis and interpretation of the Cosmic Formula.
-/
theorem f_const_one : ∀ x : ℤ, unit_k x = 1 := by
  intro x
  simp [unit_k, f_one]
  ring

/-- This theorem states that for any integer x, Space(x) is equal to Num(x) plus f(x).
- This theorem is a direct consequence of the definitions of Space, Num, and f.
- It shows the relationship between these three functions in the context of the Cosmic Formula.
- The theorem is useful for understanding how the spatial dimension relates to the numerical value and the function f.
- It provides a way to quantify the relationship between these three components, allowing for further analysis and interpretation of the Cosmic Formula.
- This is a mathematical abstraction that connects the spatial dimension, numerical value, and function f, allowing for a geometric interpretation of the Cosmic Formula.
-/
theorem space_eq_num_plus_time (x : ℤ) : Space x = Num x + unit_k x := by
  simp [Space, Num, unit_k]

#check Space -- Check the type of Space
#check Num -- Check the type of Num
#check num_eq_space_minus_f -- Check the type of num_eq_space_minus_f
#check f_const_one -- Check the type of f_const_one
#check space_eq_num_plus_time -- Check the type of space_eq_num_plus_time

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

/-- This function represents the temporal evolution of a value t over n iterations. -/
def Tn (t n : ℤ) : ℤ := Nat.iterate T n.toNat t

/-- This theorem states that Tn(t, n) is equal to the n-th iterate of T applied to t.
- This theorem is a direct consequence of the definition of Tn.
- It shows that Tn is defined as the n-th iterate of the function T applied to the initial value t.
- The theorem is useful for understanding how the value t evolves over n iterations in the context of the Cosmic Formula.
- It provides a way to quantify the temporal evolution of a value based on the function T and the number of iterations n.
- This is a mathematical abstraction that connects the initial value t to its evolution over time, allowing for further analysis and interpretation of the Cosmic Formula.
-/
theorem Tn_eq_sum (t n : ℤ) : Tn t n = Nat.iterate T n.toNat t := by
  simp [Tn]

#check Tn -- Check the type of Tn
#check Tn_eq_sum -- Check the type of Tn_eq_sum

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

/-- This function represents the spatial dimension at a specific point p after n iterations of T. -/
def SpaceTn (p n : ℤ) : ℤ := Space (Tn p n)

/-- This theorem states that SpaceTn(p, n) is equal to the spatial dimension at the n-th iterate of T applied to p.
- This theorem is a direct consequence of the definition of SpaceTn.
- It shows that SpaceTn is defined as the spatial dimension at the n-th iterate of the function T applied to the initial point p.
- The theorem is useful for understanding how the spatial dimension evolves over n iterations in the context of the Cosmic Formula.
- It provides a way to quantify the spatial evolution of a point based on the function T and the number of iterations n.
- This is a mathematical abstraction that connects the initial point p to its spatial evolution over time, allowing for further analysis and interpretation of the Cosmic Formula.
-/
theorem SpaceTn_eq_space_iterate (p n : ℤ) : SpaceTn p n = Space (Tn p n) := by
  simp [SpaceTn, Tn, Space]
  -- This shows that SpaceTn is defined as the spatial dimension at the n-th iterate of T applied to p

#check SpaceTn -- Check the type of SpaceTn
#check SpaceTn_eq_space_iterate -- Check the type of SpaceTn_eq_space_iterate

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

/-- This function generates a sequence of spatial dimensions for a given point p and number of iterations n.
- This function is used to create a list of spatial dimensions at each iteration from 0 to n.
- It provides a way to visualize the evolution of the spatial dimension over multiple iterations in the context of the Cosmic Formula.
- The sequence is generated by applying the SpaceTn function to the point p for each iteration from 0 to n.
- This is a mathematical abstraction that connects the initial point p to its spatial evolution over time, allowing for further analysis and interpretation of the Cosmic Formula.
-/
def SpaceSeq (p : ℤ) (n : ℕ) : List ℤ :=
  List.range (n+1) |>.map (λ i => SpaceTn p i)

/-- This theorem states that for any integer p and natural number n, the sequence of spatial dimensions at each iteration from 0 to n is equal to the list of spatial dimensions generated by SpaceSeq.
- This theorem is a direct consequence of the definitions of SpaceSeq and SpaceTn.
- It shows that the sequence generated by SpaceSeq is equivalent to the spatial dimensions at each iterate of T applied to p.
- The theorem is useful for understanding how the spatial dimension evolves over multiple iterations in the context of the Cosmic Formula.
- It provides a way to quantify the spatial evolution of a point based on the function T and the number of iterations n.
- This is a mathematical abstraction that connects the initial point p to its spatial evolution over time, allowing for further analysis and interpretation of the Cosmic Formula.
-/
theorem SpaceSeq_eq_space_iterate (p : ℤ) (n : ℕ) :
  SpaceSeq p n = List.map (λ i => SpaceTn p i) (List.range (n + 1)) := by
  simp [SpaceSeq, SpaceTn]
  -- This shows that SpaceSeq is defined as the list of spatial dimensions at each iterate of T applied to p

#check SpaceSeq -- Check the type of SpaceSeq
#check SpaceSeq_eq_space_iterate -- Check the type of SpaceSeq_eq_space_iterate

-- -------------------------------------------------------
-- ※ここまで検証済み --
-- -------------------------------------------------------

History

2025/07/12 15:33　初版→リファクタリング（AI コメント版）

清書版

宇宙式の恒等式との同値性の証明

至極当然、当たり前なこともこうして書き記さなければ人々は納得しない。

宇宙式は恒等式 f(x) = 1 という定数式と同等、同値であるを形式的に記述した例です。ブラウザ上でのライブ検証は以下のリンクより。

2025/07/14 18:16 version.

--! CosmicFormulaFixed.lean
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Sqrt
import Mathlib.Tactic.Ring
import Mathlib.RingTheory.Int.Basic
/-!
This file contains the definitions and proofs related to the Cosmic Formula.
It includes the definitions of P, N, and their relationships, as well as examples and theorems that demonstrate the properties of these functions.
-/
/- 日本語:
このファイルは、宇宙式に関連する定義と証明を含んでいます。
PとNの定義とその関係、さらにこれらの関数の性質を示す例や定理が含まれています。
-/

/- ident_f_one is An identity that always returns 1
$$
f(x) = (x + 1)^2 - x(x + 2) = 1
$$
-/
/-- ident_f_one_n は常に1を返す -/
def ident_f_one_n_def (x : ℕ) : ℕ := (x + 1)^2 - x * (x + 2)
/-- ident_f_one_z は常に1を返す -/
def ident_f_one_z_def (x : ℤ) : ℤ := (x + 1)^2 - x * (x + 2)
/-- ident_f_one_r は常に1を返す -/
def ident_f_one_r_def (x : ℝ) : ℝ := (x + 1)^2 - x * (x + 2)
/- 日本語:
ident_f_one_x は常に1を返す恒等式です。
-/

#check ident_f_one_n_def -- ident_f_one_n の型を確認します。
#check ident_f_one_z_def -- ident_f_one_z の型を確認します。
#check ident_f_one_r_def -- ident_f_one_r の型を確認します。

-- まず、(x + 1)^2 - x * (x + 2) が常に非負であることを calc を使って示す。
example (x : ℕ) : 0 ≤ ident_f_one_n_def x := by
  calc
    ident_f_one_n_def x
      = (x + 1)^2 - x * (x + 2) := rfl
  _ = (x^2 + 2*x + 1) - (x^2 + 2*x) := by ring
  _ = 1 := by simp
  _ ≥ 0 := by norm_num
  -- 上記の例が成り立つので定理とする

/-- 定理: ident_f_one_n は常に1を返す -/
theorem ident_f_one_n_always_one_theorem (x : ℕ) : ident_f_one_n_def x = 1 := by
  calc
    ident_f_one_n_def x
      = (x + 1)^2 - x * (x + 2) := rfl
  _ = (x^2 + 2*x + 1) - (x^2 + 2*x) := by ring
  _ = 1 := by simp
  _ = 1 := by norm_num

/-- 定理: ident_f_one_z は常に1を返す -/
theorem ident_f_one_z_always_one_theorem (x:ℤ) : ident_f_one_z_def x = 1 := by
  simp [ident_f_one_z_def]
  ring

/-- 定理: ident_f_one_r は常に1を返す -/
theorem ident_f_one_r_always_one_theorem (x:ℝ) : ident_f_one_r_def x = 1 := by
  simp [ident_f_one_r_def]
  ring

/- Cosmic Formula -/

/- P は有限の素数のリストの積です -/
/-- P_n は自然数の素数積構造を示す定義です -/
def P_n (p : ℕ) : ℕ := (p + 1)^2
/-- P_z は整数の素数積構造を示す定義です -/
def P_z (p : ℤ) : ℤ := (p + 1)^2
/-- P_r は実数の素数積構造（素数指数ベクトル）を示す定義です -/
def P_r (p : ℝ) : ℝ := (p + 1)^2

/- N は素数のリストによる最大の面積です -/
/-- N_n は自然数の最大面積を示す定義です -/
def N_n (n : ℕ) : ℕ := n^2 + 2*n
/-- N_z は整数の最大面積を示す定義です -/
def N_z (n : ℤ) : ℤ := n^2 + 2*n
/-- N_r は実数の最大面積を示す定義です -/
def N_r (n : ℝ) : ℝ := n^2 + 2*n
/- n の平方数に２辺分の面積を加えた面積となります -/

#check P_n -- P_n の型を確認します。
#check P_z -- P_z の型を確認します。
#check P_r -- P_r の型を確認します。
#check N_n -- N_n の型を確認します。
#check N_z -- N_z の型を確認します。
#check N_r -- N_r の型を確認します。

/- Cosmic Formula: Examples （宇宙式の恒等式性能の例）-/
example (n : ℕ) : N_n n + 1 = P_n n := by -- N + 1 = P
  calc
    N_n n + 1
      = n^2 + 2*n + 1 := rfl
  _ = (n + 1)^2 := by ring
  _ = P_n n := rfl

example (n : ℕ) : P_n n = N_n n + 1 := by -- P = N + 1
  calc
    P_n n
      = (n + 1)^2 := rfl
  _ = n^2 + 2*n + 1 := by ring
  _ = N_n n + 1 := by simp [N_n]

example (n : ℕ) : P_n n - N_n n = 1 := by -- P - N = 1
  calc
    P_n n - N_n n
      = (n + 1)^2 - (n^2 + 2*n) := rfl
  _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
  _ = 1 := by simp

example (n : ℕ) : P_n n - N_n n -1 = 0 := by -- P - N - 1 = 0
  calc
    P_n n - N_n n - 1
      = (n + 1)^2 - (n^2 + 2*n) - 1 := rfl
  _ = n^2 + 2*n + 1 - (n^2 + 2*n) - 1 := by ring
  _ = 0 := by simp


/-- Cosmic Formula N の補題: P-N=1 である -/
lemma cosmic_formula_n_lemma (n : ℕ) : P_n n - N_n n = 1 := by
  calc
    P_n n - N_n n
      = (n + 1)^2 - (n^2 + 2*n) := rfl
  _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
  _ = 1 := by simp

/-- Cosmic Formula N to Z の補題: P-N=1 である -/
lemma cosmic_formula_n2z_lemma (n : ℕ) : P_z n - N_z n = 1 := by
  simp [P_z, N_z]
  ring

/-- Cosmic Formula Z の補題: P-N=1 である -/
lemma cosmic_formula_z_lemma (n : ℤ) : P_z n - N_z n = 1 := by
  simp [P_z, N_z]
  ring

/-- Cosmic Formula N to R の補題: P-N=1 である -/
lemma cosmic_formula_n2r_lemma (n : ℕ) : P_r n - N_r n = 1 := by
  simp [P_r, N_r]
  ring

/-- Cosmic Formula N to R の補題: P-N=1 である -/
lemma cosmic_formula_r_lemma (n : ℝ) : P_r n - N_r n = 1 := by
  simp [P_r, N_r]
  ring

#check cosmic_formula_n_lemma -- 自然数のまま
#check cosmic_formula_n2z_lemma -- 自然数から整数への変換
#check cosmic_formula_n2r_lemma -- 自然数から実数への変換

/-- Cosmic Formula N の定義 -/
def cosmic_formula_n_def (n : ℕ) : ℕ := P_n n - N_n n
/-- Cosmic Formula Z の定義 -/
def cosmic_formula_z_def (n : ℤ) : ℤ := P_z n - N_z n
/-- Cosmic Formula R の定義 -/
def cosmic_formula_r_def (n : ℝ) : ℝ := P_r n - N_r n
/- これらの定義の結果は常に１となる -/

/-- 命題: cosmic_formula_n_def は常に1を返す -/
theorem cosmic_formula_n_def_always_one (n : ℕ) : cosmic_formula_n_def n = 1 := by
  simp [cosmic_formula_n_def, cosmic_formula_n_lemma]
/-- 命題: cosmic_formula_z_def は常に1を返す -/
theorem cosmic_formula_z_def_always_one (n : ℤ) : cosmic_formula_z_def n = 1 := by
  simp [cosmic_formula_z_def, cosmic_formula_z_lemma]
/-- 命題: cosmic_formula_r_def は常に1を返す -/
theorem cosmic_formula_r_def_always_one (n : ℝ) : cosmic_formula_r_def n = 1 := by
  simp [cosmic_formula_r_def, cosmic_formula_r_lemma]

/- ここから宇宙式と恒等式が等価であることが成り立つ -/

/-- 定理：宇宙式は恒等式である N 版 -/
theorem cosmic_formula_n_def_equiv (n : ℕ) : cosmic_formula_n_def n = 1 ↔ ident_f_one_n_def n = 1 := by
  constructor
  · intro h
    -- ident_f_one_n n = (n + 1)^2 - n * (n + 2)
    calc
      ident_f_one_n_def n = (n + 1)^2 - n * (n + 2) := rfl
      _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
      _ = 1 := by simp
  · intro h
    -- cosmic_formula_n_def n = P_n n - N_n n = 1
    simp [cosmic_formula_n_def, P_n, N_n]
    calc
      cosmic_formula_n_def n = P_n n - N_n n := rfl
      _ = (n + 1)^2 - (n^2 + 2*n) := rfl
      _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
      _ = 1 := by simp

/-- 定理：宇宙式は恒等式である Z 版 -/
theorem cosmic_formula_z_def_equiv (n : ℤ) : cosmic_formula_z_def n = 1 ↔ ident_f_one_z_def n = 1 := by
  constructor
  · intro h
    -- ident_f_one_z_def n = (n + 1)^2 - n * (n + 2)
    calc
      ident_f_one_z_def n = (n + 1)^2 - n * (n + 2) := rfl
      _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
      _ = 1 := by simp
  · intro h
    -- cosmic_formula_z_def n = P_z n - N_z n = 1
    simp [cosmic_formula_z_def, P_z, N_z]
    calc
      cosmic_formula_z_def n = P_z n - N_z n := rfl
      _ = (n + 1)^2 - (n^2 + 2*n) := rfl
      _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
      _ = 1 := by simp

/-- 定理：宇宙式は恒等式である R 版 -/
theorem cosmic_formula_r_def_equiv (n : ℝ) : cosmic_formula_r_def n = 1 ↔ ident_f_one_r_def n = 1 := by
  constructor
  · intro h
    -- ident_f_one_r n = (n + 1)^2 - n * (n + 2)
    calc
      ident_f_one_r_def n = (n + 1)^2 - n * (n + 2) := rfl
      _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
      _ = 1 := by simp
  · intro h
    -- cosmic_formula_r_def n = P_r n - N_r n = 1
    simp [cosmic_formula_r_def, P_r, N_r]
    calc
      cosmic_formula_r_def n = P_r n - N_r n := rfl
      _ = (n + 1)^2 - (n^2 + 2*n) := rfl
      _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
      _ = 1 := by simp

（解説のページのリンク✍️）

2025/07/14 18:20　宇宙式の恒等式との同値性の証明　追加
2025/07/12 15:35　新規

D.