{"id":"e-d8ffe0ceb9f858f8","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":"42baf77031e576efa949d56a6f1ff9b65beedfae7d8263705fdfddddc4b748cd","verification_polytool":"replayed","verification_lean":"not_attempted","certificate_kind":"definition_equality","certificate_raw_size":13835,"certificate_compressed_size":3121,"conclusion_name":"Bisection of Fibonacci triangle A037027: even-indexed members of column sequences of A037027 (not counting leading zeros).","claims":[],"premises":[],"cited_by":[]}