ND0054

CRTPairwiseCoprimePrefix(b,c,l)

Exact pairwise coprimality of every pair of distinct positions in a beta-coded modulus prefix.

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.

Hygienic expanded first-order definition

forall bpr_left_index_gcrt_research bpr_right_index_gcrt_research bpr_left_value_gcrt_research bpr_right_value_gcrt_research. (exists bpr_gap_gcrt_research_left_bound. bpr_gap_gcrt_research_left_bound + S (bpr_left_index_gcrt_research) = l) -> (exists bpr_gap_gcrt_research_right_bound. bpr_gap_gcrt_research_right_bound + S (bpr_right_index_gcrt_research) = l) -> (((exists bpr_height_gcrt_research_left_at. bpr_height_gcrt_research_left_at + S (bpr_left_value_gcrt_research) = S ((S (bpr_left_index_gcrt_research)) * c)) /\ exists bpr_quotient_gcrt_research_left_at. b = bpr_quotient_gcrt_research_left_at * S ((S (bpr_left_index_gcrt_research)) * c) + (bpr_left_value_gcrt_research))) -> (((exists bpr_height_gcrt_research_right_at. bpr_height_gcrt_research_right_at + S (bpr_right_value_gcrt_research) = S ((S (bpr_right_index_gcrt_research)) * c)) /\ exists bpr_quotient_gcrt_research_right_at. b = bpr_quotient_gcrt_research_right_at * S ((S (bpr_right_index_gcrt_research)) * c) + (bpr_right_value_gcrt_research))) -> ~(bpr_left_index_gcrt_research = bpr_right_index_gcrt_research) -> (forall bpr_coprime_divisor_gcrt_research_coprime. (exists bpr_coprime_left_factor_gcrt_research_coprime. bpr_left_value_gcrt_research = bpr_coprime_divisor_gcrt_research_coprime * bpr_coprime_left_factor_gcrt_research_coprime) -> (exists bpr_coprime_right_factor_gcrt_research_coprime. bpr_right_value_gcrt_research = bpr_coprime_divisor_gcrt_research_coprime * bpr_coprime_right_factor_gcrt_research_coprime) -> bpr_coprime_divisor_gcrt_research_coprime = 1)

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Beta(b,c,i,x)Lt(a,b)Coprime(a,b)

Definitions depending on this notation

none

Checked theorems using this definition

CR0004 · crt_pairwise_coprime_prefix_drop_lastCR0009 · crt_pairwise_coprime_prefix_lastCR000C · crt_pairwise_coprime_prefix_product_is_lcmCR0011 · crt_pairwise_coprime_prefix_lcm_exists_uniqueCR0012 · crt_pairwise_coprime_prefix_product_coprime_lastCR0013 · crt_pairwise_coprime_prefix_solution_existsCR001B · crt_pairwise_coprime_prefix_canonical_exists_unique

Separate complete second-wave branches: Full G011 proof · Alpha v27.