PA0001 · zero_addZero is a left identity for addition; unlike PA3, this needs induction.
layer 0 · 3 lines · Stable checked-use theorem · independently closedCurrent 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.
PA0002 · mul_oneOne is a right identity for multiplication.
layer 1 · 2 lines · Stable checked-use theorem · independently closedPA0003 · prime_divisor_eq_one_or_selfEvery divisor of a prime is one or the prime itself.
layer 2 · 19 lines · Stable checked-use theorem · independently closedPA0004 · add_eq_zero_rightA sum equal to zero has zero as its right addend.
layer 0 · 9 lines · Stable checked-use theorem · independently closedPA0005 · succ_ne_zeroNo successor is zero (the reusable PA1 lemma).
layer 0 · 1 lines · Stable checked-use theorem · independently closedPA0006 · beta_range_emptyEvery consecutive beta range of length zero is vacuous.
layer 1 · 18 lines · Stable checked-use theorem · independently closedPA0007 · mul_eq_zeroZero products have a zero factor: the 23-entry core capstone.
layer 1 · 12 lines · Stable checked-use theorem · independently closedPA0008 · zero_or_succEvery natural is either zero or the successor of a natural.
layer 0 · 6 lines · Stable checked-use theorem · independently closedPA0009 · add_assocAddition is associative.
layer 0 · 5 lines · Stable checked-use theorem · independently closedPA000A · mul_addMultiplication distributes over addition on the right.
layer 1 · 5 lines · Stable checked-use theorem · independently closedPA000B · mul_assocMultiplication is associative.
layer 2 · 5 lines · Stable checked-use theorem · independently closedPA000C · multiple_mul_rightA right multiple of a multiple remains a multiple.
layer 3 · 8 lines · Stable checked-use theorem · independently closedPA000D · mul_zero_leftZero annihilates multiplication on the left.
layer 0 · 3 lines · Stable checked-use theorem · independently closedPA000E · add_succ_leftA successor can move through addition on the left.
layer 0 · 4 lines · Stable checked-use theorem · independently closedPA000F · add_commAddition is commutative.
layer 1 · 4 lines · Stable checked-use theorem · independently closedPA000G · mul_succ_leftA successor can move through multiplication on the left.
layer 2 · 6 lines · Stable checked-use theorem · independently closedPA000H · mul_commMultiplication is commutative.
layer 3 · 4 lines · Stable checked-use theorem · independently closedPA000I · bounded_common_multiple_stepExtend a nonzero common multiple through the next positive natural.
layer 4 · 52 lines · Stable checked-use theorem · independently closedPA000J · add_eq_zero_leftA sum equal to zero has zero as its left addend.
layer 2 · 9 lines · Stable checked-use theorem · independently closedPA000K · bounded_common_multiple_existsEvery finite initial interval has a nonzero common-multiple surrogate.
layer 5 · 29 lines · Stable checked-use theorem · independently closedPA000L · scaled_bounded_common_multipleA right multiple of a bounded common multiple remains such a common multiple.
layer 4 · 15 lines · Stable checked-use theorem · independently closedPA000M · one_mulOne is a left identity for multiplication.
layer 0 · 3 lines · Stable checked-use theorem · independently closedPA000N · mul_eq_one_componentsA product is one only when both natural factors are one.
layer 1 · 39 lines · Stable checked-use theorem · independently closedPA000O · divisor_oneEvery natural divisor of one equals one.
layer 2 · 11 lines · Stable checked-use theorem · independently closedPA000P · coprime_one_leftOne is coprime to every natural in the expanded common-divisor relation.
layer 3 · 7 lines · Stable checked-use theorem · independently closedPA000Q · le_succ_selfEvery natural number is below its successor.
layer 1 · 3 lines · Stable checked-use theorem · independently closedPA000R · le_transOrder witnesses compose by addition, so the defined order is transitive.
layer 1 · 9 lines · Stable checked-use theorem · independently closedPA000S · mul_ne_zeroA product of two nonzero naturals is nonzero.
layer 2 · 15 lines · Stable checked-use theorem · independently closedPA000T · right_factor_divides_productThe right factor divides a product.
layer 4 · 4 lines · Stable checked-use theorem · independently closedPA000U · beta_modulus_nonzeroEvery Gödel-beta decoding modulus is nonzero.
layer 1 · 4 lines · Stable checked-use theorem · independently closedPA000V · le_of_succ_le_succSuccessor order reflects to the underlying naturals.
layer 0 · 10 lines · Stable checked-use theorem · independently closedPA000W · le_eq_or_ltA witnessed inequality is either equality or a witnessed strict inequality.
layer 1 · 21 lines · Stable checked-use theorem · independently closedPA000X · lt_to_leA witnessed strict inequality entails the corresponding weak inequality.
layer 1 · 11 lines · Stable checked-use theorem · independently closedPA000Y · no_succ_add_fixedAdding a positive successor cannot leave a natural number fixed.
layer 0 · 11 lines · Stable checked-use theorem · independently closedPA0010 · lt_irrefl_expandedNo natural is strictly below itself, with strict order fully expanded.
layer 1 · 12 lines · Stable checked-use theorem · independently closedPA0011 · lt_trichotomyTwo naturals are equal or strictly ordered in exactly one displayed direction.
layer 0 · 39 lines · Stable checked-use theorem · independently closedPA0012 · add_right_cancelA common right addend can be cancelled.
layer 0 · 13 lines · Stable checked-use theorem · independently closedPA0013 · factor_differenceA common-factor difference is itself a multiple of that factor.
layer 2 · 47 lines · Stable checked-use theorem · independently closedPA0014 · divides_remainderA common divisor of a dividend and divisor also divides the remainder.
layer 3 · 24 lines · Stable checked-use theorem · independently closedPA0015 · beta_modulus_coprime_baseEvery beta-shaped successor modulus is coprime to its base c.
layer 4 · 20 lines · Stable checked-use theorem · independently closedPA0016 · add_mulMultiplication distributes over addition on the left.
layer 4 · 4 lines · Stable checked-use theorem · independently closedPA0017 · common_divisor_beta_moduli_divides_gap_times_cA common divisor of two ordered beta moduli divides the index gap times c.
layer 5 · 27 lines · Stable checked-use theorem · independently closedPA0018 · multiple_transThe multiple relation is transitive.
layer 3 · 11 lines · Stable checked-use theorem · independently closedPA0019 · multiple_reflEvery natural number is a multiple of itself.
layer 2 · 4 lines · Stable checked-use theorem · independently closedPA001A · le_reflThe defined order is reflexive; zero is its witness.
layer 1 · 3 lines · Stable checked-use theorem · independently closedPA001B · le_zeroOnly zero is less than or equal to zero.
layer 1 · 5 lines · Stable checked-use theorem · independently closedPA001C · division_remainder_succEvery dividend has a quotient and bounded remainder for a successor divisor.
layer 1 · 38 lines · Stable checked-use theorem · independently closedPA001D · division_remainder_existsEvery positive divisor admits a quotient and a strictly bounded remainder.
layer 2 · 14 lines · Stable checked-use theorem · independently closedPA001E · multiple_zeroZero is a multiple of every natural number.
layer 0 · 4 lines · Stable checked-use theorem · independently closedPA001F · is_gcd_zero_rightEvery natural is the relational gcd of itself and zero.
layer 3 · 11 lines · Stable checked-use theorem · independently closedPA001G · divides_linear_stepA common divisor of a divisor and remainder divides their Euclidean linear step.
layer 3 · 17 lines · Stable checked-use theorem · independently closedPA001H · is_gcd_euclid_forwardA relational gcd of divisor and remainder is a gcd of dividend and divisor.
layer 4 · 35 lines · Stable checked-use theorem · independently closedPA001I · add_permute_outerPermute the outer entries of two additive pairs.
layer 2 · 25 lines · Stable checked-use theorem · independently closedPA001J · balanced_bezout_euclid_stepTransport balanced natural Bezout coefficients across one Euclidean division step.
layer 5 · 67 lines · Stable checked-use theorem · independently closedPA001K · gcd_balanced_bezout_exists_up_toBounded Euclidean descent simultaneously constructs a relational gcd and balanced natural Bezout witnesses.
layer 6 · 80 lines · Stable checked-use theorem · independently closedPA001L · gcd_balanced_bezout_existsEvery pair has a relational gcd together with balanced natural Bezout witnesses.
layer 7 · 11 lines · Stable checked-use theorem · independently closedPA001M · coprime_balanced_bezoutCoprime inputs admit balanced natural Bezout coefficients with result one.
layer 8 · 24 lines · Stable checked-use theorem · independently closedPA001N · balanced_combination_scale_rightScale a balanced natural combination on the right.
layer 5 · 56 lines · Stable checked-use theorem · independently closedPA001O · common_divisor_divides_balanced_resultEvery common divisor of two inputs divides the result of a balanced natural combination.
layer 3 · 48 lines · Stable checked-use theorem · independently closedPA001P · gauss_coprime_cancelCancel a coprime factor from a divisibility witness (Gauss cancellation).
layer 9 · 30 lines · Stable checked-use theorem · independently closedPA001Q · beta_moduli_coprime_of_gap_dvdBeta moduli at an additive index gap dividing c are coprime.
layer 10 · 59 lines · Stable checked-use theorem · independently closedPA001R · beta_moduli_coprime_of_lt_bounded_common_multipleOrdered bounded indices have coprime beta moduli when c is a common multiple of the bounded positive gaps.
layer 11 · 49 lines · Stable checked-use theorem · independently closedPA001S · beta_moduli_pairwise_coprime_boundedDistinct indices in a bounded prefix have pairwise coprime beta moduli under a bounded common-multiple invariant.
layer 12 · 44 lines · Stable checked-use theorem · independently closedPA001T · coprime_mul_leftCoprimality with a fixed right operand is closed under multiplication on the left.
layer 10 · 34 lines · Stable checked-use theorem · independently closedPA001U · beta_exclusive_accumulated_product_stepExtend the accumulated target-modulus product for an exclusive prefix.
layer 13 · 95 lines · Stable checked-use theorem · independently closedPA001V · nonzero_is_succEvery nonzero natural has a predecessor.
layer 0 · 8 lines · Stable checked-use theorem · independently closedPA001W · bezout_mod_leftA balanced Bezout identity selects the right coefficient modulo the left modulus.
layer 2 · 19 lines · Stable checked-use theorem · independently closedPA001X · bezout_mod_rightA balanced Bezout identity selects the left coefficient modulo the right modulus.
layer 1 · 13 lines · Stable checked-use theorem · independently closedPA001Y · mod_eq_mul_rightBalanced congruence is preserved by multiplication on the right.
layer 5 · 26 lines · Stable checked-use theorem · independently closedPA0020 · mod_eq_mul_leftBalanced congruence is preserved by multiplication on the left.
layer 6 · 25 lines · Stable checked-use theorem · independently closedPA0021 · dvd_to_mod_zeroA multiple is balanced-congruent to zero.
layer 1 · 8 lines · Stable checked-use theorem · independently closedPA0022 · mod_eq_addBalanced natural congruence respects addition.
layer 3 · 42 lines · Stable checked-use theorem · independently closedPA0023 · mod_eq_reflBalanced natural congruence is reflexive.
layer 0 · 5 lines · Stable checked-use theorem · independently closedPA0024 · mod_eq_transBalanced natural congruence is transitive.
layer 2 · 42 lines · Stable checked-use theorem · independently closedPA0025 · mod_eq_predecessor_cancelThe predecessor of a successor acts as minus one in balanced congruence.
layer 3 · 15 lines · Stable checked-use theorem · independently closedPA0026 · binary_crtConstructive binary CRT for positive coprime natural moduli using balanced congruence.
layer 9 · 276 lines · Stable checked-use theorem · independently closedPA0027 · mod_eq_of_mod_eq_multipleBalanced congruence descends from a multiple modulus to every divisor modulus.
layer 3 · 23 lines · Stable checked-use theorem · independently closedPA0028 · binary_crt_fold_stepOne binary CRT extension preserves every old congruence whose modulus divides the accumulated product.
layer 10 · 40 lines · Stable checked-use theorem · independently closedPA0029 · beta_at_existsEvery Gödel-beta position has a bounded decoded residue.
layer 4 · 24 lines · Stable checked-use theorem · independently closedPA002A · le_totalEvery pair of natural numbers is comparable in the defined order.
layer 0 · 23 lines · Stable checked-use theorem · independently closedPA002B · add_left_cancelA common left addend can be cancelled.
layer 2 · 13 lines · Stable checked-use theorem · independently closedPA002C · lt_not_eq_add_middleA strict upper bound prevents the lower term from containing that bound as an additive middle block.
layer 1 · 44 lines · Stable checked-use theorem · independently closedPA002D · positive_quotient_gap_impossibleA positive gap between quotients makes two bounded-remainder decompositions unequal.
layer 3 · 34 lines · Stable checked-use theorem · independently closedPA002E · division_remainder_uniqueBounded quotient-remainder decompositions have unique quotients and remainders.
layer 4 · 74 lines · Stable checked-use theorem · independently closedPA002F · beta_at_uniqueThe decoded residue at a Gödel-beta position is unique.
layer 5 · 37 lines · Stable checked-use theorem · independently closedPA002G · beta_exclusive_recode_congruence_stepAdd the next source value to a target-base CRT code for an exclusive prefix.
layer 11 · 92 lines · Stable checked-use theorem · independently closedPA002H · beta_exclusive_recode_invariant_stepCombine modulus-product and cross-base congruence updates for an exclusive prefix.
layer 14 · 49 lines · Stable checked-use theorem · independently closedPA002I · bounded_beta_exclusive_recode_invariantFold an empty-based, exclusive beta prefix into another base with append readiness.
layer 15 · 89 lines · Stable checked-use theorem · independently closedPA002J · le_add_leftAdding on the left produces an explicit order witness.
layer 0 · 4 lines · Stable checked-use theorem · independently closedPA002K · succ_le_succSuccessor preserves the witness-defined order.
layer 0 · 8 lines · Stable checked-use theorem · independently closedPA002L · one_le_of_ne_zeroEvery nonzero natural is at least one.
layer 0 · 8 lines · Stable checked-use theorem · independently closedPA002M · mul_le_mul_rightRight multiplication preserves the witness-defined order.
layer 5 · 12 lines · Stable checked-use theorem · independently closedPA002N · le_scaled_nonzeroScaling by a nonzero natural does not decrease a natural.
layer 6 · 16 lines · Stable checked-use theorem · independently closedPA002O · le_succA weak inequality remains true after raising its upper bound by one.
layer 1 · 9 lines · Stable checked-use theorem · independently closedPA002P · base_le_beta_modulusA beta base is at most every beta modulus over that base.
layer 3 · 13 lines · Stable checked-use theorem · independently closedPA002Q · new_value_lt_scaled_baseThe appended value fits every modulus after the same constructive scaled-base rebase.
layer 7 · 36 lines · Stable checked-use theorem · independently closedPA002R · beta_value_le_codeEvery decoded beta value is at most its code.
layer 0 · 10 lines · Stable checked-use theorem · independently closedPA002S · le_add_rightAdding on the right produces an explicit order witness.
layer 2 · 4 lines · Stable checked-use theorem · independently closedPA002T · beta_value_lt_scaled_baseAn old beta value fits every modulus after a constructive scaled-base rebase.
layer 7 · 54 lines · Stable checked-use theorem · independently closedPA002U · mod_eq_bounded_uniqueTwo balanced-congruent values below the same modulus are equal.
layer 5 · 28 lines · Stable checked-use theorem · independently closedPA002V · mod_eq_to_remainder_decompositionA bounded balanced residue has a directed quotient/remainder witness.
layer 6 · 51 lines · Stable checked-use theorem · independently closedPA002W · beta_at_of_mod_eq_boundA bounded value congruent to a code is its expanded Gödel-beta value.
layer 7 · 17 lines · Stable checked-use theorem · independently closedPA002X · beta_prefix_extendRebase an arbitrary decoded prefix and append one exact natural value.
layer 16 · 105 lines · Stable checked-use theorem · independently closedPA002Y · beta_range_succ_extendRecode a consecutive prefix and append its next value.
layer 17 · 42 lines · Stable checked-use theorem · independently closedPA0030 · beta_range_existsEvery start and length admit a beta-coded consecutive range.
layer 18 · 20 lines · Stable checked-use theorem · independently closedPA0031 · prime_nonzeroEvery prime natural is nonzero.
layer 1 · 20 lines · Stable checked-use theorem · independently closedPA0032 · beta_range_entry_eqA decoded entry of a Range prefix is its start plus its index.
layer 6 · 21 lines · Stable checked-use theorem · independently closedPA0033 · lt_of_le_of_ltWeak order followed by strict order remains strict.
layer 1 · 13 lines · Stable checked-use theorem · independently closedPA0034 · beta_half_range_entry_boundsEntries 1 through h in an odd half-range are nonzero and below p.
layer 7 · 53 lines · Stable checked-use theorem · independently closedPA0035 · gcd_exists_up_toBounded induction constructs a relational gcd whenever the right input is at most the bound.
layer 5 · 74 lines · Stable checked-use theorem · independently closedPA0036 · gcd_exists_relationalEvery pair of naturals has a relational greatest common divisor.
layer 6 · 11 lines · Stable checked-use theorem · independently closedPA0037 · is_gcd_one_to_coprimeA relational gcd witness one implies expanded coprimality.
layer 3 · 15 lines · Stable checked-use theorem · independently closedPA0038 · euclid_prime_dvd_productA prime dividing a product divides at least one factor (Euclid's lemma).
layer 10 · 36 lines · Stable checked-use theorem · independently closedPA0039 · divisor_le_nonzeroA divisor of a nonzero natural is bounded by that natural.
layer 1 · 31 lines · Stable checked-use theorem · independently closedPA003A · lt_not_leA strict inequality excludes the reverse weak inequality.
layer 0 · 34 lines · Stable checked-use theorem · independently closedPA003B · le_or_ltAny two naturals satisfy weak order in one direction or strict order in the other.
layer 0 · 26 lines · Stable checked-use theorem · independently closedPA003C · remainder_decomposition_to_mod_eqA directed quotient/remainder equation gives balanced congruence to its remainder.
layer 4 · 16 lines · Stable checked-use theorem · independently closedPA003D · finite_lt_succ_eq_or_ltA value below a successor is the predecessor or lies below it.
layer 2 · 12 lines · Stable checked-use theorem · independently closedPA003E · beta_at_self_of_boundA value below a Gödel-beta modulus decodes to itself when used as the code.
layer 1 · 12 lines · Stable checked-use theorem · independently closedPA003F · zero_leZero is below every natural number.
layer 0 · 4 lines · Stable checked-use theorem · independently closedPA003G · beta_prefix_sum_trace_existsEvery decoded beta prefix admits an exact beta-coded prefix-sum trace.
layer 17 · 136 lines · Stable checked-use theorem · independently closedPA003H · beta_sum_existsEvery decoded beta prefix has a relational finite sum.
layer 18 · 25 lines · Stable checked-use theorem · independently closedPA003I · bit_count_existsEvery all-bits prefix has a relational count of its ones.
layer 19 · 12 lines · Stable checked-use theorem · independently closedPA003J · add_le_add_rightAdding the same right summand preserves the witness-defined order.
layer 1 · 12 lines · Stable checked-use theorem · independently closedPA003K · add_le_add_leftAdding the same left summand preserves the witness-defined order.
layer 2 · 18 lines · Stable checked-use theorem · independently closedPA003L · mod_eq_symmBalanced natural congruence is symmetric.
layer 0 · 10 lines · Stable checked-use theorem · independently closedPA003M · prime_coprime_or_dividesA prime is constructively either coprime to a natural or divides it.
layer 7 · 30 lines · Stable checked-use theorem · independently closedPA003N · prime_not_divides_coprimeA prime not dividing a natural is coprime to that natural.
layer 8 · 14 lines · Stable checked-use theorem · independently closedPA003O · coprime_symmCoprimality in its expanded common-divisor form is symmetric.
layer 0 · 10 lines · Stable checked-use theorem · independently closedPA003P · coprime_balanced_mod_inverseBalanced Bezout coefficients give a subtraction-free modular inverse.
layer 9 · 20 lines · Stable checked-use theorem · independently closedPA003Q · coprime_mod_inverseA nonzero modulus turns balanced Bezout data into a natural modular inverse.
layer 10 · 66 lines · Stable checked-use theorem · independently closedPA003R · mod_eq_cancel_coprimeA coprime factor cancels from balanced congruence at nonzero modulus.
layer 11 · 114 lines · Stable checked-use theorem · independently closedPA003S · prime_mod_cancelA nonzero residue factor cancels from congruence modulo a prime.
layer 12 · 32 lines · Stable checked-use theorem · independently closedPA003T · beta_range_injectiveEqual decoded values in one consecutive range have equal indices.
layer 7 · 48 lines · Stable checked-use theorem · independently closedPA003U · ne_zero_of_one_leA natural at least one is nonzero.
layer 0 · 8 lines · Stable checked-use theorem · independently closedPA003V · succ_injectiveSuccessor is injective (the reusable PA2 lemma).
layer 0 · 1 lines · Stable checked-use theorem · independently closedPA003W · beta_prefix_product_trace_existsEvery decoded beta factor prefix admits a beta-coded exact prefix-product trace.
layer 17 · 133 lines · Stable checked-use theorem · independently closedPA003X · beta_product_existsEvery finite decoded beta prefix has an exact relational product and a coded trace.
layer 18 · 25 lines · Stable checked-use theorem · independently closedPA003Y · beta_sum_succ_decomposeA successor sum decomposes into its prefix sum and final summand.
layer 6 · 51 lines · Stable checked-use theorem · independently closedPA0040 · all_bits_prefix_succDropping the final entry preserves the all-bits invariant.
layer 2 · 15 lines · Stable checked-use theorem · independently closedPA0041 · all_bits_last_succThe final entry of a nonempty all-bits prefix is zero or one.
layer 2 · 11 lines · Stable checked-use theorem · independently closedPA0042 · bit_count_succ_decomposeA successor count is its prefix count plus a final zero-or-one bit.
layer 7 · 63 lines · Stable checked-use theorem · independently closedPA0043 · beta_repeat_emptyEvery constant beta prefix of length zero is vacuously Repeat.
layer 1 · 18 lines · Stable checked-use theorem · independently closedPA0044 · beta_repeat_succ_extendRecode a constant prefix and append one more copy of its value.
layer 17 · 40 lines · Stable checked-use theorem · independently closedPA0045 · beta_repeat_existsEvery value and length admit a beta-coded constant prefix.
layer 18 · 20 lines · Stable checked-use theorem · independently closedPA0046 · pow_existsEvery base and exponent have a relational finite-product power.
layer 19 · 22 lines · Stable checked-use theorem · independently closedPA0047 · beta_sum_zeroThe sum of an empty decoded prefix is zero.
layer 6 · 16 lines · Stable checked-use theorem · independently closedPA0048 · bit_count_zeroAn empty bit prefix contains zero ones.
layer 7 · 15 lines · Stable checked-use theorem · independently closedPA0049 · beta_product_zeroThe product of an empty decoded prefix is one.
layer 6 · 16 lines · Stable checked-use theorem · independently closedPA004A · beta_product_succ_decomposeA successor product decomposes into its prefix product and final decoded factor.
layer 6 · 51 lines · Stable checked-use theorem · independently closedPA004B · pow_zeroThe relational zeroth power is one.
layer 7 · 17 lines · Stable checked-use theorem · independently closedPA004C · beta_repeat_entry_eqEvery decoded entry of a Repeat prefix equals its repeated value.
layer 6 · 21 lines · Stable checked-use theorem · independently closedPA004D · pow_successor_decomposeA successor relational power is its predecessor power times the base.
layer 7 · 54 lines · Stable checked-use theorem · independently closedPA004E · mod_eq_mulBalanced natural congruence respects multiplication.
layer 7 · 28 lines · Stable checked-use theorem · independently closedPA004F · finite_surjective_zeroThe empty decoded prefix is surjective onto the empty interval.
layer 1 · 17 lines · Stable checked-use theorem · independently closedPA004G · eq_decidableEquality of natural numbers is constructively decidable.
layer 0 · 27 lines · Stable checked-use theorem · independently closedPA004H · finite_contains_decidableOccurrence of a value in a nonempty decoded prefix is constructively decidable.
layer 6 · 77 lines · Stable checked-use theorem · independently closedPA004I · finite_bounded_last_succA bounded successor prefix exposes a bounded final decoded value.
layer 2 · 12 lines · Stable checked-use theorem · independently closedPA004J · beta_prefix_replace_existsRecode a finite beta prefix while replacing one interior entry.
layer 17 · 122 lines · Stable checked-use theorem · independently closedPA004K · beta_prefix_swap_last_from_entriesSwap a chosen interior beta entry with the last entry, given both decoded values.
layer 18 · 87 lines · Stable checked-use theorem · independently closedPA004L · finite_bounded_entry_ltEvery explicitly decoded entry of a bounded prefix satisfies its value bound.
layer 6 · 25 lines · Stable checked-use theorem · independently closedPA004M · finite_swap_last_boundedA swap-last recoding preserves boundedness of the full successor prefix.
layer 7 · 93 lines · Stable checked-use theorem · independently closedPA004N · beta_prefix_swap_last_reflectEvery decoded swapped entry reflects to one of the two moved entries or the original index.
layer 6 · 77 lines · Stable checked-use theorem · independently closedPA004O · finite_swap_last_injectiveA swap-last recoding preserves injectivity of the full successor prefix.
layer 7 · 220 lines · Stable checked-use theorem · independently closedPA004P · finite_bounded_prefix_without_topIf a successor prefix omits its top value, its old prefix is bounded by the predecessor.
layer 3 · 37 lines · Stable checked-use theorem · independently closedPA004Q · finite_injective_prefix_succInjectivity of a successor prefix restricts to its old prefix.
layer 2 · 29 lines · Stable checked-use theorem · independently closedPA004R · finite_last_is_top_from_prefix_surjectiveA bounded injective successor sequence must place the new value last once its prefix is surjective.
layer 3 · 53 lines · Stable checked-use theorem · independently closedPA004S · finite_surjective_succ_introA surjective prefix plus its new top value is surjective at successor length.
layer 3 · 37 lines · Stable checked-use theorem · independently closedPA004T · finite_surjective_succ_from_prefixThe available successor branch extends prefix surjectivity to the full prefix.
layer 4 · 26 lines · Stable checked-use theorem · independently closedPA004U · finite_swap_last_surjective_backSurjectivity of a swapped successor prefix transports back to the original code.
layer 7 · 80 lines · Stable checked-use theorem · independently closedPA004V · finite_no_top_successor_gateThe no-top branch of the constructive successor induction is complete.
layer 5 · 48 lines · Stable checked-use theorem · independently closedPA004W · finite_bounded_injective_surjectiveEvery bounded injective beta-coded prefix is surjective onto its finite interval.
layer 19 · 178 lines · Stable checked-use theorem · independently closedPA004X · finite_fixed_last_prefix_boundedA bounded injective successor reindexing fixed at its last position is bounded on the old prefix.
layer 4 · 39 lines · Stable checked-use theorem · independently closedPA004Y · beta_product_transport_prefixOne-way extensional factor-prefix preservation transports Product without changing its trace.
layer 0 · 44 lines · Stable checked-use theorem · independently closedPA0050 · mul_congrMultiplication preserves equality in both arguments.
layer 0 · 9 lines · Stable checked-use theorem · independently closedPA0051 · beta_product_functionalThe fully expanded beta-coded Product relation is functional in its terminal product.
layer 6 · 153 lines · Stable checked-use theorem · independently closedPA0052 · beta_product_replace_balanceReplacing one factor balances the old and new finite products by the exchanged values.
layer 7 · 202 lines · Stable checked-use theorem · independently closedPA0053 · beta_product_swap_last_invariantSwapping an interior beta-coded factor with the last factor preserves the exact finite product.
layer 8 · 102 lines · Stable checked-use theorem · independently closedPA0054 · beta_reindex_alignment_swap_lastSimultaneous interior/final swaps of an index code and target factors preserve alignment.
layer 7 · 102 lines · Stable checked-use theorem · independently closedPA0055 · even_odd_exclusive_pointwiseAn even and an odd decomposition of the same natural are incompatible.
layer 5 · 24 lines · Stable checked-use theorem · independently closedPA0056 · odd_not_evenNo odd natural is even.
layer 6 · 11 lines · Stable checked-use theorem · independently closedPA0057 · parity_casesEvery natural has a constructive even-or-odd witness.
layer 0 · 14 lines · Stable checked-use theorem · independently closedPA0058 · successor_odd_of_evenThe successor of an even natural is odd.
layer 0 · 6 lines · Stable checked-use theorem · independently closedPA0059 · even_not_oddNo even natural is odd.
layer 6 · 11 lines · Stable checked-use theorem · independently closedPA005A · even_successor_to_oddIf a successor is even, its predecessor is odd.
layer 7 · 17 lines · Stable checked-use theorem · independently closedPA005B · successor_even_of_oddThe successor of an odd natural is even.
layer 0 · 6 lines · Stable checked-use theorem · independently closedPA005C · odd_successor_to_evenIf a successor is odd, its predecessor is even.
layer 7 · 17 lines · Stable checked-use theorem · independently closedPA005D · predecessor_square_mod_oneThe predecessor of a successor squares to one modulo that successor.
layer 3 · 8 lines · Stable checked-use theorem · independently closedPA005E · pow_predecessor_parity_modPowers of the predecessor of p alternate between one and the predecessor modulo p.
layer 8 · 107 lines · Stable checked-use theorem · independently closedPA005F · beta_repeat_transport_entryRepeat prefixes with one value preserve every decoded entry extensionally.
layer 7 · 28 lines · Stable checked-use theorem · independently closedPA005G · pow_functionalRelational powers have a unique natural value.
layer 8 · 56 lines · Stable checked-use theorem · independently closedPA005H · pow_successor_pair_mulA successor power paired with its predecessor equals predecessor times base.
layer 9 · 30 lines · Stable checked-use theorem · independently closedPA005I · pow_mod_congruentBalanced-congruent bases have congruent relational powers at every exponent.
layer 10 · 92 lines · Stable checked-use theorem · independently closedPA005J · mod_eq_decidable_from_remaindersCanonical bounded remainders constructively decide congruence.
layer 6 · 89 lines · Stable checked-use theorem · independently closedPA005K · mod_eq_decidable_nonzeroBalanced congruence is constructively decidable at nonzero modulus.
layer 7 · 44 lines · Stable checked-use theorem · independently closedPA005L · quadratic_residue_search_up_toInclusive bounded search constructively decides square congruence.
layer 8 · 91 lines · Stable checked-use theorem · independently closedPA005M · quadratic_residue_bounded_decidable_nonzeroA nonzero modulus admits a finite constructive residue search.
layer 9 · 46 lines · Stable checked-use theorem · independently closedPA005N · square_decompExpand a square while retaining an explicit quotient and remainder.
layer 5 · 45 lines · Stable checked-use theorem · independently closedPA005O · add_residueAbsorb a second quotient into an existing residue equation.
layer 2 · 17 lines · Stable checked-use theorem · independently closedPA005P · square_residue_liftLift one quotient-and-remainder equation through squaring.
layer 6 · 13 lines · Stable checked-use theorem · independently closedPA005Q · square_residue_witnessExistential wrapper for the generic square-residue lift.
layer 7 · 12 lines · Stable checked-use theorem · independently closedPA005R · quadratic_residue_bounded_equivEvery square witness has an equivalent canonical bounded root.
layer 8 · 64 lines · Stable checked-use theorem · independently closedPA005S · quadratic_residue_decidable_nonzeroQuadratic residuosity is constructively decidable at nonzero modulus.
layer 10 · 23 lines · Stable checked-use theorem · independently closedPA005T · pow_one_from_zero_successorA successor of a zero exponent gives the relational first power.
layer 8 · 29 lines · Stable checked-use theorem · independently closedPA005U · pow_oneThe relational first power of a natural is the natural itself.
layer 9 · 13 lines · Stable checked-use theorem · independently closedPA005V · pow_two_from_one_successorA successor of exponent one gives the relational square.
layer 10 · 28 lines · Stable checked-use theorem · independently closedPA005W · pow_twoThe relational second power is exactly the square.
layer 11 · 13 lines · Stable checked-use theorem · independently closedPA005X · pow_addRelational powers turn addition of exponents into multiplication.
layer 9 · 90 lines · Stable checked-use theorem · independently closedPA005Y · pow_mul_expIterated relational powers multiply their exponents.
layer 20 · 92 lines · Stable checked-use theorem · independently closedPA0060 · factorial_existsEvery natural has a beta-coded relational factorial value.
layer 19 · 21 lines · Stable checked-use theorem · independently closedPA0061 · prime_is_succ_succEvery prime natural is the second successor of a natural.
layer 2 · 29 lines · Stable checked-use theorem · independently closedPA0062 · prime_mod_inverseA nonzero residue modulo a prime has a natural modular inverse.
layer 11 · 29 lines · Stable checked-use theorem · independently closedPA0063 · prime_bounded_nonzero_mod_inverseA nonzero residue below a prime has a nonzero bounded inverse.
layer 12 · 125 lines · Stable checked-use theorem · independently closedPA0064 · prime_ne_two_is_oddEvery prime other than two is odd.
layer 1 · 25 lines · Stable checked-use theorem · independently closedPA0065 · factorial_succ_decomposeA successor factorial is its predecessor factorial times the successor.
layer 7 · 60 lines · Stable checked-use theorem · independently closedPA0066 · factorial_zeroThe relational factorial of zero is one.
layer 7 · 16 lines · Stable checked-use theorem · independently closedPA0067 · drop_add_prefix_from_fixedA fixed-point equation remains fixed after dropping an additive prefix.
layer 1 · 17 lines · Stable checked-use theorem · independently closedPA0068 · antisymm_from_witnessesOpposing additive witnesses force equality.
layer 2 · 19 lines · Stable checked-use theorem · independently closedPA0069 · le_antisymmThe witness-defined order is antisymmetric.
layer 3 · 9 lines · Stable checked-use theorem · independently closedPA00AK · bounded_mod_inverse_uniqueTwo bounded inverses of the same residue are equal.
layer 7 · 62 lines · Stable checked-use theorem · independently closedPA006A · beta_range_transport_entryTwo Range codes preserve every decoded entry extensionally.
layer 7 · 28 lines · Stable checked-use theorem · independently closedPA006B · factorial_functionalThe beta-coded relational factorial has a unique value.
layer 8 · 55 lines · Stable checked-use theorem · independently closedPA006C · mul_double_rightDoubling commutes through multiplication on the right.
layer 4 · 9 lines · Stable checked-use theorem · independently closedPA006D · odd_mul_oddThe product of two odd naturals is odd.
layer 5 · 14 lines · Stable checked-use theorem · independently closedPA006E · even_mul_rightA product with an even right factor is even.
layer 5 · 7 lines · Stable checked-use theorem · independently closedPA006F · even_add_oddAn even natural plus an odd natural is odd.
layer 2 · 10 lines · Stable checked-use theorem · independently closedPA006G · odd_add_evenAn odd natural plus an even natural is odd.
layer 2 · 10 lines · Stable checked-use theorem · independently closedPA006H · even_add_evenThe sum of two even naturals is even.
layer 2 · 10 lines · Stable checked-use theorem · independently closedPA006I · odd_add_oddThe sum of two odd naturals is even.
layer 2 · 10 lines · Stable checked-use theorem · independently closedPA006J · add_congrAddition preserves equality in both arguments.
layer 0 · 9 lines · Stable checked-use theorem · independently closedPA006K · beta_sum_trace_functionalTwo exact prefix-sum traces over one decoded prefix have equal endpoints.
layer 6 · 153 lines · Stable checked-use theorem · independently closedPA006L · lt_of_lt_of_leStrict order followed by weak order remains strict.
layer 2 · 11 lines · Stable checked-use theorem · independently closedPA006M · mul_le_mul_leftLeft multiplication preserves the witness-defined order.
layer 2 · 12 lines · Stable checked-use theorem · independently closedPA006N · division_block_upperA bounded remainder keeps its decomposition below the next divisor block.
layer 2 · 34 lines · Stable checked-use theorem · independently closedPA006O · lt_transStrict order is transitive.
layer 1 · 20 lines · Stable checked-use theorem · independently closedPA006P · beta_sum_functionalThe relational finite sum has a unique natural value.
layer 7 · 23 lines · Stable checked-use theorem · independently closedPA006Q · bit_count_functionalThe relational count of a fixed all-bits prefix is unique.
layer 8 · 17 lines · Stable checked-use theorem · independently closedPA006R · four_mul_eq_double_doubleMultiplication by four is iterated doubling.
layer 3 · 6 lines · Stable checked-use theorem · independently closedPA006S · mul_left_cancel_nonzeroA nonzero common left factor can be cancelled.
layer 3 · 42 lines · Stable checked-use theorem · independently closedPA006T · odd_half_uniqueThe half witness in an odd decomposition is unique.
layer 4 · 24 lines · Stable checked-use theorem · independently closedPA006U · even_mul_leftA product with an even left factor is even.
layer 3 · 7 lines · Stable checked-use theorem · independently closedPA006V · distinct_primes_left_not_divide_rightA prime cannot divide a distinct prime.
layer 3 · 19 lines · Alpha v34 checked-use theorem · independently closed; not StablePA006W · distinct_primes_right_not_divide_leftThe reverse orientation is nondivisible as well.
layer 4 · 18 lines · Alpha v34 checked-use theorem · independently closed; not StablePA006X · distinct_primes_mutually_nondivisibleDistinct primes are mutually nondivisible.
layer 5 · 22 lines · Alpha v34 checked-use theorem · independently closed; not StablePA006Y · odd_upper_remainder_reflectionA residue strictly above h and below 2*h+1 has a positive reflected magnitude at most h.
layer 3 · 50 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0070 · gauss_pointwise_signed_half_representativeA nonzero canonical product remainder has a positive half-range magnitude, with its sign recorded by a lower/reflected congruence disjunction.
layer 5 · 76 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0071 · gauss_pointwise_signed_half_choiceA canonical nonzero remainder yields one explicit zero/one signed-half choice at its decoded source index.
layer 6 · 62 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0072 · gauss_half_range_signed_choicesA prime odd half-range and a nondivisible multiplier provide a signed choice at every decoded entry.
layer 11 · 92 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0073 · gauss_signed_half_prefix_extendAppend one pointwise signed choice simultaneously to the magnitude and zero/one sign beta prefixes.
layer 17 · 108 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0074 · gauss_signed_half_prefix_existsEvery bounded family of pointwise signed choices admits aligned beta-coded magnitude and sign prefixes.
layer 18 · 60 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0075 · gauss_half_range_signed_prefix_existsThe full prime odd half-range has beta-coded positive magnitudes and explicit reflection bits.
layer 19 · 28 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0076 · gauss_signed_half_prefix_all_bitsThe sign projection of every encoded signed-half prefix is an AllBits prefix.
layer 0 · 30 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0077 · gauss_signed_half_bit_count_existsThe encoded reflection bits have a native relational count of their ones.
layer 20 · 29 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0078 · gauss_signed_half_magnitude_rangeEvery decoded signed-prefix magnitude lies constructively in 1,...,h.
layer 0 · 31 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0079 · prime_scaled_same_target_uniqueA nonzero prime residue multiplier is injective when two bounded sources have one modular target.
layer 13 · 41 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007A · gauss_same_sign_scaled_source_uniqueEqual lower signs or equal reflected signs force equality of the bounded source residues.
layer 14 · 38 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007B · gauss_mixed_sign_scaled_source_impossibleOpposite signed representatives cannot share one magnitude when their positive source sum is below p.
layer 13 · 90 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007C · gauss_signed_half_magnitude_injectiveThe positive signed-half magnitude prefix is injective over the full beta-coded half range.
layer 15 · 281 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007D · beta_magnitude_predecessor_recode_existsEvery positive bounded beta prefix can be recoded pointwise by removing one successor from each value.
layer 17 · 106 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007E · gauss_signed_half_predecessor_recode_existsThe signed-half magnitude prefix admits a beta code of its 0,...,h-1 predecessors.
layer 18 · 29 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007F · beta_sign_factor_prefix_extendAppend the selected 1/r factor while preserving every earlier decoded factor.
layer 17 · 95 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007G · beta_sign_factor_prefix_existsEvery finite beta bit prefix admits a beta-coded 1/r sign-factor prefix.
layer 18 · 75 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007H · beta_sign_factor_prefix_drop_lastDropping the final position preserves the bit-to-sign-factor relation.
layer 2 · 19 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007I · beta_sign_factor_product_powerThe product of 1/r sign factors is exactly r to the number of one bits.
layer 8 · 169 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007J · beta_sign_factor_product_power_existsFor p=S r, the recoded sign product exists and equals the relational power r^e.
layer 20 · 55 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007K · beta_pointwise_mul_prefix_extendAppend the product of the two final decoded values and preserve all earlier products.
layer 17 · 109 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007L · beta_pointwise_mul_prefix_existsTwo beta prefixes admit a third beta prefix of their pointwise products.
layer 18 · 54 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007M · beta_pointwise_mul_prefix_drop_lastPointwise multiplication alignment restricts to the predecessor prefix.
layer 2 · 28 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007N · beta_product_pointwise_mul_exactPointwise products of synchronized beta prefixes multiply their exact finite products.
layer 7 · 116 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007O · beta_pointwise_mul_product_existsThe pointwise-product code has a Product equal to the product of the two source Products.
layer 19 · 48 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007P · gauss_signed_pointwise_mul_scale_modSigned magnitudes times their 1/r factors are pointwise congruent to the scaled source prefix.
layer 6 · 110 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007Q · beta_product_pointwise_scale_modPointwise multiplication by a constant scales a finite product by its power.
layer 8 · 133 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007R · gauss_signed_pointwise_mul_product_modThe scaled canonical-source product is congruent to the product of signed magnitudes.
layer 9 · 61 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007S · beta_magnitude_predecessor_recode_boundedRemoving one successor turns the positive 1,...,l range bound into the finite 0,...,l-1 bound.
layer 1 · 38 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007T · beta_magnitude_predecessor_recode_reflectUnique target decoding reflects every predecessor-code entry back to its source successor magnitude.
layer 6 · 58 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007U · beta_magnitude_predecessor_recode_injectiveInjectivity of positive magnitudes transports to their uniquely decoded predecessor code.
layer 7 · 51 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007V · gauss_predecessor_half_range_alignedThe predecessor map aligns canonical factor 1+j with magnitude S j at every position.
layer 7 · 83 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007W · beta_product_reindex_fixed_lastA fixed-final reindex reduces successor product equality to equality of the two prefix products.
layer 7 · 65 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007X · beta_product_permutation_invariantA bounded injective beta-coded reindexing preserves the exact finite product.
layer 20 · 379 lines · Alpha v34 checked-use theorem · independently closed; not StablePA007Y · gauss_magnitude_product_eq_half_rangeA magnitude permutation has exactly the product of the canonical half range.
layer 21 · 61 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0080 · gauss_signed_products_balance_modThe four Gauss product layers compose to A*P == P*r^e modulo p.
layer 22 · 128 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0081 · beta_product_pointwise_coprimeA finite product of factors pointwise coprime to m is coprime to m.
layer 11 · 62 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0082 · prime_positive_bounded_product_coprimeA product of positive residues below a prime is coprime to that prime.
layer 12 · 51 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0083 · prime_half_range_product_coprimeThe canonical half-range product is coprime to its odd prime modulus.
layer 13 · 34 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0084 · gauss_signed_products_cancel_modCoprimality of the half-range product constructively cancels P.
layer 23 · 123 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0085 · gauss_lemma_power_congruence_existsGauss's signed half-range count controls a^h modulo the odd prime.
layer 24 · 193 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0086 · nondivisor_canonical_remainder_existsEvery nonmultiple has a nonzero canonical remainder congruent to it.
layer 5 · 39 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0087 · quadratic_residue_mod_equivQuadratic residuosity depends only on the balanced congruence class.
layer 3 · 31 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0088 · pow_congruent_base_witnessA congruent base has a relational power congruent to the supplied power.
layer 20 · 25 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0089 · bounded_nonzero_not_dividesA nonzero value strictly below a modulus is not divisible by it.
layer 2 · 16 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008A · mod_eq_zero_to_dvd_nonzeroFor a nonzero modulus, congruence to zero gives an explicit divisor witness.
layer 7 · 30 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008B · prime_mul_index_map_exists_up_toCanonical nonzero products modulo a prime form a beta-coded index map.
layer 17 · 168 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008C · beta_successor_lift_existsEvery decoded finite prefix can be recoded after successor-lifting its values.
layer 17 · 69 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008D · fermat_index_map_boundedThe canonical multiplication-residue index map is bounded.
layer 0 · 19 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008E · prime_mul_index_map_injectiveMultiplication by a nonzero prime residue is injective on 0,...,p-2.
layer 13 · 97 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008F · beta_range_one_entry_eq_succA decoded entry of the range 1,...,l is the successor of its index.
layer 7 · 30 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008G · beta_successor_range_reindex_alignedA bounded residue map aligns the range 1,...,n with its successor lift.
layer 8 · 53 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008H · beta_successor_range_scale_modThe range and its successor-lifted residue map are pointwise congruent after scaling.
layer 8 · 53 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008I · prime_mul_residue_reindex_existsA nonzero multiplier modulo a prime induces a beta-coded residue reindexing.
layer 18 · 85 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008J · prime_mul_residue_product_balanceScaling the nonzero residues modulo a prime preserves their exact product modulo p.
layer 21 · 71 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008K · prime_range_product_coprimeThe product 1*...*(p-1) is coprime to a prime p.
layer 12 · 70 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008L · fermat_predecessor_exponent_mod_oneFermat's theorem for the native predecessor exponent p-1.
layer 22 · 68 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008M · quadratic_residue_half_power_mod_oneA nonzero quadratic residue has half power one modulo an odd prime.
layer 23 · 136 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008N · scaled_inverse_from_unit_inverseMultiplying an ordinary inverse by the target gives a scaled inverse.
layer 7 · 33 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008O · scaled_inverse_transport_rightA scaled inverse survives replacement by a congruent right factor.
layer 7 · 27 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008P · prime_scaled_inverse_target_nonzeroA scaled inverse of a nonzero bounded target cannot be zero.
layer 6 · 44 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008Q · prime_scaled_inverse_existsEvery bounded nonzero prime residue has a bounded scaled inverse.
layer 13 · 83 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008R · prime_scaled_inverse_prefix_extendAppend one actual scaled-inverse value to a zero-based source prefix.
layer 17 · 76 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008S · prime_scaled_inverse_prefix_exists_boundedEvery bounded predecessor length has a beta-coded scaled-inverse prefix.
layer 18 · 63 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008T · prime_scaled_inverse_prefix_existsA prime predecessor interval has a full beta-coded scaled-inverse map.
layer 19 · 18 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008U · scaled_orbit_closed_prefix_zeroShifted orbit closure is vacuous on an empty order prefix.
layer 1 · 20 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008V · bounded_into_zeroEvery empty beta prefix is bounded into every codomain.
layer 1 · 15 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008W · injective_prefix_zeroDecoded-prefix injectivity is vacuous at length zero.
layer 1 · 19 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008X · scaled_pair_order_state_zeroZero codes witness the empty shifted, bounded, injective state.
layer 2 · 19 lines · Alpha v34 checked-use theorem · independently closed; not StablePA008Y · adjacent_scaled_orbit_history_zeroThe explicit adjacent scaled-orbit history is empty at zero pairs.
layer 1 · 16 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0090 · euler_pair_iteration_previous_balanceMove the newest pair from stored count to remaining count.
layer 2 · 3 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0091 · euler_pair_iteration_step_shortExpose a strict-prefix witness whenever at least one pair remains.
layer 2 · 3 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0092 · finite_covers_into_or_omitsBounded occurrence search either covers the target interval or returns an explicit omission.
layer 7 · 60 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0093 · finite_inverse_choice_prefix_extendAppend one chosen source preimage to a beta-coded inverse-choice prefix.
layer 17 · 55 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0094 · finite_inverse_choice_prefix_existsFull finite coverage admits a beta-coded choice of one preimage for each target value.
layer 18 · 52 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0095 · finite_inverse_choice_bounded_intoEvery inverse-choice prefix is bounded into the source domain.
layer 0 · 20 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0096 · finite_inverse_choice_injectiveA beta-coded choice of source preimages is injective by functionality of the source code.
layer 6 · 65 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0097 · finite_short_cover_impossibleA prefix shorter than the target interval cannot cover every target value.
layer 20 · 124 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0098 · finite_short_prefix_omitsEvery beta-coded prefix shorter than n explicitly omits a value below n.
layer 21 · 21 lines · Alpha v34 checked-use theorem · independently closed; not StablePA0099 · scaled_inverse_prefix_entry_soundEvery decoded scaled-inverse prefix entry satisfies its stored relation.
layer 6 · 30 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009A · scaled_inverse_prefix_mate_predecessorEvery positive decoded mate has a predecessor inside the source bound.
layer 7 · 44 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009B · scaled_inverse_symmetricThe scaled-inverse relation is symmetric.
layer 4 · 21 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009C · prime_scaled_inverse_uniqueThe bounded scaled inverse of a prime unit is unique.
layer 13 · 59 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009D · scaled_inverse_prefix_extensionalA valid scaled inverse at a covered source is decoded by the prefix.
layer 14 · 33 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009E · scaled_inverse_prefix_involutiveDecoding a scaled-inverse mate and decoding its predecessor returns the source residue.
layer 15 · 77 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009F · scaled_inverse_fixed_point_iffOn the bounded unit domain, fixed points are exactly square roots of a.
layer 0 · 17 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009G · scaled_inverse_no_fixed_of_not_qresA negative QRes witness makes the scaled involution fixed-point-free.
layer 1 · 16 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009H · scaled_inverse_prefix_no_fixed_of_not_qresA nonresidue scaled-inverse prefix has no decoded fixed point.
layer 7 · 31 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009I · scaled_inverse_prefix_choose_omitted_orbitChoose an omitted source, decode its actual mate S j, and expose a distinct involutive pair.
layer 22 · 78 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009J · scaled_orbit_closed_unused_mateShifted orbit closure transfers omission across a decoded back edge.
layer 0 · 28 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009K · beta_prefix_append_two_existsAppend two values at consecutive beta positions while preserving every old entry.
layer 17 · 52 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009L · beta_prefix_append_two_reflectEvery entry of a two-appended prefix is the second append, the first append, or an old entry.
layer 6 · 85 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009M · beta_prefix_append_two_scaled_orbit_closedAppending both zero-based sources preserves closure under actual-mate entries S j.
layer 7 · 119 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009N · beta_prefix_append_two_injectiveAppending two distinct values omitted by an injective old prefix preserves decoded-prefix injectivity.
layer 7 · 133 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009O · scaled_inverse_pair_order_choose_appendChoose one omitted fixed-point-free scaled orbit and append its two sources adjacently.
layer 23 · 114 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009P · beta_prefix_append_two_bounded_intoA two-entry append remains bounded when the old prefix and both appended values are bounded.
layer 3 · 54 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009Q · pair_index_left_below_doubleThe left position of an earlier pair lies below the doubled prefix.
layer 3 · 31 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009R · pair_index_right_below_doubleThe right position of an earlier pair lies below the doubled prefix.
layer 3 · 24 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009S · adjacent_scaled_orbit_history_appendAppend one adjacent pair while retaining its raw At(i,S j) scaled edge.
layer 4 · 73 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009T · scaled_inverse_pair_order_paired_state_stepAppend one fixed-point-free scaled orbit and preserve iterable state plus history.
layer 24 · 88 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009U · pair_order_double_succ_lengthNormalize the two-entry successor length into the next doubled pair count.
layer 1 · 6 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009V · scaled_inverse_pair_order_paired_iterationIterate exactly one adjacent scaled orbit for every stored pair.
layer 25 · 101 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009W · scaled_inverse_pair_order_terminal_packageAt n=h+h, package a complete adjacent scaled-orbit order of length n.
layer 26 · 29 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009X · scaled_pair_order_successor_lift_adjacent_targetsA successor-lifted terminal scaled-orbit history has adjacent products congruent to a.
layer 6 · 115 lines · Alpha v34 checked-use theorem · independently closed; not StablePA009Y · beta_product_double_succ_decomposeA product of length S(S k) decomposes into its k-prefix and its final two factors.
layer 7 · 44 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00A0 · beta_adjacent_target_pairs_product_powerAdjacent fixed-target pairs multiply to the corresponding relational power.
layer 8 · 118 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00A1 · scaled_pair_order_successor_lift_product_is_factorialA bounded injective order and its successor lift multiply to n factorial.
layer 21 · 82 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00A2 · prime_two_or_terminal_odd_shapeA prime is two or has exactly the doubled terminal PairOrder shape.
layer 3 · 36 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00A3 · factorial_one_valueThe relational factorial of one has value one.
layer 8 · 25 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00A4 · prime_inverse_index_existsEvery nonzero prime residue index has a bounded inverse index.
layer 13 · 44 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00A5 · prime_inverse_prefix_extendAppend one bounded zero-based inverse index to an inverse prefix.
layer 17 · 59 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00A6 · prime_inverse_prefix_exists_boundedEvery length bounded by p-1 has a beta-coded inverse prefix.
layer 18 · 51 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00A7 · prime_inverse_prefix_existsA prime predecessor interval has a full beta-coded inverse map.
layer 19 · 12 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00A8 · orbit_closed_prefix_zeroOrbit closure is vacuous on the empty decoded prefix.
layer 1 · 20 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00A9 · nonendpoint_prefix_zeroThe nonendpoint range invariant is vacuous on the empty prefix.
layer 1 · 17 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AA · pair_order_state_zeroArbitrary zero codes witness the empty PairOrder invariant state.
layer 2 · 24 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AB · paired_inverse_witness_zeroThe adjacent inverse-pair witness invariant is vacuous at zero.
layer 1 · 16 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AC · pair_order_iteration_previous_balanceRebalance one stored pair into the predecessor induction hypothesis.
layer 1 · 3 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AD · pair_order_iteration_step_roomExpose the exact one-orbit room equation in the successor case.
layer 1 · 3 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AE · finite_prefix_choose_unused_nonendpointBy temporarily appending both endpoints, finite omission constructively selects a missing nonendpoint value.
layer 22 · 86 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AF · inverse_prefix_entry_soundEvery decoded inverse-prefix entry satisfies its stored inverse relation.
layer 6 · 28 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AG · prime_bounded_square_one_casesA bounded square root of one modulo a prime is one or the prime predecessor.
layer 11 · 151 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AH · prime_inverse_prefix_fixed_casesA fixed zero-based inverse index is zero or the last index.
layer 12 · 53 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AI · prime_inverse_prefix_nonendpoint_not_fixedA decoded inverse entry from a nonendpoint source is not fixed.
layer 13 · 35 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AJ · inverse_index_symmetricThe bounded inverse-index relation is symmetric.
layer 4 · 15 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AL · bounded_inverse_index_uniqueA bounded inverse index is unique.
layer 8 · 38 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AM · inverse_prefix_extensionalA full inverse relation at a covered index is decoded by the prefix.
layer 9 · 30 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AN · inverse_prefix_involutiveDecoding an inverse mate and decoding again returns the source index.
layer 10 · 45 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AO · inverse_prefix_zero_fixedThe zero index, representing residue one, is fixed by the full inverse prefix.
layer 10 · 40 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AP · inverse_prefix_last_fixedThe last index, representing the predecessor of p, is fixed by the full inverse prefix.
layer 10 · 40 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AQ · prime_inverse_prefix_nonendpoint_mateThe decoded mate of a nonendpoint inverse index is also a nonendpoint.
layer 14 · 128 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AR · prime_choose_unused_nonendpoint_orbitChoose an omitted nonendpoint index and extract its distinct, nonendpoint inverse mate together with both decoded directions.
layer 23 · 97 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AS · orbit_closed_unused_mateOrbit closure turns omission of one endpoint of a decoded two-cycle into omission of its mate.
layer 0 · 28 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AT · beta_prefix_append_two_orbit_closedAppending both directions of a decoded two-cycle preserves orbit closure of the used prefix.
layer 7 · 109 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AU · beta_prefix_append_two_nonendpointA two-entry append preserves the nonendpoint invariant when both appended values satisfy it.
layer 7 · 48 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AV · prime_pair_order_choose_appendConstructively choose one unused inverse orbit, append its two directions adjacently, and preserve the orbit-closed nonendpoint prefix invariants.
layer 24 · 118 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AW · prime_pair_order_choose_append_injectiveThread decoded-prefix injectivity through one constructive fresh-orbit append.
layer 25 · 70 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AX · prime_pair_order_choose_append_stateThread the complete bounded PairOrder state through one fresh inverse-orbit append.
layer 26 · 73 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00AY · paired_inverse_witness_appendA two-entry append preserves every old inverse pair and adds the new one.
layer 4 · 75 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00B0 · prime_pair_order_paired_state_stepPreserve the bounded PairOrder state and every adjacent inverse-pair witness through one append.
layer 27 · 81 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00B1 · prime_pair_order_paired_iterationIterate pair appends while retaining both bounded state and adjacent inverse history.
layer 28 · 104 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00B2 · prime_pair_order_paired_terminal_state_existsSpecialize the paired iteration to a terminal n-2 prefix with full adjacency history.
layer 29 · 29 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00B3 · beta_magnitude_predecessor_recode_surjectiveThe predecessor code covers every value 0,...,l-1 by constructive finite pigeonhole.
layer 20 · 33 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00B4 · finite_bounded_nonendpoint_injective_coverageA bounded injective terminal prefix covers exactly every nonendpoint value below n = l+2.
layer 21 · 126 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00B5 · pair_order_state_terminal_coverageThe strengthened PairOrder state is complete at the exact terminal length n-2.
layer 22 · 24 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00B6 · pair_order_successor_lift_existsEvery zero-based pair order has a beta code of successor-valued factors.
layer 18 · 7 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00B7 · paired_successor_lift_adjacent_unitsSuccessor-lifted adjacent inverse indices multiply to one modulo p.
layer 6 · 106 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00B8 · paired_pair_order_factor_code_existsPackage a successor-valued factor code with adjacent unit pairs.
layer 19 · 35 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00B9 · beta_adjacent_unit_pairs_product_oneAdjacent inverse pairs multiply to one across an exact beta-coded even prefix.
layer 8 · 96 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BA · paired_pair_order_product_one_existsThe complete successor-lifted nonendpoint factor product is one modulo p.
layer 20 · 52 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BB · pair_order_terminal_state_magnitude_rangeA terminal PairOrder state decodes exactly positive values bounded by its length.
layer 2 · 54 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BC · pair_order_predecessor_range_two_successor_lift_alignedThe predecessor map aligns canonical residues 2+j with successor-lifted PairOrder entries.
layer 7 · 86 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BD · pair_order_terminal_successor_product_eq_range_twoThe lifted terminal product equals the product of the canonical nonendpoint range.
layer 21 · 67 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BE · prime_wilson_terminal_product_package_existsPackage terminal PairOrder history, coverage, lifted product, and equality with residues 2,...,p-2.
layer 30 · 144 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BF · prime_terminal_range_two_product_mod_one_existsProject the terminal PairOrder package to its canonical nonendpoint product modulo one.
layer 31 · 57 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BG · beta_range_two_product_is_factorial_succA product of 2,...,l+1 is the factorial of l+1; the missing leading factor is one.
layer 20 · 115 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BH · beta_range_two_product_restore_lastRestore the final factor l+2 after the leading unit has been absorbed.
layer 21 · 45 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BI · mod_one_product_restore_predecessorMultiplying a residue-one product by n restores the predecessor residue n.
layer 6 · 19 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BJ · prime_factorial_wilson_congruenceWilson's factorial congruence for every prime, with p=2 handled before terminal pairing.
layer 32 · 77 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BK · scaled_pair_order_terminal_power_mod_predecessorA completed terminal scaled pairing sends a^h to the predecessor p-1 modulo p.
layer 33 · 114 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BL · scaled_inverse_nonresidue_half_power_mod_predecessorA full nonresidue scaled-inverse prefix satisfies Euler's minus-one branch.
layer 34 · 46 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BM · quadratic_nonresidue_half_power_mod_predecessorFor a reduced nonzero nonresidue, a^((p-1)/2) is p-1 modulo p.
layer 35 · 37 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BN · bounded_euler_criterion_dichotomyEvery bounded nonzero input lands constructively in exactly the appropriate Euler endpoint.
layer 36 · 72 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BO · double_predecessor_ne_oneA doubled predecessor cannot equal one.
layer 6 · 21 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BP · odd_prime_one_not_mod_predecessorFor an odd-prime predecessor, the canonical residues one and p-1 are distinct.
layer 7 · 36 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BQ · bounded_euler_criterion_residue_iffFor bounded nonzero inputs, quadratic residuosity is equivalent to the half-power residue one.
layer 37 · 63 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BR · arbitrary_euler_criterion_residue_iffEuler's residue equivalence for an arbitrary nonmultiple representative.
layer 38 · 92 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BS · bounded_euler_criterion_nonresidue_iffFor bounded nonzero inputs, nonresiduosity is equivalent to the half-power residue p-1.
layer 38 · 76 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BT · arbitrary_euler_criterion_nonresidue_iffEuler's nonresidue equivalence for an arbitrary nonmultiple representative.
layer 39 · 98 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BU · arbitrary_euler_criterion_completeComplete Euler criterion for every representative coprime to the prime.
layer 40 · 33 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BV · arbitrary_gauss_lemma_completeAn arbitrary prime unit is a quadratic residue exactly when its Gauss reflection count is even, and a nonresidue exactly when it is odd.
layer 41 · 188 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BW · beta_scaled_successor_prefix_from_pointwiseA constant prefix times 1,...,h decodes exactly as a*(1+i).
layer 0 · 32 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BX · beta_division_prefix_extendAppend one quotient/remainder pair while preserving the decoded prefix.
layer 17 · 94 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00BY · beta_division_prefix_existsEvery finite beta source prefix has beta-coded quotients and bounded remainders for a nonzero modulus.
layer 18 · 62 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00C0 · prime_scaled_half_division_prefix_existsAn odd-prime half range has exact scaled quotient/remainder codes.
layer 19 · 62 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00C1 · prime_scaled_half_quotient_sum_existsThe quotient code additionally carries its native finite floor sum.
layer 20 · 43 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00C2 · odd_half_strictly_below_modulusThe half of an odd modulus p=2h+1 is strictly below p.
layer 3 · 6 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00C3 · odd_half_positive_complement_existsA positive magnitude at most the odd half has a complement below the modulus.
layer 4 · 59 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00C4 · predecessor_multiple_mod_complementThe predecessor multiplier is congruent to the complementary remainder.
layer 3 · 30 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00C5 · canonical_remainder_from_modA bounded value congruent to an exact division input is its canonical remainder.
layer 6 · 43 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00C6 · odd_signed_division_branch_exactA Gauss signed congruence determines the exact canonical lower/reflected remainder branch.
layer 7 · 90 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00C7 · odd_multiplier_even_product_iffMultiplication by an odd natural preserves and reflects evenness.
layer 7 · 29 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00C8 · odd_multiplier_odd_product_iffMultiplication by an odd natural preserves and reflects oddness.
layer 7 · 29 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00C9 · odd_multiplier_parity_iffAn odd multiplier preserves both parity classes exactly.
layer 8 · 12 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CA · even_sum_parity_casesAn even sum has summands of the same parity.
layer 7 · 52 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CB · even_sum_iff_same_parityA sum is even exactly when its summands have the same parity.
layer 8 · 22 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CC · odd_division_even_iffFor odd divisor coefficient p, n=p*q+r is even exactly when q+r is even.
layer 9 · 71 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CD · odd_sum_parity_casesAn odd sum has summands of opposite parity.
layer 7 · 52 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CE · odd_sum_iff_opposite_parityA sum is odd exactly when its summands have opposite parity.
layer 8 · 22 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CF · odd_division_odd_iffFor odd divisor coefficient p, n=p*q+r is odd exactly when q+r is odd.
layer 9 · 71 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CG · odd_division_parity_iffAn exact quotient-remainder equation with odd coefficient preserves the complete parity classification.
layer 10 · 21 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CH · even_to_mod_two_zeroEvery even natural is congruent to zero modulo two.
layer 2 · 6 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CI · odd_to_mod_two_oneEvery odd natural is congruent to one modulo two.
layer 2 · 11 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CJ · matching_parity_mod_twoNaturals with the same constructive parity are congruent modulo two.
layer 3 · 48 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CK · odd_product_division_mod_twoOdd scale and modulus transport an exact division equation to x == q+r modulo two.
layer 11 · 58 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CL · odd_reflected_remainder_mod_twoReflecting two remainders across an odd modulus flips parity.
layer 4 · 27 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CM · signed_remainder_sum_mod_twoA lower/reflected signed remainder changes q+r to q+m+s only by an even amount.
layer 5 · 44 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CN · odd_scaled_division_signed_mod_twoThe generic Gauss-Eisenstein pointwise join: x == q+m+s modulo two.
layer 12 · 37 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CO · odd_signed_division_congruence_mod_twoExact signed division data gives the Gauss--Eisenstein modulo-two relation.
layer 13 · 50 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CP · gauss_eisenstein_prefix_pointwise_mod_twoAligned Gauss and Eisenstein prefixes satisfy x == q+m+s modulo two pointwise.
layer 14 · 155 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CQ · beta_sum_pointwise_mod_three_addPointwise x==q+m+s congruence lifts to the four exact Sum endpoints.
layer 7 · 181 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CR · gauss_eisenstein_terminal_sums_mod_twoThe pointwise Gauss--Eisenstein congruence aggregates to exact terminal Sums.
layer 15 · 72 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CS · beta_magnitude_predecessor_recode_aligned_half_rangeThe magnitude-predecessor code aligns positive magnitudes with the canonical half range.
layer 7 · 77 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CT · beta_sum_transport_prefixPointwise-equal decoded prefixes preserve an exact relational Sum.
layer 0 · 44 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CU · beta_sum_replace_balanceReplacing one summand balances the old and new finite sums by the exchanged values.
layer 7 · 202 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CV · beta_sum_swap_last_invariantSwapping an interior beta-coded summand with the last summand preserves the exact finite sum.
layer 8 · 102 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CW · beta_sum_reindex_fixed_lastA fixed-final reindex reduces successor sum equality to equality of the two prefix sums.
layer 7 · 65 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CX · beta_sum_permutation_invariantA bounded injective beta-coded reindexing preserves the exact finite sum.
layer 20 · 379 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00CY · beta_magnitude_sum_permutation_exactA positive magnitude permutation has exactly the canonical half-range Sum.
layer 21 · 61 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00D0 · gauss_signed_half_magnitude_sum_equals_half_sumGauss signed-half data makes the magnitude Sum equal the canonical half Sum.
layer 22 · 77 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00D1 · mod_eq_add_cancel_leftBalanced congruence cancels a common additive left term constructively.
layer 3 · 19 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00D2 · mod_two_cancel_middleFrom x == q+x+s modulo two, cancel x and obtain 0 == q+s.
layer 4 · 16 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00D3 · gauss_eisenstein_terminal_cancel_magnitude_mod_twoCancel the exact Gauss magnitude Sum: 0 == quotient Sum + sign Sum modulo two.
layer 23 · 88 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00D4 · mod_two_zero_to_evenCongruence to zero modulo two supplies an even witness.
layer 8 · 9 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00D5 · mod_two_zero_sum_to_congruentIf q+e is zero modulo two, q and e have the same parity and are congruent.
layer 9 · 22 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00D6 · gauss_eisenstein_sign_count_mod_quotient_sumThe Gauss sign BitCount is congruent modulo two to its orientation's quotient Sum.
layer 24 · 77 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00D7 · odd_prime_gauss_eisenstein_orientation_data_existsOne odd prime orientation has complete Gauss classification and a congruent exact Eisenstein quotient sum.
layer 42 · 102 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00D8 · distinct_odd_prime_half_products_neDistinct odd primes have no bounded positive point on q*x=p*y.
layer 11 · 64 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00D9 · distinct_odd_prime_half_cell_orientedEvery bounded half-rectangle cell has one exclusive orientation.
layer 12 · 65 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DA · distinct_odd_prime_half_cell_indicator_choiceEvery bounded lattice cell has a constructive exact indicator bit.
layer 13 · 39 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DB · distinct_odd_prime_half_row_indicator_choicesA fixed bounded row has a constructive exact bit choice in every column.
layer 14 · 27 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DC · eisenstein_row_indicator_prefix_extendAppend one exact orientation bit while preserving the previous row prefix.
layer 17 · 50 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DD · eisenstein_row_indicator_prefix_existsEvery finite family of exact cell choices has a beta-coded row prefix.
layer 18 · 50 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DE · eisenstein_row_indicator_prefix_all_bitsThe beta-coded indicator projection contains only zero and one.
layer 0 · 27 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DF · distinct_odd_prime_half_row_count_existsEvery fixed half-rectangle row has an exact beta-coded indicator and BitCount witness.
layer 20 · 55 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DG · distinct_odd_prime_half_row_count_choiceEach bounded row has one semantic row-count witness.
layer 21 · 31 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DH · distinct_odd_prime_half_row_count_choices_boundedEvery prefix length at most h has semantic row-count choices.
layer 22 · 32 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DI · eisenstein_rectangle_row_count_prefix_extendAppend one semantic row count while preserving all earlier rows.
layer 17 · 50 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DJ · eisenstein_rectangle_row_count_prefix_existsEvery finite family of semantic row counts has an outer beta prefix.
layer 18 · 50 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DK · distinct_odd_prime_half_row_count_prefix_exists_boundedEvery bounded initial set of rows has a semantic count prefix.
layer 23 · 30 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DL · distinct_odd_prime_half_row_count_prefix_existsAll h rows have one outer beta prefix of semantic counts.
layer 24 · 24 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DM · distinct_odd_prime_half_rectangle_total_existsThe nested row counts have a native beta-sum rectangle total.
layer 25 · 34 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DN · prime_nondivisor_bounded_scaled_remainder_nonzeroA bounded positive factor times a prime nondivisor cannot have zero remainder modulo that prime.
layer 11 · 40 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DO · distinct_primes_bounded_scaled_remainder_nonzeroDistinct primes give the nondivisibility needed by the bounded scaled-remainder theorem.
layer 12 · 37 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DP · distinct_primes_own_odd_half_scaled_remainder_nonzeroAn index below the divisor's own odd half has nonzero scaled remainder for a distinct prime multiplier.
layer 13 · 37 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DQ · odd_half_cross_product_gapThe odd half-products differ by the explicit positive gap h+k+1.
layer 5 · 13 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DR · odd_half_division_quotient_boundedA division row from the first odd half has quotient at most the second half.
layer 6 · 62 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DS · nonzero_remainder_division_positive_multiple_thresholdA positive multiple lies below a nonintegral division value exactly through the quotient threshold.
layer 3 · 67 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DT · eisenstein_row_indicator_prefix_to_initial_segmentA semantic row prefix is the exact initial segment cut out by its nonzero division quotient.
layer 4 · 55 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DU · eisenstein_initial_segment_prefix_all_bitsEvery exact threshold prefix is an AllBits prefix.
layer 0 · 23 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DV · eisenstein_initial_segment_decoded_choiceEvery decoded bit recovers its exact threshold semantics.
layer 6 · 27 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DW · beta_all_one_bit_count_exactA length-k beta prefix consisting only of ones has BitCount k.
layer 8 · 62 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DX · eisenstein_initial_segment_bit_count_functionalThe BitCount of a bounded exact initial segment is its threshold.
layer 9 · 129 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00DY · eisenstein_initial_segment_bit_count_exactA bounded exact initial-segment prefix has native BitCount q.
layer 20 · 33 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00E0 · distinct_odd_prime_row_bit_count_equals_division_quotientA semantic row BitCount is the quotient in its bounded nonzero division.
layer 21 · 79 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00E1 · distinct_odd_prime_row_bit_count_equals_decoded_quotientThe semantic row count equals the quotient decoded by the scaled division prefix at that row.
layer 22 · 96 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00E2 · distinct_odd_prime_semantic_row_equals_decoded_quotientThe outer rectangle's semantic row witness is extensionally its decoded division quotient.
layer 23 · 53 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00E3 · distinct_odd_prime_quotient_entry_matches_rectangleEvery decoded quotient entry is the corresponding semantic rectangle entry.
layer 24 · 58 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00E4 · distinct_odd_prime_quotient_sum_transports_to_rectangleThe quotient Sum trace transports exactly to the semantic rectangle prefix.
layer 25 · 61 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00E5 · distinct_odd_prime_quotient_sum_equals_rectangle_totalThe quotient floor-sum endpoint equals the independently summed semantic rectangle total.
layer 26 · 56 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00E6 · eisenstein_rectangle_decoded_row_countEvery decoded outer entry is semantically a BitCount of its row.
layer 6 · 29 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00E7 · eisenstein_transposed_outer_column_choicesA fixed bounded index has one provenance-carrying bit in every swapped row.
layer 7 · 37 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00E8 · eisenstein_transposed_column_prefix_extendAppend one provenance-carrying swapped-row bit to a transposed column.
layer 17 · 55 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00E9 · eisenstein_transposed_column_prefix_existsEvery finite family of swapped-row cell choices has one beta-coded column.
layer 18 · 56 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EA · eisenstein_row_indicator_decoded_choiceEvery decoded row bit recovers its exact strict-orientation meaning.
layer 6 · 29 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EB · eisenstein_transposed_column_prefix_all_bitsEvery provenance-carrying transposed column is a zero/one prefix.
layer 7 · 48 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EC · eisenstein_transposed_decoded_cell_bits_complementaryA decoded cell bit and its swapped-row transpose are exact complements.
layer 7 · 71 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00ED · eisenstein_transposed_column_pointwise_complementEvery decoded original-row bit and constructed column bit are exact complements.
layer 8 · 64 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EE · complementary_bit_counts_add_lengthComplementary decoded bit prefixes have counts summing to their length.
layer 8 · 112 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EF · eisenstein_row_transposed_column_count_partitionOne semantic row and the constructed whole transposed column partition all k cells.
layer 20 · 105 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EG · eisenstein_transposed_column_count_choicesEvery original row index has a fully witnessed complementary column count.
layer 21 · 57 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EH · eisenstein_transposed_column_count_prefix_extendAppend one fully witnessed column count to the outer count prefix.
layer 17 · 59 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EI · eisenstein_transposed_column_count_prefix_existsEvery bounded family of column-count witnesses has one outer beta prefix.
layer 18 · 60 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EJ · eisenstein_transposed_column_count_total_existsThe provenance-carrying column counts have an exact relational outer Sum.
layer 22 · 48 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EK · beta_repeat_sum_exactA constant beta prefix has exact relational sum length times value.
layer 7 · 64 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EL · beta_repeat_sum_exists_exactEvery value and length admit a constant prefix with its exact sum.
layer 19 · 31 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EM · eisenstein_transposed_column_count_decoded_witnessEvery decoded column-count outer entry recovers its full partition witness.
layer 6 · 34 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EN · eisenstein_transposed_column_count_decoded_partitionDecoded original-row and constructed-column counts partition the row width.
layer 7 · 52 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EO · eisenstein_transposed_column_count_matches_decoded_constantThe decoded row and column counts add to the decoded entry of any constant-k prefix.
layer 8 · 56 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EP · beta_sum_pointwise_addPointwise sums of decoded entries induce exact addition of finite sums.
layer 7 · 127 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EQ · eisenstein_rectangle_plus_column_count_totalThe original row total plus the constructed column-count total is exactly h*k.
layer 23 · 100 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00ER · eisenstein_transposed_column_count_prefix_forgetForget complement-partition provenance while retaining every genuine transposed-column count.
layer 0 · 33 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00ES · eisenstein_zero_width_rectangle_sum_zeroEvery semantic zero-width rectangle has relational outer Sum zero.
layer 19 · 82 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00ET · eisenstein_row_indicator_prefix_succ_restrictA successor indicator row restricts to the same code's predecessor prefix.
layer 2 · 18 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EU · eisenstein_successor_row_count_decomposeA semantic successor row count is its restricted count plus its final decoded bit.
layer 8 · 53 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EV · eisenstein_successor_row_split_choicesEvery stored successor row constructively chooses an aligned reduced count and terminal bit.
layer 9 · 35 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EW · eisenstein_successor_row_split_prefix_extendAppend aligned reduced-count and terminal-bit entries while preserving complete row provenance.
layer 17 · 99 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EX · eisenstein_successor_row_split_prefix_existsAny bounded family of successor-row splits has aligned β-coded reduced and terminal prefixes.
layer 18 · 62 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00EY · eisenstein_successor_rectangle_row_split_prefix_existsA semantic successor-width rectangle yields aligned reduced-count and terminal-bit β-prefixes.
layer 19 · 29 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00F0 · eisenstein_successor_row_split_reduced_rectangle_prefixThe reduced-count code in a split prefix is itself a semantic predecessor-width rectangle prefix.
layer 0 · 39 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00F1 · eisenstein_successor_row_split_decoded_addEvery aligned decoded successor count is exactly its decoded reduced count plus terminal bit.
layer 6 · 67 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00F2 · eisenstein_successor_row_split_sum_addThe successor outer Sum is exactly the reduced-row Sum plus the terminal-bit Sum.
layer 8 · 63 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00F3 · eisenstein_fubini_column_count_prefix_succ_restrictA semantic column-count prefix restricts from successor length to predecessor length.
layer 2 · 20 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00F4 · eisenstein_transposed_column_decoded_choiceA decoded entry of any genuine transposed column has the exact Eisenstein cell orientation.
layer 7 · 52 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00F5 · eisenstein_cell_indicator_choice_uniqueThe exact orientation predicate determines its zero-or-one indicator uniquely.
layer 0 · 35 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00F6 · eisenstein_transposed_column_counts_extensionalCounts of extensionally identical semantic transposed columns are equal across arbitrary provenance codes.
layer 8 · 100 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00F7 · eisenstein_fubini_column_count_witness_retargetRebuild a counted column over another semantic outer code without changing its count.
layer 20 · 92 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00F8 · eisenstein_fubini_column_count_prefix_retarget_predecessorRetarget every predecessor column count from the successor outer code to the reduced semantic rows.
layer 21 · 49 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00F9 · eisenstein_successor_terminal_bit_matches_last_columnThe terminal-bit prefix and the constructed last column decode the same bit at every bounded row.
layer 7 · 111 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FA · eisenstein_successor_terminal_prefix_to_last_columnEvery terminal-prefix decode transports extensionally to the constructed last-column code.
layer 8 · 53 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FB · eisenstein_successor_terminal_sum_matches_last_columnThe terminal-bit Sum is exactly the relational count Sum of the constructed last column.
layer 9 · 64 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FC · eisenstein_fubini_universalAny genuine transposed-column count total equals the swapped semantic row total.
layer 22 · 216 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FD · eisenstein_constructed_column_total_equals_swapped_totalThe constructed complementary-column total is exactly the swapped semantic row total.
layer 23 · 44 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FE · eisenstein_rectangle_floor_sum_identityThe two semantic Eisenstein row totals add exactly to the rectangle area.
layer 24 · 53 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FF · distinct_odd_prime_eisenstein_quotient_sum_identityFor distinct odd primes, the two decoded finite quotient sums add exactly to h*k.
layer 27 · 123 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FG · distinct_odd_primes_gauss_eisenstein_data_existsDistinct odd primes admit both Gauss classification counts, their mod-two quotient sums, and the exact Eisenstein sum identity.
layer 43 · 150 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FH · gauss_count_sum_mod_two_from_quotient_sumsTwo oriented count/quotient congruences plus the exact floor-sum identity give e+f == h*k modulo two.
layer 4 · 20 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FI · odd_half_of_mod4_one_exactThe half of a fixed odd number congruent to one modulo four is exactly even.
layer 5 · 17 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FJ · odd_half_even_iff_mod4_oneFor a fixed odd decomposition, a modulo-four-one modulus is equivalent to an even half.
layer 6 · 22 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FK · mod_two_one_to_oddCongruence to one modulo two supplies an odd witness.
layer 7 · 20 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FL · mod_two_preserves_parityBalanced congruence modulo two preserves both parity predicates.
layer 9 · 76 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FM · qres_same_status_from_even_count_sumAn even sum of Gauss counts gives equal cross-residue status.
layer 8 · 37 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FN · qres_same_status_from_even_half_product_mod_twoModulo-two equality with an even half product gives equal residue status.
layer 10 · 28 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FO · qres_same_status_from_mod_four_oneA one-mod-four input forces equal cross-residue status.
layer 11 · 51 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FP · conditional_qres_same_status_from_oriented_gauss_countsConditional one-mod-four reciprocity: the two cross-residue propositions have the same truth status.
layer 12 · 40 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FQ · odd_half_of_mod4_three_exactThe half of a fixed odd number congruent to three modulo four is exactly odd.
layer 5 · 19 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FR · odd_half_odd_iff_mod4_threeFor a fixed odd decomposition, a modulo-four-three modulus is equivalent to an odd half.
layer 6 · 24 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FS · qres_opposite_status_from_odd_count_sumAn odd sum of Gauss counts gives opposite cross-residue status.
layer 8 · 37 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FT · qres_opposite_status_from_odd_half_product_mod_twoModulo-two equality with an odd half product gives opposite residue status.
layer 10 · 28 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FU · qres_opposite_status_from_mod_four_threeTwo three-mod-four inputs force opposite cross-residue status.
layer 11 · 48 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FV · conditional_qres_opposite_status_from_oriented_gauss_countsConditional three-mod-four reciprocity: exactly one cross-residue proposition holds.
layer 12 · 40 lines · Alpha v34 checked-use theorem · independently closed; not StablePA00FW · quadratic_reciprocity_combinedThe exact sign-free two-case quadratic-reciprocity endpoint.
layer 44 · 65 lines · Alpha v34 checked-use theorem · independently closed; not Stable