ND0262

BetaPrefixInto(b,c,l,B)

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

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.

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

none

Checked theorems using this definition

PP0004 · prime_field_polynomial_normalization_boundedPP0006 · prime_field_polynomial_normalization_reflexivePP0009 · prime_field_polynomial_repeat_coefficientsPP000A · prime_field_polynomial_repeat_existsPP000B · prime_field_polynomial_zero_existsPP000C · prime_field_polynomial_add_from_normalizationPP000D · prime_field_polynomial_add_existsPP000F · prime_field_polynomial_add_boundedPP0013 · prime_field_polynomial_add_zero_rightPP0014 · prime_field_polynomial_scale_from_normalizationPP0015 · prime_field_polynomial_scale_existsPP0017 · prime_field_polynomial_scale_boundedPP001A · prime_field_polynomial_scale_onePP001B · prime_field_polynomial_scale_zeroPP0021 · prime_field_polynomial_horner_trace_from_normalizationPP0022 · prime_field_polynomial_horner_existsPP0023 · prime_field_polynomial_horner_input_boundsPP0027 · prime_field_polynomial_horner_normalization_residuePP0028 · prime_field_polynomial_horner_residuePP002A · prime_field_polynomial_horner_exists_uniquePP002C · prime_field_polynomial_horner_successor_construct