noncomputable def Frourio.φ : ℝ

黄金比の定義

Equations

• Frourio.φ = (1 + √5) / 2

theorem Frourio.φ_gt_one : 1 < φ

The golden ratio is greater than 1

noncomputable def Frourio.metallic (p : ℝ) : ℝ

金属比の定義（パラメータpに対して）

Equations

• Frourio.metallic p = (p + √(p ^ 2 + 4)) / 2

inductive Frourio.Sign : Type

符号型（+1 または -1）

• pos : Sign
• neg : Sign

def Frourio.Sign.toInt : Sign → ℤ

Sign を整数に写像する（+1 または -1）。

Equations

• Frourio.Sign.pos.toInt = 1
• Frourio.Sign.neg.toInt = -1