GF0070

gaussian_norm_bounded_coordinates

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

An actual Gaussian norm bounds both canonical signed-coordinate codes; arbitrary non-normal representatives are never bounded.

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 z N. (exists ge_norm_rp_search_given_norm ge_norm_rn_search_given_norm ge_norm_ip_search_given_norm ge_norm_in_search_given_norm. ((exists ge_representation_real_code_search_given_normrepresentation ge_representation_imaginary_code_search_given_normrepresentation. (((z) = ((ge_representation_real_code_search_given_normrepresentation) + (ge_representation_imaginary_code_search_given_normrepresentation)) * S ((ge_representation_real_code_search_given_normrepresentation) + (ge_representation_imaginary_code_search_given_normrepresentation)) + ((ge_representation_imaginary_code_search_given_normrepresentation) + (ge_representation_imaginary_code_search_given_normrepresentation))) /\ ((exists ge_balance_positive_search_given_normrepresentationreal ge_balance_negative_search_given_normrepresentationreal. (((((ge_representation_real_code_search_given_normrepresentation) = 2 * (ge_balance_positive_search_given_normrepresentationreal) /\ (ge_balance_negative_search_given_normrepresentationreal) = 0) \/ exists ge_signed_half_search_given_normrepresentationrealdecode. (((ge_representation_real_code_search_given_normrepresentation) = 2 * ge_signed_half_search_given_normrepresentationrealdecode + 1 /\ (ge_balance_positive_search_given_normrepresentationreal) = 0) /\ (ge_balance_negative_search_given_normrepresentationreal) = S ge_signed_half_search_given_normrepresentationrealdecode))) /\ ((ge_norm_rp_search_given_norm) + ge_balance_negative_search_given_normrepresentationreal = (ge_norm_rn_search_given_norm) + ge_balance_positive_search_given_normrepresentationreal))) /\ (exists ge_balance_positive_search_given_normrepresentationimaginary ge_balance_negative_search_given_normrepresentationimaginary. (((((ge_representation_imaginary_code_search_given_normrepresentation) = 2 * (ge_balance_positive_search_given_normrepresentationimaginary) /\ (ge_balance_negative_search_given_normrepresentationimaginary) = 0) \/ exists ge_signed_half_search_given_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_search_given_normrepresentation) = 2 * ge_signed_half_search_given_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_search_given_normrepresentationimaginary) = 0) /\ (ge_balance_negative_search_given_normrepresentationimaginary) = S ge_signed_half_search_given_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_search_given_norm) + ge_balance_negative_search_given_normrepresentationimaginary = (ge_norm_in_search_given_norm) + ge_balance_positive_search_given_normrepresentationimaginary)))))) /\ (exists ge_real_square_search_given_normsquare ge_imaginary_square_search_given_normsquare. ((((((ge_norm_rp_search_given_norm) * (ge_norm_rp_search_given_norm))) + (((ge_norm_rn_search_given_norm) * (ge_norm_rn_search_given_norm)))) = ((ge_real_square_search_given_normsquare) + (((((ge_norm_rp_search_given_norm) * (ge_norm_rn_search_given_norm))) + (((ge_norm_rn_search_given_norm) * (ge_norm_rp_search_given_norm))))))) /\ ((((((ge_norm_ip_search_given_norm) * (ge_norm_ip_search_given_norm))) + (((ge_norm_in_search_given_norm) * (ge_norm_in_search_given_norm)))) = ((ge_imaginary_square_search_given_normsquare) + (((((ge_norm_ip_search_given_norm) * (ge_norm_in_search_given_norm))) + (((ge_norm_in_search_given_norm) * (ge_norm_ip_search_given_norm))))))) /\ ((N) = ge_real_square_search_given_normsquare + ge_imaginary_square_search_given_normsquare)))))) -> (exists gr_search_real_search_bounded_coordinates gr_search_imaginary_search_bounded_coordinates. (((z)=((gr_search_real_search_bounded_coordinates) + (gr_search_imaginary_search_bounded_coordinates)) * S ((gr_search_real_search_bounded_coordinates) + (gr_search_imaginary_search_bounded_coordinates)) + ((gr_search_imaginary_search_bounded_coordinates) + (gr_search_imaginary_search_bounded_coordinates))) /\ ((exists ge_gap_search_bounded_coordinatesreal_bound. ge_gap_search_bounded_coordinatesreal_bound + (gr_search_real_search_bounded_coordinates) = (2*(N))) /\ (exists ge_gap_search_bounded_coordinatesimaginary_bound. ge_gap_search_bounded_coordinatesimaginary_bound + (gr_search_imaginary_search_bounded_coordinates) = (2*(N))))))

