GF0019

gaussian_unit_has_norm_one

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

An actual inverse multiplies norms to one, forcing the unit norm to equal one.

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. (exists gr_inverse_unit_norm_given. (exists ge_first_rp_unit_norm_givenidentity ge_first_rn_unit_norm_givenidentity ge_first_ip_unit_norm_givenidentity ge_first_in_unit_norm_givenidentity ge_second_rp_unit_norm_givenidentity ge_second_rn_unit_norm_givenidentity ge_second_ip_unit_norm_givenidentity ge_second_in_unit_norm_givenidentity. ((exists ge_representation_real_code_unit_norm_givenidentityfirst ge_representation_imaginary_code_unit_norm_givenidentityfirst. (((z) = ((ge_representation_real_code_unit_norm_givenidentityfirst) + (ge_representation_imaginary_code_unit_norm_givenidentityfirst)) * S ((ge_representation_real_code_unit_norm_givenidentityfirst) + (ge_representation_imaginary_code_unit_norm_givenidentityfirst)) + ((ge_representation_imaginary_code_unit_norm_givenidentityfirst) + (ge_representation_imaginary_code_unit_norm_givenidentityfirst))) /\ ((exists ge_balance_positive_unit_norm_givenidentityfirstreal ge_balance_negative_unit_norm_givenidentityfirstreal. (((((ge_representation_real_code_unit_norm_givenidentityfirst) = 2 * (ge_balance_positive_unit_norm_givenidentityfirstreal) /\ (ge_balance_negative_unit_norm_givenidentityfirstreal) = 0) \/ exists ge_signed_half_unit_norm_givenidentityfirstrealdecode. (((ge_representation_real_code_unit_norm_givenidentityfirst) = 2 * ge_signed_half_unit_norm_givenidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_norm_givenidentityfirstreal) = 0) /\ (ge_balance_negative_unit_norm_givenidentityfirstreal) = S ge_signed_half_unit_norm_givenidentityfirstrealdecode))) /\ ((ge_first_rp_unit_norm_givenidentity) + ge_balance_negative_unit_norm_givenidentityfirstreal = (ge_first_rn_unit_norm_givenidentity) + ge_balance_positive_unit_norm_givenidentityfirstreal))) /\ (exists ge_balance_positive_unit_norm_givenidentityfirstimaginary ge_balance_negative_unit_norm_givenidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_norm_givenidentityfirst) = 2 * (ge_balance_positive_unit_norm_givenidentityfirstimaginary) /\ (ge_balance_negative_unit_norm_givenidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_norm_givenidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_norm_givenidentityfirst) = 2 * ge_signed_half_unit_norm_givenidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_norm_givenidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_norm_givenidentityfirstimaginary) = S ge_signed_half_unit_norm_givenidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_norm_givenidentity) + ge_balance_negative_unit_norm_givenidentityfirstimaginary = (ge_first_in_unit_norm_givenidentity) + ge_balance_positive_unit_norm_givenidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_norm_givenidentitysecond ge_representation_imaginary_code_unit_norm_givenidentitysecond. (((gr_inverse_unit_norm_given) = ((ge_representation_real_code_unit_norm_givenidentitysecond) + (ge_representation_imaginary_code_unit_norm_givenidentitysecond)) * S ((ge_representation_real_code_unit_norm_givenidentitysecond) + (ge_representation_imaginary_code_unit_norm_givenidentitysecond)) + ((ge_representation_imaginary_code_unit_norm_givenidentitysecond) + (ge_representation_imaginary_code_unit_norm_givenidentitysecond))) /\ ((exists ge_balance_positive_unit_norm_givenidentitysecondreal ge_balance_negative_unit_norm_givenidentitysecondreal. (((((ge_representation_real_code_unit_norm_givenidentitysecond) = 2 * (ge_balance_positive_unit_norm_givenidentitysecondreal) /\ (ge_balance_negative_unit_norm_givenidentitysecondreal) = 0) \/ exists ge_signed_half_unit_norm_givenidentitysecondrealdecode. (((ge_representation_real_code_unit_norm_givenidentitysecond) = 2 * ge_signed_half_unit_norm_givenidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_norm_givenidentitysecondreal) = 0) /\ (ge_balance_negative_unit_norm_givenidentitysecondreal) = S ge_signed_half_unit_norm_givenidentitysecondrealdecode))) /\ ((ge_second_rp_unit_norm_givenidentity) + ge_balance_negative_unit_norm_givenidentitysecondreal = (ge_second_rn_unit_norm_givenidentity) + ge_balance_positive_unit_norm_givenidentitysecondreal))) /\ (exists ge_balance_positive_unit_norm_givenidentitysecondimaginary ge_balance_negative_unit_norm_givenidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_norm_givenidentitysecond) = 2 * (ge_balance_positive_unit_norm_givenidentitysecondimaginary) /\ (ge_balance_negative_unit_norm_givenidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_norm_givenidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_norm_givenidentitysecond) = 2 * ge_signed_half_unit_norm_givenidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_norm_givenidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_norm_givenidentitysecondimaginary) = S ge_signed_half_unit_norm_givenidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_norm_givenidentity) + ge_balance_negative_unit_norm_givenidentitysecondimaginary = (ge_second_in_unit_norm_givenidentity) + ge_balance_positive_unit_norm_givenidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_norm_givenidentityoutput ge_representation_imaginary_code_unit_norm_givenidentityoutput. (((6) = ((ge_representation_real_code_unit_norm_givenidentityoutput) + (ge_representation_imaginary_code_unit_norm_givenidentityoutput)) * S ((ge_representation_real_code_unit_norm_givenidentityoutput) + (ge_representation_imaginary_code_unit_norm_givenidentityoutput)) + ((ge_representation_imaginary_code_unit_norm_givenidentityoutput) + (ge_representation_imaginary_code_unit_norm_givenidentityoutput))) /\ ((exists ge_balance_positive_unit_norm_givenidentityoutputreal ge_balance_negative_unit_norm_givenidentityoutputreal. (((((ge_representation_real_code_unit_norm_givenidentityoutput) = 2 * (ge_balance_positive_unit_norm_givenidentityoutputreal) /\ (ge_balance_negative_unit_norm_givenidentityoutputreal) = 0) \/ exists ge_signed_half_unit_norm_givenidentityoutputrealdecode. (((ge_representation_real_code_unit_norm_givenidentityoutput) = 2 * ge_signed_half_unit_norm_givenidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_norm_givenidentityoutputreal) = 0) /\ (ge_balance_negative_unit_norm_givenidentityoutputreal) = S ge_signed_half_unit_norm_givenidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_norm_givenidentity) * (ge_second_rp_unit_norm_givenidentity))) + (((ge_first_rn_unit_norm_givenidentity) * (ge_second_rn_unit_norm_givenidentity))))) + (((((ge_first_ip_unit_norm_givenidentity) * (ge_second_in_unit_norm_givenidentity))) + (((ge_first_in_unit_norm_givenidentity) * (ge_second_ip_unit_norm_givenidentity))))))) + ge_balance_negative_unit_norm_givenidentityoutputreal = (((((((ge_first_rp_unit_norm_givenidentity) * (ge_second_rn_unit_norm_givenidentity))) + (((ge_first_rn_unit_norm_givenidentity) * (ge_second_rp_unit_norm_givenidentity))))) + (((((ge_first_ip_unit_norm_givenidentity) * (ge_second_ip_unit_norm_givenidentity))) + (((ge_first_in_unit_norm_givenidentity) * (ge_second_in_unit_norm_givenidentity))))))) + ge_balance_positive_unit_norm_givenidentityoutputreal))) /\ (exists ge_balance_positive_unit_norm_givenidentityoutputimaginary ge_balance_negative_unit_norm_givenidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_norm_givenidentityoutput) = 2 * (ge_balance_positive_unit_norm_givenidentityoutputimaginary) /\ (ge_balance_negative_unit_norm_givenidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_norm_givenidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_norm_givenidentityoutput) = 2 * ge_signed_half_unit_norm_givenidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_norm_givenidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_norm_givenidentityoutputimaginary) = S ge_signed_half_unit_norm_givenidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_norm_givenidentity) * (ge_second_ip_unit_norm_givenidentity))) + (((ge_first_rn_unit_norm_givenidentity) * (ge_second_in_unit_norm_givenidentity))))) + (((((ge_first_ip_unit_norm_givenidentity) * (ge_second_rp_unit_norm_givenidentity))) + (((ge_first_in_unit_norm_givenidentity) * (ge_second_rn_unit_norm_givenidentity))))))) + ge_balance_negative_unit_norm_givenidentityoutputimaginary = (((((((ge_first_rp_unit_norm_givenidentity) * (ge_second_in_unit_norm_givenidentity))) + (((ge_first_rn_unit_norm_givenidentity) * (ge_second_ip_unit_norm_givenidentity))))) + (((((ge_first_ip_unit_norm_givenidentity) * (ge_second_rn_unit_norm_givenidentity))) + (((ge_first_in_unit_norm_givenidentity) * (ge_second_rp_unit_norm_givenidentity))))))) + ge_balance_positive_unit_norm_givenidentityoutputimaginary)))))))))) -> (exists ge_norm_rp_unit_norm_value ge_norm_rn_unit_norm_value ge_norm_ip_unit_norm_value ge_norm_in_unit_norm_value. ((exists ge_representation_real_code_unit_norm_valuerepresentation ge_representation_imaginary_code_unit_norm_valuerepresentation. (((z) = ((ge_representation_real_code_unit_norm_valuerepresentation) + (ge_representation_imaginary_code_unit_norm_valuerepresentation)) * S ((ge_representation_real_code_unit_norm_valuerepresentation) + (ge_representation_imaginary_code_unit_norm_valuerepresentation)) + ((ge_representation_imaginary_code_unit_norm_valuerepresentation) + (ge_representation_imaginary_code_unit_norm_valuerepresentation))) /\ ((exists ge_balance_positive_unit_norm_valuerepresentationreal ge_balance_negative_unit_norm_valuerepresentationreal. (((((ge_representation_real_code_unit_norm_valuerepresentation) = 2 * (ge_balance_positive_unit_norm_valuerepresentationreal) /\ (ge_balance_negative_unit_norm_valuerepresentationreal) = 0) \/ exists ge_signed_half_unit_norm_valuerepresentationrealdecode. (((ge_representation_real_code_unit_norm_valuerepresentation) = 2 * ge_signed_half_unit_norm_valuerepresentationrealdecode + 1 /\ (ge_balance_positive_unit_norm_valuerepresentationreal) = 0) /\ (ge_balance_negative_unit_norm_valuerepresentationreal) = S ge_signed_half_unit_norm_valuerepresentationrealdecode))) /\ ((ge_norm_rp_unit_norm_value) + ge_balance_negative_unit_norm_valuerepresentationreal = (ge_norm_rn_unit_norm_value) + ge_balance_positive_unit_norm_valuerepresentationreal))) /\ (exists ge_balance_positive_unit_norm_valuerepresentationimaginary ge_balance_negative_unit_norm_valuerepresentationimaginary. (((((ge_representation_imaginary_code_unit_norm_valuerepresentation) = 2 * (ge_balance_positive_unit_norm_valuerepresentationimaginary) /\ (ge_balance_negative_unit_norm_valuerepresentationimaginary) = 0) \/ exists ge_signed_half_unit_norm_valuerepresentationimaginarydecode. (((ge_representation_imaginary_code_unit_norm_valuerepresentation) = 2 * ge_signed_half_unit_norm_valuerepresentationimaginarydecode + 1 /\ (ge_balance_positive_unit_norm_valuerepresentationimaginary) = 0) /\ (ge_balance_negative_unit_norm_valuerepresentationimaginary) = S ge_signed_half_unit_norm_valuerepresentationimaginarydecode))) /\ ((ge_norm_ip_unit_norm_value) + ge_balance_negative_unit_norm_valuerepresentationimaginary = (ge_norm_in_unit_norm_value) + ge_balance_positive_unit_norm_valuerepresentationimaginary)))))) /\ (exists ge_real_square_unit_norm_valuesquare ge_imaginary_square_unit_norm_valuesquare. ((((((ge_norm_rp_unit_norm_value) * (ge_norm_rp_unit_norm_value))) + (((ge_norm_rn_unit_norm_value) * (ge_norm_rn_unit_norm_value)))) = ((ge_real_square_unit_norm_valuesquare) + (((((ge_norm_rp_unit_norm_value) * (ge_norm_rn_unit_norm_value))) + (((ge_norm_rn_unit_norm_value) * (ge_norm_rp_unit_norm_value))))))) /\ ((((((ge_norm_ip_unit_norm_value) * (ge_norm_ip_unit_norm_value))) + (((ge_norm_in_unit_norm_value) * (ge_norm_in_unit_norm_value)))) = ((ge_imaginary_square_unit_norm_valuesquare) + (((((ge_norm_ip_unit_norm_value) * (ge_norm_in_unit_norm_value))) + (((ge_norm_in_unit_norm_value) * (ge_norm_ip_unit_norm_value))))))) /\ ((1) = ge_real_square_unit_norm_valuesquare + ge_imaginary_square_unit_norm_valuesquare))))))

