Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
S x ≤ S (S i · c) ∧ (∃ y. b = y · S (S i · c) + x)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((exists ff_h_defined_beta_at. ff_h_defined_beta_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_defined_beta_at. b = ff_q_defined_beta_at * S ((S (i)) * c) + (x))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
none — first-order arithmetic only
Definitions depending on this notation
Sum(b,c,l,z)Repeat(b,c,a,l)BetaPrefixInto(b,c,l,B)BetaPrefixEqual(b,c,d,e,l)FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l)FpPolyScale(p,k,ab,ac,bb,bc,l)BetaZeroExtend(b,c,L,i,a)PolynomialDiagonalPrefix(ab,ac,L,bb,bc,M,i,db,dc,l)FpConvolutionPrefix(p,ab,ac,L,bb,bc,M,cb,cc,l)FpRepresentedDegree(p,b,c,L,d)FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L)PolynomialSuffix(b,c,t,d,e,M)FpPolynomialTrim(p,b,c,L,t,d,e,M)PolynomialLeftPad(b,c,L,t,d,e)PolynomialPowerCoefficient(b,c,L,k,a)FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,M,qb,qc,i,q)FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,N)FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,qb,qc,q,rb,rc,R)
Checked theorems using this definition
PX0001 · polynomial_diagonal_left_prefix_transportPX0002 · polynomial_diagonal_prefix_left_transportPX0003 · prime_field_convolution_coefficient_prefix_transportPX0006 · polynomial_diagonal_last_term_left_appendPX0007 · polynomial_diagonal_sum_left_appendPX0008 · prime_field_convolution_coefficient_appendPX000C · prime_field_polynomial_power_coefficient_existsPX0012 · prime_field_polynomial_equivalent_implies_equal_same_lengthPX0014 · prime_field_polynomial_left_pad_existsPX0015 · prime_field_polynomial_left_pad_entryPX0016 · prime_field_polynomial_left_pad_boundedPX0017 · prime_field_polynomial_left_pad_functionalPX0018 · prime_field_polynomial_zero_suffix_left_padPX001E · prime_field_polynomial_add_left_pad_transportPX001F · prime_field_polynomial_subtract_left_pad_transportPX0020 · prime_field_polynomial_scale_left_pad_transportPX0023 · prime_field_polynomial_constant_right_coefficientPX0024 · prime_field_polynomial_constant_product_to_scalePX0025 · prime_field_polynomial_scale_to_constant_productPX002B · prime_field_polynomial_quotient_prefix_entryPX002C · prime_field_polynomial_quotient_prefix_boundedPX002D · prime_field_polynomial_quotient_prefix_appendPX002E · prime_field_polynomial_quotient_prefix_existsPX002F · prime_field_polynomial_quotient_prefix_convolution_entryPX0030 · prime_field_polynomial_quotient_prefix_product_matchesPX0031 · prime_field_polynomial_quotient_prefix_remainder_zeroPX0037 · prime_field_polynomial_division_quotient_data_existsPX0039 · prime_field_polynomial_division_execution_existsPX003E · prime_field_convolution_prefix_empty_left_zeroPX0040 · beta_sum_pointwise_mod_addPX0041 · polynomial_zero_extended_add_congruentPX0048 · prime_field_convolution_prefix_left_addPX0049 · prime_field_convolution_prefix_right_addPX0054 · prime_field_polynomial_quotient_prefix_functionalPX0057 · prime_field_polynomial_division_quotient_data_functionalPX005E · polynomial_left_pad_natural_sum_invariantPX005F · polynomial_zero_tail_natural_sum_invariantPX0064 · polynomial_diagonal_left_padding_leftPX0065 · polynomial_diagonal_left_padding_rightPX0067 · prime_field_convolution_coefficient_left_padding_rightPX0068 · prime_field_convolution_coefficient_before_left_padding_leftPX0069 · prime_field_convolution_coefficient_before_left_padding_rightPX006C · prime_field_polynomial_convolution_left_padding_nonempty_leftPX006D · prime_field_polynomial_convolution_left_padding_nonempty_right