Constructive proof overview

Generated structural guide

An actual Gaussian norm bounds both canonical signed-coordinate codes; arbitrary non-normal representatives are never bounded.

The unchanged tactic script uses 5 declared prerequisites and contains 63 exact native proof lines.

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

Proof neighborhood

Direct dependencies

GF0003 gaussian_norm_input_valid gaussian_decode_representation Alpha theorem; checked-use authorized gaussian_norm_for_representation Alpha theorem; checked-use authorized GF006E gaussian_search_signed_code_bound add_comm Stable theorem; checked-use authorized

Direct dependents

GF0078 gaussian_factor_search_complete

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

63 script commands · 17 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.

Named ingredients (2)
gaussian norm input validgaussian search signed code bound

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro z
  2. L2
    intro N
  3. L3
    intro hnorm
02Establish hvalidL4–8

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian norm input valid.

  1. L4
    have hvalid : ZPairValid(z)Definitions: ZPairValid
  2. L5
    specialize gaussian_norm_input_valid (z)
  3. L6
    specialize gaussian_norm_input_valid (N)
  4. L7
    apply gaussian_norm_input_valid
  5. L8
    exact hnorm
03Separate the logical casesL9–12

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

  1. L9
    cases hvalid
  2. L10
    cases hvalid_witness
  3. L11
    cases hvalid_witness_witness
  4. L12
    cases hvalid_witness_witness_witness
04Establish hrawL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian norm for representation.

  1. L13
    have hraw : (exists ge_real_square_search_canonical_norm ge_imaginary_square_search_canonical_norm. ((((((x) * (x))) + (((x1) * (x1)))) = ((ge_real_square_search_canonical_norm) + (((((x) * (x1))) + (((x1) * (x))))))) /\ ((((((x2) * (x2))) + (((x3) * (x3)))) = ((ge_imaginary_square_search_canonical_norm) + (((((x2) * (x3))) + (((x3) * (x2))))))) /\ ((N) = ge_real_square_search_canonical_norm + ge_imaginary_square_search_canonical_norm))))
  2. L14
    specialize gaussian_norm_for_representation (z)
  3. L15
    specialize gaussian_norm_for_representation (x)
  4. L16
    specialize gaussian_norm_for_representation (x1)
  5. L17
    specialize gaussian_norm_for_representation (x2)
  6. L18
    specialize gaussian_norm_for_representation (x3)
  7. L19
    specialize gaussian_norm_for_representation (N)
  8. L20
    apply gaussian_norm_for_representation
  9. L21
    specialize gaussian_decode_representation (z)
  10. L22
    specialize gaussian_decode_representation (x)
05Use earlier factsL23–28

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

  1. L23
    specialize gaussian_decode_representation (x1)
  2. L24
    specialize gaussian_decode_representation (x2)
  3. L25
    specialize gaussian_decode_representation (x3)
  4. L26
    apply gaussian_decode_representation
  5. L27
    exact hvalid_witness_witness_witness_witness
  6. L28
    exact hnorm
06Separate the logical casesL29–36

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

  1. L29
    cases hvalid_witness_witness_witness_witness
  2. L30
    cases hvalid_witness_witness_witness_witness_witness
  3. L31
    cases hvalid_witness_witness_witness_witness_witness_witness
  4. L32
    cases hvalid_witness_witness_witness_witness_witness_witness_right
  5. L33
    cases hraw
  6. L34
    cases hraw_witness
  7. L35
    cases hraw_witness_witness
  8. L36
    cases hraw_witness_witness_right
