def hi_bound

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqr.bend:94

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqa.bend as AQ
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend as SK

94# S0 <= isqrt(N) + 2, for q < 2^32 and isqrt(N) >= 2^62
95def hi_bound(+one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}, +hQ: {Nat.is_lt(Q, C.shift(32n, one)) == True{} : Bool}, +hT: {Nat.is_le(C.shift(62n, one), M.isqrt(C.shift(64n, n))) == True{} : Bool}) -> {Nat.is_le(Nat.add(Q, C.shift(32n, s)), Nat.add(M.isqrt(C.shift(64n, n)), 2n)) == True{} : Bool}:
96  +e64 = Equal.trans(Nat, Nat.mul(C.shift(32n, one), C.shift(32n, one)), C.shift(32n, C.shift(32n, Nat.mul(one, one))), C.shift(2n, C.shift(62n, one)), AQ.sh_sq(32n, one), Equal.trans(Nat, C.shift(32n, C.shift(32n, Nat.mul(one, one))), C.shift(32n, C.shift(32n, one)), C.shift(2n, C.shift(62n, one)), Equal.cong(Nat, Nat, z => C.shift(32n, C.shift(32n, z)), Nat.mul(one, one), one, L.subst(Nat, o => {Nat.mul(o, o) == o : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})), Equal.trans(Nat, C.shift(32n, C.shift(32n, one)), C.shift(64n, one), C.shift(2n, C.shift(62n, one)), Equal.sym(Nat, C.shift(64n, one), C.shift(32n, C.shift(32n, one)), WW.shift_comp(32n, 32n, one)), WW.shift_comp(2n, 62n, one))))
97  +hq2 = N.le_trans(Nat.mul(Q, Q), Nat.mul(C.shift(32n, one), C.shift(32n, one)), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n)))), AQ.sqmono(Q, C.shift(32n, one), N.lt_le(Q, C.shift(32n, one), hQ)), L.subst(Nat, z => {Nat.is_le(Nat.mul(C.shift(32n, one), C.shift(32n, one)), z) == True{} : Bool}, C.shift(2n, M.isqrt(C.shift(64n, n))), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n)))), SK.four(M.isqrt(C.shift(64n, n))), L.subst(Nat, z => {Nat.is_le(z, C.shift(2n, M.isqrt(C.shift(64n, n)))) == True{} : Bool}, C.shift(2n, C.shift(62n, one)), Nat.mul(C.shift(32n, one), C.shift(32n, one)), Equal.sym(Nat, Nat.mul(C.shift(32n, one), C.shift(32n, one)), C.shift(2n, C.shift(62n, one)), e64), WW.shift_mono(2n, C.shift(62n, one), M.isqrt(C.shift(64n, n)), hT))))
98  +a1 = N.le_add_right(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U))
99  +a2 = L.subst(Nat, z => {Nat.is_le(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), z) == True{} : Bool}, Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Equal.sym(Nat, Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), identN(s, rr, n, Q, U, D, hn, hD, hc)), a1)
100  +a3 = N.le_lt_trans(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))))), a2, N.lt_le_trans(Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), Nat.mul(Q, Q)), Nat.add(Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))))), N.lt_add_r2(C.shift(64n, n), Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), Nat.mul(Q, Q), AQ.ilt(C.shift(64n, n))), N.le_add_left(Nat.mul(Q, Q), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n)))), Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), hq2)))
101  SK.k_hi_c(C.shift(64n, n), M.isqrt(C.shift(64n, n)), Nat.add(Q, C.shift(32n, s)), a3, Nat.is_le(Nat.add(Q, C.shift(32n, s)), Nat.add(M.isqrt(C.shift(64n, n)), 2n)), {==})