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. Exact original first-admission records.

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

PrimeBitPrefix(b,c,l)Sum(b,c,l,z)BetaCutoffPrefix(u,b,c,d,f,l)Product(b,c,l,z)Repeat(b,c,a,l)Primorial(n,z)Choose(n,k,z)

Checked theorems using this definition

PC0004 · prime_bit_prefix_entryPC0005 · prime_bit_prefix_extendPC0007 · prime_bit_prefix_all_bitsPC000A · beta_sum_entry_lePC000B · prime_count_positive_above_onePC000C · beta_product_bit_weighted_upper_powerPC000D · beta_product_bit_weighted_lower_powerPC000E · beta_cutoff_choice_existsPC0011 · beta_cutoff_prefix_entryPC0012 · beta_cutoff_prefix_extendPC0013 · beta_cutoff_prefix_existsPC0014 · beta_cutoff_count_comparisonPC001A · primorial_prefix_decoded_choicePC001C · prime_contribution_prefix_decoded_choicePC001D · central_binom_prime_mask_weighted_upperPC001E · primorial_cutoff_weighted_lowerPC001F · central_binom_prime_count_power_boundPC0033 · prime_bit_prefix_equal_entryPC0036 · prime_count_one