07Construct an explicit witnessL37–38

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

  1. L37
    exists (x4)
  2. L38
    exists (x5)
08Separate the logical casesL39–39

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

  1. L39
    split
09Use earlier factsL40–40

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

  1. L40
    exact hvalid_witness_witness_witness_witness_witness_witness_left
10Separate the logical casesL41–41

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

  1. L41
    split
11Use earlier factsL42–49

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

  1. L42
    specialize gaussian_search_signed_code_bound (x4)
  2. L43
    specialize gaussian_search_signed_code_bound (x)
  3. L44
    specialize gaussian_search_signed_code_bound (x1)
  4. L45
    specialize gaussian_search_signed_code_bound (x6)
  5. L46
    specialize gaussian_search_signed_code_bound (N)
  6. L47
    apply gaussian_search_signed_code_bound
  7. L48
    exact hvalid_witness_witness_witness_witness_witness_witness_right_left
  8. L49
    exact hraw_witness_witness_left
12Construct an explicit witnessL50–50

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

  1. L50
    exists x7
13Calculate and transport equalitiesL51–51

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

  1. L51
    rewrite hraw_witness_witness_right_right
14Use earlier factsL52–60

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

  1. L52
    apply add_comm
  2. L53
    specialize gaussian_search_signed_code_bound (x5)
  3. L54
    specialize gaussian_search_signed_code_bound (x2)
  4. L55
    specialize gaussian_search_signed_code_bound (x3)
  5. L56
    specialize gaussian_search_signed_code_bound (x7)
  6. L57
    specialize gaussian_search_signed_code_bound (N)
  7. L58
    apply gaussian_search_signed_code_bound
  8. L59
    exact hvalid_witness_witness_witness_witness_witness_witness_right_right
  9. L60
    exact hraw_witness_witness_right_left
15Construct an explicit witnessL61–61

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

  1. L61
    exists x6
16Calculate and transport equalitiesL62–62

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

  1. L62
    symm
