GI0045

gaussian_representation_is_gaussian

A genuinely represented pair always belongs to the canonical signed-coordinate Gaussian carrier.

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) → ZPairValid(z)

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

Definition DAG

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

Actual proof prerequisites

gaussian_representation_decode
Original expanded first-order statement 
forall z a b c d. (exists ge_representation_real_code_valid_representation ge_representation_imaginary_code_valid_representation. (((z) = ((ge_representation_real_code_valid_representation) + (ge_representation_imaginary_code_valid_representation)) * S ((ge_representation_real_code_valid_representation) + (ge_representation_imaginary_code_valid_representation)) + ((ge_representation_imaginary_code_valid_representation) + (ge_representation_imaginary_code_valid_representation))) /\ ((exists ge_balance_positive_valid_representationreal ge_balance_negative_valid_representationreal. (((((ge_representation_real_code_valid_representation) = 2 * (ge_balance_positive_valid_representationreal) /\ (ge_balance_negative_valid_representationreal) = 0) \/ exists ge_signed_half_valid_representationrealdecode. (((ge_representation_real_code_valid_representation) = 2 * ge_signed_half_valid_representationrealdecode + 1 /\ (ge_balance_positive_valid_representationreal) = 0) /\ (ge_balance_negative_valid_representationreal) = S ge_signed_half_valid_representationrealdecode))) /\ ((a) + ge_balance_negative_valid_representationreal = (b) + ge_balance_positive_valid_representationreal))) /\ (exists ge_balance_positive_valid_representationimaginary ge_balance_negative_valid_representationimaginary. (((((ge_representation_imaginary_code_valid_representation) = 2 * (ge_balance_positive_valid_representationimaginary) /\ (ge_balance_negative_valid_representationimaginary) = 0) \/ exists ge_signed_half_valid_representationimaginarydecode. (((ge_representation_imaginary_code_valid_representation) = 2 * ge_signed_half_valid_representationimaginarydecode + 1 /\ (ge_balance_positive_valid_representationimaginary) = 0) /\ (ge_balance_negative_valid_representationimaginary) = S ge_signed_half_valid_representationimaginarydecode))) /\ ((c) + ge_balance_negative_valid_representationimaginary = (d) + ge_balance_positive_valid_representationimaginary)))))) -> (exists ge_real_positive_valid_gaussian ge_real_negative_valid_gaussian ge_imaginary_positive_valid_gaussian ge_imaginary_negative_valid_gaussian. (exists ge_real_code_valid_gaussiandecode ge_imaginary_code_valid_gaussiandecode. (((z) = ((ge_real_code_valid_gaussiandecode) + (ge_imaginary_code_valid_gaussiandecode)) * S ((ge_real_code_valid_gaussiandecode) + (ge_imaginary_code_valid_gaussiandecode)) + ((ge_imaginary_code_valid_gaussiandecode) + (ge_imaginary_code_valid_gaussiandecode))) /\ (((((ge_real_code_valid_gaussiandecode) = 2 * (ge_real_positive_valid_gaussian) /\ (ge_real_negative_valid_gaussian) = 0) \/ exists ge_signed_half_ge_valid_gaussiandecode_real. (((ge_real_code_valid_gaussiandecode) = 2 * ge_signed_half_ge_valid_gaussiandecode_real + 1 /\ (ge_real_positive_valid_gaussian) = 0) /\ (ge_real_negative_valid_gaussian) = S ge_signed_half_ge_valid_gaussiandecode_real))) /\ ((((ge_imaginary_code_valid_gaussiandecode) = 2 * (ge_imaginary_positive_valid_gaussian) /\ (ge_imaginary_negative_valid_gaussian) = 0) \/ exists ge_signed_half_ge_valid_gaussiandecode_imaginary. (((ge_imaginary_code_valid_gaussiandecode) = 2 * ge_signed_half_ge_valid_gaussiandecode_imaginary + 1 /\ (ge_imaginary_positive_valid_gaussian) = 0) /\ (ge_imaginary_negative_valid_gaussian) = S ge_signed_half_ge_valid_gaussiandecode_imaginary)))))))

Complete tactic proof in conservative notation

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

24 script commands · 5 reading checkpoints · 1 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 (1)
gaussian representation decode
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
02Establish hdecodeL7–14

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

  1. L7
    have hdecode : ∃ e. ∃ f. ∃ g. ∃ h. ZPairDecode(z,e,f,g,h) ∧ (a + f = e + b ∧ c + h = g + d)Definitions: ZPairDecode(z,e,f,g,h)Original native command in the exact edition
  2. L8
    specialize gaussian_representation_decode z
  3. L9
    specialize gaussian_representation_decode a
  4. L10
    specialize gaussian_representation_decode b
  5. L11
    specialize gaussian_representation_decode c
  6. L12
    specialize gaussian_representation_decode d
  7. L13
    apply gaussian_representation_decode
  8. L14
    exact hrepresentation
03Separate the logical casesL15–19

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

  1. L15
    cases hdecode
  2. L16
    cases hdecode_witness
  3. L17
    cases hdecode_witness_witness
  4. L18
    cases hdecode_witness_witness_witness
  5. L19
    cases hdecode_witness_witness_witness_witness
04Construct an explicit witnessL20–23

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

  1. L20
    exists x
  2. L21
    exists x1
  3. L22
    exists x2
  4. L23
    exists x3
05Use earlier factsL24–24

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

  1. L24
    exact hdecode_witness_witness_witness_witness_left

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro z
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro hrepresentation
  7. 0007have hdecode : ∃ e. ∃ f. ∃ g. ∃ h. ZPairDecode(z,e,f,g,h) ∧ (a + f = e + b ∧ c + h = g + d)
  8. 0008specialize gaussian_representation_decode z
  9. 0009specialize gaussian_representation_decode a
  10. 0010specialize gaussian_representation_decode b
  11. 0011specialize gaussian_representation_decode c
  12. 0012specialize gaussian_representation_decode d
  13. 0013apply gaussian_representation_decode
  14. 0014exact hrepresentation
  15. 0015cases hdecode
  16. 0016cases hdecode_witness
  17. 0017cases hdecode_witness_witness
  18. 0018cases hdecode_witness_witness_witness
  19. 0019cases hdecode_witness_witness_witness_witness
  20. 0020exists x
  21. 0021exists x1
  22. 0022exists x2
  23. 0023exists x3
  24. 0024exact hdecode_witness_witness_witness_witness_left