GI003E

gaussian_decode_functional

A canonical Gaussian coordinate code has exactly one normalized four-component signed decoding.

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. ∀ e. ∀ f. ∀ g. ∀ h. ZPairDecode(z,a,b,c,d) → ZPairDecode(z,e,f,g,h) → a = e ∧ (b = f ∧ (c = g ∧ d = h))

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

Definition DAG

ZPairDecode(z,ap,an,bp,bn) · 2

Actual proof prerequisites

pair_code_injective · checked external prerequisitesigned_decode_functional · checked external prerequisite
Original expanded first-order statement 
forall z a b c d e f g h. (exists ge_real_code_decode_first ge_imaginary_code_decode_first. (((z) = ((ge_real_code_decode_first) + (ge_imaginary_code_decode_first)) * S ((ge_real_code_decode_first) + (ge_imaginary_code_decode_first)) + ((ge_imaginary_code_decode_first) + (ge_imaginary_code_decode_first))) /\ (((((ge_real_code_decode_first) = 2 * (a) /\ (b) = 0) \/ exists ge_signed_half_ge_decode_first_real. (((ge_real_code_decode_first) = 2 * ge_signed_half_ge_decode_first_real + 1 /\ (a) = 0) /\ (b) = S ge_signed_half_ge_decode_first_real))) /\ ((((ge_imaginary_code_decode_first) = 2 * (c) /\ (d) = 0) \/ exists ge_signed_half_ge_decode_first_imaginary. (((ge_imaginary_code_decode_first) = 2 * ge_signed_half_ge_decode_first_imaginary + 1 /\ (c) = 0) /\ (d) = S ge_signed_half_ge_decode_first_imaginary)))))) -> (exists ge_real_code_decode_second ge_imaginary_code_decode_second. (((z) = ((ge_real_code_decode_second) + (ge_imaginary_code_decode_second)) * S ((ge_real_code_decode_second) + (ge_imaginary_code_decode_second)) + ((ge_imaginary_code_decode_second) + (ge_imaginary_code_decode_second))) /\ (((((ge_real_code_decode_second) = 2 * (e) /\ (f) = 0) \/ exists ge_signed_half_ge_decode_second_real. (((ge_real_code_decode_second) = 2 * ge_signed_half_ge_decode_second_real + 1 /\ (e) = 0) /\ (f) = S ge_signed_half_ge_decode_second_real))) /\ ((((ge_imaginary_code_decode_second) = 2 * (g) /\ (h) = 0) \/ exists ge_signed_half_ge_decode_second_imaginary. (((ge_imaginary_code_decode_second) = 2 * ge_signed_half_ge_decode_second_imaginary + 1 /\ (g) = 0) /\ (h) = S ge_signed_half_ge_decode_second_imaginary)))))) -> ((((a) = (e)) /\ (((b) = (f)) /\ (((c) = (g)) /\ ((d) = (h))))))

Complete tactic proof in conservative notation

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

60 script commands · 15 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.

01Fix variables and assumptionsL1–10

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 e
  7. L7
    intro f
  8. L8
    intro g
  9. L9
    intro h
  10. L10
    intro hfirst
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hsecond
03Separate the logical casesL12–19

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

  1. L12
    cases hfirst
  2. L13
    cases hfirst_witness
  3. L14
    cases hfirst_witness_witness
  4. L15
    cases hfirst_witness_witness_right
  5. L16
    cases hsecond
  6. L17
    cases hsecond_witness
  7. L18
    cases hsecond_witness_witness
  8. L19
    cases hsecond_witness_witness_right
04Establish hcodesL20–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair code injective.

  1. L20
    have hcodes : x = x2 /\ x1 = x3
  2. L21
    specialize pair_code_injective z
  3. L22
    specialize pair_code_injective x
  4. L23
    specialize pair_code_injective x1
  5. L24
    specialize pair_code_injective x2
  6. L25
    specialize pair_code_injective x3
  7. L26
    apply pair_code_injective
  8. L27
    exact hfirst_witness_witness_left
  9. L28
    exact hsecond_witness_witness_left
05Separate the logical casesL29–29

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

  1. L29
    cases hcodes
06Calculate and transport equalitiesL30–33

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

  1. L30
    rewrite hcodes_left at hfirst_witness_witness_right_left
  2. L31
    rewrite hcodes_left at hfirst_witness_witness_right_left
  3. L32
    rewrite hcodes_right at hfirst_witness_witness_right_right
  4. L33
    rewrite hcodes_right at hfirst_witness_witness_right_right
