9.1. The exact target🔗

The conjecture uses two pairs of complex numbers. Each pair is linearly independent over the rational numbers. Six additional parameters are algebraic. The parameter gamma is nonzero. Five specified exponential values must also be algebraic. The conclusion gives exact equalities for all four products and for the ratio term.

def Conjecture : Prop :=
  ∀ (x y : Fin 2 → ℂ) (α γ : ℂ) (β : Fin 2 → Fin 2 → ℂ),
    LinearIndependent ℚ x → LinearIndependent ℚ y →
    IsAlgebraic ℚ α → IsAlgebraic ℚ γ → γ ≠ 0 →
    (∀ i j, IsAlgebraic ℚ (β i j)) →
    (∀ i j, IsAlgebraic ℚ (Complex.exp (x i * y j - β i j))) →
    IsAlgebraic ℚ (Complex.exp (γ * x 1 / x 0 - α)) →
    (∀ i j, x i * y j = β i j) ∧ γ * x 1 = α * x 0

An algebraic number is a root of a nonzero polynomial with rational coefficients. Lean uses indices 0 and 1 for each pair. Move the pointer over a Lean term to see its type. This definition is not a proof.