PD0004 · Primep is nonunit and every factorization of p has a unit factor.
conservative definition · not a theoremCurrent 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.
dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged.
PD0011 · Mod4Onen is one modulo four by an explicit quotient.
conservative definition · not a theoremPD0012 · Mod4Threen is three modulo four by an explicit quotient.
conservative definition · not a theoremPD0008 · ModEqBalanced-natural congruence modulo m.
conservative definition · not a theoremPD0021 · QResa has a square root modulo m.
conservative definition · not a theoremPD0002 · LtWitness-defined strict order on natural numbers.
conservative definition · not a theoremPD0022 · BoundedQResa has a square root strictly below m modulo m.
conservative definition · not a theoremPD0001 · LeWitness-defined non-strict order on natural numbers.
conservative definition · not a theoremPD0051 · FloorSqrts is the integer floor square root: s² ≤ n < (s+1)².
conservative definition · not a theoremPD0003 · DvdThe natural number d divides n.
conservative definition · not a theoremPD0013 · BetaAtx is the bounded beta-decoded value at index i.
conservative definition · not a theoremPD0025 · InjectivePrefixEqual decoded values below l have equal indices.
conservative definition · not a theoremPD0028 · AllPrimeEvery decoded factor below l is prime.
conservative definition · not a theoremPD0029 · SortedAdjacent decoded entries form a nondecreasing prefix.
conservative definition · not a theoremPD0014 · Productz is the product of a beta-coded prefix of length l.
conservative definition · not a theoremPD0019 · RepeatThe decoded prefix repeats a for l positions.
conservative definition · not a theoremPD0020 · Powz is the relational e-th power of a.
conservative definition · not a theoremPD0044 · PowerDividesThe relational power p to exponent e divides n.
conservative definition · not a theoremPD0045 · BoundedPowerValuatione is the greatest exponent at most b for which p to that exponent divides n.
conservative definition · not a theoremPD0046 · PowerValuatione is the canonical bounded p-adic power valuation of n.
conservative definition · not a theoremCF0002 · SumTwoSquaresn has explicitly witnessed natural two-square coordinates.
conservative definition · not a theoremCF0001 · AbsoluteDifferenced is an explicitly witnessed natural absolute difference.
conservative definition · not a theoremPD0005 · CoprimeEvery common divisor of a and b is one.
conservative definition · not a theoremPD0007 · DivRemq and r are a quotient and a strict remainder for n by d.
conservative definition · not a theoremPD0009 · Evenn has an even decomposition.
conservative definition · not a theoremPD0010 · Oddn has an odd decomposition.
conservative definition · not a theoremPD0024 · BoundedPrefixEvery decoded entry below l is itself below l.
conservative definition · not a theoremPD0026 · SurjectivePrefixEvery value below l occurs at an index below l.
conservative definition · not a theoremPD0027 · ContainsPrefixx occurs in the decoded prefix below l.
conservative definition · not a theoremPD0031 · BalancedInversea times b is congruent to one modulo m.
conservative definition · not a theoremTS0000 · even_square_is_four_multipleThe square of an even natural has an explicit multiple-of-four witness.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0001 · odd_square_is_four_multiple_plus_oneThe square of an odd natural has an explicit residue-one witness modulo four.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0002 · square_mod_four_zero_or_oneEvery natural square is constructively either zero or one modulo four.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0003 · sum_two_squares_mod_four_casesA sum of two natural squares has residue zero, one, or two modulo four.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0004 · sum_two_squares_not_four_mod_threeNo natural congruent to three modulo four is a sum of two squares.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0005 · prime_mod_four_one_minus_one_square_existsEvery prime congruent to one modulo four has a constructive square root of minus one.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0006 · prime_mod_four_one_bounded_minus_one_square_existsEvery prime congruent to one modulo four has a canonical root of minus one strictly below the prime.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0007 · predecessor_square_congruence_yields_divisible_normA square congruent to the predecessor of a successor yields an explicit divisor of its norm r²+1.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0008 · prime_mod_four_one_divisible_two_square_norm_existsA prime equal to one modulo four divides an explicitly witnessed two-square norm r²+1.
theorem body · 4 linked definitions · unenrolled candidate · no checked-use authorityTS0009 · prime_mod_four_one_bounded_divisible_two_square_norm_existsA prime equal to one modulo four divides the norm of a canonical root strictly below the prime.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000A · positive_multiple_below_twice_equals_baseA positive multiple strictly below twice its divisor must equal that divisor.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000B · bounded_divisible_two_square_norm_equals_primeA positive two-square norm divisible by p and strictly below 2p is exactly p.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000C · prime_is_not_natural_squareNo natural square satisfies the nonunit factor-pair definition of primality.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000D · natural_square_monotone_expandedWitnessed weak order on natural coordinates transports to their squares.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000E · prime_floor_square_strictly_below_primeFor a prime, its floor-square lower endpoint is strictly smaller than the prime.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000F · prime_floor_bounded_coordinate_square_strictEvery coordinate at most the floor square root of a prime has square below that prime.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000G · two_strict_values_sum_below_doubleTwo natural values each strictly below p have sum strictly below 2p.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000H · prime_floor_bounded_two_square_norm_below_doubleAny two coordinates bounded by the prime floor square root have norm strictly below twice the prime.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000I · floor_square_successor_grid_strictly_exceeds_inputThe successor-floor-square grid has strictly more points than the input modulus.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000J · floor_square_oversized_grid_existsEvery natural admits an explicitly witnessed floor-square grid with more cells than that natural.
theorem body · 2 linked definitions · unenrolled candidate · no checked-use authorityTS000K · prime_floor_bounded_divisible_norm_represents_primeA positive divisible norm with floor-square-bounded coordinates is already an exact prime representation.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000L · finite_bounded_into_oversized_not_injectiveAn explicitly bounded beta-coded map from a larger finite domain cannot be injective.
theorem body · 7 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000M · floor_square_oversized_bounded_grid_not_injectiveEvery beta-coded prime-residue-bounded map on the oversized floor-square grid has a collision obstruction.
theorem body · 4 linked definitions · unenrolled candidate · no checked-use authorityTS000N · finite_bounded_into_collision_from_constructive_decisionOnce collision-versus-injectivity is constructively decided, oversized bounded maps yield an actual collision witness.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000O · finite_prefix_collision_succA witnessed collision in a finite prefix remains a collision after adjoining one more decoded entry.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000P · finite_prefix_last_occurrence_collisionIf the last decoded value already occurs, its earlier index and final index form an explicit witnessed collision.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000Q · finite_prefix_injective_extend_freshAn injective decoded prefix stays injective when its new final value has no earlier occurrence.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000R · finite_prefix_collision_or_injectiveEvery finite beta-coded prefix constructively yields either explicit distinct equal-value indices or a proof of injectivity.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000S · finite_bounded_into_oversized_collisionAn oversized beta-coded map into a bounded finite interval has an actual existentially witnessed collision.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000T · floor_square_oversized_bounded_grid_collisionEvery residue-bounded beta map on the floor-square oversized grid contains explicit distinct colliding indices.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000U · affine_grid_point_remainder_existsEvery flat grid index has canonical row, column, affine quotient, and strictly bounded residue witnesses.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000V · beta_affine_residue_grid_extendAppend the next canonical affine residue while preserving every decoded row, column, quotient, and earlier residue.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000W · beta_affine_residue_grid_existsEvery nonzero modulus and positive grid width admit a full beta-coded prefix of bounded affine residues.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000X · beta_affine_residue_grid_boundedThe encoded affine residue grid is an explicit BoundedInto map from its full domain into the modulus.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000Y · prime_floor_affine_residue_grid_existsA prime floor-square grid admits a canonical beta-coded affine residue map on all successor-square points.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS000Z · prime_floor_affine_residue_grid_collisionThe actual affine prime-residue grid on all square-root points has explicit distinct flat indices with the same residue.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0010 · equal_affine_remainders_balancedEqual affine remainders yield an exact subtraction-free balanced congruence between their two grid values.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0011 · balanced_zero_congruence_implies_multipleA balanced congruence to zero yields an actual natural divisibility witness.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0012 · multiple_implies_balanced_zero_congruenceEvery witnessed natural multiple is balanced-congruent to zero.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0013 · negative_one_scaled_square_identityDistributivity identifies the scaled negative-one polynomial with the linear square plus its coordinate square.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0014 · negative_one_scaled_square_congruent_zeroA witnessed root of minus one forces its scaled linear square plus the coordinate square to vanish modulo the modulus.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0015 · balanced_linear_congruence_implies_squared_congruenceBalanced congruence respects squaring of a direct linear relation.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0016 · balanced_zero_sum_implies_squared_congruenceIf two naturals sum to zero modulo a modulus, their squares are balanced-congruent without subtraction.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0017 · negative_one_congruent_square_norm_multipleA root of minus one and either matching linear square yield an actual divisible two-square norm.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0018 · negative_one_linear_congruence_norm_multipleThe same-sign coordinate-difference branch produces a witnessed divisible norm.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0019 · negative_one_opposite_linear_congruence_norm_multipleThe opposite-sign coordinate-difference branch also produces a witnessed divisible norm.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001A · natural_absolute_difference_existsTotal natural order supplies an explicit absolute coordinate difference without subtraction.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001B · bounded_natural_absolute_differenceAn absolute difference between two coordinates bounded by s is itself bounded by s.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001C · affine_collision_difference_linear_or_oppositeEvery affine collision and both absolute coordinate differences yield exactly one of the constructive same-sign or opposite-sign linear congruences.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001D · affine_collision_absolute_difference_norm_multipleAn actual balanced affine collision produces explicit natural absolute differences and an actual prime-divisible two-square norm.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001E · flat_square_index_row_not_at_least_widthA flat index strictly inside a square grid cannot have row index at least the grid width.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001F · flat_square_index_row_below_widthDivision decoding of a flat index strictly inside a square grid yields a strictly width-bounded row.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001G · absolute_difference_zero_forces_coordinate_equalityA zero witnessed absolute difference forces equality of its source coordinates.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001H · nonzero_coordinate_pair_has_positive_square_normA natural coordinate pair not identically zero has a witnessed strictly positive two-square norm.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001I · distinct_flat_indices_have_positive_difference_normDistinct decoded flat indices force strictly positive norm of their witnessed absolute coordinate differences.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001J · strict_successor_coordinate_bound_is_weak_boundA coordinate strictly below S s carries an explicit weak-order witness below s.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001K · shared_beta_collision_remainders_equalBoth independently decoded affine remainders equal the same witnessed beta-collision value.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001L · equal_remainder_affine_values_balanced_congruentEqual witnessed affine remainders produce an actual balanced affine-congruence certificate.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001M · prime_floor_decoded_affine_collision_represents_primeA genuinely decoded, distinct affine collision at the floor-square grid produces an exact representation of the prime as two natural squares.
theorem body · 6 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001N · prime_floor_affine_grid_collision_represents_primeDecoding both entries of a genuine beta-coded affine collision yields a complete constructive prime two-square representation.
theorem body · 6 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001O · prime_mod_four_one_is_sum_of_two_squaresEvery prime congruent to one modulo four has an explicitly witnessed constructive representation as the sum of two natural squares.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001P · two_square_add_swap_nestedAdjacent terms can be constructively exchanged under a shared additive tail.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001Q · two_square_sum_square_expandsThe square of a natural sum expands into its two squares and two equal cross terms.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001R · two_square_absolute_difference_square_balanceA witnessed natural absolute difference satisfies the exact subtraction-free square balance.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001S · two_square_cross_product_interchangeThe cross products ac·bd and ad·bc coincide by associativity and commutativity.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001T · two_square_product_expandsDistributivity expands a product of two natural two-square norms into four squared products.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001U · two_square_product_norm_blocksThe four squared products regroup into diagonal and off-diagonal norm blocks.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001V · two_square_sum_square_blocksThe square of a sum separates into its diagonal square block and repeated cross-product block.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001W · brahmagupta_fibonacci_two_square_identityBrahmagupta–Fibonacci: the product of two witnessed norms is the norm of ac+bd and the natural magnitude of ad−bc.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001X · two_square_representation_multiplicatively_closedTwo explicit natural two-square representations compose into an explicit representation of their product.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS001Y · zero_one_and_two_have_two_square_representationsThe zero boundary, multiplicative unit, and exceptional prime two have explicit two-square witnesses.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authorityTS001Z · every_natural_square_is_sum_of_two_squaresEvery natural square has the direct representation n²+0².
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0020 · prime_is_two_or_oddEvery prime is constructively either the exceptional prime two or an odd number.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0021 · prime_mod_four_trichotomyEvery prime lies in exactly the constructive residue branches two, one modulo four, or three modulo four.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0022 · two_square_scaled_norm_identityScaling a two-square norm by z² scales both coordinates by z.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0023 · negative_one_norm_multiple_yields_predecessor_residueIf a successor divides r²+1, its predecessor is constructively a quadratic residue.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0024 · prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_rootA prime dividing a²+b² but not b supplies an explicit modular root of minus one through the modular inverse of b.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0025 · three_mod_four_prime_has_no_negative_one_rootFor an odd prime congruent to three modulo four, the first supplementary law excludes square roots of minus one.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0026 · three_mod_four_prime_norm_divisor_forces_second_coordinateA three-modulo-four prime dividing a²+b² must divide the second coordinate, by the constructive first supplementary law.
theorem body · 6 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0027 · three_mod_four_prime_divides_two_square_norm_divides_bothA prime congruent to three modulo four divides a two-square norm only when it divides both coordinates.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0028 · prime_is_two_squares_iff_two_or_one_mod_fourA prime has a natural two-square representation exactly when it is two or congruent to one modulo four.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0029 · two_square_add_left_commAssociativity and commutativity swap the first two entries of a right-associated natural sum.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authorityTS002A · two_square_mul_left_commAssociativity and commutativity swap the first two factors of a right-associated natural product.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authorityTS002B · two_square_cross_products_equalThe two cross products in the Brahmagupta identity are exactly equal.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authorityTS002C · two_square_product_norm_expandedThe product of two natural two-square norms expands into its four squared coordinate products.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authorityTS002D · two_square_balanced_difference_identityEqual cross products and a witnessed natural difference imply the exact balanced sum-of-two-squares identity.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authorityTS002E · two_square_product_difference_forwardThe nonnegative a*d-b*c branch gives an explicit natural Brahmagupta representation.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authorityTS002F · two_square_product_difference_reverseThe nonnegative b*c-a*d branch gives the same natural Brahmagupta representation.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authorityTS002G · two_square_product_explicit_witnessThe product of two two-square norms has the explicit coordinates a*c+b*d and a constructively witnessed absolute difference |a*d-b*c|.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authorityTS002H · two_square_product_is_two_squareThe complete constructive Brahmagupta--Fibonacci identity supplies actual natural coordinates for every product of two-square norms.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authorityTS002I · two_square_representations_closed_under_multiplicationTwo explicitly represented sums of two natural squares multiply to another explicitly represented sum of two squares.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authorityTS002J · beta_two_square_prefix_drop_lastRestricting a successor-length prefix preserves every witnessed two-square factor representation.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS002K · beta_witnessed_two_square_prefix_implies_pointwiseExistentially witnessed represented entries imply representation of every actual decoded value by beta uniqueness.
theorem body · 2 linked definitions · unenrolled candidate · no checked-use authorityTS002L · beta_two_square_prefix_last_representedThe final decoded factor of a represented successor prefix has its own explicit two-square witnesses.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS002M · beta_two_square_represented_factor_productInduction on an arbitrary beta-coded product constructs a two-square representation from represented decoded factors.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS002N · beta_witnessed_two_square_factor_productA represented decoded factor supplied existentially at every bounded index suffices for an explicit representation of the whole product.
theorem body · 3 linked definitions · unenrolled candidate · no checked-use authorityTS002O · prime_two_or_one_mod_four_is_sum_of_two_squaresThe exceptional prime two and every prime congruent to one modulo four have explicit constructive two-square representations.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS002P · beta_all_prime_entry_is_primeEvery concrete decoded entry in the canonical all-prime prefix is prime, by uniqueness of beta decoding.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS002Q · 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.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS002R · represented_factor_product_times_square_is_two_squareA represented-factor beta product remains constructively representable after multiplication by any explicitly witnessed natural square.
theorem body · 3 linked definitions · unenrolled candidate · no checked-use authorityTS002S · beta_grouped_prime_square_factor_product_is_two_squareA beta-coded grouped product folds represented prime singletons together with explicit square blocks pairing primes congruent to three modulo four.
theorem body · 5 linked definitions · unenrolled candidate · no checked-use authorityTS002T · beta_product_adjacent_equal_pair_decomposes_as_squareTwo equal adjacent decoded suffix factors collapse constructively to one explicit square times the shorter beta-coded prefix product.
theorem body · 2 linked definitions · unenrolled candidate · no checked-use authorityTS002U · beta_two_square_prefix_append_equal_pairAppending two equal adjacent decoded factors to any represented beta-coded prefix preserves constructive two-square representability.
theorem body · 3 linked definitions · unenrolled candidate · no checked-use authorityTS002V · 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.
theorem body · 6 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS002W · prime_divisor_of_prime_forces_equalityA prime can divide another prime only when both prime values agree.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS002X · distinct_prime_power_valuation_zeroThe prime-power valuation of a distinct prime factor is exactly zero.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS002Y · positive_double_at_least_twoThe double of a positive natural has an explicit witness for being at least two.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS002Z · even_positive_prime_valuation_has_square_divisorA positive even valuation at a prime yields an actual constructive divisor witness for the prime square.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0030 · prime_square_divisibility_forces_suffix_prime_divisorIf a prime square divides a product with one terminal prime factor, that same prime divides the remaining prefix product.
theorem body · 2 linked definitions · unenrolled candidate · no checked-use authorityTS0031 · beta_sorted_prime_prefix_divisor_equals_bounded_lastA prime dividing a sorted prime prefix equals its terminal factor whenever that terminal factor is bounded by the prime.
theorem body · 8 linked definitions · unenrolled candidate · no checked-use authorityTS0032 · even_valuation_sorted_terminal_prime_has_equal_predecessorIn a sorted all-prime beta factorization, a terminal prime with positive even valuation has the identical immediately preceding factor.
theorem body · 8 linked definitions · unenrolled candidate · no checked-use authorityTS0033 · pairing_double_equals_two_mulThe additive double of a natural equals its standard multiplicative parity witness.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0034 · even_double_sum_reflects_even_tailIf an additive even block plus a tail is even, the tail has its own constructive additive half witness.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0035 · distinct_prime_factor_even_valuation_reflects_prefixRemoving a distinct prime singleton preserves the even valuation of every other prime in a nonzero product.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0036 · square_factor_even_valuation_reflects_cofactorRemoving any nonzero natural-square factor preserves the even valuation of every prime in the remaining cofactor.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0037 · three_mod_four_number_not_equal_representedA number congruent to three modulo four cannot equal any explicitly represented two-square number.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0038 · all_bad_prime_even_valuations_strip_represented_primeRemoving a represented prime singleton preserves the entire universal three-modulo-four even-valuation invariant.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS0039 · all_bad_prime_even_valuations_strip_square_factorRemoving a nonzero natural-square block preserves every three-modulo-four prime's constructive even-valuation invariant.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003A · all_bad_prime_even_valuation_value_eq_transportThe universally quantified bad-prime even-valuation invariant transports constructively along equality of natural values.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003B · prime_mod_four_good_or_threeThe constructive prime residue trichotomy splits into one represented-prime branch and one three-modulo-four branch.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003C · all_bad_prime_even_two_square_sufficiency_boundedBounded constructive descent on the natural value proves sufficiency of even valuations at every three-modulo-four prime.
theorem body · 7 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003D · positive_number_with_even_bad_prime_valuations_is_two_squareEvery nonzero natural whose three-modulo-four prime valuations are all even has an explicitly witnessed two-square representation.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003E · nonzero_two_square_iff_even_three_mod_four_prime_valuationsComplete nonzero Fermat two-square classification: witnessed representation is equivalent to even valuation at every three-modulo-four prime.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003F · two_square_iff_zero_or_even_three_mod_four_prime_valuationsFull all-natural two-square theorem, with zero explicitly separated from the nonzero even-prime-valuation criterion.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003G · two_square_self_square_zero_reflectsA natural square is zero only when its coordinate is zero.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authorityTS003H · two_square_norm_zero_iff_coordinates_zeroZero is an explicit boundary: a two-square norm vanishes exactly when both natural coordinates vanish.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authorityTS003I · prime_power_valuation_square_evenAt every prime, the valuation of a nonzero square is exactly twice the valuation of its coordinate.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003J · two_square_common_factor_norm_identityA common factor of both coordinates extracts as its exact square from their two-square norm.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003K · two_square_common_divisor_extracts_squared_factorTwo witnessed coordinate divisors provide both quotient coordinates and the exact squared-factor norm identity.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003L · two_square_common_squared_factor_divides_normAny common coordinate divisor has its square as an actual divisor of the two-square norm.
theorem body · 1 linked definitions · unenrolled candidate · no checked-use authorityTS003M · two_square_representation_preserved_by_square_factorEvery represented natural remains represented after multiplication by an arbitrary natural square.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003N · three_mod_four_prime_two_square_norm_extracts_squared_factorA three-modulo-four prime dividing a two-square norm extracts as an exact prime square while preserving a represented quotient.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003O · three_mod_four_prime_nonzero_two_square_norm_extracts_nonzero_quotientOn the explicit nonzero domain, a three-modulo-four prime square extracts with a nonzero represented quotient.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003P · prime_power_valuation_square_factor_shiftMultiplying a nonzero value by a nonzero square increases its prime valuation by exactly twice the factor valuation.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003Q · prime_power_valuation_square_factor_preserves_evennessA square-factor valuation step preserves constructive evenness of a nonzero quotient's prime valuation.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003R · three_mod_four_prime_nonzero_norm_positive_valuation_extractsA positive valuation of a nonzero represented norm at a three-modulo-four prime yields an exact nonzero represented prime-square quotient.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003S · prime_square_times_nonzero_strictly_increasesMultiplication of a nonzero natural by a prime square is strictly increasing in witnessed constructive order.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003T · three_mod_four_prime_two_square_norm_valuation_even_boundedBounded natural induction proves that a three-modulo-four prime has even valuation in every nonzero represented norm below the bound.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003U · three_mod_four_prime_two_square_norm_valuation_evenEvery three-modulo-four prime has a constructively even valuation in every explicitly nonzero two-square norm.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableTS003V · three_mod_four_prime_represented_nonzero_valuation_evenNecessity direction: every prime congruent to three modulo four has an explicitly even valuation in any represented nonzero natural.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not Stable