Documentation

FUST.Basic

noncomputable def FUST.φ :

Equations

FUST.φ = (1 + √5) / 2

Instances For

noncomputable def FUST.ψ :

Equations

FUST.ψ = (1 - √5) / 2

Instances For

theorem FUST.golden_ratio_property :

φ ^ 2 = φ + 1

theorem FUST.phi_pos :

0 < φ

theorem FUST.φ_gt_one :

1 < φ

theorem FUST.phi_inv :

φ ⁻¹ = φ - 1

theorem FUST.phi_cubed :

φ ^ 3 = 2 * φ + 1

theorem FUST.psi_neg :

ψ < 0

theorem FUST.phi_sub_psi :

theorem FUST.phi_add_psi :

theorem FUST.phi_mul_psi :

φ * ψ = -1

theorem FUST.psi_sq :

ψ ^ 2 = ψ + 1

theorem FUST.abs_psi_lt_one :

theorem FUST.phi_ne_zero :

theorem FUST.psi_ne_zero :

theorem FUST.phi_sub_psi_ne :

theorem FUST.phi_sub_psi_complex_ne :

↑φ - ↑ψ ≠ 0

theorem FUST.golden_ratio_property_complex :

↑φ ^ 2 = ↑φ + 1

theorem FUST.psi_sq_complex :

↑ψ ^ 2 = ↑ψ + 1

theorem FUST.phi_cubed_complex :

↑φ ^ 3 = 2 * ↑φ + 1

theorem FUST.psi_cubed_complex :

↑ψ ^ 3 = 2 * ↑ψ + 1

theorem FUST.phi_mul_psi_complex :

↑φ * ↑ψ = -1

theorem FUST.phi_add_psi_complex :

↑φ + ↑ψ = 1

theorem FUST.psi_cubed_alt :

ψ ^ 3 = 2 * ψ + 1

theorem FUST.phi_pow4_complex :

↑φ ^ 4 = 3 * ↑φ + 2

theorem FUST.psi_pow4_complex :

↑ψ ^ 4 = 3 * ↑ψ + 2

theorem FUST.phi_pow6_complex :

↑φ ^ 6 = 8 * ↑φ + 5

theorem FUST.psi_pow6_complex :

↑ψ ^ 6 = 8 * ↑ψ + 5

theorem FUST.phi_pow8_complex :

↑φ ^ 8 = 21 * ↑φ + 13

theorem FUST.psi_pow8_complex :

↑ψ ^ 8 = 21 * ↑ψ + 13

noncomputable def FUST.ζ₆ :

ζ₆ = e^{iπ/3} = (1 + i√3)/2

Equations

FUST.ζ₆ = { re := 1 / 2, im := √3 / 2 }

Instances For

noncomputable def FUST.ζ₆' :

ζ₆' = e^{-iπ/3} = (1 - i√3)/2

Equations

FUST.ζ₆' = { re := 1 / 2, im := -(√3 / 2) }

Instances For

theorem FUST.sqrt3_pos :

0 < √3

theorem FUST.sqrt3_sq :

√3 ^ 2 = 3

theorem FUST.zeta6_add_conj :

ζ₆ + ζ₆' = 1

ζ₆ + ζ₆' = 1 (same trace as φ + ψ = 1)

theorem FUST.zeta6_mul_conj :

ζ₆ * ζ₆' = 1

ζ₆ · ζ₆' = +1 (contrast with φψ = -1)

theorem FUST.zeta6_sq :

ζ₆ ^ 2 = ζ₆ - 1

ζ₆² = ζ₆ - 1 (contrast with φ² = φ + 1)

theorem FUST.zeta6_cubed :

ζ₆ ^ 3 = -1

ζ₆³ = -1

theorem FUST.zeta6_pow_six :

ζ₆⁶ = 1

theorem FUST.norm_zeta6 :

‖ζ₆ ‖ = 1

|ζ₆| = 1 (compact: isometric action)

theorem FUST.zeta6_ne_zero :

ζ₆ ≠ 0

theorem FUST.zeta6_pow_four :

ζ₆ ^ 4 = -ζ₆

ζ₆⁴ = -ζ₆

theorem FUST.zeta6_pow_five :

ζ₆ ^ 5 = 1 - ζ₆

ζ₆⁵ = 1 - ζ₆

ζ₆ - ζ₆' properties #

theorem FUST.zeta6_sub_conj :

ζ₆ - ζ₆' = { re := 0, im := √3 }

ζ₆ - ζ₆' = i√3

theorem FUST.zeta6_sub_conj_ne_zero :

ζ₆ - ζ₆' ≠ 0

ζ₆ - ζ₆' ≠ 0

theorem FUST.zeta6'_ne_zero :

ζ₆' ≠ 0

theorem FUST.zeta6'_eq_inv :

ζ₆' = ζ₆ ⁻¹

ζ₆' = ζ₆⁻¹

theorem FUST.norm_zeta6' :

‖ζ₆'‖ = 1

|ζ₆'| = 1

theorem FUST.zeta6'_eq_starRingEnd :

ζ₆' = (starRingEnd ℂ) ζ₆

ζ₆' = starRingEnd ℂ ζ₆ (complex conjugate)