GF008E

gaussian_product_result_valid

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

Every actual finite Gaussian product has a valid carrier code, including the empty product.

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 l b c P. (exists gr_product_trace_product_result_valid gr_product_scale_product_result_valid. ((((exists ff_h_gprod_product_result_validstart. ff_h_gprod_product_result_validstart + S (6) = S ((S (0)) * gr_product_scale_product_result_valid)) /\ exists ff_q_gprod_product_result_validstart. gr_product_trace_product_result_valid = ff_q_gprod_product_result_validstart * S ((S (0)) * gr_product_scale_product_result_valid) + (6))) /\ ((((exists ff_h_gprod_product_result_validend. ff_h_gprod_product_result_validend + S (P) = S ((S (l)) * gr_product_scale_product_result_valid)) /\ exists ff_q_gprod_product_result_validend. gr_product_trace_product_result_valid = ff_q_gprod_product_result_validend * S ((S (l)) * gr_product_scale_product_result_valid) + (P))) /\ (forall gr_product_index_product_result_validsteps. (exists ge_gap_product_result_validstepsindex_bound. ge_gap_product_result_validstepsindex_bound + S (gr_product_index_product_result_validsteps) = (l)) -> exists gr_product_factor_product_result_validsteps gr_product_before_product_result_validsteps gr_product_after_product_result_validsteps. ((((exists ff_h_gprod_product_result_validstepsfactor. ff_h_gprod_product_result_validstepsfactor + S (gr_product_factor_product_result_validsteps) = S ((S (gr_product_index_product_result_validsteps)) * c)) /\ exists ff_q_gprod_product_result_validstepsfactor. b = ff_q_gprod_product_result_validstepsfactor * S ((S (gr_product_index_product_result_validsteps)) * c) + (gr_product_factor_product_result_validsteps))) /\ ((((exists ff_h_gprod_product_result_validstepsbefore. ff_h_gprod_product_result_validstepsbefore + S (gr_product_before_product_result_validsteps) = S ((S (gr_product_index_product_result_validsteps)) * gr_product_scale_product_result_valid)) /\ exists ff_q_gprod_product_result_validstepsbefore. gr_product_trace_product_result_valid = ff_q_gprod_product_result_validstepsbefore * S ((S (gr_product_index_product_result_validsteps)) * gr_product_scale_product_result_valid) + (gr_product_before_product_result_validsteps))) /\ ((((exists ff_h_gprod_product_result_validstepsafter. ff_h_gprod_product_result_validstepsafter + S (gr_product_after_product_result_validsteps) = S ((S (S (gr_product_index_product_result_validsteps))) * gr_product_scale_product_result_valid)) /\ exists ff_q_gprod_product_result_validstepsafter. gr_product_trace_product_result_valid = ff_q_gprod_product_result_validstepsafter * S ((S (S (gr_product_index_product_result_validsteps))) * gr_product_scale_product_result_valid) + (gr_product_after_product_result_validsteps))) /\ (exists ge_first_rp_product_result_validstepsmultiply ge_first_rn_product_result_validstepsmultiply ge_first_ip_product_result_validstepsmultiply ge_first_in_product_result_validstepsmultiply ge_second_rp_product_result_validstepsmultiply ge_second_rn_product_result_validstepsmultiply ge_second_ip_product_result_validstepsmultiply ge_second_in_product_result_validstepsmultiply. ((exists ge_representation_real_code_product_result_validstepsmultiplyfirst ge_representation_imaginary_code_product_result_validstepsmultiplyfirst. (((gr_product_before_product_result_validsteps) = ((ge_representation_real_code_product_result_validstepsmultiplyfirst) + (ge_representation_imaginary_code_product_result_validstepsmultiplyfirst)) * S ((ge_representation_real_code_product_result_validstepsmultiplyfirst) + (ge_representation_imaginary_code_product_result_validstepsmultiplyfirst)) + ((ge_representation_imaginary_code_product_result_validstepsmultiplyfirst) + (ge_representation_imaginary_code_product_result_validstepsmultiplyfirst))) /\ ((exists ge_balance_positive_product_result_validstepsmultiplyfirstreal ge_balance_negative_product_result_validstepsmultiplyfirstreal. (((((ge_representation_real_code_product_result_validstepsmultiplyfirst) = 2 * (ge_balance_positive_product_result_validstepsmultiplyfirstreal) /\ (ge_balance_negative_product_result_validstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_product_result_validstepsmultiplyfirstrealdecode. (((ge_representation_real_code_product_result_validstepsmultiplyfirst) = 2 * ge_signed_half_product_result_validstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_product_result_validstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_product_result_validstepsmultiplyfirstreal) = S ge_signed_half_product_result_validstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_product_result_validstepsmultiply) + ge_balance_negative_product_result_validstepsmultiplyfirstreal = (ge_first_rn_product_result_validstepsmultiply) + ge_balance_positive_product_result_validstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_product_result_validstepsmultiplyfirstimaginary ge_balance_negative_product_result_validstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_product_result_validstepsmultiplyfirst) = 2 * (ge_balance_positive_product_result_validstepsmultiplyfirstimaginary) /\ (ge_balance_negative_product_result_validstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_product_result_validstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_product_result_validstepsmultiplyfirst) = 2 * ge_signed_half_product_result_validstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_product_result_validstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_product_result_validstepsmultiplyfirstimaginary) = S ge_signed_half_product_result_validstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_product_result_validstepsmultiply) + ge_balance_negative_product_result_validstepsmultiplyfirstimaginary = (ge_first_in_product_result_validstepsmultiply) + ge_balance_positive_product_result_validstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_product_result_validstepsmultiplysecond ge_representation_imaginary_code_product_result_validstepsmultiplysecond. (((gr_product_factor_product_result_validsteps) = ((ge_representation_real_code_product_result_validstepsmultiplysecond) + (ge_representation_imaginary_code_product_result_validstepsmultiplysecond)) * S ((ge_representation_real_code_product_result_validstepsmultiplysecond) + (ge_representation_imaginary_code_product_result_validstepsmultiplysecond)) + ((ge_representation_imaginary_code_product_result_validstepsmultiplysecond) + (ge_representation_imaginary_code_product_result_validstepsmultiplysecond))) /\ ((exists ge_balance_positive_product_result_validstepsmultiplysecondreal ge_balance_negative_product_result_validstepsmultiplysecondreal. (((((ge_representation_real_code_product_result_validstepsmultiplysecond) = 2 * (ge_balance_positive_product_result_validstepsmultiplysecondreal) /\ (ge_balance_negative_product_result_validstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_product_result_validstepsmultiplysecondrealdecode. (((ge_representation_real_code_product_result_validstepsmultiplysecond) = 2 * ge_signed_half_product_result_validstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_product_result_validstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_product_result_validstepsmultiplysecondreal) = S ge_signed_half_product_result_validstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_product_result_validstepsmultiply) + ge_balance_negative_product_result_validstepsmultiplysecondreal = (ge_second_rn_product_result_validstepsmultiply) + ge_balance_positive_product_result_validstepsmultiplysecondreal))) /\ (exists ge_balance_positive_product_result_validstepsmultiplysecondimaginary ge_balance_negative_product_result_validstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_product_result_validstepsmultiplysecond) = 2 * (ge_balance_positive_product_result_validstepsmultiplysecondimaginary) /\ (ge_balance_negative_product_result_validstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_product_result_validstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_product_result_validstepsmultiplysecond) = 2 * ge_signed_half_product_result_validstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_product_result_validstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_product_result_validstepsmultiplysecondimaginary) = S ge_signed_half_product_result_validstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_product_result_validstepsmultiply) + ge_balance_negative_product_result_validstepsmultiplysecondimaginary = (ge_second_in_product_result_validstepsmultiply) + ge_balance_positive_product_result_validstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_product_result_validstepsmultiplyoutput ge_representation_imaginary_code_product_result_validstepsmultiplyoutput. (((gr_product_after_product_result_validsteps) = ((ge_representation_real_code_product_result_validstepsmultiplyoutput) + (ge_representation_imaginary_code_product_result_validstepsmultiplyoutput)) * S ((ge_representation_real_code_product_result_validstepsmultiplyoutput) + (ge_representation_imaginary_code_product_result_validstepsmultiplyoutput)) + ((ge_representation_imaginary_code_product_result_validstepsmultiplyoutput) + (ge_representation_imaginary_code_product_result_validstepsmultiplyoutput))) /\ ((exists ge_balance_positive_product_result_validstepsmultiplyoutputreal ge_balance_negative_product_result_validstepsmultiplyoutputreal. (((((ge_representation_real_code_product_result_validstepsmultiplyoutput) = 2 * (ge_balance_positive_product_result_validstepsmultiplyoutputreal) /\ (ge_balance_negative_product_result_validstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_product_result_validstepsmultiplyoutputrealdecode. (((ge_representation_real_code_product_result_validstepsmultiplyoutput) = 2 * ge_signed_half_product_result_validstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_product_result_validstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_product_result_validstepsmultiplyoutputreal) = S ge_signed_half_product_result_validstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_product_result_validstepsmultiply) * (ge_second_rp_product_result_validstepsmultiply))) + (((ge_first_rn_product_result_validstepsmultiply) * (ge_second_rn_product_result_validstepsmultiply))))) + (((((ge_first_ip_product_result_validstepsmultiply) * (ge_second_in_product_result_validstepsmultiply))) + (((ge_first_in_product_result_validstepsmultiply) * (ge_second_ip_product_result_validstepsmultiply))))))) + ge_balance_negative_product_result_validstepsmultiplyoutputreal = (((((((ge_first_rp_product_result_validstepsmultiply) * (ge_second_rn_product_result_validstepsmultiply))) + (((ge_first_rn_product_result_validstepsmultiply) * (ge_second_rp_product_result_validstepsmultiply))))) + (((((ge_first_ip_product_result_validstepsmultiply) * (ge_second_ip_product_result_validstepsmultiply))) + (((ge_first_in_product_result_validstepsmultiply) * (ge_second_in_product_result_validstepsmultiply))))))) + ge_balance_positive_product_result_validstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_product_result_validstepsmultiplyoutputimaginary ge_balance_negative_product_result_validstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_product_result_validstepsmultiplyoutput) = 2 * (ge_balance_positive_product_result_validstepsmultiplyoutputimaginary) /\ (ge_balance_negative_product_result_validstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_product_result_validstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_product_result_validstepsmultiplyoutput) = 2 * ge_signed_half_product_result_validstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_product_result_validstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_product_result_validstepsmultiplyoutputimaginary) = S ge_signed_half_product_result_validstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_result_validstepsmultiply) * (ge_second_ip_product_result_validstepsmultiply))) + (((ge_first_rn_product_result_validstepsmultiply) * (ge_second_in_product_result_validstepsmultiply))))) + (((((ge_first_ip_product_result_validstepsmultiply) * (ge_second_rp_product_result_validstepsmultiply))) + (((ge_first_in_product_result_validstepsmultiply) * (ge_second_rn_product_result_validstepsmultiply))))))) + ge_balance_negative_product_result_validstepsmultiplyoutputimaginary = (((((((ge_first_rp_product_result_validstepsmultiply) * (ge_second_in_product_result_validstepsmultiply))) + (((ge_first_rn_product_result_validstepsmultiply) * (ge_second_ip_product_result_validstepsmultiply))))) + (((((ge_first_ip_product_result_validstepsmultiply) * (ge_second_rn_product_result_validstepsmultiply))) + (((ge_first_in_product_result_validstepsmultiply) * (ge_second_rp_product_result_validstepsmultiply))))))) + ge_balance_positive_product_result_validstepsmultiplyoutputimaginary)))))))))))))))) -> (exists ge_real_positive_product_carrier ge_real_negative_product_carrier ge_imaginary_positive_product_carrier ge_imaginary_negative_product_carrier. (exists ge_real_code_product_carrierdecode ge_imaginary_code_product_carrierdecode. (((P) = ((ge_real_code_product_carrierdecode) + (ge_imaginary_code_product_carrierdecode)) * S ((ge_real_code_product_carrierdecode) + (ge_imaginary_code_product_carrierdecode)) + ((ge_imaginary_code_product_carrierdecode) + (ge_imaginary_code_product_carrierdecode))) /\ (((((ge_real_code_product_carrierdecode) = 2 * (ge_real_positive_product_carrier) /\ (ge_real_negative_product_carrier) = 0) \/ exists ge_signed_half_ge_product_carrierdecode_real. (((ge_real_code_product_carrierdecode) = 2 * ge_signed_half_ge_product_carrierdecode_real + 1 /\ (ge_real_positive_product_carrier) = 0) /\ (ge_real_negative_product_carrier) = S ge_signed_half_ge_product_carrierdecode_real))) /\ ((((ge_imaginary_code_product_carrierdecode) = 2 * (ge_imaginary_positive_product_carrier) /\ (ge_imaginary_negative_product_carrier) = 0) \/ exists ge_signed_half_ge_product_carrierdecode_imaginary. (((ge_imaginary_code_product_carrierdecode) = 2 * ge_signed_half_ge_product_carrierdecode_imaginary + 1 /\ (ge_imaginary_positive_product_carrier) = 0) /\ (ge_imaginary_negative_product_carrier) = S ge_signed_half_ge_product_carrierdecode_imaginary)))))))

