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. ∀ i. p = 2 · h + 1 → q = 2 · k + 1 → Prime(p) → Prime(q) → ¬p = q → Lt(i,h) → ∃ x. ∃ y. ∃ z. (∀ n. Lt(n,k) → ∃ m. BetaAt(y,z,n,m) ∧ (m = 0 ∧ (Lt(q · S i,p · S n) ∧ ¬Lt(p · S n,q · S i)) ∨ m = 1 ∧ (Lt(p · S n,q · S i) ∧ ¬Lt(q · S i,p · S n)))) ∧ BitCount(y,z,k,x)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
10 occurrences
In local proof propositions
7 occurrences
Exact expanded native-PA statement
forall p q h k i. 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 erc_lt_gap_rectangle_count_row_bound. erc_lt_gap_rectangle_count_row_bound + S (i) = h) -> exists n. (exists erc_row_code_rectangle_count_point_witness erc_row_scale_rectangle_count_point_witness. ((forall eri_column_erc_rectangle_count_point_witness_row. (exists eri_gap_erc_rectangle_count_point_witness_row_bound. eri_gap_erc_rectangle_count_point_witness_row_bound + S (eri_column_erc_rectangle_count_point_witness_row) = k) -> exists eri_bit_erc_rectangle_count_point_witness_row. ((((exists ff_h_eri_erc_rectangle_count_point_witness_row_decoded. ff_h_eri_erc_rectangle_count_point_witness_row_decoded + S (eri_bit_erc_rectangle_count_point_witness_row) = S ((S (eri_column_erc_rectangle_count_point_witness_row)) * erc_row_scale_rectangle_count_point_witness)) /\ exists ff_q_eri_erc_rectangle_count_point_witness_row_decoded. erc_row_code_rectangle_count_point_witness = ff_q_eri_erc_rectangle_count_point_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_point_witness_row)) * erc_row_scale_rectangle_count_point_witness) + (eri_bit_erc_rectangle_count_point_witness_row))) /\ (((eri_bit_erc_rectangle_count_point_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_point_witness_row_choice_left. eri_gap_erc_rectangle_count_point_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_rectangle_count_point_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_point_witness_row_choice_right. eri_gap_erc_rectangle_count_point_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_point_witness_row) = q * S i))) \/ (eri_bit_erc_rectangle_count_point_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_point_witness_row_choice_right. eri_gap_erc_rectangle_count_point_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_point_witness_row) = q * S i) /\ ~(exists eri_gap_erc_rectangle_count_point_witness_row_choice_left. eri_gap_erc_rectangle_count_point_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_rectangle_count_point_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_point_witness_count_sum ff_v_erc_rectangle_count_point_witness_count_sum. ((((exists ff_h_erc_rectangle_count_point_witness_count_sum_start. ff_h_erc_rectangle_count_point_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_point_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_point_witness_count_sum_start. ff_u_erc_rectangle_count_point_witness_count_sum = ff_q_erc_rectangle_count_point_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_point_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_point_witness_count_sum_terminal. ff_h_erc_rectangle_count_point_witness_count_sum_terminal + S (n) = S ((S (k)) * ff_v_erc_rectangle_count_point_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_point_witness_count_sum_terminal. ff_u_erc_rectangle_count_point_witness_count_sum = ff_q_erc_rectangle_count_point_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_point_witness_count_sum) + (n))) /\ forall ff_i_erc_rectangle_count_point_witness_count_sum. (exists ff_lt_erc_rectangle_count_point_witness_count_sum_bound. ff_lt_erc_rectangle_count_point_witness_count_sum_bound + S ff_i_erc_rectangle_count_point_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_point_witness_count_sum ff_r_erc_rectangle_count_point_witness_count_sum ff_s_erc_rectangle_count_point_witness_count_sum. ((((exists ff_h_erc_rectangle_count_point_witness_count_sum_summand. ff_h_erc_rectangle_count_point_witness_count_sum_summand + S (ff_a_erc_rectangle_count_point_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_point_witness_count_sum)) * erc_row_scale_rectangle_count_point_witness)) /\ exists ff_q_erc_rectangle_count_point_witness_count_sum_summand. erc_row_code_rectangle_count_point_witness = ff_q_erc_rectangle_count_point_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_point_witness_count_sum)) * erc_row_scale_rectangle_count_point_witness) + (ff_a_erc_rectangle_count_point_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_point_witness_count_sum_partial. ff_h_erc_rectangle_count_point_witness_count_sum_partial + S (ff_r_erc_rectangle_count_point_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_point_witness_count_sum)) * ff_v_erc_rectangle_count_point_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_point_witness_count_sum_partial. ff_u_erc_rectangle_count_point_witness_count_sum = ff_q_erc_rectangle_count_point_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_point_witness_count_sum)) * ff_v_erc_rectangle_count_point_witness_count_sum) + (ff_r_erc_rectangle_count_point_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_point_witness_count_sum_successor. ff_h_erc_rectangle_count_point_witness_count_sum_successor + S (ff_s_erc_rectangle_count_point_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_point_witness_count_sum)) * ff_v_erc_rectangle_count_point_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_point_witness_count_sum_successor. ff_u_erc_rectangle_count_point_witness_count_sum = ff_q_erc_rectangle_count_point_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_point_witness_count_sum)) * ff_v_erc_rectangle_count_point_witness_count_sum) + (ff_s_erc_rectangle_count_point_witness_count_sum))) /\ ff_s_erc_rectangle_count_point_witness_count_sum = ff_r_erc_rectangle_count_point_witness_count_sum + ff_a_erc_rectangle_count_point_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_point_witness_count_bits. (exists ff_lt_erc_rectangle_count_point_witness_count_bits_bound. ff_lt_erc_rectangle_count_point_witness_count_bits_bound + S ff_i_erc_rectangle_count_point_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_point_witness_count_bits. ((((exists ff_h_erc_rectangle_count_point_witness_count_bits_decoded. ff_h_erc_rectangle_count_point_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_point_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_point_witness_count_bits)) * erc_row_scale_rectangle_count_point_witness)) /\ exists ff_q_erc_rectangle_count_point_witness_count_bits_decoded. erc_row_code_rectangle_count_point_witness = ff_q_erc_rectangle_count_point_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_point_witness_count_bits)) * erc_row_scale_rectangle_count_point_witness) + (ff_bit_erc_rectangle_count_point_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_point_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_point_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 (1)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–11
Work with arbitrary variables or the premises of the current implication.
- L11
intro hi
03Establish hpackageL12–21
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct odd prime half row count exists.
- L12
have hpackage : ∃ rb. ∃ rc. ∃ n. (∀ x. Lt(x,k) → ∃ y. BetaAt(rb,rc,x,y) ∧ (y = 0 ∧ (Lt(q · S i,p · S x) ∧ ¬Lt(p · S x,q · S i)) ∨ y = 1 ∧ (Lt(p · S x,q · S i) ∧ ¬Lt(q · S i,p · S x)))) ∧ BitCount(rb,rc,k,n)Definitions: Lt(x,k)BetaAt(rb,rc,x,y)Lt(q · S i,p · S x)Lt(p · S x,q · S i)BitCount(rb,rc,k,n)Original native command in the exact edition - L13
specialize distinct_odd_prime_half_row_count_exists p - L14
specialize distinct_odd_prime_half_row_count_exists q - L15
specialize distinct_odd_prime_half_row_count_exists h - L16
specialize distinct_odd_prime_half_row_count_exists k - L17
specialize distinct_odd_prime_half_row_count_exists i - L18
apply distinct_odd_prime_half_row_count_exists - L19
exact hpodd - L20
exact hqodd - L21
exact hp
04Use earlier factsL22–24
05Separate the logical casesL25–27
06Construct an explicit witnessL28–30
07Use earlier factsL31–31
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L31
exact hpackage_witness_witness_witness
Original defined command ledger · 31 lines
- 0001
intro p - 0002
intro q - 0003
intro h - 0004
intro k - 0005
intro i - 0006
intro hpodd - 0007
intro hqodd - 0008
intro hp - 0009
intro hq - 0010
intro hpq - 0011
intro hi - 0012
have hpackage : ∃ rb. ∃ rc. ∃ n. (∀ x. Lt(x,k) → ∃ y. BetaAt(rb,rc,x,y) ∧ (y = 0 ∧ (Lt(q · S i,p · S x) ∧ ¬Lt(p · S x,q · S i)) ∨ y = 1 ∧ (Lt(p · S x,q · S i) ∧ ¬Lt(q · S i,p · S x)))) ∧ BitCount(rb,rc,k,n)Exact native replay line
have hpackage : exists rb rc n. ((forall eri_column_rectangle_count_point_row. (exists eri_gap_rectangle_count_point_row_bound. eri_gap_rectangle_count_point_row_bound + S (eri_column_rectangle_count_point_row) = k) -> exists eri_bit_rectangle_count_point_row. ((((exists ff_h_eri_rectangle_count_point_row_decoded. ff_h_eri_rectangle_count_point_row_decoded + S (eri_bit_rectangle_count_point_row) = S ((S (eri_column_rectangle_count_point_row)) * rc)) /\ exists ff_q_eri_rectangle_count_point_row_decoded. rb = ff_q_eri_rectangle_count_point_row_decoded * S ((S (eri_column_rectangle_count_point_row)) * rc) + (eri_bit_rectangle_count_point_row))) /\ (((eri_bit_rectangle_count_point_row = 0 /\ ((exists eri_gap_rectangle_count_point_row_choice_left. eri_gap_rectangle_count_point_row_choice_left + S (q * S i) = p * S eri_column_rectangle_count_point_row) /\ ~(exists eri_gap_rectangle_count_point_row_choice_right. eri_gap_rectangle_count_point_row_choice_right + S (p * S eri_column_rectangle_count_point_row) = q * S i))) \/ (eri_bit_rectangle_count_point_row = 1 /\ ((exists eri_gap_rectangle_count_point_row_choice_right. eri_gap_rectangle_count_point_row_choice_right + S (p * S eri_column_rectangle_count_point_row) = q * S i) /\ ~(exists eri_gap_rectangle_count_point_row_choice_left. eri_gap_rectangle_count_point_row_choice_left + S (q * S i) = p * S eri_column_rectangle_count_point_row))))))) /\ (((exists ff_u_rectangle_count_point_count_sum ff_v_rectangle_count_point_count_sum. ((((exists ff_h_rectangle_count_point_count_sum_start. ff_h_rectangle_count_point_count_sum_start + S (0) = S ((S (0)) * ff_v_rectangle_count_point_count_sum)) /\ exists ff_q_rectangle_count_point_count_sum_start. ff_u_rectangle_count_point_count_sum = ff_q_rectangle_count_point_count_sum_start * S ((S (0)) * ff_v_rectangle_count_point_count_sum) + (0))) /\ ((((exists ff_h_rectangle_count_point_count_sum_terminal. ff_h_rectangle_count_point_count_sum_terminal + S (n) = S ((S (k)) * ff_v_rectangle_count_point_count_sum)) /\ exists ff_q_rectangle_count_point_count_sum_terminal. ff_u_rectangle_count_point_count_sum = ff_q_rectangle_count_point_count_sum_terminal * S ((S (k)) * ff_v_rectangle_count_point_count_sum) + (n))) /\ forall ff_i_rectangle_count_point_count_sum. (exists ff_lt_rectangle_count_point_count_sum_bound. ff_lt_rectangle_count_point_count_sum_bound + S ff_i_rectangle_count_point_count_sum = k) -> exists ff_a_rectangle_count_point_count_sum ff_r_rectangle_count_point_count_sum ff_s_rectangle_count_point_count_sum. ((((exists ff_h_rectangle_count_point_count_sum_summand. ff_h_rectangle_count_point_count_sum_summand + S (ff_a_rectangle_count_point_count_sum) = S ((S (ff_i_rectangle_count_point_count_sum)) * rc)) /\ exists ff_q_rectangle_count_point_count_sum_summand. rb = ff_q_rectangle_count_point_count_sum_summand * S ((S (ff_i_rectangle_count_point_count_sum)) * rc) + (ff_a_rectangle_count_point_count_sum))) /\ ((((exists ff_h_rectangle_count_point_count_sum_partial. ff_h_rectangle_count_point_count_sum_partial + S (ff_r_rectangle_count_point_count_sum) = S ((S (ff_i_rectangle_count_point_count_sum)) * ff_v_rectangle_count_point_count_sum)) /\ exists ff_q_rectangle_count_point_count_sum_partial. ff_u_rectangle_count_point_count_sum = ff_q_rectangle_count_point_count_sum_partial * S ((S (ff_i_rectangle_count_point_count_sum)) * ff_v_rectangle_count_point_count_sum) + (ff_r_rectangle_count_point_count_sum))) /\ ((((exists ff_h_rectangle_count_point_count_sum_successor. ff_h_rectangle_count_point_count_sum_successor + S (ff_s_rectangle_count_point_count_sum) = S ((S (S ff_i_rectangle_count_point_count_sum)) * ff_v_rectangle_count_point_count_sum)) /\ exists ff_q_rectangle_count_point_count_sum_successor. ff_u_rectangle_count_point_count_sum = ff_q_rectangle_count_point_count_sum_successor * S ((S (S ff_i_rectangle_count_point_count_sum)) * ff_v_rectangle_count_point_count_sum) + (ff_s_rectangle_count_point_count_sum))) /\ ff_s_rectangle_count_point_count_sum = ff_r_rectangle_count_point_count_sum + ff_a_rectangle_count_point_count_sum)))))) /\ (forall ff_i_rectangle_count_point_count_bits. (exists ff_lt_rectangle_count_point_count_bits_bound. ff_lt_rectangle_count_point_count_bits_bound + S ff_i_rectangle_count_point_count_bits = k) -> exists ff_bit_rectangle_count_point_count_bits. ((((exists ff_h_rectangle_count_point_count_bits_decoded. ff_h_rectangle_count_point_count_bits_decoded + S (ff_bit_rectangle_count_point_count_bits) = S ((S (ff_i_rectangle_count_point_count_bits)) * rc)) /\ exists ff_q_rectangle_count_point_count_bits_decoded. rb = ff_q_rectangle_count_point_count_bits_decoded * S ((S (ff_i_rectangle_count_point_count_bits)) * rc) + (ff_bit_rectangle_count_point_count_bits))) /\ (ff_bit_rectangle_count_point_count_bits = 0 \/ ff_bit_rectangle_count_point_count_bits = 1)))))) - 0013
specialize distinct_odd_prime_half_row_count_exists p - 0014
specialize distinct_odd_prime_half_row_count_exists q - 0015
specialize distinct_odd_prime_half_row_count_exists h - 0016
specialize distinct_odd_prime_half_row_count_exists k - 0017
specialize distinct_odd_prime_half_row_count_exists i - 0018
apply distinct_odd_prime_half_row_count_exists - 0019
exact hpodd - 0020
exact hqodd - 0021
exact hp - 0022
exact hq - 0023
exact hpq - 0024
exact hi - 0025
cases hpackage - 0026
cases hpackage_witness - 0027
cases hpackage_witness_witness - 0028
exists x2 - 0029
exists x - 0030
exists x1 - 0031
exact hpackage_witness_witness_witness