GF006E

gaussian_search_signed_code_bound

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 first-order arithmetic 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))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 6 declared prerequisites and contains 59 exact native proof lines.

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

Proof neighborhood

Direct dependencies

GF006D gaussian_search_natural_le_square le_trans Stable theorem; checked-use authorized mul_le_mul_left Stable theorem; checked-use authorized add_succ_left Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized mul_zero_left Stable theorem; checked-use authorized

Direct dependents

GF0070 gaussian_norm_bounded_coordinates

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 : (exists ge_gap_negative_magnitude_bound. ge_gap_negative_magnitude_bound + (S x) = (N))
  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 exact 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 : (exists ge_gap_negative_magnitude_bound. ge_gap_negative_magnitude_bound + (S 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