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.
Exact expanded PA statement
forall p q e f h k. (((((exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq) -> (exists qrp_even_e_even. e = 2 * qrp_even_e_even)) /\ ((exists qrp_even_e_even. e = 2 * qrp_even_e_even) -> (exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq))) /\ (((~(exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq)) -> (exists qrp_odd_e_odd. e = 2 * qrp_odd_e_odd + 1)) /\ ((exists qrp_odd_e_odd. e = 2 * qrp_odd_e_odd + 1) -> ~(exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq))))) -> (((((exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp) -> (exists qrp_even_f_even. f = 2 * qrp_even_f_even)) /\ ((exists qrp_even_f_even. f = 2 * qrp_even_f_even) -> (exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp))) /\ (((~(exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp)) -> (exists qrp_odd_f_odd. f = 2 * qrp_odd_f_odd + 1)) /\ ((exists qrp_odd_f_odd. f = 2 * qrp_odd_f_odd + 1) -> ~(exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp))))) -> (exists qrp_u_count_product qrp_v_count_product. e + f + 2 * qrp_u_count_product = h * k + 2 * qrp_v_count_product) -> (exists qrp_even_half_product. h * k = 2 * qrp_even_half_product) -> ((((exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq) /\ (exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp)) \/ (~(exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq) /\ ~(exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp))))Structural proof guide
Generated structural guide
Modulo-two equality with an even half product gives equal residue status.
Use the direct prerequisites mod_two_preserves_parity, qres_same_status_from_even_count_sum as previously established PA formulas.
The proof proceeds by case analysis (2), intermediate claims (2).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.
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–10
02Establish htransportL11–15
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod two preserves parity.
03Separate the logical casesL16–17
04Establish hcountL18–27
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply htransport left right.
- L18
have hcount : exists qrp_even_transport_count. e + f = 2 * qrp_even_transport_count - L19
apply htransport_left_right - L20
exact hproduct - L21
specialize qres_same_status_from_even_count_sum p - L22
specialize qres_same_status_from_even_count_sum q - L23
specialize qres_same_status_from_even_count_sum e - L24
specialize qres_same_status_from_even_count_sum f - L25
apply qres_same_status_from_even_count_sum - L26
exact heclass - L27
exact hfclass
05Use earlier factsL28–28
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L28
exact hcount
Original exact command ledger · 28 lines
- 0001
intro p - 0002
intro q - 0003
intro e - 0004
intro f - 0005
intro h - 0006
intro k - 0007
intro heclass - 0008
intro hfclass - 0009
intro hmod - 0010
intro hproduct - 0011
have htransport : (((((exists qrp_even_transport_count. e + f = 2 * qrp_even_transport_count) -> (exists qrp_even_transport_product. h * k = 2 * qrp_even_transport_product)) /\ ((exists qrp_even_transport_product. h * k = 2 * qrp_even_transport_product) -> (exists qrp_even_transport_count. e + f = 2 * qrp_even_transport_count)))) /\ ((((exists qrp_odd_transport_count. e + f = 2 * qrp_odd_transport_count + 1) -> (exists qrp_odd_transport_product. h * k = 2 * qrp_odd_transport_product + 1)) /\ ((exists qrp_odd_transport_product. h * k = 2 * qrp_odd_transport_product + 1) -> (exists qrp_odd_transport_count. e + f = 2 * qrp_odd_transport_count + 1))))) - 0012
specialize mod_two_preserves_parity (e + f) - 0013
specialize mod_two_preserves_parity (h * k) - 0014
apply mod_two_preserves_parity - 0015
exact hmod - 0016
cases htransport - 0017
cases htransport_left - 0018
have hcount : exists qrp_even_transport_count. e + f = 2 * qrp_even_transport_count - 0019
apply htransport_left_right - 0020
exact hproduct - 0021
specialize qres_same_status_from_even_count_sum p - 0022
specialize qres_same_status_from_even_count_sum q - 0023
specialize qres_same_status_from_even_count_sum e - 0024
specialize qres_same_status_from_even_count_sum f - 0025
apply qres_same_status_from_even_count_sum - 0026
exact heclass - 0027
exact hfclass - 0028
exact hcount