{"arithmetic":"exact integers","finite_scope":{"index_max":24,"index_min":1},"records":[{"f_n":1,"f_next":1,"f_prev":0,"lhs":-1,"n":1,"rhs":-1},{"f_n":1,"f_next":2,"f_prev":1,"lhs":1,"n":2,"rhs":1},{"f_n":2,"f_next":3,"f_prev":1,"lhs":-1,"n":3,"rhs":-1},{"f_n":3,"f_next":5,"f_prev":2,"lhs":1,"n":4,"rhs":1},{"f_n":5,"f_next":8,"f_prev":3,"lhs":-1,"n":5,"rhs":-1},{"f_n":8,"f_next":13,"f_prev":5,"lhs":1,"n":6,"rhs":1},{"f_n":13,"f_next":21,"f_prev":8,"lhs":-1,"n":7,"rhs":-1},{"f_n":21,"f_next":34,"f_prev":13,"lhs":1,"n":8,"rhs":1},{"f_n":34,"f_next":55,"f_prev":21,"lhs":-1,"n":9,"rhs":-1},{"f_n":55,"f_next":89,"f_prev":34,"lhs":1,"n":10,"rhs":1},{"f_n":89,"f_next":144,"f_prev":55,"lhs":-1,"n":11,"rhs":-1},{"f_n":144,"f_next":233,"f_prev":89,"lhs":1,"n":12,"rhs":1},{"f_n":233,"f_next":377,"f_prev":144,"lhs":-1,"n":13,"rhs":-1},{"f_n":377,"f_next":610,"f_prev":233,"lhs":1,"n":14,"rhs":1},{"f_n":610,"f_next":987,"f_prev":377,"lhs":-1,"n":15,"rhs":-1},{"f_n":987,"f_next":1597,"f_prev":610,"lhs":1,"n":16,"rhs":1},{"f_n":1597,"f_next":2584,"f_prev":987,"lhs":-1,"n":17,"rhs":-1},{"f_n":2584,"f_next":4181,"f_prev":1597,"lhs":1,"n":18,"rhs":1},{"f_n":4181,"f_next":6765,"f_prev":2584,"lhs":-1,"n":19,"rhs":-1},{"f_n":6765,"f_next":10946,"f_prev":4181,"lhs":1,"n":20,"rhs":1},{"f_n":10946,"f_next":17711,"f_prev":6765,"lhs":-1,"n":21,"rhs":-1},{"f_n":17711,"f_next":28657,"f_prev":10946,"lhs":1,"n":22,"rhs":1},{"f_n":28657,"f_next":46368,"f_prev":17711,"lhs":-1,"n":23,"rhs":-1},{"f_n":46368,"f_next":75025,"f_prev":28657,"lhs":1,"n":24,"rhs":1}],"records_sha256":"37866b46aa1bf0854b4b4ad1a6476fb65419e0e52305d860c7bec0f18979e4b5","schema":"o017-u06-recurrence-witness-v1","statement":"F[n-1]*F[n+1]-F[n]^2=(-1)^n","summary":{"all_records_valid":true,"record_count":24,"tamper_control_detected":true},"universal_status":"not established by this finite computation"}