Constructive proof overview

Generated structural guide

An actual inverse multiplies norms to one, forcing the unit norm to equal one.

The unchanged tactic script uses 8 declared prerequisites and contains 48 exact native proof lines.

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

Proof neighborhood

Direct dependencies

gaussian_norm_exists Alpha theorem; checked-use authorized GF0007 gaussian_multiply_input_left_valid GF0008 gaussian_multiply_input_right_valid gaussian_norm_multiply Alpha theorem; checked-use authorized gaussian_norm_functional Alpha theorem; checked-use authorized GF0010 gaussian_one_norm divisor_one Stable theorem; checked-use authorized GF0015 gaussian_norm_value_transport

Direct dependents

GF001B gaussian_unit_iff_norm_one GF001C gaussian_unit_decidable GF001D gaussian_unit_nonzero GF003F gaussian_unit_product GF0059 gaussian_associate_norm GF007D gaussian_proper_norm_divisor_split

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

48 script commands · 12 reading checkpoints · 4 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 (4)
gaussian multiply input left validgaussian multiply input right validgaussian one normgaussian norm value transport

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–2

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

  1. L1
    intro z
  2. L2
    intro hu
02Separate the logical casesL3–3

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

  1. L3
    cases hu
03Establish hNL4–11

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

  1. L4
    have hN : ∃ N. GNorm(z,N)Definitions: GNorm
  2. L5
    specialize gaussian_norm_exists (z)
  3. L6
    apply gaussian_norm_exists
  4. L7
    specialize gaussian_multiply_input_left_valid (z)
  5. L8
    specialize gaussian_multiply_input_left_valid (x)
  6. L9
    specialize gaussian_multiply_input_left_valid (6)
  7. L10
    apply gaussian_multiply_input_left_valid
  8. L11
    exact hu_witness
