Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Statement with defined notation
∀ p. ∀ q. ∀ h. ∀ k. p = 2 · h + 1 → q = 2 · k + 1 → Prime(p) → Prime(q) → ¬p = q → ∃ x. ∃ y. ∀ z. Lt(z,h) → ∃ n. BetaAt(x,y,z,n) ∧ (∃ m. ∃ i. (∀ j. Lt(j,k) → ∃ u. BetaAt(m,i,j,u) ∧ (u = 0 ∧ (Lt(q · S z,p · S j) ∧ ¬Lt(p · S j,q · S z)) ∨ u = 1 ∧ (Lt(p · S j,q · S z) ∧ ¬Lt(q · S z,p · S j)))) ∧ BitCount(m,i,k,n))Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.
Definitions used by this theorem
In the theorem statement
11 occurrences
In local proof propositions
1 occurrences
Exact expanded native-PA statement
forall p q h k. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_rectangle_count_prime_p frp_prime_right_rectangle_count_prime_p. p = frp_prime_left_rectangle_count_prime_p * frp_prime_right_rectangle_count_prime_p -> frp_prime_left_rectangle_count_prime_p = 1 \/ frp_prime_right_rectangle_count_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_rectangle_count_prime_q frp_prime_right_rectangle_count_prime_q. q = frp_prime_left_rectangle_count_prime_q * frp_prime_right_rectangle_count_prime_q -> frp_prime_left_rectangle_count_prime_q = 1 \/ frp_prime_right_rectangle_count_prime_q = 1)) -> ~(p = q) -> (exists cb cc. (forall erc_row_rectangle_count_full_prefix. (exists erc_lt_gap_rectangle_count_full_prefix_bound. erc_lt_gap_rectangle_count_full_prefix_bound + S (erc_row_rectangle_count_full_prefix) = h) -> exists erc_count_rectangle_count_full_prefix. ((((exists ff_h_erc_rectangle_count_full_prefix_decoded. ff_h_erc_rectangle_count_full_prefix_decoded + S (erc_count_rectangle_count_full_prefix) = S ((S (erc_row_rectangle_count_full_prefix)) * cc)) /\ exists ff_q_erc_rectangle_count_full_prefix_decoded. cb = ff_q_erc_rectangle_count_full_prefix_decoded * S ((S (erc_row_rectangle_count_full_prefix)) * cc) + (erc_count_rectangle_count_full_prefix))) /\ (exists erc_row_code_rectangle_count_full_prefix_witness erc_row_scale_rectangle_count_full_prefix_witness. ((forall eri_column_erc_rectangle_count_full_prefix_witness_row. (exists eri_gap_erc_rectangle_count_full_prefix_witness_row_bound. eri_gap_erc_rectangle_count_full_prefix_witness_row_bound + S (eri_column_erc_rectangle_count_full_prefix_witness_row) = k) -> exists eri_bit_erc_rectangle_count_full_prefix_witness_row. ((((exists ff_h_eri_erc_rectangle_count_full_prefix_witness_row_decoded. ff_h_eri_erc_rectangle_count_full_prefix_witness_row_decoded + S (eri_bit_erc_rectangle_count_full_prefix_witness_row) = S ((S (eri_column_erc_rectangle_count_full_prefix_witness_row)) * erc_row_scale_rectangle_count_full_prefix_witness)) /\ exists ff_q_eri_erc_rectangle_count_full_prefix_witness_row_decoded. erc_row_code_rectangle_count_full_prefix_witness = ff_q_eri_erc_rectangle_count_full_prefix_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_full_prefix_witness_row)) * erc_row_scale_rectangle_count_full_prefix_witness) + (eri_bit_erc_rectangle_count_full_prefix_witness_row))) /\ (((eri_bit_erc_rectangle_count_full_prefix_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_full_prefix) = p * S eri_column_erc_rectangle_count_full_prefix_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_full_prefix_witness_row) = q * S erc_row_rectangle_count_full_prefix))) \/ (eri_bit_erc_rectangle_count_full_prefix_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_full_prefix_witness_row) = q * S erc_row_rectangle_count_full_prefix) /\ ~(exists eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_full_prefix) = p * S eri_column_erc_rectangle_count_full_prefix_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_full_prefix_witness_count_sum ff_v_erc_rectangle_count_full_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_start. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_start. ff_u_erc_rectangle_count_full_prefix_witness_count_sum = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_terminal. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_terminal + S (erc_count_rectangle_count_full_prefix) = S ((S (k)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_terminal. ff_u_erc_rectangle_count_full_prefix_witness_count_sum = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum) + (erc_count_rectangle_count_full_prefix))) /\ forall ff_i_erc_rectangle_count_full_prefix_witness_count_sum. (exists ff_lt_erc_rectangle_count_full_prefix_witness_count_sum_bound. ff_lt_erc_rectangle_count_full_prefix_witness_count_sum_bound + S ff_i_erc_rectangle_count_full_prefix_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_full_prefix_witness_count_sum ff_r_erc_rectangle_count_full_prefix_witness_count_sum ff_s_erc_rectangle_count_full_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_summand. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_summand + S (ff_a_erc_rectangle_count_full_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_full_prefix_witness)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_summand. erc_row_code_rectangle_count_full_prefix_witness = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_full_prefix_witness) + (ff_a_erc_rectangle_count_full_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_partial. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_partial + S (ff_r_erc_rectangle_count_full_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_partial. ff_u_erc_rectangle_count_full_prefix_witness_count_sum = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum) + (ff_r_erc_rectangle_count_full_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_successor. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_successor + S (ff_s_erc_rectangle_count_full_prefix_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_successor. ff_u_erc_rectangle_count_full_prefix_witness_count_sum = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum) + (ff_s_erc_rectangle_count_full_prefix_witness_count_sum))) /\ ff_s_erc_rectangle_count_full_prefix_witness_count_sum = ff_r_erc_rectangle_count_full_prefix_witness_count_sum + ff_a_erc_rectangle_count_full_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_full_prefix_witness_count_bits. (exists ff_lt_erc_rectangle_count_full_prefix_witness_count_bits_bound. ff_lt_erc_rectangle_count_full_prefix_witness_count_bits_bound + S ff_i_erc_rectangle_count_full_prefix_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_full_prefix_witness_count_bits. ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_bits_decoded. ff_h_erc_rectangle_count_full_prefix_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_full_prefix_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_full_prefix_witness)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_bits_decoded. erc_row_code_rectangle_count_full_prefix_witness = ff_q_erc_rectangle_count_full_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_full_prefix_witness) + (ff_bit_erc_rectangle_count_full_prefix_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_full_prefix_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_full_prefix_witness_count_bits = 1))))))))))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (2)
01Fix variables and assumptionsL1–9
02Establish hleL10–19
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct odd prime half row count prefix exists bounded.
- L10
- L11
specialize le_refl h - L12
exact le_refl - L13
specialize distinct_odd_prime_half_row_count_prefix_exists_bounded p - L14
specialize distinct_odd_prime_half_row_count_prefix_exists_bounded q - L15
specialize distinct_odd_prime_half_row_count_prefix_exists_bounded h - L16
specialize distinct_odd_prime_half_row_count_prefix_exists_bounded k - L17
specialize distinct_odd_prime_half_row_count_prefix_exists_bounded h - L18
apply distinct_odd_prime_half_row_count_prefix_exists_bounded - L19
exact hpodd
Original defined command ledger · 24 lines
- 0001
intro p - 0002
intro q - 0003
intro h - 0004
intro k - 0005
intro hpodd - 0006
intro hqodd - 0007
intro hp - 0008
intro hq - 0009
intro hpq - 0010
have hle : Le(h,h)Exact native replay line
have hle : exists erc_le_gap_rectangle_count_full_reflexive. erc_le_gap_rectangle_count_full_reflexive + (h) = h - 0011
specialize le_refl h - 0012
exact le_refl - 0013
specialize distinct_odd_prime_half_row_count_prefix_exists_bounded p - 0014
specialize distinct_odd_prime_half_row_count_prefix_exists_bounded q - 0015
specialize distinct_odd_prime_half_row_count_prefix_exists_bounded h - 0016
specialize distinct_odd_prime_half_row_count_prefix_exists_bounded k - 0017
specialize distinct_odd_prime_half_row_count_prefix_exists_bounded h - 0018
apply distinct_odd_prime_half_row_count_prefix_exists_bounded - 0019
exact hpodd - 0020
exact hqodd - 0021
exact hp - 0022
exact hq - 0023
exact hpq - 0024
exact hle