PD0013

BetaAt(b,c,i,x)

x is the bounded beta-decoded value at index i.

Conservative notation; not a theorem, primitive, or axiom.

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)BetaPrefixEqual(b,c,d,e,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)BetaPrefixInto(b,c,l,B)FpRepresentedDegree(p,b,c,L,d)

Checked theorems using this definition

PC0001 · polynomial_zero_extended_entry_existsPC0003 · polynomial_zero_extended_entry_insidePC0009 · polynomial_diagonal_term_leadingPC000D · polynomial_diagonal_prefix_entryPC000E · polynomial_diagonal_prefix_recodingPC000F · polynomial_diagonal_prefix_from_pointwisePC0010 · polynomial_diagonal_prefix_functionalPC0012 · polynomial_diagonal_prefix_input_transportPC0017 · prime_field_convolution_coefficient_leadingPC0018 · prime_field_convolution_coefficient_zero_leftPC0019 · prime_field_convolution_coefficient_zero_rightPC001A · prime_field_convolution_coefficient_zero_past_supportPC001B · prime_field_convolution_prefix_entryPC001C · prime_field_convolution_prefix_recodingPC001D · prime_field_convolution_prefix_from_pointwisePC001E · prime_field_convolution_prefix_functionalPC0020 · prime_field_convolution_prefix_boundedPC0021 · prime_field_convolution_prefix_input_transportPC0025 · prime_field_polynomial_convolution_entryPC002B · prime_field_polynomial_convolution_zero_leftPC002C · prime_field_polynomial_convolution_zero_rightPC002F · prime_field_polynomial_represented_degree_leading_nonzeroPC0033 · prime_field_polynomial_convolution_leading_coefficientPC0034 · prime_field_polynomial_convolution_represented_degree