04Separate the logical casesL12–12

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

  1. L12
    cases hN
05Establish hML13–20

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

  1. L13
    have hM : ∃ M. GNorm(x,M)Definitions: GNorm
  2. L14
    specialize gaussian_norm_exists (x)
  3. L15
    apply gaussian_norm_exists
  4. L16
    specialize gaussian_multiply_input_right_valid (z)
  5. L17
    specialize gaussian_multiply_input_right_valid (x)
  6. L18
    specialize gaussian_multiply_input_right_valid (6)
  7. L19
    apply gaussian_multiply_input_right_valid
  8. L20
    exact hu_witness
06Separate the logical casesL21–21

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

  1. L21
    cases hM
07Establish hproductL22–31

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

  1. L22
    have hproduct : x1*x2=1
  2. L23
    specialize gaussian_norm_functional (6)
  3. L24
    specialize gaussian_norm_functional (x1*x2)
  4. L25
    specialize gaussian_norm_functional (1)
  5. L26
    apply gaussian_norm_functional
  6. L27
    specialize gaussian_norm_multiply (z)
  7. L28
    specialize gaussian_norm_multiply (x)
  8. L29
    specialize gaussian_norm_multiply (6)
  9. L30
    specialize gaussian_norm_multiply (x1)
  10. L31
    specialize gaussian_norm_multiply (x2)
