{"id":"e-05b27694ad6bb7e9","operation":{"operation":"basis_map_theorem"},"operation_detail":null,"conclusion_id":"n-39194b37db596ae8","premise_count":0,"theorem":"geometric family P_k = g(t) (a + d t)^k: T(p) = g(t) p(a + d t), so the roots of T(p) are those of g and the points (r - a)/d for the roots r of p (elementary)","lean_route":null,"lean_declarations":[],"certificate_hash":"13a78b7404877090184ee9df3ef1f6501f03fdcecec033d304812d0027b41555","verification_polytool":"replayed","verification_lean":"not_attempted","certificate_kind":"basis_map_theorem","certificate_raw_size":1619,"certificate_compressed_size":671,"conclusion_name":"a(n) = 1 if n is a triangular number, otherwise 0.","claims":[{"claim":"basis_map_preserver","input_interval":"(-inf, 1]","output_interval":"(-inf, 0]","statement":"T(p) = p(a) g; an input with every root <= a has p(a) of the sign of its leading coefficient"}],"premises":[],"cited_by":[{"node_id":"n-39194b37db596ae8","claim":"basis_map_preserver"}]}