GI0043

gaussian_representation_decode

Every possibly overlapping signed representation yields actual unique normalized decoder coordinates of the same canonical code.

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

∀ z. ∀ a. ∀ b. ∀ c. ∀ d. ZPairRep(z,a,b,c,d) → ∃ x. ∃ y. ∃ n. ∃ m. ZPairDecode(z,x,y,n,m) ∧ (a + y = x + b ∧ c + m = n + d)

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

Definition DAG

ZPairDecode(z,ap,an,bp,bn) · 1ZPairRep(z,ap,an,bp,bn) · 1

Actual proof prerequisites

add_comm · checked external prerequisite
Original expanded first-order statement 
forall z a b c d. (exists ge_representation_real_code_normalization_source ge_representation_imaginary_code_normalization_source. (((z) = ((ge_representation_real_code_normalization_source) + (ge_representation_imaginary_code_normalization_source)) * S ((ge_representation_real_code_normalization_source) + (ge_representation_imaginary_code_normalization_source)) + ((ge_representation_imaginary_code_normalization_source) + (ge_representation_imaginary_code_normalization_source))) /\ ((exists ge_balance_positive_normalization_sourcereal ge_balance_negative_normalization_sourcereal. (((((ge_representation_real_code_normalization_source) = 2 * (ge_balance_positive_normalization_sourcereal) /\ (ge_balance_negative_normalization_sourcereal) = 0) \/ exists ge_signed_half_normalization_sourcerealdecode. (((ge_representation_real_code_normalization_source) = 2 * ge_signed_half_normalization_sourcerealdecode + 1 /\ (ge_balance_positive_normalization_sourcereal) = 0) /\ (ge_balance_negative_normalization_sourcereal) = S ge_signed_half_normalization_sourcerealdecode))) /\ ((a) + ge_balance_negative_normalization_sourcereal = (b) + ge_balance_positive_normalization_sourcereal))) /\ (exists ge_balance_positive_normalization_sourceimaginary ge_balance_negative_normalization_sourceimaginary. (((((ge_representation_imaginary_code_normalization_source) = 2 * (ge_balance_positive_normalization_sourceimaginary) /\ (ge_balance_negative_normalization_sourceimaginary) = 0) \/ exists ge_signed_half_normalization_sourceimaginarydecode. (((ge_representation_imaginary_code_normalization_source) = 2 * ge_signed_half_normalization_sourceimaginarydecode + 1 /\ (ge_balance_positive_normalization_sourceimaginary) = 0) /\ (ge_balance_negative_normalization_sourceimaginary) = S ge_signed_half_normalization_sourceimaginarydecode))) /\ ((c) + ge_balance_negative_normalization_sourceimaginary = (d) + ge_balance_positive_normalization_sourceimaginary)))))) -> exists e f g h. (((exists ge_real_code_normalization_decode ge_imaginary_code_normalization_decode. (((z) = ((ge_real_code_normalization_decode) + (ge_imaginary_code_normalization_decode)) * S ((ge_real_code_normalization_decode) + (ge_imaginary_code_normalization_decode)) + ((ge_imaginary_code_normalization_decode) + (ge_imaginary_code_normalization_decode))) /\ (((((ge_real_code_normalization_decode) = 2 * (e) /\ (f) = 0) \/ exists ge_signed_half_ge_normalization_decode_real. (((ge_real_code_normalization_decode) = 2 * ge_signed_half_ge_normalization_decode_real + 1 /\ (e) = 0) /\ (f) = S ge_signed_half_ge_normalization_decode_real))) /\ ((((ge_imaginary_code_normalization_decode) = 2 * (g) /\ (h) = 0) \/ exists ge_signed_half_ge_normalization_decode_imaginary. (((ge_imaginary_code_normalization_decode) = 2 * ge_signed_half_ge_normalization_decode_imaginary + 1 /\ (g) = 0) /\ (h) = S ge_signed_half_ge_normalization_decode_imaginary)))))) /\ (((((a) + (f)) = ((e) + (b))) /\ (((c) + (h)) = ((g) + (d)))))))

Complete tactic proof in conservative notation

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

35 script commands · 14 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–6

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

  1. L1
    intro z
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro hrepresentation
02Separate the logical casesL7–16

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

  1. L7
    cases hrepresentation
  2. L8
    cases hrepresentation_witness
  3. L9
    cases hrepresentation_witness_witness
  4. L10
    cases hrepresentation_witness_witness_right
  5. L11
    cases hrepresentation_witness_witness_right_left
  6. L12
    cases hrepresentation_witness_witness_right_left_witness
  7. L13
    cases hrepresentation_witness_witness_right_left_witness_witness
  8. L14
    cases hrepresentation_witness_witness_right_right
  9. L15
    cases hrepresentation_witness_witness_right_right_witness
  10. L16
    cases hrepresentation_witness_witness_right_right_witness_witness
03Construct an explicit witnessL17–20

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

  1. L17
    exists x2
  2. L18
    exists x3
  3. L19
    exists x4
  4. L20
    exists x5
04Separate the logical casesL21–21

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

  1. L21
    split
05Construct an explicit witnessL22–23

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

  1. L22
    exists x
  2. L23
    exists x1
06Separate the logical casesL24–24

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

  1. L24
    split
07Use earlier factsL25–25

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

  1. L25
    exact hrepresentation_witness_witness_left
08Separate the logical casesL26–26

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

  1. L26
    split
09Use earlier factsL27–28

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

  1. L27
    exact hrepresentation_witness_witness_right_left_witness_witness_left
  2. L28
    exact hrepresentation_witness_witness_right_right_witness_witness_left
10Separate the logical casesL29–29

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

  1. L29
    split
11Calculate and transport equalitiesL30–30

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

  1. L30
    trans b + x2
12Use earlier factsL31–32

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

  1. L31
    exact hrepresentation_witness_witness_right_left_witness_witness_right
  2. L32
    apply add_comm
13Calculate and transport equalitiesL33–33

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

  1. L33
    trans d + x4
14Use earlier factsL34–35

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

  1. L34
    exact hrepresentation_witness_witness_right_right_witness_witness_right
  2. L35
    apply add_comm

Library-wide reading audit

Original defined command ledger · 35 lines
  1. 0001intro z
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro hrepresentation
  7. 0007cases hrepresentation
  8. 0008cases hrepresentation_witness
  9. 0009cases hrepresentation_witness_witness
  10. 0010cases hrepresentation_witness_witness_right
  11. 0011cases hrepresentation_witness_witness_right_left
  12. 0012cases hrepresentation_witness_witness_right_left_witness
  13. 0013cases hrepresentation_witness_witness_right_left_witness_witness
  14. 0014cases hrepresentation_witness_witness_right_right
  15. 0015cases hrepresentation_witness_witness_right_right_witness
  16. 0016cases hrepresentation_witness_witness_right_right_witness_witness
  17. 0017exists x2
  18. 0018exists x3
  19. 0019exists x4
  20. 0020exists x5
  21. 0021split
  22. 0022exists x
  23. 0023exists x1
  24. 0024split
  25. 0025exact hrepresentation_witness_witness_left
  26. 0026split
  27. 0027exact hrepresentation_witness_witness_right_left_witness_witness_left
  28. 0028exact hrepresentation_witness_witness_right_right_witness_witness_left
  29. 0029split
  30. 0030trans b + x2
  31. 0031exact hrepresentation_witness_witness_right_left_witness_witness_right
  32. 0032apply add_comm
  33. 0033trans d + x4
  34. 0034exact hrepresentation_witness_witness_right_right_witness_witness_right
  35. 0035apply add_comm