07Establish hrealL34–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed decode functional.

  1. L34
    have hreal : a = e /\ b = f
  2. L35
    specialize signed_decode_functional x2
  3. L36
    specialize signed_decode_functional a
  4. L37
    specialize signed_decode_functional b
  5. L38
    specialize signed_decode_functional e
  6. L39
    specialize signed_decode_functional f
  7. L40
    apply signed_decode_functional
  8. L41
    exact hfirst_witness_witness_right_left
  9. L42
    exact hsecond_witness_witness_right_left
08Separate the logical casesL43–43

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

  1. L43
    cases hreal
09Establish himaginaryL44–52

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed decode functional.

  1. L44
    have himaginary : c = g /\ d = h
  2. L45
    specialize signed_decode_functional x3
  3. L46
    specialize signed_decode_functional c
  4. L47
    specialize signed_decode_functional d
  5. L48
    specialize signed_decode_functional g
  6. L49
    specialize signed_decode_functional h
  7. L50
    apply signed_decode_functional
  8. L51
    exact hfirst_witness_witness_right_right
  9. L52
    exact hsecond_witness_witness_right_right
10Separate the logical casesL53–54

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

  1. L53
    cases himaginary
  2. L54
    split
11Use earlier factsL55–55

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

  1. L55
    exact hreal_left
12Separate the logical casesL56–56

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

  1. L56
    split
13Use earlier factsL57–57

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

  1. L57
    exact hreal_right
14Separate the logical casesL58–58

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

  1. L58
    split
15Use earlier factsL59–60

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

  1. L59
    exact himaginary_left
  2. L60
    exact himaginary_right

Library-wide reading audit

Original defined command ledger · 60 lines
  1. 0001intro z
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro f
  8. 0008intro g
  9. 0009intro h
  10. 0010intro hfirst
  11. 0011intro hsecond
  12. 0012cases hfirst
  13. 0013cases hfirst_witness
  14. 0014cases hfirst_witness_witness
  15. 0015cases hfirst_witness_witness_right
  16. 0016cases hsecond
  17. 0017cases hsecond_witness
  18. 0018cases hsecond_witness_witness
  19. 0019cases hsecond_witness_witness_right
  20. 0020have hcodes : x = x2 /\ x1 = x3
  21. 0021specialize pair_code_injective z
  22. 0022specialize pair_code_injective x
  23. 0023specialize pair_code_injective x1
  24. 0024specialize pair_code_injective x2
  25. 0025specialize pair_code_injective x3
  26. 0026apply pair_code_injective
  27. 0027exact hfirst_witness_witness_left
  28. 0028exact hsecond_witness_witness_left
  29. 0029cases hcodes
  30. 0030rewrite hcodes_left at hfirst_witness_witness_right_left
  31. 0031rewrite hcodes_left at hfirst_witness_witness_right_left
  32. 0032rewrite hcodes_right at hfirst_witness_witness_right_right
  33. 0033rewrite hcodes_right at hfirst_witness_witness_right_right
  34. 0034have hreal : a = e /\ b = f
  35. 0035specialize signed_decode_functional x2
  36. 0036specialize signed_decode_functional a
  37. 0037specialize signed_decode_functional b
  38. 0038specialize signed_decode_functional e
  39. 0039specialize signed_decode_functional f
  40. 0040apply signed_decode_functional
  41. 0041exact hfirst_witness_witness_right_left
  42. 0042exact hsecond_witness_witness_right_left
  43. 0043cases hreal
  44. 0044have himaginary : c = g /\ d = h
  45. 0045specialize signed_decode_functional x3
  46. 0046specialize signed_decode_functional c
  47. 0047specialize signed_decode_functional d
  48. 0048specialize signed_decode_functional g
  49. 0049specialize signed_decode_functional h
  50. 0050apply signed_decode_functional
  51. 0051exact hfirst_witness_witness_right_right
  52. 0052exact hsecond_witness_witness_right_right
  53. 0053cases himaginary
  54. 0054split
  55. 0055exact hreal_left
  56. 0056split
  57. 0057exact hreal_right
  58. 0058split
  59. 0059exact himaginary_left
  60. 0060exact himaginary_right