08Use earlier factsL32–36

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

  1. L32
    apply gaussian_norm_multiply
  2. L33
    exact hN_witness
  3. L34
    exact hM_witness
  4. L35
    exact hu_witness
  5. L36
    exact gaussian_one_norm
09Establish honeL37–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor one.

  1. L37
    have hone : x1=1
  2. L38
    specialize divisor_one (x1)
  3. L39
    apply divisor_one
10Construct an explicit witnessL40–40

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

  1. L40
    exists (x2)
11Calculate and transport equalitiesL41–41

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

  1. L41
    symm
12Use earlier factsL42–48

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

  1. L42
    exact hproduct
  2. L43
    specialize gaussian_norm_value_transport (z)
  3. L44
    specialize gaussian_norm_value_transport (x1)
  4. L45
    specialize gaussian_norm_value_transport (1)
  5. L46
    apply gaussian_norm_value_transport
  6. L47
    exact hone
  7. L48
    exact hN_witness

Library-wide reading audit

Original exact command ledger · 48 lines
  1. 0001intro z
  2. 0002intro hu
  3. 0003cases hu
  4. 0004have hN : exists N. (exists ge_norm_rp_unit_first_norm ge_norm_rn_unit_first_norm ge_norm_ip_unit_first_norm ge_norm_in_unit_first_norm. ((exists ge_representation_real_code_unit_first_normrepresentation ge_representation_imaginary_code_unit_first_normrepresentation. (((z) = ((ge_representation_real_code_unit_first_normrepresentation) + (ge_representation_imaginary_code_unit_first_normrepresentation)) * S ((ge_representation_real_code_unit_first_normrepresentation) + (ge_representation_imaginary_code_unit_first_normrepresentation)) + ((ge_representation_imaginary_code_unit_first_normrepresentation) + (ge_representation_imaginary_code_unit_first_normrepresentation))) /\ ((exists ge_balance_positive_unit_first_normrepresentationreal ge_balance_negative_unit_first_normrepresentationreal. (((((ge_representation_real_code_unit_first_normrepresentation) = 2 * (ge_balance_positive_unit_first_normrepresentationreal) /\ (ge_balance_negative_unit_first_normrepresentationreal) = 0) \/ exists ge_signed_half_unit_first_normrepresentationrealdecode. (((ge_representation_real_code_unit_first_normrepresentation) = 2 * ge_signed_half_unit_first_normrepresentationrealdecode + 1 /\ (ge_balance_positive_unit_first_normrepresentationreal) = 0) /\ (ge_balance_negative_unit_first_normrepresentationreal) = S ge_signed_half_unit_first_normrepresentationrealdecode))) /\ ((ge_norm_rp_unit_first_norm) + ge_balance_negative_unit_first_normrepresentationreal = (ge_norm_rn_unit_first_norm) + ge_balance_positive_unit_first_normrepresentationreal))) /\ (exists ge_balance_positive_unit_first_normrepresentationimaginary ge_balance_negative_unit_first_normrepresentationimaginary. (((((ge_representation_imaginary_code_unit_first_normrepresentation) = 2 * (ge_balance_positive_unit_first_normrepresentationimaginary) /\ (ge_balance_negative_unit_first_normrepresentationimaginary) = 0) \/ exists ge_signed_half_unit_first_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_unit_first_normrepresentation) = 2 * ge_signed_half_unit_first_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_unit_first_normrepresentationimaginary) = 0) /\ (ge_balance_negative_unit_first_normrepresentationimaginary) = S ge_signed_half_unit_first_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_unit_first_norm) + ge_balance_negative_unit_first_normrepresentationimaginary = (ge_norm_in_unit_first_norm) + ge_balance_positive_unit_first_normrepresentationimaginary)))))) /\ (exists ge_real_square_unit_first_normsquare ge_imaginary_square_unit_first_normsquare. ((((((ge_norm_rp_unit_first_norm) * (ge_norm_rp_unit_first_norm))) + (((ge_norm_rn_unit_first_norm) * (ge_norm_rn_unit_first_norm)))) = ((ge_real_square_unit_first_normsquare) + (((((ge_norm_rp_unit_first_norm) * (ge_norm_rn_unit_first_norm))) + (((ge_norm_rn_unit_first_norm) * (ge_norm_rp_unit_first_norm))))))) /\ ((((((ge_norm_ip_unit_first_norm) * (ge_norm_ip_unit_first_norm))) + (((ge_norm_in_unit_first_norm) * (ge_norm_in_unit_first_norm)))) = ((ge_imaginary_square_unit_first_normsquare) + (((((ge_norm_ip_unit_first_norm) * (ge_norm_in_unit_first_norm))) + (((ge_norm_in_unit_first_norm) * (ge_norm_ip_unit_first_norm))))))) /\ ((N) = ge_real_square_unit_first_normsquare + ge_imaginary_square_unit_first_normsquare))))))
  5. 0005specialize gaussian_norm_exists (z)
  6. 0006apply gaussian_norm_exists
  7. 0007specialize gaussian_multiply_input_left_valid (z)
  8. 0008specialize gaussian_multiply_input_left_valid (x)
  9. 0009specialize gaussian_multiply_input_left_valid (6)
  10. 0010apply gaussian_multiply_input_left_valid
  11. 0011exact hu_witness
  12. 0012cases hN
  13. 0013have hM : exists M. (exists ge_norm_rp_unit_inverse_norm ge_norm_rn_unit_inverse_norm ge_norm_ip_unit_inverse_norm ge_norm_in_unit_inverse_norm. ((exists ge_representation_real_code_unit_inverse_normrepresentation ge_representation_imaginary_code_unit_inverse_normrepresentation. (((x) = ((ge_representation_real_code_unit_inverse_normrepresentation) + (ge_representation_imaginary_code_unit_inverse_normrepresentation)) * S ((ge_representation_real_code_unit_inverse_normrepresentation) + (ge_representation_imaginary_code_unit_inverse_normrepresentation)) + ((ge_representation_imaginary_code_unit_inverse_normrepresentation) + (ge_representation_imaginary_code_unit_inverse_normrepresentation))) /\ ((exists ge_balance_positive_unit_inverse_normrepresentationreal ge_balance_negative_unit_inverse_normrepresentationreal. (((((ge_representation_real_code_unit_inverse_normrepresentation) = 2 * (ge_balance_positive_unit_inverse_normrepresentationreal) /\ (ge_balance_negative_unit_inverse_normrepresentationreal) = 0) \/ exists ge_signed_half_unit_inverse_normrepresentationrealdecode. (((ge_representation_real_code_unit_inverse_normrepresentation) = 2 * ge_signed_half_unit_inverse_normrepresentationrealdecode + 1 /\ (ge_balance_positive_unit_inverse_normrepresentationreal) = 0) /\ (ge_balance_negative_unit_inverse_normrepresentationreal) = S ge_signed_half_unit_inverse_normrepresentationrealdecode))) /\ ((ge_norm_rp_unit_inverse_norm) + ge_balance_negative_unit_inverse_normrepresentationreal = (ge_norm_rn_unit_inverse_norm) + ge_balance_positive_unit_inverse_normrepresentationreal))) /\ (exists ge_balance_positive_unit_inverse_normrepresentationimaginary ge_balance_negative_unit_inverse_normrepresentationimaginary. (((((ge_representation_imaginary_code_unit_inverse_normrepresentation) = 2 * (ge_balance_positive_unit_inverse_normrepresentationimaginary) /\ (ge_balance_negative_unit_inverse_normrepresentationimaginary) = 0) \/ exists ge_signed_half_unit_inverse_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_unit_inverse_normrepresentation) = 2 * ge_signed_half_unit_inverse_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_unit_inverse_normrepresentationimaginary) = 0) /\ (ge_balance_negative_unit_inverse_normrepresentationimaginary) = S ge_signed_half_unit_inverse_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_unit_inverse_norm) + ge_balance_negative_unit_inverse_normrepresentationimaginary = (ge_norm_in_unit_inverse_norm) + ge_balance_positive_unit_inverse_normrepresentationimaginary)))))) /\ (exists ge_real_square_unit_inverse_normsquare ge_imaginary_square_unit_inverse_normsquare. ((((((ge_norm_rp_unit_inverse_norm) * (ge_norm_rp_unit_inverse_norm))) + (((ge_norm_rn_unit_inverse_norm) * (ge_norm_rn_unit_inverse_norm)))) = ((ge_real_square_unit_inverse_normsquare) + (((((ge_norm_rp_unit_inverse_norm) * (ge_norm_rn_unit_inverse_norm))) + (((ge_norm_rn_unit_inverse_norm) * (ge_norm_rp_unit_inverse_norm))))))) /\ ((((((ge_norm_ip_unit_inverse_norm) * (ge_norm_ip_unit_inverse_norm))) + (((ge_norm_in_unit_inverse_norm) * (ge_norm_in_unit_inverse_norm)))) = ((ge_imaginary_square_unit_inverse_normsquare) + (((((ge_norm_ip_unit_inverse_norm) * (ge_norm_in_unit_inverse_norm))) + (((ge_norm_in_unit_inverse_norm) * (ge_norm_ip_unit_inverse_norm))))))) /\ ((M) = ge_real_square_unit_inverse_normsquare + ge_imaginary_square_unit_inverse_normsquare))))))
  14. 0014specialize gaussian_norm_exists (x)
  15. 0015apply gaussian_norm_exists
  16. 0016specialize gaussian_multiply_input_right_valid (z)
  17. 0017specialize gaussian_multiply_input_right_valid (x)
  18. 0018specialize gaussian_multiply_input_right_valid (6)
  19. 0019apply gaussian_multiply_input_right_valid
  20. 0020exact hu_witness
  21. 0021cases hM
  22. 0022have hproduct : x1*x2=1
  23. 0023specialize gaussian_norm_functional (6)
  24. 0024specialize gaussian_norm_functional (x1*x2)
  25. 0025specialize gaussian_norm_functional (1)
  26. 0026apply gaussian_norm_functional
  27. 0027specialize gaussian_norm_multiply (z)
  28. 0028specialize gaussian_norm_multiply (x)
  29. 0029specialize gaussian_norm_multiply (6)
  30. 0030specialize gaussian_norm_multiply (x1)
  31. 0031specialize gaussian_norm_multiply (x2)
  32. 0032apply gaussian_norm_multiply
  33. 0033exact hN_witness
  34. 0034exact hM_witness
  35. 0035exact hu_witness
  36. 0036exact gaussian_one_norm
  37. 0037have hone : x1=1
  38. 0038specialize divisor_one (x1)
  39. 0039apply divisor_one
  40. 0040exists (x2)
  41. 0041symm
  42. 0042exact hproduct
  43. 0043specialize gaussian_norm_value_transport (z)
  44. 0044specialize gaussian_norm_value_transport (x1)
  45. 0045specialize gaussian_norm_value_transport (1)
  46. 0046apply gaussian_norm_value_transport
  47. 0047exact hone
  48. 0048exact hN_witness