17Use earlier factsL63–63

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

  1. L63
    exact hraw_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 63 lines
  1. 0001intro z
  2. 0002intro N
  3. 0003intro hnorm
  4. 0004have hvalid : (exists ge_real_positive_search_norm_valid ge_real_negative_search_norm_valid ge_imaginary_positive_search_norm_valid ge_imaginary_negative_search_norm_valid. (exists ge_real_code_search_norm_validdecode ge_imaginary_code_search_norm_validdecode. (((z) = ((ge_real_code_search_norm_validdecode) + (ge_imaginary_code_search_norm_validdecode)) * S ((ge_real_code_search_norm_validdecode) + (ge_imaginary_code_search_norm_validdecode)) + ((ge_imaginary_code_search_norm_validdecode) + (ge_imaginary_code_search_norm_validdecode))) /\ (((((ge_real_code_search_norm_validdecode) = 2 * (ge_real_positive_search_norm_valid) /\ (ge_real_negative_search_norm_valid) = 0) \/ exists ge_signed_half_ge_search_norm_validdecode_real. (((ge_real_code_search_norm_validdecode) = 2 * ge_signed_half_ge_search_norm_validdecode_real + 1 /\ (ge_real_positive_search_norm_valid) = 0) /\ (ge_real_negative_search_norm_valid) = S ge_signed_half_ge_search_norm_validdecode_real))) /\ ((((ge_imaginary_code_search_norm_validdecode) = 2 * (ge_imaginary_positive_search_norm_valid) /\ (ge_imaginary_negative_search_norm_valid) = 0) \/ exists ge_signed_half_ge_search_norm_validdecode_imaginary. (((ge_imaginary_code_search_norm_validdecode) = 2 * ge_signed_half_ge_search_norm_validdecode_imaginary + 1 /\ (ge_imaginary_positive_search_norm_valid) = 0) /\ (ge_imaginary_negative_search_norm_valid) = S ge_signed_half_ge_search_norm_validdecode_imaginary)))))))
  5. 0005specialize gaussian_norm_input_valid (z)
  6. 0006specialize gaussian_norm_input_valid (N)
  7. 0007apply gaussian_norm_input_valid
  8. 0008exact hnorm
  9. 0009cases hvalid
  10. 0010cases hvalid_witness
  11. 0011cases hvalid_witness_witness
  12. 0012cases hvalid_witness_witness_witness
  13. 0013have hraw : (exists ge_real_square_search_canonical_norm ge_imaginary_square_search_canonical_norm. ((((((x) * (x))) + (((x1) * (x1)))) = ((ge_real_square_search_canonical_norm) + (((((x) * (x1))) + (((x1) * (x))))))) /\ ((((((x2) * (x2))) + (((x3) * (x3)))) = ((ge_imaginary_square_search_canonical_norm) + (((((x2) * (x3))) + (((x3) * (x2))))))) /\ ((N) = ge_real_square_search_canonical_norm + ge_imaginary_square_search_canonical_norm))))
  14. 0014specialize gaussian_norm_for_representation (z)
  15. 0015specialize gaussian_norm_for_representation (x)
  16. 0016specialize gaussian_norm_for_representation (x1)
  17. 0017specialize gaussian_norm_for_representation (x2)
  18. 0018specialize gaussian_norm_for_representation (x3)
  19. 0019specialize gaussian_norm_for_representation (N)
  20. 0020apply gaussian_norm_for_representation
  21. 0021specialize gaussian_decode_representation (z)
  22. 0022specialize gaussian_decode_representation (x)
  23. 0023specialize gaussian_decode_representation (x1)
  24. 0024specialize gaussian_decode_representation (x2)
  25. 0025specialize gaussian_decode_representation (x3)
  26. 0026apply gaussian_decode_representation
  27. 0027exact hvalid_witness_witness_witness_witness
  28. 0028exact hnorm
  29. 0029cases hvalid_witness_witness_witness_witness
  30. 0030cases hvalid_witness_witness_witness_witness_witness
  31. 0031cases hvalid_witness_witness_witness_witness_witness_witness
  32. 0032cases hvalid_witness_witness_witness_witness_witness_witness_right
  33. 0033cases hraw
  34. 0034cases hraw_witness
  35. 0035cases hraw_witness_witness
  36. 0036cases hraw_witness_witness_right
  37. 0037exists (x4)
  38. 0038exists (x5)
  39. 0039split
  40. 0040exact hvalid_witness_witness_witness_witness_witness_witness_left
  41. 0041split
  42. 0042specialize gaussian_search_signed_code_bound (x4)
  43. 0043specialize gaussian_search_signed_code_bound (x)
  44. 0044specialize gaussian_search_signed_code_bound (x1)
  45. 0045specialize gaussian_search_signed_code_bound (x6)
  46. 0046specialize gaussian_search_signed_code_bound (N)
  47. 0047apply gaussian_search_signed_code_bound
  48. 0048exact hvalid_witness_witness_witness_witness_witness_witness_right_left
  49. 0049exact hraw_witness_witness_left
  50. 0050exists x7
  51. 0051rewrite hraw_witness_witness_right_right
  52. 0052apply add_comm
  53. 0053specialize gaussian_search_signed_code_bound (x5)
  54. 0054specialize gaussian_search_signed_code_bound (x2)
  55. 0055specialize gaussian_search_signed_code_bound (x3)
  56. 0056specialize gaussian_search_signed_code_bound (x7)
  57. 0057specialize gaussian_search_signed_code_bound (N)
  58. 0058apply gaussian_search_signed_code_bound
  59. 0059exact hvalid_witness_witness_witness_witness_witness_witness_right_right
  60. 0060exact hraw_witness_witness_right_left
  61. 0061exists x6
  62. 0062symm
  63. 0063exact hraw_witness_witness_right_right