def sq_spec

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqs.bend:78

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
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/math/typed/f64rtools.bend as RT

78# the spec's rounded root equals roundPackToF64 of the sticky floor root
79def sq_spec(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +j: Nat, +h62: {Nat.is_le(C.shift(62n, one), M.isqrt(n)) == True{} : Bool}, +Es: Nat, +x: Nat, +hEx: {Nat.add(Es, 1n+j) == x : Nat}) -> {SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Es) == SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x) : F.F64}:
80  +r1 = RT.round_jam(False{}, 1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Es, s_bl(one, h1, n, j, h62))
81  +r2 = Equal.cong(Nat, F.F64, z => SF.round(False{}, SW.jam(z, C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), M.isqrt(n), s_high(n, j))
82  +r3 = Equal.cong(Nat, F.F64, z => SF.round(False{}, SW.jam(M.isqrt(n), z), Nat.add(Es, 1n+j)), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), s_low(n, j))
83  +r4 = Equal.cong(Nat, F.F64, z => SF.round(False{}, z, Nat.add(Es, 1n+j)), SW.jam(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))), SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)))), Equal.sym(Nat, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)))), SW.jam(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))), FL.jmin(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))))))
84  +r5 = Equal.cong(Bool, F.F64, t => SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(t)), Nat.add(Es, 1n+j)), Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)), s_st(n, j))
85  +r6 = Equal.cong(Nat, F.F64, z => SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), z), Nat.add(Es, 1n+j), x, hEx)
86  Equal.trans(F.F64, SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Es), SF.round(False{}, SW.jam(C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r1, Equal.trans(F.F64, SF.round(False{}, SW.jam(C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r2, Equal.trans(F.F64, SF.round(False{}, SW.jam(M.isqrt(n), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r3, Equal.trans(F.F64, SF.round(False{}, SW.jam(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r4, Equal.trans(F.F64, SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r5, r6)))))