Constructive proof overview

Generated structural guide

Every actual finite Gaussian product has a valid carrier code, including the empty product.

The unchanged tactic script uses 4 declared prerequisites and contains 33 exact native proof lines.

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

Proof neighborhood

Direct dependencies

GF0087 gaussian_product_empty_value GF000F gaussian_one_valid GF0089 gaussian_product_successor_decompose GF0009 gaussian_multiply_output_valid

Direct dependents

GF0093 gaussian_factorization_append_irreducible GF009A gaussian_all_irreducible_product_exists GF00A0 gaussian_product_replace_balance

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

33 script commands · 6 reading checkpoints · 2 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 product empty valuegaussian one validgaussian product successor decomposegaussian multiply output valid

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.

01Induction on lL1–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction l
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro P
  5. L5
    intro hp
02Establish heqL6–15

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

  1. L6
    have heq : P=6
  2. L7
    specialize gaussian_product_empty_value (b)
  3. L8
    specialize gaussian_product_empty_value (c)
  4. L9
    specialize gaussian_product_empty_value (P)
  5. L10
    apply gaussian_product_empty_value
  6. L11
    exact hp
  7. L12
    rewrite heq
  8. L13
    exact gaussian_one_valid
  9. L14
    intro b
  10. L15
    intro c
