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)

Checked theorems using this definition

PC0017 · prime_field_convolution_coefficient_leadingPC0020 · prime_field_convolution_prefix_boundedPC0024 · prime_field_polynomial_convolution_boundedPC0028 · prime_field_polynomial_convolution_at_length_existsPC0029 · prime_field_polynomial_convolution_exists_uniquePC002A · prime_field_polynomial_convolution_emptyPC0032 · prime_field_polynomial_monic_degree_examples