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 h k i j. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_lattice_prime_p frp_prime_right_lattice_prime_p. p = frp_prime_left_lattice_prime_p * frp_prime_right_lattice_prime_p -> frp_prime_left_lattice_prime_p = 1 \/ frp_prime_right_lattice_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_lattice_prime_q frp_prime_right_lattice_prime_q. q = frp_prime_left_lattice_prime_q * frp_prime_right_lattice_prime_q -> frp_prime_left_lattice_prime_q = 1 \/ frp_prime_right_lattice_prime_q = 1)) -> ~(p = q) -> (exists elo_gap_lattice_i_bound. elo_gap_lattice_i_bound + S (i) = h) -> (exists elo_gap_lattice_j_bound. elo_gap_lattice_j_bound + S (j) = k) -> ((((exists elo_gap_lattice_cell_result_left. elo_gap_lattice_cell_result_left + S (q * S i) = p * S j) /\ ~(exists elo_gap_lattice_cell_result_right. elo_gap_lattice_cell_result_right + S (p * S j) = q * S i)) \/ ((exists elo_gap_lattice_cell_result_right. elo_gap_lattice_cell_result_right + S (p * S j) = q * S i) /\ ~(exists elo_gap_lattice_cell_result_left. elo_gap_lattice_cell_result_left + S (q * S i) = p * S j))))Structural proof guide
Generated structural guide
Every bounded half-rectangle cell has one exclusive orientation.
Use the direct prerequisites distinct_odd_prime_half_products_ne, lt_trichotomy, lt_to_le, lt_not_le as previously established PA formulas.
The proof proceeds by case analysis (2), intermediate claims (3).
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 (4)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–13
03Establish hneL14–23
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct odd prime half products ne.
- L14
have hne : ~(q * S i = p * S j) - L15
intro heq - L16
specialize distinct_odd_prime_half_products_ne p - L17
specialize distinct_odd_prime_half_products_ne q - L18
specialize distinct_odd_prime_half_products_ne h - L19
specialize distinct_odd_prime_half_products_ne k - L20
specialize distinct_odd_prime_half_products_ne i - L21
specialize distinct_odd_prime_half_products_ne j - L22
apply distinct_odd_prime_half_products_ne - L23
exact hpodd
04Use earlier factsL24–32
05Separate the logical casesL33–34
06Use earlier factsL35–36
07Separate the logical casesL37–39
08Use earlier factsL40–40
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L40
exact lt_trichotomy_right_left
09Fix variables and assumptionsL41–41
Work with arbitrary variables or the premises of the current implication.
- L41
intro hreverse
10Establish hleL42–51
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt to le.
11Separate the logical casesL52–53
12Use earlier factsL54–54
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L54
exact lt_trichotomy_right_right
13Fix variables and assumptionsL55–55
Work with arbitrary variables or the premises of the current implication.
- L55
intro hreverse
14Establish hleL56–65
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt to le.
Original exact command ledger · 65 lines
- 0001
intro p - 0002
intro q - 0003
intro h - 0004
intro k - 0005
intro i - 0006
intro j - 0007
intro hpodd - 0008
intro hqodd - 0009
intro hp - 0010
intro hq - 0011
intro hpq - 0012
intro hi - 0013
intro hj - 0014
have hne : ~(q * S i = p * S j) - 0015
intro heq - 0016
specialize distinct_odd_prime_half_products_ne p - 0017
specialize distinct_odd_prime_half_products_ne q - 0018
specialize distinct_odd_prime_half_products_ne h - 0019
specialize distinct_odd_prime_half_products_ne k - 0020
specialize distinct_odd_prime_half_products_ne i - 0021
specialize distinct_odd_prime_half_products_ne j - 0022
apply distinct_odd_prime_half_products_ne - 0023
exact hpodd - 0024
exact hqodd - 0025
exact hp - 0026
exact hq - 0027
exact hpq - 0028
exact hi - 0029
exact hj - 0030
exact heq - 0031
specialize lt_trichotomy (q * S i) - 0032
specialize lt_trichotomy (p * S j) - 0033
cases lt_trichotomy - 0034
exfalso - 0035
apply hne - 0036
exact lt_trichotomy_left - 0037
cases lt_trichotomy_right - 0038
left - 0039
split - 0040
exact lt_trichotomy_right_left - 0041
intro hreverse - 0042
have hle : exists gap. gap + (p * S j) = q * S i - 0043
specialize lt_to_le (p * S j) - 0044
specialize lt_to_le (q * S i) - 0045
apply lt_to_le - 0046
exact hreverse - 0047
specialize lt_not_le (q * S i) - 0048
specialize lt_not_le (p * S j) - 0049
apply lt_not_le - 0050
exact lt_trichotomy_right_left - 0051
exact hle - 0052
right - 0053
split - 0054
exact lt_trichotomy_right_right - 0055
intro hreverse - 0056
have hle : exists gap. gap + (q * S i) = p * S j - 0057
specialize lt_to_le (q * S i) - 0058
specialize lt_to_le (p * S j) - 0059
apply lt_to_le - 0060
exact hreverse - 0061
specialize lt_not_le (p * S j) - 0062
specialize lt_not_le (q * S i) - 0063
apply lt_not_le - 0064
exact lt_trichotomy_right_right - 0065
exact hle