the columns whose frequency is rational, held to the definition: column 0
is base^0 = 1, exact in one word; column columns/2 is base^(-1/2) = 1/100
(base 10000), the binary32 nearest a hundredth
1776def cgRotaryThetaColumnZero :
1777 (equal Nat (naturalAdd (cgIndex cgRotaryThetas 0) (cgIndex cgRotaryThetas 1)) (float32ExactRational 1 1)) =
1778 (refl Nat (float32ExactRational 1 1))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.