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
∀ k. ∀ a. ∀ b. ∀ c. ∀ d. ¬k = 0 → ∃ x. ∃ y. ∃ z. ∃ n. Le(x + x,k) ∧ ((∃ m. a = k · m + x) ∨ Dvd(k,a + x)) ∧ (Le(y + y,k) ∧ ((∃ m. b = k · m + y) ∨ Dvd(k,b + y)) ∧ (Le(z + z,k) ∧ ((∃ m. c = k · m + z) ∨ Dvd(k,c + z)) ∧ (Le(n + n,k) ∧ ((∃ m. d = k · m + n) ∨ Dvd(k,d + n)))))Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.
Definitions used by this theorem
In the theorem statement
In local proof propositions
Exact expanded first-order statement
forall k a b c d. ~(k = 0) -> exists e f g h. ((((exists fsd_center_bound_four_0. fsd_center_bound_four_0 + (e + e) = k) /\ ((exists fsd_center_lower_four_0. a = k * fsd_center_lower_four_0 + e) \/ (exists fsd_center_upper_four_0. a + e = k * fsd_center_upper_four_0)))) /\ ((((exists fsd_center_bound_four_1. fsd_center_bound_four_1 + (f + f) = k) /\ ((exists fsd_center_lower_four_1. b = k * fsd_center_lower_four_1 + f) \/ (exists fsd_center_upper_four_1. b + f = k * fsd_center_upper_four_1)))) /\ ((((exists fsd_center_bound_four_2. fsd_center_bound_four_2 + (g + g) = k) /\ ((exists fsd_center_lower_four_2. c = k * fsd_center_lower_four_2 + g) \/ (exists fsd_center_upper_four_2. c + g = k * fsd_center_upper_four_2)))) /\ (((exists fsd_center_bound_four_3. fsd_center_bound_four_3 + (h + h) = k) /\ ((exists fsd_center_lower_four_3. d = k * fsd_center_lower_four_3 + h) \/ (exists fsd_center_upper_four_3. d + h = k * fsd_center_upper_four_3)))))))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay 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–6
02Establish haL7–11
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square descent centered signed remainder exists.
- L7
have ha : ∃ e. Le(e + e,k) ∧ ((∃ x. a = k · x + e) ∨ Dvd(k,a + e))Definitions: Le(e + e,k)Dvd(k,a + e)Original native command in the exact edition - L8
specialize four_square_descent_centered_signed_remainder_exists k - L9
specialize four_square_descent_centered_signed_remainder_exists a - L10
apply four_square_descent_centered_signed_remainder_exists - L11
exact hnonzero
03Establish hbL12–14
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square descent centered signed remainder exists.
- L12
have hb : ∃ f. Le(f + f,k) ∧ ((∃ x. b = k · x + f) ∨ Dvd(k,b + f))Definitions: Le(f + f,k)Dvd(k,b + f)Original native command in the exact edition - L13
apply four_square_descent_centered_signed_remainder_exists - L14
exact hnonzero
04Establish hcL15–17
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square descent centered signed remainder exists.
- L15
have hc : ∃ g. Le(g + g,k) ∧ ((∃ x. c = k · x + g) ∨ Dvd(k,c + g))Definitions: Le(g + g,k)Dvd(k,c + g)Original native command in the exact edition - L16
apply four_square_descent_centered_signed_remainder_exists - L17
exact hnonzero
05Establish hdL18–20
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square descent centered signed remainder exists.
- L18
have hd : ∃ h. Le(h + h,k) ∧ ((∃ x. d = k · x + h) ∨ Dvd(k,d + h))Definitions: Le(h + h,k)Dvd(k,d + h)Original native command in the exact edition - L19
apply four_square_descent_centered_signed_remainder_exists - L20
exact hnonzero
06Separate the logical casesL21–24
07Construct an explicit witnessL25–28
08Separate the logical casesL29–29
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L29
split
09Use earlier factsL30–30
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L30
exact ha_witness
10Separate the logical casesL31–31
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L31
split
11Use earlier factsL32–32
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L32
exact hb_witness
12Separate the logical casesL33–33
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L33
split
Original defined command ledger · 35 lines
- 0001
intro k - 0002
intro a - 0003
intro b - 0004
intro c - 0005
intro d - 0006
intro hnonzero - 0007
have ha : ∃ e. Le(e + e,k) ∧ ((∃ x. a = k · x + e) ∨ Dvd(k,a + e))Exact native replay line
have ha : exists e. (((exists fsd_center_bound_four_a. fsd_center_bound_four_a + (e + e) = k) /\ ((exists fsd_center_lower_four_a. a = k * fsd_center_lower_four_a + e) \/ (exists fsd_center_upper_four_a. a + e = k * fsd_center_upper_four_a)))) - 0008
specialize four_square_descent_centered_signed_remainder_exists k - 0009
specialize four_square_descent_centered_signed_remainder_exists a - 0010
apply four_square_descent_centered_signed_remainder_exists - 0011
exact hnonzero - 0012
have hb : ∃ f. Le(f + f,k) ∧ ((∃ x. b = k · x + f) ∨ Dvd(k,b + f))Exact native replay line
have hb : exists f. (((exists fsd_center_bound_four_b. fsd_center_bound_four_b + (f + f) = k) /\ ((exists fsd_center_lower_four_b. b = k * fsd_center_lower_four_b + f) \/ (exists fsd_center_upper_four_b. b + f = k * fsd_center_upper_four_b)))) - 0013
apply four_square_descent_centered_signed_remainder_exists - 0014
exact hnonzero - 0015
have hc : ∃ g. Le(g + g,k) ∧ ((∃ x. c = k · x + g) ∨ Dvd(k,c + g))Exact native replay line
have hc : exists g. (((exists fsd_center_bound_four_c. fsd_center_bound_four_c + (g + g) = k) /\ ((exists fsd_center_lower_four_c. c = k * fsd_center_lower_four_c + g) \/ (exists fsd_center_upper_four_c. c + g = k * fsd_center_upper_four_c)))) - 0016
apply four_square_descent_centered_signed_remainder_exists - 0017
exact hnonzero - 0018
have hd : ∃ h. Le(h + h,k) ∧ ((∃ x. d = k · x + h) ∨ Dvd(k,d + h))Exact native replay line
have hd : exists h. (((exists fsd_center_bound_four_d. fsd_center_bound_four_d + (h + h) = k) /\ ((exists fsd_center_lower_four_d. d = k * fsd_center_lower_four_d + h) \/ (exists fsd_center_upper_four_d. d + h = k * fsd_center_upper_four_d)))) - 0019
apply four_square_descent_centered_signed_remainder_exists - 0020
exact hnonzero - 0021
cases ha - 0022
cases hb - 0023
cases hc - 0024
cases hd - 0025
exists x - 0026
exists x1 - 0027
exists x2 - 0028
exists x3 - 0029
split - 0030
exact ha_witness - 0031
split - 0032
exact hb_witness - 0033
split - 0034
exact hc_witness - 0035
exact hd_witness