TF0001 · beta_two_square_prefix_drop_lastRestricting a successor-length prefix preserves every witnessed two-square factor representation.
layer 0 · 16 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableCurrent 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.
TF0002 · beta_two_square_prefix_last_representedThe final decoded factor of a represented successor prefix has its own explicit two-square witnesses.
layer 0 · 12 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF0003 · beta_two_square_represented_factor_productInduction on an arbitrary beta-coded product constructs a two-square representation from represented decoded factors.
layer 1 · 55 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF0004 · beta_all_prime_entry_is_primeEvery concrete decoded entry in the canonical all-prime prefix is prime, by uniqueness of beta decoding.
layer 0 · 26 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF0005 · beta_admissible_prime_factor_product_is_two_squareAny finite product whose decoded factors are prime two or prime one modulo four is constructively a sum of two squares.
layer 2 · 27 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF0006 · positive_number_with_admissible_prime_divisors_is_two_squareA positive natural number all of whose prime divisors are two or one modulo four has an explicitly constructed two-square representation via its canonical prime factorization.
layer 3 · 47 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF0007 · three_mod_four_progression_nonzeroEvery witnessed natural of the form 4k+3 is nonzero.
layer 0 · 8 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF0008 · three_mod_four_progression_nonunitEvery witnessed natural of the form 4k+3 differs from the unit one.
layer 0 · 12 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF0009 · three_mod_four_progression_not_two_squareA witnessed three-modulo-four natural cannot have a two-square representation.
layer 0 · 9 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF000A · three_mod_four_good_prime_exclusiveA prime equal to two or one modulo four cannot also be three modulo four.
layer 1 · 11 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF000B · three_mod_four_prime_divisor_decidableFor every candidate and dividend, actual three-mod-four prime divisibility is constructively decidable.
layer 2 · 34 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF000C · three_mod_four_prime_divisor_bounded_searchFinite induction either excludes every three-mod-four prime divisor up to the supplied bound or returns an actual bounded prime-divisor witness.
layer 3 · 66 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF000D · three_mod_four_prime_divisor_existsEvery natural congruent to three modulo four has an actual prime divisor congruent to three modulo four, obtained by constructive finite search and beta-coded prime factorization.
layer 4 · 46 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF000E · euclid_three_number_successor_balanceThe subtraction-free Euclid number 4d+3 satisfies the exact identity (4d+3)+1=4(d+1).
layer 0 · 2 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF000F · euclid_three_progression_prime_existsEvery actual subtraction-free Euclid number 4d+3 has a witnessed prime divisor congruent to three modulo four.
layer 5 · 5 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF0010 · euclid_three_common_multiple_exclusionNo prime dividing a nonzero common multiple can also divide its subtraction-free Euclid number 4c−1.
layer 1 · 35 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF0011 · euclid_three_prime_divisor_exceeds_boundEvery prime divisor of the exact Euclid number 4c−1 lies strictly above the bound encoded by its nonzero common multiple c.
layer 2 · 29 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableTF0012 · infinitely_many_primes_three_mod_fourFor every natural bound, construct an actual strictly larger prime with an explicit residue witness p=4k+3.
layer 6 · 27 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableExactly 18 displayed theorems have independently verified Alpha checked-use authority; none is admitted to Stable. Body-only enrollment never grants checked theorem use.