{"id":"e-bc0a3892b1359edd","operation":{"operation":"definition_equality"},"operation_detail":null,"conclusion_id":"n-fac4d4a000d744e8","premise_count":0,"theorem":"all-index identity Q_n = P_n certified by exact Ore-algebra division and identifying rows (polytool preserver-image certificate of the identity map)","lean_route":null,"lean_declarations":[],"certificate_hash":"37151570af96a94283157b34a6ba951814a8d1a15f21f20055c4916bc792cea4","verification_polytool":"replayed","verification_lean":"not_attempted","certificate_kind":"definition_equality","certificate_raw_size":16194,"certificate_compressed_size":3763,"conclusion_name":"Bisection of Fibonacci triangle A037027: even-indexed members of column sequences of A037027 (not counting leading zeros).","claims":[],"premises":[],"cited_by":[]}