{"id":"e-3864cd74360cd35e","operation":{"operation":"definition_equality"},"operation_detail":null,"conclusion_id":"n-cf38558d99f4fe37","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":"81147553b888d671ac8d2314bfff160ea0efe9247b625f4af164e8c278c04901","verification_polytool":"replayed","verification_lean":"not_attempted","certificate_kind":"definition_equality","certificate_raw_size":7733,"certificate_compressed_size":2275,"conclusion_name":"Triangle T(n,k), 0 <= k <= n, read by rows, defined by T(n,k) = 4^k * C(n+1,2*k+1).","claims":[],"premises":[],"cited_by":[]}