GF006E

gaussian_search_signed_code_bound

A canonical signed code for an integer whose square is bounded by N is at most 2N, for both signs and zero.

Alpha v34 checked-use · first admitted v30 · 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.

Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.

Exact theorem in conservative defined notation

∀ code. ∀ p. ∀ n. ∀ R. ∀ N. SignedDecode(code,p,n) → SignedDifferenceSquare(p,n,R) → Le(R,N) → Le(code,2 · N)

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

Definition DAG

SignedDecode(z,p,n) · 1SignedDifferenceSquare(p,n,s) · 1Le(a,b) · 2Lt(a,b) · 1

Actual proof prerequisites

gaussian_search_natural_le_squarele_trans · checked external prerequisitemul_le_mul_left · checked external prerequisiteadd_succ_left · checked external prerequisitezero_add · checked external prerequisitemul_zero_left · checked external prerequisite
Original expanded first-order statement 
forall code p n R N. ((((code) = 2 * (p) /\ (n) = 0) \/ exists ge_signed_half_search_signed_decode. (((code) = 2 * ge_signed_half_search_signed_decode + 1 /\ (p) = 0) /\ (n) = S ge_signed_half_search_signed_decode))) -> (((((p) * (p))) + (((n) * (n)))) = ((R) + (((((p) * (n))) + (((n) * (p))))))) -> (exists ge_gap_search_square_bound. ge_gap_search_square_bound + (R) = (N)) -> (exists ge_gap_search_code_bound. ge_gap_search_code_bound + (code) = (2*N))

Complete tactic proof in conservative notation

All 59 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

59 script commands · 13 reading checkpoints · 3 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)
gaussian search natural le square
01Fix variables and assumptionsL1–8

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

  1. L1
    intro code
  2. L2
    intro p
  3. L3
    intro n
  4. L4
    intro R
  5. L5
    intro N
  6. L6
    intro hsigned
  7. L7
    intro hsquare
  8. L8
    intro hbound
02Separate the logical casesL9–10

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

  1. L9
    cases hsigned
  2. L10
    cases hsigned_left
03Establish heqL11–20

Establish this local claim before using it. It is not an additional assumption.

  1. L11
    have heq : p*p=R
  2. L12
    trans p*p+n*n
  3. L13
    simp [hsigned_left_right]
  4. L14
    trans R+(p*n+n*p)
  5. L15
    exact hsquare
  6. L16
    simp [hsigned_left_right, zero_add, mul_zero_left]
  7. L17
    rewrite hsigned_left_left
  8. L18
    specialize mul_le_mul_left (p)
  9. L19
    specialize mul_le_mul_left (N)
  10. L20
    specialize mul_le_mul_left (2)
04Use earlier factsL21–27

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

  1. L21
    apply mul_le_mul_left
  2. L22
    specialize le_trans (p)
  3. L23
    specialize le_trans (p*p)
  4. L24
    specialize le_trans (N)
  5. L25
    apply le_trans
  6. L26
    specialize gaussian_search_natural_le_square (p)
  7. L27
    apply gaussian_search_natural_le_square
05Calculate and transport equalitiesL28–28

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

  1. L28
    rewrite heq
06Use earlier factsL29–29

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

  1. L29
    exact hbound
07Separate the logical casesL30–32

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

  1. L30
    cases hsigned_right
  2. L31
    cases hsigned_right_witness
  3. L32
    cases hsigned_right_witness_left
08Establish heqL33–38

Establish this local claim before using it. It is not an additional assumption.

  1. L33
    have heq : S x*S x=R
  2. L34
    trans p*p+n*n
  3. L35
    simp [hsigned_right_witness_left_right, hsigned_right_witness_right, zero_add]
  4. L36
    trans R+(p*n+n*p)
  5. L37
    exact hsquare
  6. L38
    simp [hsigned_right_witness_left_right, mul_zero_left]
