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.
Readable signature
BetaAt(b, c, i, x)Exact expansion
((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))This node is conservative notation, not a theorem, axiom, predicate constant, or kernel rule. Its expansion remains in the unchanged first-order language.
Definition neighborhood
Depends on conservative definitions
none
Used by conservative definitions
PD0041 Choose PD0014 Product PD0018 Range PD0019 Repeat PD0015 Sum PD0049 PowerQuotPrefix PD0016 AllBitsAll transitive conservative prerequisites
none
Used by theorem statements or local proof propositions
KU0006 add_quotient_carry_choice KU0007 add_quotient_carry_prefix_extend KU0008 add_quotient_carry_prefix_exists KU0009 add_quotient_carry_prefix_all_bits KU000A add_quotient_carry_prefix_restrict KU000B beta_sum_add_carry_exact KU000C kummer_binomial_carry_bit_count KU000E kummer_carry_free_iff_not_dividesGrand-campaign planning vocabulary
Locate Beta in the global campaign vocabulary →
Reviewed BetaAt corresponds to blueprint Beta with checked argument positions [0, 1, 2, 3].
The global atlas describes planning vocabulary and does not itself certify a definition or theorem. The reviewed expansion and conservative dependency DAG on this page are the actual family-local reading definitions.