GF001F

gaussian_multiply_zero_implies_zero_factor

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

The actual Gaussian ring has no zero divisors, proved from multiplicative norms and natural multiplication.

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 a b. (exists ge_first_rp_zero_product ge_first_rn_zero_product ge_first_ip_zero_product ge_first_in_zero_product ge_second_rp_zero_product ge_second_rn_zero_product ge_second_ip_zero_product ge_second_in_zero_product. ((exists ge_representation_real_code_zero_productfirst ge_representation_imaginary_code_zero_productfirst. (((a) = ((ge_representation_real_code_zero_productfirst) + (ge_representation_imaginary_code_zero_productfirst)) * S ((ge_representation_real_code_zero_productfirst) + (ge_representation_imaginary_code_zero_productfirst)) + ((ge_representation_imaginary_code_zero_productfirst) + (ge_representation_imaginary_code_zero_productfirst))) /\ ((exists ge_balance_positive_zero_productfirstreal ge_balance_negative_zero_productfirstreal. (((((ge_representation_real_code_zero_productfirst) = 2 * (ge_balance_positive_zero_productfirstreal) /\ (ge_balance_negative_zero_productfirstreal) = 0) \/ exists ge_signed_half_zero_productfirstrealdecode. (((ge_representation_real_code_zero_productfirst) = 2 * ge_signed_half_zero_productfirstrealdecode + 1 /\ (ge_balance_positive_zero_productfirstreal) = 0) /\ (ge_balance_negative_zero_productfirstreal) = S ge_signed_half_zero_productfirstrealdecode))) /\ ((ge_first_rp_zero_product) + ge_balance_negative_zero_productfirstreal = (ge_first_rn_zero_product) + ge_balance_positive_zero_productfirstreal))) /\ (exists ge_balance_positive_zero_productfirstimaginary ge_balance_negative_zero_productfirstimaginary. (((((ge_representation_imaginary_code_zero_productfirst) = 2 * (ge_balance_positive_zero_productfirstimaginary) /\ (ge_balance_negative_zero_productfirstimaginary) = 0) \/ exists ge_signed_half_zero_productfirstimaginarydecode. (((ge_representation_imaginary_code_zero_productfirst) = 2 * ge_signed_half_zero_productfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_productfirstimaginary) = 0) /\ (ge_balance_negative_zero_productfirstimaginary) = S ge_signed_half_zero_productfirstimaginarydecode))) /\ ((ge_first_ip_zero_product) + ge_balance_negative_zero_productfirstimaginary = (ge_first_in_zero_product) + ge_balance_positive_zero_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_productsecond ge_representation_imaginary_code_zero_productsecond. (((b) = ((ge_representation_real_code_zero_productsecond) + (ge_representation_imaginary_code_zero_productsecond)) * S ((ge_representation_real_code_zero_productsecond) + (ge_representation_imaginary_code_zero_productsecond)) + ((ge_representation_imaginary_code_zero_productsecond) + (ge_representation_imaginary_code_zero_productsecond))) /\ ((exists ge_balance_positive_zero_productsecondreal ge_balance_negative_zero_productsecondreal. (((((ge_representation_real_code_zero_productsecond) = 2 * (ge_balance_positive_zero_productsecondreal) /\ (ge_balance_negative_zero_productsecondreal) = 0) \/ exists ge_signed_half_zero_productsecondrealdecode. (((ge_representation_real_code_zero_productsecond) = 2 * ge_signed_half_zero_productsecondrealdecode + 1 /\ (ge_balance_positive_zero_productsecondreal) = 0) /\ (ge_balance_negative_zero_productsecondreal) = S ge_signed_half_zero_productsecondrealdecode))) /\ ((ge_second_rp_zero_product) + ge_balance_negative_zero_productsecondreal = (ge_second_rn_zero_product) + ge_balance_positive_zero_productsecondreal))) /\ (exists ge_balance_positive_zero_productsecondimaginary ge_balance_negative_zero_productsecondimaginary. (((((ge_representation_imaginary_code_zero_productsecond) = 2 * (ge_balance_positive_zero_productsecondimaginary) /\ (ge_balance_negative_zero_productsecondimaginary) = 0) \/ exists ge_signed_half_zero_productsecondimaginarydecode. (((ge_representation_imaginary_code_zero_productsecond) = 2 * ge_signed_half_zero_productsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_productsecondimaginary) = 0) /\ (ge_balance_negative_zero_productsecondimaginary) = S ge_signed_half_zero_productsecondimaginarydecode))) /\ ((ge_second_ip_zero_product) + ge_balance_negative_zero_productsecondimaginary = (ge_second_in_zero_product) + ge_balance_positive_zero_productsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_productoutput ge_representation_imaginary_code_zero_productoutput. (((0) = ((ge_representation_real_code_zero_productoutput) + (ge_representation_imaginary_code_zero_productoutput)) * S ((ge_representation_real_code_zero_productoutput) + (ge_representation_imaginary_code_zero_productoutput)) + ((ge_representation_imaginary_code_zero_productoutput) + (ge_representation_imaginary_code_zero_productoutput))) /\ ((exists ge_balance_positive_zero_productoutputreal ge_balance_negative_zero_productoutputreal. (((((ge_representation_real_code_zero_productoutput) = 2 * (ge_balance_positive_zero_productoutputreal) /\ (ge_balance_negative_zero_productoutputreal) = 0) \/ exists ge_signed_half_zero_productoutputrealdecode. (((ge_representation_real_code_zero_productoutput) = 2 * ge_signed_half_zero_productoutputrealdecode + 1 /\ (ge_balance_positive_zero_productoutputreal) = 0) /\ (ge_balance_negative_zero_productoutputreal) = S ge_signed_half_zero_productoutputrealdecode))) /\ ((((((((ge_first_rp_zero_product) * (ge_second_rp_zero_product))) + (((ge_first_rn_zero_product) * (ge_second_rn_zero_product))))) + (((((ge_first_ip_zero_product) * (ge_second_in_zero_product))) + (((ge_first_in_zero_product) * (ge_second_ip_zero_product))))))) + ge_balance_negative_zero_productoutputreal = (((((((ge_first_rp_zero_product) * (ge_second_rn_zero_product))) + (((ge_first_rn_zero_product) * (ge_second_rp_zero_product))))) + (((((ge_first_ip_zero_product) * (ge_second_ip_zero_product))) + (((ge_first_in_zero_product) * (ge_second_in_zero_product))))))) + ge_balance_positive_zero_productoutputreal))) /\ (exists ge_balance_positive_zero_productoutputimaginary ge_balance_negative_zero_productoutputimaginary. (((((ge_representation_imaginary_code_zero_productoutput) = 2 * (ge_balance_positive_zero_productoutputimaginary) /\ (ge_balance_negative_zero_productoutputimaginary) = 0) \/ exists ge_signed_half_zero_productoutputimaginarydecode. (((ge_representation_imaginary_code_zero_productoutput) = 2 * ge_signed_half_zero_productoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_productoutputimaginary) = 0) /\ (ge_balance_negative_zero_productoutputimaginary) = S ge_signed_half_zero_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_product) * (ge_second_ip_zero_product))) + (((ge_first_rn_zero_product) * (ge_second_in_zero_product))))) + (((((ge_first_ip_zero_product) * (ge_second_rp_zero_product))) + (((ge_first_in_zero_product) * (ge_second_rn_zero_product))))))) + ge_balance_negative_zero_productoutputimaginary = (((((((ge_first_rp_zero_product) * (ge_second_in_zero_product))) + (((ge_first_rn_zero_product) * (ge_second_ip_zero_product))))) + (((((ge_first_ip_zero_product) * (ge_second_rn_zero_product))) + (((ge_first_in_zero_product) * (ge_second_rp_zero_product))))))) + ge_balance_positive_zero_productoutputimaginary))))))))) -> a=0 \/ b=0

Constructive proof overview

Generated structural guide

The actual Gaussian ring has no zero divisors, proved from multiplicative norms and natural multiplication.

The unchanged tactic script uses 9 declared prerequisites and contains 60 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_functional Alpha theorem; checked-use authorized gaussian_norm_multiply Alpha theorem; checked-use authorized GF000D gaussian_zero_norm mul_eq_zero Stable theorem; checked-use authorized GF0017 gaussian_norm_zero_implies_code_zero GF0015 gaussian_norm_value_transport

Direct dependents

GF003B gaussian_multiply_cancel_left GF009B gaussian_all_irreducible_product_nonzero GF009E gaussian_factorization_value_nonzero

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

60 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 (5)
gaussian multiply input left validgaussian multiply input right validgaussian zero normgaussian norm zero implies code zerogaussian 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–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro h
02Establish hAL4–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 hA : ∃ N. GNorm(a,N)Definitions: GNorm
  2. L5
    specialize gaussian_norm_exists (a)
  3. L6
    apply gaussian_norm_exists
  4. L7
    specialize gaussian_multiply_input_left_valid (a)
  5. L8
    specialize gaussian_multiply_input_left_valid (b)
  6. L9
    specialize gaussian_multiply_input_left_valid (0)
  7. L10
    apply gaussian_multiply_input_left_valid
  8. L11
    exact h
03Separate the logical casesL12–12

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

  1. L12
    cases hA
04Establish hBL13–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 hB : ∃ M. GNorm(b,M)Definitions: GNorm
  2. L14
    specialize gaussian_norm_exists (b)
  3. L15
    apply gaussian_norm_exists
  4. L16
    specialize gaussian_multiply_input_right_valid (a)
  5. L17
    specialize gaussian_multiply_input_right_valid (b)
  6. L18
    specialize gaussian_multiply_input_right_valid (0)
  7. L19
    apply gaussian_multiply_input_right_valid
  8. L20
    exact h
05Separate the logical casesL21–21

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

  1. L21
    cases hB
06Establish hpL22–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 hp : x*x1=0
  2. L23
    specialize gaussian_norm_functional (0)
  3. L24
    specialize gaussian_norm_functional (x*x1)
  4. L25
    specialize gaussian_norm_functional (0)
  5. L26
    apply gaussian_norm_functional
  6. L27
    specialize gaussian_norm_multiply (a)
  7. L28
    specialize gaussian_norm_multiply (b)
  8. L29
    specialize gaussian_norm_multiply (0)
  9. L30
    specialize gaussian_norm_multiply (x)
  10. L31
    specialize gaussian_norm_multiply (x1)
07Use earlier factsL32–36

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

  1. L32
    apply gaussian_norm_multiply
  2. L33
    exact hA_witness
  3. L34
    exact hB_witness
  4. L35
    exact h
  5. L36
    exact gaussian_zero_norm
08Establish hcasesL37–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul eq zero.

  1. L37
    have hcases : x=0 \/ x1=0
  2. L38
    specialize mul_eq_zero (x)
  3. L39
    specialize mul_eq_zero (x1)
  4. L40
    apply mul_eq_zero
  5. L41
    exact hp
09Separate the logical casesL42–43

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

  1. L42
    cases hcases
  2. L43
    left
10Use earlier factsL44–51

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

  1. L44
    specialize gaussian_norm_zero_implies_code_zero (a)
  2. L45
    apply gaussian_norm_zero_implies_code_zero
  3. L46
    specialize gaussian_norm_value_transport (a)
  4. L47
    specialize gaussian_norm_value_transport (x)
  5. L48
    specialize gaussian_norm_value_transport (0)
  6. L49
    apply gaussian_norm_value_transport
  7. L50
    exact hcases_left
  8. L51
    exact hA_witness
11Separate the logical casesL52–52

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

  1. L52
    right
12Use earlier factsL53–60

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

  1. L53
    specialize gaussian_norm_zero_implies_code_zero (b)
  2. L54
    apply gaussian_norm_zero_implies_code_zero
  3. L55
    specialize gaussian_norm_value_transport (b)
  4. L56
    specialize gaussian_norm_value_transport (x1)
  5. L57
    specialize gaussian_norm_value_transport (0)
  6. L58
    apply gaussian_norm_value_transport
  7. L59
    exact hcases_right
  8. L60
    exact hB_witness

Library-wide reading audit

Original exact command ledger · 60 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004have hA : exists N. (exists ge_norm_rp_zero_product_first ge_norm_rn_zero_product_first ge_norm_ip_zero_product_first ge_norm_in_zero_product_first. ((exists ge_representation_real_code_zero_product_firstrepresentation ge_representation_imaginary_code_zero_product_firstrepresentation. (((a) = ((ge_representation_real_code_zero_product_firstrepresentation) + (ge_representation_imaginary_code_zero_product_firstrepresentation)) * S ((ge_representation_real_code_zero_product_firstrepresentation) + (ge_representation_imaginary_code_zero_product_firstrepresentation)) + ((ge_representation_imaginary_code_zero_product_firstrepresentation) + (ge_representation_imaginary_code_zero_product_firstrepresentation))) /\ ((exists ge_balance_positive_zero_product_firstrepresentationreal ge_balance_negative_zero_product_firstrepresentationreal. (((((ge_representation_real_code_zero_product_firstrepresentation) = 2 * (ge_balance_positive_zero_product_firstrepresentationreal) /\ (ge_balance_negative_zero_product_firstrepresentationreal) = 0) \/ exists ge_signed_half_zero_product_firstrepresentationrealdecode. (((ge_representation_real_code_zero_product_firstrepresentation) = 2 * ge_signed_half_zero_product_firstrepresentationrealdecode + 1 /\ (ge_balance_positive_zero_product_firstrepresentationreal) = 0) /\ (ge_balance_negative_zero_product_firstrepresentationreal) = S ge_signed_half_zero_product_firstrepresentationrealdecode))) /\ ((ge_norm_rp_zero_product_first) + ge_balance_negative_zero_product_firstrepresentationreal = (ge_norm_rn_zero_product_first) + ge_balance_positive_zero_product_firstrepresentationreal))) /\ (exists ge_balance_positive_zero_product_firstrepresentationimaginary ge_balance_negative_zero_product_firstrepresentationimaginary. (((((ge_representation_imaginary_code_zero_product_firstrepresentation) = 2 * (ge_balance_positive_zero_product_firstrepresentationimaginary) /\ (ge_balance_negative_zero_product_firstrepresentationimaginary) = 0) \/ exists ge_signed_half_zero_product_firstrepresentationimaginarydecode. (((ge_representation_imaginary_code_zero_product_firstrepresentation) = 2 * ge_signed_half_zero_product_firstrepresentationimaginarydecode + 1 /\ (ge_balance_positive_zero_product_firstrepresentationimaginary) = 0) /\ (ge_balance_negative_zero_product_firstrepresentationimaginary) = S ge_signed_half_zero_product_firstrepresentationimaginarydecode))) /\ ((ge_norm_ip_zero_product_first) + ge_balance_negative_zero_product_firstrepresentationimaginary = (ge_norm_in_zero_product_first) + ge_balance_positive_zero_product_firstrepresentationimaginary)))))) /\ (exists ge_real_square_zero_product_firstsquare ge_imaginary_square_zero_product_firstsquare. ((((((ge_norm_rp_zero_product_first) * (ge_norm_rp_zero_product_first))) + (((ge_norm_rn_zero_product_first) * (ge_norm_rn_zero_product_first)))) = ((ge_real_square_zero_product_firstsquare) + (((((ge_norm_rp_zero_product_first) * (ge_norm_rn_zero_product_first))) + (((ge_norm_rn_zero_product_first) * (ge_norm_rp_zero_product_first))))))) /\ ((((((ge_norm_ip_zero_product_first) * (ge_norm_ip_zero_product_first))) + (((ge_norm_in_zero_product_first) * (ge_norm_in_zero_product_first)))) = ((ge_imaginary_square_zero_product_firstsquare) + (((((ge_norm_ip_zero_product_first) * (ge_norm_in_zero_product_first))) + (((ge_norm_in_zero_product_first) * (ge_norm_ip_zero_product_first))))))) /\ ((N) = ge_real_square_zero_product_firstsquare + ge_imaginary_square_zero_product_firstsquare))))))
  5. 0005specialize gaussian_norm_exists (a)
  6. 0006apply gaussian_norm_exists
  7. 0007specialize gaussian_multiply_input_left_valid (a)
  8. 0008specialize gaussian_multiply_input_left_valid (b)
  9. 0009specialize gaussian_multiply_input_left_valid (0)
  10. 0010apply gaussian_multiply_input_left_valid
  11. 0011exact h
  12. 0012cases hA
  13. 0013have hB : exists M. (exists ge_norm_rp_zero_product_second ge_norm_rn_zero_product_second ge_norm_ip_zero_product_second ge_norm_in_zero_product_second. ((exists ge_representation_real_code_zero_product_secondrepresentation ge_representation_imaginary_code_zero_product_secondrepresentation. (((b) = ((ge_representation_real_code_zero_product_secondrepresentation) + (ge_representation_imaginary_code_zero_product_secondrepresentation)) * S ((ge_representation_real_code_zero_product_secondrepresentation) + (ge_representation_imaginary_code_zero_product_secondrepresentation)) + ((ge_representation_imaginary_code_zero_product_secondrepresentation) + (ge_representation_imaginary_code_zero_product_secondrepresentation))) /\ ((exists ge_balance_positive_zero_product_secondrepresentationreal ge_balance_negative_zero_product_secondrepresentationreal. (((((ge_representation_real_code_zero_product_secondrepresentation) = 2 * (ge_balance_positive_zero_product_secondrepresentationreal) /\ (ge_balance_negative_zero_product_secondrepresentationreal) = 0) \/ exists ge_signed_half_zero_product_secondrepresentationrealdecode. (((ge_representation_real_code_zero_product_secondrepresentation) = 2 * ge_signed_half_zero_product_secondrepresentationrealdecode + 1 /\ (ge_balance_positive_zero_product_secondrepresentationreal) = 0) /\ (ge_balance_negative_zero_product_secondrepresentationreal) = S ge_signed_half_zero_product_secondrepresentationrealdecode))) /\ ((ge_norm_rp_zero_product_second) + ge_balance_negative_zero_product_secondrepresentationreal = (ge_norm_rn_zero_product_second) + ge_balance_positive_zero_product_secondrepresentationreal))) /\ (exists ge_balance_positive_zero_product_secondrepresentationimaginary ge_balance_negative_zero_product_secondrepresentationimaginary. (((((ge_representation_imaginary_code_zero_product_secondrepresentation) = 2 * (ge_balance_positive_zero_product_secondrepresentationimaginary) /\ (ge_balance_negative_zero_product_secondrepresentationimaginary) = 0) \/ exists ge_signed_half_zero_product_secondrepresentationimaginarydecode. (((ge_representation_imaginary_code_zero_product_secondrepresentation) = 2 * ge_signed_half_zero_product_secondrepresentationimaginarydecode + 1 /\ (ge_balance_positive_zero_product_secondrepresentationimaginary) = 0) /\ (ge_balance_negative_zero_product_secondrepresentationimaginary) = S ge_signed_half_zero_product_secondrepresentationimaginarydecode))) /\ ((ge_norm_ip_zero_product_second) + ge_balance_negative_zero_product_secondrepresentationimaginary = (ge_norm_in_zero_product_second) + ge_balance_positive_zero_product_secondrepresentationimaginary)))))) /\ (exists ge_real_square_zero_product_secondsquare ge_imaginary_square_zero_product_secondsquare. ((((((ge_norm_rp_zero_product_second) * (ge_norm_rp_zero_product_second))) + (((ge_norm_rn_zero_product_second) * (ge_norm_rn_zero_product_second)))) = ((ge_real_square_zero_product_secondsquare) + (((((ge_norm_rp_zero_product_second) * (ge_norm_rn_zero_product_second))) + (((ge_norm_rn_zero_product_second) * (ge_norm_rp_zero_product_second))))))) /\ ((((((ge_norm_ip_zero_product_second) * (ge_norm_ip_zero_product_second))) + (((ge_norm_in_zero_product_second) * (ge_norm_in_zero_product_second)))) = ((ge_imaginary_square_zero_product_secondsquare) + (((((ge_norm_ip_zero_product_second) * (ge_norm_in_zero_product_second))) + (((ge_norm_in_zero_product_second) * (ge_norm_ip_zero_product_second))))))) /\ ((M) = ge_real_square_zero_product_secondsquare + ge_imaginary_square_zero_product_secondsquare))))))
  14. 0014specialize gaussian_norm_exists (b)
  15. 0015apply gaussian_norm_exists
  16. 0016specialize gaussian_multiply_input_right_valid (a)
  17. 0017specialize gaussian_multiply_input_right_valid (b)
  18. 0018specialize gaussian_multiply_input_right_valid (0)
  19. 0019apply gaussian_multiply_input_right_valid
  20. 0020exact h
  21. 0021cases hB
  22. 0022have hp : x*x1=0
  23. 0023specialize gaussian_norm_functional (0)
  24. 0024specialize gaussian_norm_functional (x*x1)
  25. 0025specialize gaussian_norm_functional (0)
  26. 0026apply gaussian_norm_functional
  27. 0027specialize gaussian_norm_multiply (a)
  28. 0028specialize gaussian_norm_multiply (b)
  29. 0029specialize gaussian_norm_multiply (0)
  30. 0030specialize gaussian_norm_multiply (x)
  31. 0031specialize gaussian_norm_multiply (x1)
  32. 0032apply gaussian_norm_multiply
  33. 0033exact hA_witness
  34. 0034exact hB_witness
  35. 0035exact h
  36. 0036exact gaussian_zero_norm
  37. 0037have hcases : x=0 \/ x1=0
  38. 0038specialize mul_eq_zero (x)
  39. 0039specialize mul_eq_zero (x1)
  40. 0040apply mul_eq_zero
  41. 0041exact hp
  42. 0042cases hcases
  43. 0043left
  44. 0044specialize gaussian_norm_zero_implies_code_zero (a)
  45. 0045apply gaussian_norm_zero_implies_code_zero
  46. 0046specialize gaussian_norm_value_transport (a)
  47. 0047specialize gaussian_norm_value_transport (x)
  48. 0048specialize gaussian_norm_value_transport (0)
  49. 0049apply gaussian_norm_value_transport
  50. 0050exact hcases_left
  51. 0051exact hA_witness
  52. 0052right
  53. 0053specialize gaussian_norm_zero_implies_code_zero (b)
  54. 0054apply gaussian_norm_zero_implies_code_zero
  55. 0055specialize gaussian_norm_value_transport (b)
  56. 0056specialize gaussian_norm_value_transport (x1)
  57. 0057specialize gaussian_norm_value_transport (0)
  58. 0058apply gaussian_norm_value_transport
  59. 0059exact hcases_right
  60. 0060exact hB_witness