The EX2 attention path needs score/sqrt(n) in base-two units. Bound both
sqrt(n) and ln(2) from their rational intervals, then require that the
bounds round to the same F32 word. This avoids rounding 1/sqrt(n) before
multiplying by log2(e), which can choose a different final word.
93def float32ExactInverseRootNaturalLogTwo =
94 (lambda unrestricted n : Nat .
95 (let unrestricted rootLow = (float32ExactRootLow n 1) in
96 (float32ExactBetween
97 (naturalMultiply float32RootScale float32Places)
98 (naturalMultiply (succ rootLow) (succ float32Ln2Digits))
99 (naturalMultiply float32RootScale float32Places)
100 (naturalMultiply rootLow float32Ln2Digits))))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.