GI0045

gaussian_representation_is_gaussian

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

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

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 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)))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 1 declared prerequisite and contains 24 exact native proof lines.

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

Proof neighborhood

Direct dependencies

GI0043 gaussian_representation_decode

Direct dependents

GI005D gaussian_euclidean_division_exists

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

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.

Named ingredients (1)
gaussian representation decode

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–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
  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 exact 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 : exists e f g h. (((exists ge_real_code_valid_normalized_decode ge_imaginary_code_valid_normalized_decode. (((z) = ((ge_real_code_valid_normalized_decode) + (ge_imaginary_code_valid_normalized_decode)) * S ((ge_real_code_valid_normalized_decode) + (ge_imaginary_code_valid_normalized_decode)) + ((ge_imaginary_code_valid_normalized_decode) + (ge_imaginary_code_valid_normalized_decode))) /\ (((((ge_real_code_valid_normalized_decode) = 2 * (e) /\ (f) = 0) \/ exists ge_signed_half_ge_valid_normalized_decode_real. (((ge_real_code_valid_normalized_decode) = 2 * ge_signed_half_ge_valid_normalized_decode_real + 1 /\ (e) = 0) /\ (f) = S ge_signed_half_ge_valid_normalized_decode_real))) /\ ((((ge_imaginary_code_valid_normalized_decode) = 2 * (g) /\ (h) = 0) \/ exists ge_signed_half_ge_valid_normalized_decode_imaginary. (((ge_imaginary_code_valid_normalized_decode) = 2 * ge_signed_half_ge_valid_normalized_decode_imaginary + 1 /\ (g) = 0) /\ (h) = S ge_signed_half_ge_valid_normalized_decode_imaginary)))))) /\ (((((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