Nuprl Definition : twosquareinv

This function defines an involution on the type
x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} where p is a prime.

It is used in
"A One-Sentence Proof that Every Prime p == 1 (mod 4) Is a Sum of Two Squares"
by D. Zaiger.

He says that it is a simplification of an argument by Heath-Brown.⋅

twosquareinv(t) ==
  let x,y,z = t in
  if x <z y - z then <x + z + z, z, y - z - x>
  if x <z y + y then <(y + y) - x, y, (x - y) + z>
  else <x - y + y, (x - y) + z, y>
  fi

Definitions occuring in Statement : ifthenelse: if b then t else f fi , lt_int: i <z j, spreadn: spread3, pair: <a, b>, subtract: n - m, add: n + m
Definitions occuring in definition : spreadn: spread3, ifthenelse: if b then t else f fi , lt_int: i <z j, pair: <a, b>, add: n + m, subtract: n - m
FDL editor aliases : twosquareinv

Latex:
twosquareinv(t) == let x,y,z = t in if x <z y - z then <x + z + z, z, y - z - x> if x <z y + y then <(y + y) - x, y, (x - y) + z> else <x - y + y, (x - y) + z, y> fi Date html generated: 2019_06_20-PM-02_40_56 Last ObjectModification: 2018_09_24-PM-02_52_40 Theory : num_thy_1 Home Index