03Fix variables and assumptionsL16–17

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

  1. L16
    intro P
  2. L17
    intro hp
04Establish hsL18–24

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

  1. L18
    have hs : ∃ a. ∃ Q. BetaAt(b,c,l,a) ∧ (GProduct(b,c,l,Q) ∧ GMul(Q,a,P))Definitions: GMulGProductBetaAt
  2. L19
    specialize gaussian_product_successor_decompose (b)
  3. L20
    specialize gaussian_product_successor_decompose (c)
  4. L21
    specialize gaussian_product_successor_decompose (l)
  5. L22
    specialize gaussian_product_successor_decompose (P)
  6. L23
    apply gaussian_product_successor_decompose
  7. L24
    exact hp
05Separate the logical casesL25–28

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

  1. L25
    cases hs
  2. L26
    cases hs_witness
  3. L27
    cases hs_witness_witness
  4. L28
    cases hs_witness_witness_right
06Use earlier factsL29–33

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

  1. L29
    specialize gaussian_multiply_output_valid (x1)
  2. L30
    specialize gaussian_multiply_output_valid (x)
  3. L31
    specialize gaussian_multiply_output_valid (P)
  4. L32
    apply gaussian_multiply_output_valid
  5. L33
    exact hs_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 33 lines
  1. 0001induction l
  2. 0002intro b
  3. 0003intro c
  4. 0004intro P
  5. 0005intro hp
  6. 0006have heq : P=6
  7. 0007specialize gaussian_product_empty_value (b)
  8. 0008specialize gaussian_product_empty_value (c)
  9. 0009specialize gaussian_product_empty_value (P)
  10. 0010apply gaussian_product_empty_value
  11. 0011exact hp
  12. 0012rewrite heq
  13. 0013exact gaussian_one_valid
  14. 0014intro b
  15. 0015intro c
  16. 0016intro P
  17. 0017intro hp
  18. 0018have hs : exists a Q. ((((exists ff_h_gprod_result_valid_factor. ff_h_gprod_result_valid_factor + S (a) = S ((S (l)) * c)) /\ exists ff_q_gprod_result_valid_factor. b = ff_q_gprod_result_valid_factor * S ((S (l)) * c) + (a))) /\ ((exists gr_product_trace_result_valid_prefix gr_product_scale_result_valid_prefix. ((((exists ff_h_gprod_result_valid_prefixstart. ff_h_gprod_result_valid_prefixstart + S (6) = S ((S (0)) * gr_product_scale_result_valid_prefix)) /\ exists ff_q_gprod_result_valid_prefixstart. gr_product_trace_result_valid_prefix = ff_q_gprod_result_valid_prefixstart * S ((S (0)) * gr_product_scale_result_valid_prefix) + (6))) /\ ((((exists ff_h_gprod_result_valid_prefixend. ff_h_gprod_result_valid_prefixend + S (Q) = S ((S (l)) * gr_product_scale_result_valid_prefix)) /\ exists ff_q_gprod_result_valid_prefixend. gr_product_trace_result_valid_prefix = ff_q_gprod_result_valid_prefixend * S ((S (l)) * gr_product_scale_result_valid_prefix) + (Q))) /\ (forall gr_product_index_result_valid_prefixsteps. (exists ge_gap_result_valid_prefixstepsindex_bound. ge_gap_result_valid_prefixstepsindex_bound + S (gr_product_index_result_valid_prefixsteps) = (l)) -> exists gr_product_factor_result_valid_prefixsteps gr_product_before_result_valid_prefixsteps gr_product_after_result_valid_prefixsteps. ((((exists ff_h_gprod_result_valid_prefixstepsfactor. ff_h_gprod_result_valid_prefixstepsfactor + S (gr_product_factor_result_valid_prefixsteps) = S ((S (gr_product_index_result_valid_prefixsteps)) * c)) /\ exists ff_q_gprod_result_valid_prefixstepsfactor. b = ff_q_gprod_result_valid_prefixstepsfactor * S ((S (gr_product_index_result_valid_prefixsteps)) * c) + (gr_product_factor_result_valid_prefixsteps))) /\ ((((exists ff_h_gprod_result_valid_prefixstepsbefore. ff_h_gprod_result_valid_prefixstepsbefore + S (gr_product_before_result_valid_prefixsteps) = S ((S (gr_product_index_result_valid_prefixsteps)) * gr_product_scale_result_valid_prefix)) /\ exists ff_q_gprod_result_valid_prefixstepsbefore. gr_product_trace_result_valid_prefix = ff_q_gprod_result_valid_prefixstepsbefore * S ((S (gr_product_index_result_valid_prefixsteps)) * gr_product_scale_result_valid_prefix) + (gr_product_before_result_valid_prefixsteps))) /\ ((((exists ff_h_gprod_result_valid_prefixstepsafter. ff_h_gprod_result_valid_prefixstepsafter + S (gr_product_after_result_valid_prefixsteps) = S ((S (S (gr_product_index_result_valid_prefixsteps))) * gr_product_scale_result_valid_prefix)) /\ exists ff_q_gprod_result_valid_prefixstepsafter. gr_product_trace_result_valid_prefix = ff_q_gprod_result_valid_prefixstepsafter * S ((S (S (gr_product_index_result_valid_prefixsteps))) * gr_product_scale_result_valid_prefix) + (gr_product_after_result_valid_prefixsteps))) /\ (exists ge_first_rp_result_valid_prefixstepsmultiply ge_first_rn_result_valid_prefixstepsmultiply ge_first_ip_result_valid_prefixstepsmultiply ge_first_in_result_valid_prefixstepsmultiply ge_second_rp_result_valid_prefixstepsmultiply ge_second_rn_result_valid_prefixstepsmultiply ge_second_ip_result_valid_prefixstepsmultiply ge_second_in_result_valid_prefixstepsmultiply. ((exists ge_representation_real_code_result_valid_prefixstepsmultiplyfirst ge_representation_imaginary_code_result_valid_prefixstepsmultiplyfirst. (((gr_product_before_result_valid_prefixsteps) = ((ge_representation_real_code_result_valid_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_result_valid_prefixstepsmultiplyfirst)) * S ((ge_representation_real_code_result_valid_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_result_valid_prefixstepsmultiplyfirst)) + ((ge_representation_imaginary_code_result_valid_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_result_valid_prefixstepsmultiplyfirst))) /\ ((exists ge_balance_positive_result_valid_prefixstepsmultiplyfirstreal ge_balance_negative_result_valid_prefixstepsmultiplyfirstreal. (((((ge_representation_real_code_result_valid_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_result_valid_prefixstepsmultiplyfirstreal) /\ (ge_balance_negative_result_valid_prefixstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_result_valid_prefixstepsmultiplyfirstrealdecode. (((ge_representation_real_code_result_valid_prefixstepsmultiplyfirst) = 2 * ge_signed_half_result_valid_prefixstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_result_valid_prefixstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_result_valid_prefixstepsmultiplyfirstreal) = S ge_signed_half_result_valid_prefixstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_result_valid_prefixstepsmultiply) + ge_balance_negative_result_valid_prefixstepsmultiplyfirstreal = (ge_first_rn_result_valid_prefixstepsmultiply) + ge_balance_positive_result_valid_prefixstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_result_valid_prefixstepsmultiplyfirstimaginary ge_balance_negative_result_valid_prefixstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_result_valid_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_result_valid_prefixstepsmultiplyfirstimaginary) /\ (ge_balance_negative_result_valid_prefixstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_result_valid_prefixstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_result_valid_prefixstepsmultiplyfirst) = 2 * ge_signed_half_result_valid_prefixstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_result_valid_prefixstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_result_valid_prefixstepsmultiplyfirstimaginary) = S ge_signed_half_result_valid_prefixstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_result_valid_prefixstepsmultiply) + ge_balance_negative_result_valid_prefixstepsmultiplyfirstimaginary = (ge_first_in_result_valid_prefixstepsmultiply) + ge_balance_positive_result_valid_prefixstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_result_valid_prefixstepsmultiplysecond ge_representation_imaginary_code_result_valid_prefixstepsmultiplysecond. (((gr_product_factor_result_valid_prefixsteps) = ((ge_representation_real_code_result_valid_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_result_valid_prefixstepsmultiplysecond)) * S ((ge_representation_real_code_result_valid_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_result_valid_prefixstepsmultiplysecond)) + ((ge_representation_imaginary_code_result_valid_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_result_valid_prefixstepsmultiplysecond))) /\ ((exists ge_balance_positive_result_valid_prefixstepsmultiplysecondreal ge_balance_negative_result_valid_prefixstepsmultiplysecondreal. (((((ge_representation_real_code_result_valid_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_result_valid_prefixstepsmultiplysecondreal) /\ (ge_balance_negative_result_valid_prefixstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_result_valid_prefixstepsmultiplysecondrealdecode. (((ge_representation_real_code_result_valid_prefixstepsmultiplysecond) = 2 * ge_signed_half_result_valid_prefixstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_result_valid_prefixstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_result_valid_prefixstepsmultiplysecondreal) = S ge_signed_half_result_valid_prefixstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_result_valid_prefixstepsmultiply) + ge_balance_negative_result_valid_prefixstepsmultiplysecondreal = (ge_second_rn_result_valid_prefixstepsmultiply) + ge_balance_positive_result_valid_prefixstepsmultiplysecondreal))) /\ (exists ge_balance_positive_result_valid_prefixstepsmultiplysecondimaginary ge_balance_negative_result_valid_prefixstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_result_valid_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_result_valid_prefixstepsmultiplysecondimaginary) /\ (ge_balance_negative_result_valid_prefixstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_result_valid_prefixstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_result_valid_prefixstepsmultiplysecond) = 2 * ge_signed_half_result_valid_prefixstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_result_valid_prefixstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_result_valid_prefixstepsmultiplysecondimaginary) = S ge_signed_half_result_valid_prefixstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_result_valid_prefixstepsmultiply) + ge_balance_negative_result_valid_prefixstepsmultiplysecondimaginary = (ge_second_in_result_valid_prefixstepsmultiply) + ge_balance_positive_result_valid_prefixstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_result_valid_prefixstepsmultiplyoutput ge_representation_imaginary_code_result_valid_prefixstepsmultiplyoutput. (((gr_product_after_result_valid_prefixsteps) = ((ge_representation_real_code_result_valid_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_result_valid_prefixstepsmultiplyoutput)) * S ((ge_representation_real_code_result_valid_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_result_valid_prefixstepsmultiplyoutput)) + ((ge_representation_imaginary_code_result_valid_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_result_valid_prefixstepsmultiplyoutput))) /\ ((exists ge_balance_positive_result_valid_prefixstepsmultiplyoutputreal ge_balance_negative_result_valid_prefixstepsmultiplyoutputreal. (((((ge_representation_real_code_result_valid_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_result_valid_prefixstepsmultiplyoutputreal) /\ (ge_balance_negative_result_valid_prefixstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_result_valid_prefixstepsmultiplyoutputrealdecode. (((ge_representation_real_code_result_valid_prefixstepsmultiplyoutput) = 2 * ge_signed_half_result_valid_prefixstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_result_valid_prefixstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_result_valid_prefixstepsmultiplyoutputreal) = S ge_signed_half_result_valid_prefixstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_result_valid_prefixstepsmultiply) * (ge_second_rp_result_valid_prefixstepsmultiply))) + (((ge_first_rn_result_valid_prefixstepsmultiply) * (ge_second_rn_result_valid_prefixstepsmultiply))))) + (((((ge_first_ip_result_valid_prefixstepsmultiply) * (ge_second_in_result_valid_prefixstepsmultiply))) + (((ge_first_in_result_valid_prefixstepsmultiply) * (ge_second_ip_result_valid_prefixstepsmultiply))))))) + ge_balance_negative_result_valid_prefixstepsmultiplyoutputreal = (((((((ge_first_rp_result_valid_prefixstepsmultiply) * (ge_second_rn_result_valid_prefixstepsmultiply))) + (((ge_first_rn_result_valid_prefixstepsmultiply) * (ge_second_rp_result_valid_prefixstepsmultiply))))) + (((((ge_first_ip_result_valid_prefixstepsmultiply) * (ge_second_ip_result_valid_prefixstepsmultiply))) + (((ge_first_in_result_valid_prefixstepsmultiply) * (ge_second_in_result_valid_prefixstepsmultiply))))))) + ge_balance_positive_result_valid_prefixstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_result_valid_prefixstepsmultiplyoutputimaginary ge_balance_negative_result_valid_prefixstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_result_valid_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_result_valid_prefixstepsmultiplyoutputimaginary) /\ (ge_balance_negative_result_valid_prefixstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_result_valid_prefixstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_result_valid_prefixstepsmultiplyoutput) = 2 * ge_signed_half_result_valid_prefixstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_result_valid_prefixstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_result_valid_prefixstepsmultiplyoutputimaginary) = S ge_signed_half_result_valid_prefixstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_result_valid_prefixstepsmultiply) * (ge_second_ip_result_valid_prefixstepsmultiply))) + (((ge_first_rn_result_valid_prefixstepsmultiply) * (ge_second_in_result_valid_prefixstepsmultiply))))) + (((((ge_first_ip_result_valid_prefixstepsmultiply) * (ge_second_rp_result_valid_prefixstepsmultiply))) + (((ge_first_in_result_valid_prefixstepsmultiply) * (ge_second_rn_result_valid_prefixstepsmultiply))))))) + ge_balance_negative_result_valid_prefixstepsmultiplyoutputimaginary = (((((((ge_first_rp_result_valid_prefixstepsmultiply) * (ge_second_in_result_valid_prefixstepsmultiply))) + (((ge_first_rn_result_valid_prefixstepsmultiply) * (ge_second_ip_result_valid_prefixstepsmultiply))))) + (((((ge_first_ip_result_valid_prefixstepsmultiply) * (ge_second_rn_result_valid_prefixstepsmultiply))) + (((ge_first_in_result_valid_prefixstepsmultiply) * (ge_second_rp_result_valid_prefixstepsmultiply))))))) + ge_balance_positive_result_valid_prefixstepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_result_valid_multiply ge_first_rn_result_valid_multiply ge_first_ip_result_valid_multiply ge_first_in_result_valid_multiply ge_second_rp_result_valid_multiply ge_second_rn_result_valid_multiply ge_second_ip_result_valid_multiply ge_second_in_result_valid_multiply. ((exists ge_representation_real_code_result_valid_multiplyfirst ge_representation_imaginary_code_result_valid_multiplyfirst. (((Q) = ((ge_representation_real_code_result_valid_multiplyfirst) + (ge_representation_imaginary_code_result_valid_multiplyfirst)) * S ((ge_representation_real_code_result_valid_multiplyfirst) + (ge_representation_imaginary_code_result_valid_multiplyfirst)) + ((ge_representation_imaginary_code_result_valid_multiplyfirst) + (ge_representation_imaginary_code_result_valid_multiplyfirst))) /\ ((exists ge_balance_positive_result_valid_multiplyfirstreal ge_balance_negative_result_valid_multiplyfirstreal. (((((ge_representation_real_code_result_valid_multiplyfirst) = 2 * (ge_balance_positive_result_valid_multiplyfirstreal) /\ (ge_balance_negative_result_valid_multiplyfirstreal) = 0) \/ exists ge_signed_half_result_valid_multiplyfirstrealdecode. (((ge_representation_real_code_result_valid_multiplyfirst) = 2 * ge_signed_half_result_valid_multiplyfirstrealdecode + 1 /\ (ge_balance_positive_result_valid_multiplyfirstreal) = 0) /\ (ge_balance_negative_result_valid_multiplyfirstreal) = S ge_signed_half_result_valid_multiplyfirstrealdecode))) /\ ((ge_first_rp_result_valid_multiply) + ge_balance_negative_result_valid_multiplyfirstreal = (ge_first_rn_result_valid_multiply) + ge_balance_positive_result_valid_multiplyfirstreal))) /\ (exists ge_balance_positive_result_valid_multiplyfirstimaginary ge_balance_negative_result_valid_multiplyfirstimaginary. (((((ge_representation_imaginary_code_result_valid_multiplyfirst) = 2 * (ge_balance_positive_result_valid_multiplyfirstimaginary) /\ (ge_balance_negative_result_valid_multiplyfirstimaginary) = 0) \/ exists ge_signed_half_result_valid_multiplyfirstimaginarydecode. (((ge_representation_imaginary_code_result_valid_multiplyfirst) = 2 * ge_signed_half_result_valid_multiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_result_valid_multiplyfirstimaginary) = 0) /\ (ge_balance_negative_result_valid_multiplyfirstimaginary) = S ge_signed_half_result_valid_multiplyfirstimaginarydecode))) /\ ((ge_first_ip_result_valid_multiply) + ge_balance_negative_result_valid_multiplyfirstimaginary = (ge_first_in_result_valid_multiply) + ge_balance_positive_result_valid_multiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_result_valid_multiplysecond ge_representation_imaginary_code_result_valid_multiplysecond. (((a) = ((ge_representation_real_code_result_valid_multiplysecond) + (ge_representation_imaginary_code_result_valid_multiplysecond)) * S ((ge_representation_real_code_result_valid_multiplysecond) + (ge_representation_imaginary_code_result_valid_multiplysecond)) + ((ge_representation_imaginary_code_result_valid_multiplysecond) + (ge_representation_imaginary_code_result_valid_multiplysecond))) /\ ((exists ge_balance_positive_result_valid_multiplysecondreal ge_balance_negative_result_valid_multiplysecondreal. (((((ge_representation_real_code_result_valid_multiplysecond) = 2 * (ge_balance_positive_result_valid_multiplysecondreal) /\ (ge_balance_negative_result_valid_multiplysecondreal) = 0) \/ exists ge_signed_half_result_valid_multiplysecondrealdecode. (((ge_representation_real_code_result_valid_multiplysecond) = 2 * ge_signed_half_result_valid_multiplysecondrealdecode + 1 /\ (ge_balance_positive_result_valid_multiplysecondreal) = 0) /\ (ge_balance_negative_result_valid_multiplysecondreal) = S ge_signed_half_result_valid_multiplysecondrealdecode))) /\ ((ge_second_rp_result_valid_multiply) + ge_balance_negative_result_valid_multiplysecondreal = (ge_second_rn_result_valid_multiply) + ge_balance_positive_result_valid_multiplysecondreal))) /\ (exists ge_balance_positive_result_valid_multiplysecondimaginary ge_balance_negative_result_valid_multiplysecondimaginary. (((((ge_representation_imaginary_code_result_valid_multiplysecond) = 2 * (ge_balance_positive_result_valid_multiplysecondimaginary) /\ (ge_balance_negative_result_valid_multiplysecondimaginary) = 0) \/ exists ge_signed_half_result_valid_multiplysecondimaginarydecode. (((ge_representation_imaginary_code_result_valid_multiplysecond) = 2 * ge_signed_half_result_valid_multiplysecondimaginarydecode + 1 /\ (ge_balance_positive_result_valid_multiplysecondimaginary) = 0) /\ (ge_balance_negative_result_valid_multiplysecondimaginary) = S ge_signed_half_result_valid_multiplysecondimaginarydecode))) /\ ((ge_second_ip_result_valid_multiply) + ge_balance_negative_result_valid_multiplysecondimaginary = (ge_second_in_result_valid_multiply) + ge_balance_positive_result_valid_multiplysecondimaginary)))))) /\ (exists ge_representation_real_code_result_valid_multiplyoutput ge_representation_imaginary_code_result_valid_multiplyoutput. (((P) = ((ge_representation_real_code_result_valid_multiplyoutput) + (ge_representation_imaginary_code_result_valid_multiplyoutput)) * S ((ge_representation_real_code_result_valid_multiplyoutput) + (ge_representation_imaginary_code_result_valid_multiplyoutput)) + ((ge_representation_imaginary_code_result_valid_multiplyoutput) + (ge_representation_imaginary_code_result_valid_multiplyoutput))) /\ ((exists ge_balance_positive_result_valid_multiplyoutputreal ge_balance_negative_result_valid_multiplyoutputreal. (((((ge_representation_real_code_result_valid_multiplyoutput) = 2 * (ge_balance_positive_result_valid_multiplyoutputreal) /\ (ge_balance_negative_result_valid_multiplyoutputreal) = 0) \/ exists ge_signed_half_result_valid_multiplyoutputrealdecode. (((ge_representation_real_code_result_valid_multiplyoutput) = 2 * ge_signed_half_result_valid_multiplyoutputrealdecode + 1 /\ (ge_balance_positive_result_valid_multiplyoutputreal) = 0) /\ (ge_balance_negative_result_valid_multiplyoutputreal) = S ge_signed_half_result_valid_multiplyoutputrealdecode))) /\ ((((((((ge_first_rp_result_valid_multiply) * (ge_second_rp_result_valid_multiply))) + (((ge_first_rn_result_valid_multiply) * (ge_second_rn_result_valid_multiply))))) + (((((ge_first_ip_result_valid_multiply) * (ge_second_in_result_valid_multiply))) + (((ge_first_in_result_valid_multiply) * (ge_second_ip_result_valid_multiply))))))) + ge_balance_negative_result_valid_multiplyoutputreal = (((((((ge_first_rp_result_valid_multiply) * (ge_second_rn_result_valid_multiply))) + (((ge_first_rn_result_valid_multiply) * (ge_second_rp_result_valid_multiply))))) + (((((ge_first_ip_result_valid_multiply) * (ge_second_ip_result_valid_multiply))) + (((ge_first_in_result_valid_multiply) * (ge_second_in_result_valid_multiply))))))) + ge_balance_positive_result_valid_multiplyoutputreal))) /\ (exists ge_balance_positive_result_valid_multiplyoutputimaginary ge_balance_negative_result_valid_multiplyoutputimaginary. (((((ge_representation_imaginary_code_result_valid_multiplyoutput) = 2 * (ge_balance_positive_result_valid_multiplyoutputimaginary) /\ (ge_balance_negative_result_valid_multiplyoutputimaginary) = 0) \/ exists ge_signed_half_result_valid_multiplyoutputimaginarydecode. (((ge_representation_imaginary_code_result_valid_multiplyoutput) = 2 * ge_signed_half_result_valid_multiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_result_valid_multiplyoutputimaginary) = 0) /\ (ge_balance_negative_result_valid_multiplyoutputimaginary) = S ge_signed_half_result_valid_multiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_result_valid_multiply) * (ge_second_ip_result_valid_multiply))) + (((ge_first_rn_result_valid_multiply) * (ge_second_in_result_valid_multiply))))) + (((((ge_first_ip_result_valid_multiply) * (ge_second_rp_result_valid_multiply))) + (((ge_first_in_result_valid_multiply) * (ge_second_rn_result_valid_multiply))))))) + ge_balance_negative_result_valid_multiplyoutputimaginary = (((((((ge_first_rp_result_valid_multiply) * (ge_second_in_result_valid_multiply))) + (((ge_first_rn_result_valid_multiply) * (ge_second_ip_result_valid_multiply))))) + (((((ge_first_ip_result_valid_multiply) * (ge_second_rn_result_valid_multiply))) + (((ge_first_in_result_valid_multiply) * (ge_second_rp_result_valid_multiply))))))) + ge_balance_positive_result_valid_multiplyoutputimaginary)))))))))))
  19. 0019specialize gaussian_product_successor_decompose (b)
  20. 0020specialize gaussian_product_successor_decompose (c)
  21. 0021specialize gaussian_product_successor_decompose (l)
  22. 0022specialize gaussian_product_successor_decompose (P)
  23. 0023apply gaussian_product_successor_decompose
  24. 0024exact hp
  25. 0025cases hs
  26. 0026cases hs_witness
  27. 0027cases hs_witness_witness
  28. 0028cases hs_witness_witness_right
  29. 0029specialize gaussian_multiply_output_valid (x1)
  30. 0030specialize gaussian_multiply_output_valid (x)
  31. 0031specialize gaussian_multiply_output_valid (P)
  32. 0032apply gaussian_multiply_output_valid
  33. 0033exact hs_witness_witness_right_right