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
PD0025 InjectivePrefix PD0028 AllPrime PD0029 Sorted PD0014 Product PD0019 Repeat PD0024 BoundedPrefix PD0026 SurjectivePrefix PD0027 ContainsPrefixAll transitive conservative prerequisites
none
Used by theorem statements or local proof propositions
TS000L finite_bounded_into_oversized_not_injective TS000M floor_square_oversized_bounded_grid_not_injective TS000N finite_bounded_into_collision_from_constructive_decision TS000O finite_prefix_collision_succ TS000P finite_prefix_last_occurrence_collision TS000Q finite_prefix_injective_extend_fresh TS000R finite_prefix_collision_or_injective TS000S finite_bounded_into_oversized_collision TS000T floor_square_oversized_bounded_grid_collision TS000V beta_affine_residue_grid_extend TS000W beta_affine_residue_grid_exists TS000X beta_affine_residue_grid_bounded TS000Y prime_floor_affine_residue_grid_exists TS000Z prime_floor_affine_residue_grid_collision TS001K shared_beta_collision_remainders_equal TS001N prime_floor_affine_grid_collision_represents_prime TS001O prime_mod_four_one_is_sum_of_two_squares TS002J beta_two_square_prefix_drop_last TS002K beta_witnessed_two_square_prefix_implies_pointwise TS002L beta_two_square_prefix_last_represented TS002M beta_two_square_represented_factor_product TS002N beta_witnessed_two_square_factor_product TS002P beta_all_prime_entry_is_prime TS002Q beta_admissible_prime_factor_product_is_two_square TS002R represented_factor_product_times_square_is_two_square TS002S beta_grouped_prime_square_factor_product_is_two_square TS002T beta_product_adjacent_equal_pair_decomposes_as_square TS002U beta_two_square_prefix_append_equal_pair TS0031 beta_sorted_prime_prefix_divisor_equals_bounded_last TS0032 even_valuation_sorted_terminal_prime_has_equal_predecessorGrand-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.