ND0262

BetaPrefixInto(b,c,l,B)

Every actual beta entry below the strict length l has a witnessed value below B. The same generic graph describes canonical polynomial coefficients when B is the modulus; empty prefixes are allowed.

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

∀ fom_index_pfp_lowertier. Lt(fom_index_pfp_lowertier,l) → ∃ x. BetaAt(b,c,fom_index_pfp_lowertier,x) ∧ Lt(x,B)

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
forall fom_index_pfp_lowertier. (exists fom_gap_pfp_lowertier_index_bound. fom_gap_pfp_lowertier_index_bound + S (fom_index_pfp_lowertier) = (l)) -> exists fom_value_pfp_lowertier. ((((exists fom_beta_height_pfp_lowertier_entry. fom_beta_height_pfp_lowertier_entry + S (fom_value_pfp_lowertier) = S ((S (fom_index_pfp_lowertier)) * (c))) /\ exists fom_beta_quotient_pfp_lowertier_entry. (b) = fom_beta_quotient_pfp_lowertier_entry * S ((S (fom_index_pfp_lowertier)) * (c)) + (fom_value_pfp_lowertier))) /\ (exists fom_gap_pfp_lowertier_value_bound. fom_gap_pfp_lowertier_value_bound + S (fom_value_pfp_lowertier) = (B)))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Lt(a,b)BetaAt(b,c,i,x)

Definitions depending on this notation

FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N)FpRepresentedDegree(p,b,c,L,d)FpPolynomialTrim(p,b,c,L,t,d,e,M)FpMonic(p,b,c,L)FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,qb,qc,q,rb,rc,R)FpPolynomialRightDivides(p,db,dc,D,ab,ac,L)FpPolynomialAlignedAdd(p,ab,ac,L,bb,bc,M,rb,rc,N)

Checked theorems using this definition

PG0002 · prime_field_polynomial_shift_boundedPG0017 · prime_field_polynomial_convolution_right_scale_existsPG001A · prime_field_polynomial_append_shift_constant_addPG001B · prime_field_polynomial_append_shift_constant_decomposition_existsPG001C · prime_field_convolution_coefficient_right_append_addPG001D · prime_field_polynomial_shift_scale_aligned_sum_existsPG001E · prime_field_polynomial_convolution_right_append_equivalentPG001F · prime_field_polynomial_convolution_right_append_existsPG0021 · prime_field_polynomial_convolution_shift_scale_aligned_equivalentPG0023 · prime_field_polynomial_convolution_associativity_append_stepPG0025 · prime_field_polynomial_convolution_associative_equivalentPG0026 · prime_field_polynomial_right_divides_from_productPG0027 · prime_field_polynomial_right_divides_divisor_boundedPG0028 · prime_field_polynomial_right_divides_dividend_boundedPG0029 · prime_field_polynomial_right_divides_equivalent_targetPG002A · prime_field_polynomial_right_divides_emptyPG002B · prime_field_polynomial_right_divides_equivalent_divisorPG002C · prime_field_polynomial_right_divides_transitivePG0031 · prime_field_polynomial_convolution_left_unit_equalPG0033 · prime_field_polynomial_convolution_left_unit_existsPG0034 · prime_field_polynomial_right_divides_reflexivePG0035 · prime_field_polynomial_bounded_representative_at_length_existsPG0038 · prime_field_polynomial_common_representatives_at_length_existsPG0039 · prime_field_polynomial_common_representatives_existsPG003C · prime_field_polynomial_aligned_add_from_commonPG003D · prime_field_polynomial_aligned_add_boundedPG003E · prime_field_polynomial_aligned_add_from_fixedPG003F · prime_field_polynomial_aligned_add_transportPG0042 · prime_field_polynomial_aligned_add_existsPG0043 · prime_field_polynomial_aligned_add_realizePG0045 · prime_field_polynomial_aligned_subtract_existsPG0046 · prime_field_polynomial_aligned_add_cancel_leftPG0047 · prime_field_polynomial_aligned_add_associativePG0049 · prime_field_polynomial_add_trim_alignedPG004A · prime_field_polynomial_division_execution_aligned_identityPG0051 · prime_field_polynomial_scale_to_left_constant_productPG0052 · prime_field_polynomial_left_constant_product_existsPG0055 · prime_field_polynomial_scale_implies_right_dividesPG0057 · prime_field_polynomial_normalized_right_associate_existsPG0058 · prime_field_polynomial_right_divides_aligned_addPG0059 · prime_field_polynomial_right_divides_aligned_subtractPG005D · prime_field_polynomial_euclidean_backward_coefficient_identityPG005E · prime_field_polynomial_bezout_euclidean_backwardPG0060 · prime_field_polynomial_aligned_add_empty_rightPG0061 · prime_field_polynomial_bezout_from_right_multiplePG0062 · prime_field_polynomial_bezout_equivalent_transportPG0064 · prime_field_polynomial_division_remainder_boundedPG0065 · prime_field_polynomial_reduced_representative_existsPG0066 · prime_field_polynomial_gcd_bezout_empty_secondPG0067 · prime_field_polynomial_gcd_bezout_equivalent_secondPG0069 · prime_field_polynomial_gcd_bezout_exists_up_toPG006A · prime_field_polynomial_gcd_bezout_existsPG006C · prime_field_polynomial_normalized_gcd_bezout_existsPG0070 · prime_field_polynomial_right_divides_represented_factorization