GF0070

gaussian_norm_bounded_coordinates

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

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

∀ z. ∀ N. GNorm(z,N) → GNormBoundedCoordinates(z,N)

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

Definition DAG

GaussianSignedNorm(ap,an,bp,bn,N) · 1ZPairValid(z) · 1GNorm(z,n) · 1GNormBoundedCoordinates(z,N) · 1

Actual proof prerequisites

gaussian_norm_input_validgaussian_decode_representation · checked external prerequisitegaussian_norm_for_representation · checked external prerequisitegaussian_search_signed_code_boundadd_comm · checked external prerequisite
Original expanded first-order 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))))))

Complete tactic proof in conservative notation

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

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.

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 (2)
gaussian norm input validgaussian search signed code bound
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(z)Original native command in the exact edition
  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 : GaussianSignedNorm(x,x1,x2,x3,N)Definitions: GaussianSignedNorm(x,x1,x2,x3,N)Original native command in the exact edition
  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 defined command ledger · 63 lines
  1. 0001intro z
  2. 0002intro N
  3. 0003intro hnorm
  4. 0004have hvalid : ZPairValid(z)
  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 : GaussianSignedNorm(x,x1,x2,x3,N)
  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