GI0039

gaussian_nearest_signed_quotient_exists

Construct an actual nearest signed quotient, signed error, and half-bounded magnitude from one floor division and the checked centered natural remainder constructor.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

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.

The natural-code carrier consists of genuine pairs of the existing signed integers; no new primitive arithmetic is trusted. The theorem constructs quotient, remainder, and actual norm witnesses. Gaussian gcd, unique factorization, and prime classification are separate targets.

Exact theorem in conservative defined notation

∀ p. ∀ n. ∀ N. ¬N = 0 → ∃ x. ∃ y. ∃ z. ∃ m. ∃ k. RoundedSignedDivision(p,n,N,x,y,z,m,k)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedFloor(p,n,m,q,t,r) · 1RoundedSignedDivision(p,n,N,qp,qn,ep,en,t) · 1Le(a,b) · 1

Actual proof prerequisites

signed_integer_floor_existsfour_square_descent_centered_signed_remainder_exists · checked external prerequisitemul_add · checked external prerequisiteadd_assoc · checked external prerequisitemul_zero_left · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall p n N. ~(N = 0) -> exists qp qn ep en t. (((((p) + (N) * (qn)) + (en) = ((n) + (N) * (qp)) + (ep)) /\ ((((((ep) * (ep))) + (((en) * (en)))) = ((((t) * (t))) + (((((ep) * (en))) + (((en) * (ep))))))) /\ (exists ge_gap_nearesthalf_bound. ge_gap_nearesthalf_bound + (((t) + (t))) = (N)))))

Complete tactic proof in conservative notation

All 56 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

56 script commands · 26 reading checkpoints · 2 local claims

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
signed integer floor exists
01Fix variables and assumptionsL1–4

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro N
  4. L4
    intro hN
02Establish hfloorL5–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed integer floor exists.

  1. L5
    have hfloor : ∃ qp. ∃ qn. ∃ r. SignedFloor(p,n,N,qp,qn,r)Definitions: SignedFloor(p,n,N,qp,qn,r)Original native command in the exact edition
  2. L6
    specialize signed_integer_floor_exists p
  3. L7
    specialize signed_integer_floor_exists n
  4. L8
    specialize signed_integer_floor_exists N
  5. L9
    apply signed_integer_floor_exists
  6. L10
    exact hN
03Separate the logical casesL11–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L11
    cases hfloor
  2. L12
    cases hfloor_witness
  3. L13
    cases hfloor_witness_witness
  4. L14
    cases hfloor_witness_witness_witness
04Establish hcenterL15–19

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.

  1. L15
    have hcenter : ∃ t. Le(t + t,N) ∧ ((∃ x. x2 = N · x + t) ∨ (∃ x. x2 + t = N · x))Definitions: Le(t + t,N)Original native command in the exact edition
  2. L16
    specialize four_square_descent_centered_signed_remainder_exists N
  3. L17
    specialize four_square_descent_centered_signed_remainder_exists x2
  4. L18
    apply four_square_descent_centered_signed_remainder_exists
  5. L19
    exact hN
05Separate the logical casesL20–23

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L20
    cases hcenter
  2. L21
    cases hcenter_witness
  3. L22
    cases hcenter_witness_right
  4. L23
    cases hcenter_witness_right_left
06Construct an explicit witnessL24–28

Supply the displayed value, then prove that it has the required property.

  1. L24
    exists x + x4
  2. L25
    exists x1
  3. L26
    exists x3
  4. L27
    exists 0
  5. L28
    exists x3
07Separate the logical casesL29–29

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    split
08Calculate and transport equalitiesL30–30

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L30
    trans p + N * x1
09Use earlier factsL31–31

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L31
    apply PA3
10Calculate and transport equalitiesL32–32

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L32
    trans (n + N * x) + x2
11Use earlier factsL33–33

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L33
    exact hfloor_witness_witness_witness_left
12Calculate and transport equalitiesL34–35

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L34
    rewrite hcenter_witness_right_left_witness
  2. L35
    simp [mul_add, add_assoc]