09Establish hsmallL39–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.

  1. L39
    have hsmall : Lt(x,N)Definitions: Lt(x,N)Original native command in the exact edition
  2. L40
    specialize le_trans (S x)
  3. L41
    specialize le_trans (S x*S x)
  4. L42
    specialize le_trans (N)
  5. L43
    apply le_trans
  6. L44
    specialize gaussian_search_natural_le_square (S x)
  7. L45
    apply gaussian_search_natural_le_square
  8. L46
    rewrite heq
  9. L47
    exact hbound
  10. L48
    rewrite hsigned_right_witness_left_left
10Use earlier factsL49–52

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

  1. L49
    specialize le_trans (2*x+1)
  2. L50
    specialize le_trans (2*S x)
  3. L51
    specialize le_trans (2*N)
  4. L52
    apply le_trans
11Construct an explicit witnessL53–53

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

  1. L53
    exists 1
12Calculate and transport equalitiesL54–54

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

  1. L54
    simp [add_succ_left, zero_add]
13Use earlier factsL55–59

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

  1. L55
    specialize mul_le_mul_left (S x)
  2. L56
    specialize mul_le_mul_left (N)
  3. L57
    specialize mul_le_mul_left (2)
  4. L58
    apply mul_le_mul_left
  5. L59
    exact hsmall

Library-wide reading audit

Original defined command ledger · 59 lines
  1. 0001intro code
  2. 0002intro p
  3. 0003intro n
  4. 0004intro R
  5. 0005intro N
  6. 0006intro hsigned
  7. 0007intro hsquare
  8. 0008intro hbound
  9. 0009cases hsigned
  10. 0010cases hsigned_left
  11. 0011have heq : p*p=R
  12. 0012trans p*p+n*n
  13. 0013simp [hsigned_left_right]
  14. 0014trans R+(p*n+n*p)
  15. 0015exact hsquare
  16. 0016simp [hsigned_left_right, zero_add, mul_zero_left]
  17. 0017rewrite hsigned_left_left
  18. 0018specialize mul_le_mul_left (p)
  19. 0019specialize mul_le_mul_left (N)
  20. 0020specialize mul_le_mul_left (2)
  21. 0021apply mul_le_mul_left
  22. 0022specialize le_trans (p)
  23. 0023specialize le_trans (p*p)
  24. 0024specialize le_trans (N)
  25. 0025apply le_trans
  26. 0026specialize gaussian_search_natural_le_square (p)
  27. 0027apply gaussian_search_natural_le_square
  28. 0028rewrite heq
  29. 0029exact hbound
  30. 0030cases hsigned_right
  31. 0031cases hsigned_right_witness
  32. 0032cases hsigned_right_witness_left
  33. 0033have heq : S x*S x=R
  34. 0034trans p*p+n*n
  35. 0035simp [hsigned_right_witness_left_right, hsigned_right_witness_right, zero_add]
  36. 0036trans R+(p*n+n*p)
  37. 0037exact hsquare
  38. 0038simp [hsigned_right_witness_left_right, mul_zero_left]
  39. 0039have hsmall : Lt(x,N)
  40. 0040specialize le_trans (S x)
  41. 0041specialize le_trans (S x*S x)
  42. 0042specialize le_trans (N)
  43. 0043apply le_trans
  44. 0044specialize gaussian_search_natural_le_square (S x)
  45. 0045apply gaussian_search_natural_le_square
  46. 0046rewrite heq
  47. 0047exact hbound
  48. 0048rewrite hsigned_right_witness_left_left
  49. 0049specialize le_trans (2*x+1)
  50. 0050specialize le_trans (2*S x)
  51. 0051specialize le_trans (2*N)
  52. 0052apply le_trans
  53. 0053exists 1
  54. 0054simp [add_succ_left, zero_add]
  55. 0055specialize mul_le_mul_left (S x)
  56. 0056specialize mul_le_mul_left (N)
  57. 0057specialize mul_le_mul_left (2)
  58. 0058apply mul_le_mul_left
  59. 0059exact hsmall