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.

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

JordanTupleEnumeration(k,n,B,C,D,E,j)JordanTupleScan(k,n,c,limit,B,C,D,E,j)JordanTupleRepresentatives(k,n,c,T)JordanCanonicalTupleCRT(m,n,b,c,d,e,f,g,k)

Checked theorems using this definition

JT0020 · jordan_tuple_bounded_transportJT0023 · jordan_tuple_scan_skipJT0026 · jordan_tuple_scan_appendJT0027 · jordan_tuple_scan_existsJT002F · jordan_tuple_normalize_existsJT0032 · jordan_canonical_crt_tuple_existsJT0039 · jordan_tuple_bounded_congruence_equalJT003B · jordan_crt_component_recoveryJT003D · jordan_enumeration_actual_valueJT003E · jordan_enumeration_completeJT0040 · jordan_rectangle_crt_appendJT0045 · jordan_enumeration_reduce_primitiveJT0046 · jordan_rectangle_crt_distinctJT0047 · jordan_rectangle_crt_coversJT004D · jordan_enumeration_position_match_existsJT0052 · jordan_enumeration_index_map_bounded_injectiveJT0057 · jordan_tuple_bounded_one_entry_zeroJT0058 · jordan_zero_tuple_bounded_oneJT0059 · jordan_tuples_bounded_one_equal