13Separate the logical casesL36–36

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L36
    split
14Calculate and transport equalitiesL37–37

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L37
    simp [mul_zero_left, zero_add]
15Use earlier factsL38–38

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L38
    exact hcenter_witness_left
16Separate the logical casesL39–39

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L39
    cases hcenter_witness_right_right
17Construct an explicit witnessL40–44

Supply the displayed value, then prove that it has the required property.

  1. L40
    exists x + x4
  2. L41
    exists x1
  3. L42
    exists 0
  4. L43
    exists x3
  5. L44
    exists x3
18Separate the logical casesL45–45

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L45
    split
19Calculate and transport equalitiesL46–47

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L46
    trans ((n + N * x) + x2) + x3
  2. L47
    congr
20Use earlier factsL48–48

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L48
    exact hfloor_witness_witness_witness_left
21Calculate and transport equalitiesL49–50

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L49
    refl
  2. L50
    trans (n + N * x) + (x2 + x3)
22Use earlier factsL51–51

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L51
    apply add_assoc
23Calculate and transport equalitiesL52–53

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L52
    rewrite hcenter_witness_right_right_witness
  2. L53
    simp [mul_add, add_assoc]
24Separate the logical casesL54–54

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L54
    split
25Calculate and transport equalitiesL55–55

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L55
    simp [mul_zero_left, zero_add]
26Use earlier factsL56–56

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L56
    exact hcenter_witness_left

Library-wide reading audit

Original defined command ledger · 56 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro N
  4. 0004intro hN
  5. 0005have hfloor : ∃ qp. ∃ qn. ∃ r. SignedFloor(p,n,N,qp,qn,r)
  6. 0006specialize signed_integer_floor_exists p
  7. 0007specialize signed_integer_floor_exists n
  8. 0008specialize signed_integer_floor_exists N
  9. 0009apply signed_integer_floor_exists
  10. 0010exact hN
  11. 0011cases hfloor
  12. 0012cases hfloor_witness
  13. 0013cases hfloor_witness_witness
  14. 0014cases hfloor_witness_witness_witness
  15. 0015have hcenter : ∃ t. Le(t + t,N) ∧ ((∃ x. x2 = N · x + t) ∨ (∃ x. x2 + t = N · x))
  16. 0016specialize four_square_descent_centered_signed_remainder_exists N
  17. 0017specialize four_square_descent_centered_signed_remainder_exists x2
  18. 0018apply four_square_descent_centered_signed_remainder_exists
  19. 0019exact hN
  20. 0020cases hcenter
  21. 0021cases hcenter_witness
  22. 0022cases hcenter_witness_right
  23. 0023cases hcenter_witness_right_left
  24. 0024exists x + x4
  25. 0025exists x1
  26. 0026exists x3
  27. 0027exists 0
  28. 0028exists x3
  29. 0029split
  30. 0030trans p + N * x1
  31. 0031apply PA3
  32. 0032trans (n + N * x) + x2
  33. 0033exact hfloor_witness_witness_witness_left
  34. 0034rewrite hcenter_witness_right_left_witness
  35. 0035simp [mul_add, add_assoc]
  36. 0036split
  37. 0037simp [mul_zero_left, zero_add]
  38. 0038exact hcenter_witness_left
  39. 0039cases hcenter_witness_right_right
  40. 0040exists x + x4
  41. 0041exists x1
  42. 0042exists 0
  43. 0043exists x3
  44. 0044exists x3
  45. 0045split
  46. 0046trans ((n + N * x) + x2) + x3
  47. 0047congr
  48. 0048exact hfloor_witness_witness_witness_left
  49. 0049refl
  50. 0050trans (n + N * x) + (x2 + x3)
  51. 0051apply add_assoc
  52. 0052rewrite hcenter_witness_right_right_witness
  53. 0053simp [mul_add, add_assoc]
  54. 0054split
  55. 0055simp [mul_zero_left, zero_add]
  56. 0056exact hcenter_witness_left