GF0053

gaussian_divides_decidable

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

Constructively decide actual Gaussian divisibility by computing Euclidean quotient/remainder data; handle a zero divisor explicitly.

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 d z. (exists ge_real_positive_decision_divisor ge_real_negative_decision_divisor ge_imaginary_positive_decision_divisor ge_imaginary_negative_decision_divisor. (exists ge_real_code_decision_divisordecode ge_imaginary_code_decision_divisordecode. (((d) = ((ge_real_code_decision_divisordecode) + (ge_imaginary_code_decision_divisordecode)) * S ((ge_real_code_decision_divisordecode) + (ge_imaginary_code_decision_divisordecode)) + ((ge_imaginary_code_decision_divisordecode) + (ge_imaginary_code_decision_divisordecode))) /\ (((((ge_real_code_decision_divisordecode) = 2 * (ge_real_positive_decision_divisor) /\ (ge_real_negative_decision_divisor) = 0) \/ exists ge_signed_half_ge_decision_divisordecode_real. (((ge_real_code_decision_divisordecode) = 2 * ge_signed_half_ge_decision_divisordecode_real + 1 /\ (ge_real_positive_decision_divisor) = 0) /\ (ge_real_negative_decision_divisor) = S ge_signed_half_ge_decision_divisordecode_real))) /\ ((((ge_imaginary_code_decision_divisordecode) = 2 * (ge_imaginary_positive_decision_divisor) /\ (ge_imaginary_negative_decision_divisor) = 0) \/ exists ge_signed_half_ge_decision_divisordecode_imaginary. (((ge_imaginary_code_decision_divisordecode) = 2 * ge_signed_half_ge_decision_divisordecode_imaginary + 1 /\ (ge_imaginary_positive_decision_divisor) = 0) /\ (ge_imaginary_negative_decision_divisor) = S ge_signed_half_ge_decision_divisordecode_imaginary))))))) -> (exists ge_real_positive_decision_dividend ge_real_negative_decision_dividend ge_imaginary_positive_decision_dividend ge_imaginary_negative_decision_dividend. (exists ge_real_code_decision_dividenddecode ge_imaginary_code_decision_dividenddecode. (((z) = ((ge_real_code_decision_dividenddecode) + (ge_imaginary_code_decision_dividenddecode)) * S ((ge_real_code_decision_dividenddecode) + (ge_imaginary_code_decision_dividenddecode)) + ((ge_imaginary_code_decision_dividenddecode) + (ge_imaginary_code_decision_dividenddecode))) /\ (((((ge_real_code_decision_dividenddecode) = 2 * (ge_real_positive_decision_dividend) /\ (ge_real_negative_decision_dividend) = 0) \/ exists ge_signed_half_ge_decision_dividenddecode_real. (((ge_real_code_decision_dividenddecode) = 2 * ge_signed_half_ge_decision_dividenddecode_real + 1 /\ (ge_real_positive_decision_dividend) = 0) /\ (ge_real_negative_decision_dividend) = S ge_signed_half_ge_decision_dividenddecode_real))) /\ ((((ge_imaginary_code_decision_dividenddecode) = 2 * (ge_imaginary_positive_decision_dividend) /\ (ge_imaginary_negative_decision_dividend) = 0) \/ exists ge_signed_half_ge_decision_dividenddecode_imaginary. (((ge_imaginary_code_decision_dividenddecode) = 2 * ge_signed_half_ge_decision_dividenddecode_imaginary + 1 /\ (ge_imaginary_positive_decision_dividend) = 0) /\ (ge_imaginary_negative_decision_dividend) = S ge_signed_half_ge_decision_dividenddecode_imaginary))))))) -> (exists gr_quotient_decision_yes. (exists ge_first_rp_decision_yesproduct ge_first_rn_decision_yesproduct ge_first_ip_decision_yesproduct ge_first_in_decision_yesproduct ge_second_rp_decision_yesproduct ge_second_rn_decision_yesproduct ge_second_ip_decision_yesproduct ge_second_in_decision_yesproduct. ((exists ge_representation_real_code_decision_yesproductfirst ge_representation_imaginary_code_decision_yesproductfirst. (((d) = ((ge_representation_real_code_decision_yesproductfirst) + (ge_representation_imaginary_code_decision_yesproductfirst)) * S ((ge_representation_real_code_decision_yesproductfirst) + (ge_representation_imaginary_code_decision_yesproductfirst)) + ((ge_representation_imaginary_code_decision_yesproductfirst) + (ge_representation_imaginary_code_decision_yesproductfirst))) /\ ((exists ge_balance_positive_decision_yesproductfirstreal ge_balance_negative_decision_yesproductfirstreal. (((((ge_representation_real_code_decision_yesproductfirst) = 2 * (ge_balance_positive_decision_yesproductfirstreal) /\ (ge_balance_negative_decision_yesproductfirstreal) = 0) \/ exists ge_signed_half_decision_yesproductfirstrealdecode. (((ge_representation_real_code_decision_yesproductfirst) = 2 * ge_signed_half_decision_yesproductfirstrealdecode + 1 /\ (ge_balance_positive_decision_yesproductfirstreal) = 0) /\ (ge_balance_negative_decision_yesproductfirstreal) = S ge_signed_half_decision_yesproductfirstrealdecode))) /\ ((ge_first_rp_decision_yesproduct) + ge_balance_negative_decision_yesproductfirstreal = (ge_first_rn_decision_yesproduct) + ge_balance_positive_decision_yesproductfirstreal))) /\ (exists ge_balance_positive_decision_yesproductfirstimaginary ge_balance_negative_decision_yesproductfirstimaginary. (((((ge_representation_imaginary_code_decision_yesproductfirst) = 2 * (ge_balance_positive_decision_yesproductfirstimaginary) /\ (ge_balance_negative_decision_yesproductfirstimaginary) = 0) \/ exists ge_signed_half_decision_yesproductfirstimaginarydecode. (((ge_representation_imaginary_code_decision_yesproductfirst) = 2 * ge_signed_half_decision_yesproductfirstimaginarydecode + 1 /\ (ge_balance_positive_decision_yesproductfirstimaginary) = 0) /\ (ge_balance_negative_decision_yesproductfirstimaginary) = S ge_signed_half_decision_yesproductfirstimaginarydecode))) /\ ((ge_first_ip_decision_yesproduct) + ge_balance_negative_decision_yesproductfirstimaginary = (ge_first_in_decision_yesproduct) + ge_balance_positive_decision_yesproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_decision_yesproductsecond ge_representation_imaginary_code_decision_yesproductsecond. (((gr_quotient_decision_yes) = ((ge_representation_real_code_decision_yesproductsecond) + (ge_representation_imaginary_code_decision_yesproductsecond)) * S ((ge_representation_real_code_decision_yesproductsecond) + (ge_representation_imaginary_code_decision_yesproductsecond)) + ((ge_representation_imaginary_code_decision_yesproductsecond) + (ge_representation_imaginary_code_decision_yesproductsecond))) /\ ((exists ge_balance_positive_decision_yesproductsecondreal ge_balance_negative_decision_yesproductsecondreal. (((((ge_representation_real_code_decision_yesproductsecond) = 2 * (ge_balance_positive_decision_yesproductsecondreal) /\ (ge_balance_negative_decision_yesproductsecondreal) = 0) \/ exists ge_signed_half_decision_yesproductsecondrealdecode. (((ge_representation_real_code_decision_yesproductsecond) = 2 * ge_signed_half_decision_yesproductsecondrealdecode + 1 /\ (ge_balance_positive_decision_yesproductsecondreal) = 0) /\ (ge_balance_negative_decision_yesproductsecondreal) = S ge_signed_half_decision_yesproductsecondrealdecode))) /\ ((ge_second_rp_decision_yesproduct) + ge_balance_negative_decision_yesproductsecondreal = (ge_second_rn_decision_yesproduct) + ge_balance_positive_decision_yesproductsecondreal))) /\ (exists ge_balance_positive_decision_yesproductsecondimaginary ge_balance_negative_decision_yesproductsecondimaginary. (((((ge_representation_imaginary_code_decision_yesproductsecond) = 2 * (ge_balance_positive_decision_yesproductsecondimaginary) /\ (ge_balance_negative_decision_yesproductsecondimaginary) = 0) \/ exists ge_signed_half_decision_yesproductsecondimaginarydecode. (((ge_representation_imaginary_code_decision_yesproductsecond) = 2 * ge_signed_half_decision_yesproductsecondimaginarydecode + 1 /\ (ge_balance_positive_decision_yesproductsecondimaginary) = 0) /\ (ge_balance_negative_decision_yesproductsecondimaginary) = S ge_signed_half_decision_yesproductsecondimaginarydecode))) /\ ((ge_second_ip_decision_yesproduct) + ge_balance_negative_decision_yesproductsecondimaginary = (ge_second_in_decision_yesproduct) + ge_balance_positive_decision_yesproductsecondimaginary)))))) /\ (exists ge_representation_real_code_decision_yesproductoutput ge_representation_imaginary_code_decision_yesproductoutput. (((z) = ((ge_representation_real_code_decision_yesproductoutput) + (ge_representation_imaginary_code_decision_yesproductoutput)) * S ((ge_representation_real_code_decision_yesproductoutput) + (ge_representation_imaginary_code_decision_yesproductoutput)) + ((ge_representation_imaginary_code_decision_yesproductoutput) + (ge_representation_imaginary_code_decision_yesproductoutput))) /\ ((exists ge_balance_positive_decision_yesproductoutputreal ge_balance_negative_decision_yesproductoutputreal. (((((ge_representation_real_code_decision_yesproductoutput) = 2 * (ge_balance_positive_decision_yesproductoutputreal) /\ (ge_balance_negative_decision_yesproductoutputreal) = 0) \/ exists ge_signed_half_decision_yesproductoutputrealdecode. (((ge_representation_real_code_decision_yesproductoutput) = 2 * ge_signed_half_decision_yesproductoutputrealdecode + 1 /\ (ge_balance_positive_decision_yesproductoutputreal) = 0) /\ (ge_balance_negative_decision_yesproductoutputreal) = S ge_signed_half_decision_yesproductoutputrealdecode))) /\ ((((((((ge_first_rp_decision_yesproduct) * (ge_second_rp_decision_yesproduct))) + (((ge_first_rn_decision_yesproduct) * (ge_second_rn_decision_yesproduct))))) + (((((ge_first_ip_decision_yesproduct) * (ge_second_in_decision_yesproduct))) + (((ge_first_in_decision_yesproduct) * (ge_second_ip_decision_yesproduct))))))) + ge_balance_negative_decision_yesproductoutputreal = (((((((ge_first_rp_decision_yesproduct) * (ge_second_rn_decision_yesproduct))) + (((ge_first_rn_decision_yesproduct) * (ge_second_rp_decision_yesproduct))))) + (((((ge_first_ip_decision_yesproduct) * (ge_second_ip_decision_yesproduct))) + (((ge_first_in_decision_yesproduct) * (ge_second_in_decision_yesproduct))))))) + ge_balance_positive_decision_yesproductoutputreal))) /\ (exists ge_balance_positive_decision_yesproductoutputimaginary ge_balance_negative_decision_yesproductoutputimaginary. (((((ge_representation_imaginary_code_decision_yesproductoutput) = 2 * (ge_balance_positive_decision_yesproductoutputimaginary) /\ (ge_balance_negative_decision_yesproductoutputimaginary) = 0) \/ exists ge_signed_half_decision_yesproductoutputimaginarydecode. (((ge_representation_imaginary_code_decision_yesproductoutput) = 2 * ge_signed_half_decision_yesproductoutputimaginarydecode + 1 /\ (ge_balance_positive_decision_yesproductoutputimaginary) = 0) /\ (ge_balance_negative_decision_yesproductoutputimaginary) = S ge_signed_half_decision_yesproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_decision_yesproduct) * (ge_second_ip_decision_yesproduct))) + (((ge_first_rn_decision_yesproduct) * (ge_second_in_decision_yesproduct))))) + (((((ge_first_ip_decision_yesproduct) * (ge_second_rp_decision_yesproduct))) + (((ge_first_in_decision_yesproduct) * (ge_second_rn_decision_yesproduct))))))) + ge_balance_negative_decision_yesproductoutputimaginary = (((((((ge_first_rp_decision_yesproduct) * (ge_second_in_decision_yesproduct))) + (((ge_first_rn_decision_yesproduct) * (ge_second_ip_decision_yesproduct))))) + (((((ge_first_ip_decision_yesproduct) * (ge_second_rn_decision_yesproduct))) + (((ge_first_in_decision_yesproduct) * (ge_second_rp_decision_yesproduct))))))) + ge_balance_positive_decision_yesproductoutputimaginary)))))))))) \/ ~(exists gr_quotient_decision_no. (exists ge_first_rp_decision_noproduct ge_first_rn_decision_noproduct ge_first_ip_decision_noproduct ge_first_in_decision_noproduct ge_second_rp_decision_noproduct ge_second_rn_decision_noproduct ge_second_ip_decision_noproduct ge_second_in_decision_noproduct. ((exists ge_representation_real_code_decision_noproductfirst ge_representation_imaginary_code_decision_noproductfirst. (((d) = ((ge_representation_real_code_decision_noproductfirst) + (ge_representation_imaginary_code_decision_noproductfirst)) * S ((ge_representation_real_code_decision_noproductfirst) + (ge_representation_imaginary_code_decision_noproductfirst)) + ((ge_representation_imaginary_code_decision_noproductfirst) + (ge_representation_imaginary_code_decision_noproductfirst))) /\ ((exists ge_balance_positive_decision_noproductfirstreal ge_balance_negative_decision_noproductfirstreal. (((((ge_representation_real_code_decision_noproductfirst) = 2 * (ge_balance_positive_decision_noproductfirstreal) /\ (ge_balance_negative_decision_noproductfirstreal) = 0) \/ exists ge_signed_half_decision_noproductfirstrealdecode. (((ge_representation_real_code_decision_noproductfirst) = 2 * ge_signed_half_decision_noproductfirstrealdecode + 1 /\ (ge_balance_positive_decision_noproductfirstreal) = 0) /\ (ge_balance_negative_decision_noproductfirstreal) = S ge_signed_half_decision_noproductfirstrealdecode))) /\ ((ge_first_rp_decision_noproduct) + ge_balance_negative_decision_noproductfirstreal = (ge_first_rn_decision_noproduct) + ge_balance_positive_decision_noproductfirstreal))) /\ (exists ge_balance_positive_decision_noproductfirstimaginary ge_balance_negative_decision_noproductfirstimaginary. (((((ge_representation_imaginary_code_decision_noproductfirst) = 2 * (ge_balance_positive_decision_noproductfirstimaginary) /\ (ge_balance_negative_decision_noproductfirstimaginary) = 0) \/ exists ge_signed_half_decision_noproductfirstimaginarydecode. (((ge_representation_imaginary_code_decision_noproductfirst) = 2 * ge_signed_half_decision_noproductfirstimaginarydecode + 1 /\ (ge_balance_positive_decision_noproductfirstimaginary) = 0) /\ (ge_balance_negative_decision_noproductfirstimaginary) = S ge_signed_half_decision_noproductfirstimaginarydecode))) /\ ((ge_first_ip_decision_noproduct) + ge_balance_negative_decision_noproductfirstimaginary = (ge_first_in_decision_noproduct) + ge_balance_positive_decision_noproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_decision_noproductsecond ge_representation_imaginary_code_decision_noproductsecond. (((gr_quotient_decision_no) = ((ge_representation_real_code_decision_noproductsecond) + (ge_representation_imaginary_code_decision_noproductsecond)) * S ((ge_representation_real_code_decision_noproductsecond) + (ge_representation_imaginary_code_decision_noproductsecond)) + ((ge_representation_imaginary_code_decision_noproductsecond) + (ge_representation_imaginary_code_decision_noproductsecond))) /\ ((exists ge_balance_positive_decision_noproductsecondreal ge_balance_negative_decision_noproductsecondreal. (((((ge_representation_real_code_decision_noproductsecond) = 2 * (ge_balance_positive_decision_noproductsecondreal) /\ (ge_balance_negative_decision_noproductsecondreal) = 0) \/ exists ge_signed_half_decision_noproductsecondrealdecode. (((ge_representation_real_code_decision_noproductsecond) = 2 * ge_signed_half_decision_noproductsecondrealdecode + 1 /\ (ge_balance_positive_decision_noproductsecondreal) = 0) /\ (ge_balance_negative_decision_noproductsecondreal) = S ge_signed_half_decision_noproductsecondrealdecode))) /\ ((ge_second_rp_decision_noproduct) + ge_balance_negative_decision_noproductsecondreal = (ge_second_rn_decision_noproduct) + ge_balance_positive_decision_noproductsecondreal))) /\ (exists ge_balance_positive_decision_noproductsecondimaginary ge_balance_negative_decision_noproductsecondimaginary. (((((ge_representation_imaginary_code_decision_noproductsecond) = 2 * (ge_balance_positive_decision_noproductsecondimaginary) /\ (ge_balance_negative_decision_noproductsecondimaginary) = 0) \/ exists ge_signed_half_decision_noproductsecondimaginarydecode. (((ge_representation_imaginary_code_decision_noproductsecond) = 2 * ge_signed_half_decision_noproductsecondimaginarydecode + 1 /\ (ge_balance_positive_decision_noproductsecondimaginary) = 0) /\ (ge_balance_negative_decision_noproductsecondimaginary) = S ge_signed_half_decision_noproductsecondimaginarydecode))) /\ ((ge_second_ip_decision_noproduct) + ge_balance_negative_decision_noproductsecondimaginary = (ge_second_in_decision_noproduct) + ge_balance_positive_decision_noproductsecondimaginary)))))) /\ (exists ge_representation_real_code_decision_noproductoutput ge_representation_imaginary_code_decision_noproductoutput. (((z) = ((ge_representation_real_code_decision_noproductoutput) + (ge_representation_imaginary_code_decision_noproductoutput)) * S ((ge_representation_real_code_decision_noproductoutput) + (ge_representation_imaginary_code_decision_noproductoutput)) + ((ge_representation_imaginary_code_decision_noproductoutput) + (ge_representation_imaginary_code_decision_noproductoutput))) /\ ((exists ge_balance_positive_decision_noproductoutputreal ge_balance_negative_decision_noproductoutputreal. (((((ge_representation_real_code_decision_noproductoutput) = 2 * (ge_balance_positive_decision_noproductoutputreal) /\ (ge_balance_negative_decision_noproductoutputreal) = 0) \/ exists ge_signed_half_decision_noproductoutputrealdecode. (((ge_representation_real_code_decision_noproductoutput) = 2 * ge_signed_half_decision_noproductoutputrealdecode + 1 /\ (ge_balance_positive_decision_noproductoutputreal) = 0) /\ (ge_balance_negative_decision_noproductoutputreal) = S ge_signed_half_decision_noproductoutputrealdecode))) /\ ((((((((ge_first_rp_decision_noproduct) * (ge_second_rp_decision_noproduct))) + (((ge_first_rn_decision_noproduct) * (ge_second_rn_decision_noproduct))))) + (((((ge_first_ip_decision_noproduct) * (ge_second_in_decision_noproduct))) + (((ge_first_in_decision_noproduct) * (ge_second_ip_decision_noproduct))))))) + ge_balance_negative_decision_noproductoutputreal = (((((((ge_first_rp_decision_noproduct) * (ge_second_rn_decision_noproduct))) + (((ge_first_rn_decision_noproduct) * (ge_second_rp_decision_noproduct))))) + (((((ge_first_ip_decision_noproduct) * (ge_second_ip_decision_noproduct))) + (((ge_first_in_decision_noproduct) * (ge_second_in_decision_noproduct))))))) + ge_balance_positive_decision_noproductoutputreal))) /\ (exists ge_balance_positive_decision_noproductoutputimaginary ge_balance_negative_decision_noproductoutputimaginary. (((((ge_representation_imaginary_code_decision_noproductoutput) = 2 * (ge_balance_positive_decision_noproductoutputimaginary) /\ (ge_balance_negative_decision_noproductoutputimaginary) = 0) \/ exists ge_signed_half_decision_noproductoutputimaginarydecode. (((ge_representation_imaginary_code_decision_noproductoutput) = 2 * ge_signed_half_decision_noproductoutputimaginarydecode + 1 /\ (ge_balance_positive_decision_noproductoutputimaginary) = 0) /\ (ge_balance_negative_decision_noproductoutputimaginary) = S ge_signed_half_decision_noproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_decision_noproduct) * (ge_second_ip_decision_noproduct))) + (((ge_first_rn_decision_noproduct) * (ge_second_in_decision_noproduct))))) + (((((ge_first_ip_decision_noproduct) * (ge_second_rp_decision_noproduct))) + (((ge_first_in_decision_noproduct) * (ge_second_rn_decision_noproduct))))))) + ge_balance_negative_decision_noproductoutputimaginary = (((((((ge_first_rp_decision_noproduct) * (ge_second_in_decision_noproduct))) + (((ge_first_rn_decision_noproduct) * (ge_second_ip_decision_noproduct))))) + (((((ge_first_ip_decision_noproduct) * (ge_second_rn_decision_noproduct))) + (((ge_first_in_decision_noproduct) * (ge_second_rp_decision_noproduct))))))) + ge_balance_positive_decision_noproductoutputimaginary))))))))))

Constructive proof overview

Generated structural guide

Constructively decide actual Gaussian divisibility by computing Euclidean quotient/remainder data; handle a zero divisor explicitly.

The unchanged tactic script uses 7 declared prerequisites and contains 72 exact native proof lines.

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

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized GF002A gaussian_multiply_zero_right GF000C gaussian_zero_valid GF0047 gaussian_zero_divides_only_zero gaussian_euclidean_division_exists Alpha theorem; checked-use authorized GF0051 gaussian_division_zero_remainder_divides GF0052 gaussian_division_divisible_remainder_zero

Direct dependents

GF0074 gaussian_proper_norm_divisor_decidable

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

72 script commands · 22 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 zero rightgaussian zero validgaussian zero divides only zerogaussian division zero remainder dividesgaussian division divisible remainder zero

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

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

  1. L1
    intro d
  2. L2
    intro z
  3. L3
    intro hd
  4. L4
    intro hz
02Establish hdcL5–8

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

  1. L5
    have hdc : d=0 \/ ~(d=0)
  2. L6
    specialize eq_decidable (d)
  3. L7
    specialize eq_decidable (0)
  4. L8
    apply eq_decidable
03Separate the logical casesL9–9

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

  1. L9
    cases hdc
04Establish hzcL10–13

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

  1. L10
    have hzc : z=0 \/ ~(z=0)
  2. L11
    specialize eq_decidable (z)
  3. L12
    specialize eq_decidable (0)
  4. L13
    apply eq_decidable
05Separate the logical casesL14–15

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

  1. L14
    cases hzc
  2. L15
    left
06Construct an explicit witnessL16–16

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

  1. L16
    exists (0)
07Calculate and transport equalitiesL17–18

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

  1. L17
    rewrite hdc_left
  2. L18
    rewrite hzc_left
08Use earlier factsL19–21

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

  1. L19
    specialize gaussian_multiply_zero_right (0)
  2. L20
    apply gaussian_multiply_zero_right
  3. L21
    exact gaussian_zero_valid
09Separate the logical casesL22–22

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

  1. L22
    right
10Fix variables and assumptionsL23–23

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

  1. L23
    intro hdiv
11Use earlier factsL24–26

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

  1. L24
    apply hzc_right
  2. L25
    specialize gaussian_zero_divides_only_zero (z)
  3. L26
    apply gaussian_zero_divides_only_zero
12Calculate and transport equalitiesL27–27

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

  1. L27
    rewrite hdc_left at hdiv
13Use earlier factsL28–28

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

  1. L28
    exact hdiv
14Establish hexL29–35

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

  1. L29
    have hex : ∃ q. ∃ r. ∃ U. ∃ V. ZPairValid(q) ∧ (ZPairValid(r) ∧ ((∃ x. GMul(d,q,x) ∧ ZPairAdd(x,r,z)) ∧ (GNorm(r,U) ∧ (GNorm(d,V) ∧ Lt(U,V)))))Definitions: ZPairValidGNormZPairAddGMulLt
  2. L30
    specialize gaussian_euclidean_division_exists (z)
  3. L31
    specialize gaussian_euclidean_division_exists (d)
  4. L32
    apply gaussian_euclidean_division_exists
  5. L33
    exact hz
  6. L34
    exact hd
  7. L35
    exact hdc_right
15Separate the logical casesL36–44

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

  1. L36
    cases hex
  2. L37
    cases hex_witness
  3. L38
    cases hex_witness_witness
  4. L39
    cases hex_witness_witness_witness
  5. L40
    cases hex_witness_witness_witness_witness
  6. L41
    cases hex_witness_witness_witness_witness_right
  7. L42
    cases hex_witness_witness_witness_witness_right_right
  8. L43
    cases hex_witness_witness_witness_witness_right_right_right
  9. L44
    cases hex_witness_witness_witness_witness_right_right_right_right
16Establish hrcL45–48

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

  1. L45
    have hrc : x1=0 \/ ~(x1=0)
  2. L46
    specialize eq_decidable (x1)
  3. L47
    specialize eq_decidable (0)
  4. L48
    apply eq_decidable
17Separate the logical casesL49–50

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

  1. L49
    cases hrc
  2. L50
    left
18Use earlier factsL51–57

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

  1. L51
    specialize gaussian_division_zero_remainder_divides (z)
  2. L52
    specialize gaussian_division_zero_remainder_divides (d)
  3. L53
    specialize gaussian_division_zero_remainder_divides (x)
  4. L54
    specialize gaussian_division_zero_remainder_divides (x1)
  5. L55
    apply gaussian_division_zero_remainder_divides
  6. L56
    exact hex_witness_witness_witness_witness_right_right_left
  7. L57
    exact hrc_left
19Separate the logical casesL58–58

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

  1. L58
    right
20Fix variables and assumptionsL59–59

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

  1. L59
    intro hdiv
21Use earlier factsL60–69

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

  1. L60
    apply hrc_right
  2. L61
    specialize gaussian_division_divisible_remainder_zero (z)
  3. L62
    specialize gaussian_division_divisible_remainder_zero (d)
  4. L63
    specialize gaussian_division_divisible_remainder_zero (x)
  5. L64
    specialize gaussian_division_divisible_remainder_zero (x1)
  6. L65
    specialize gaussian_division_divisible_remainder_zero (x2)
  7. L66
    specialize gaussian_division_divisible_remainder_zero (x3)
  8. L67
    apply gaussian_division_divisible_remainder_zero
  9. L68
    exact hex_witness_witness_witness_witness_right_right_left
  10. L69
    exact hex_witness_witness_witness_witness_right_right_right_left
22Use earlier factsL70–72

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

  1. L70
    exact hex_witness_witness_witness_witness_right_right_right_right_left
  2. L71
    exact hex_witness_witness_witness_witness_right_right_right_right_right
  3. L72
    exact hdiv

Library-wide reading audit

Original exact command ledger · 72 lines
  1. 0001intro d
  2. 0002intro z
  3. 0003intro hd
  4. 0004intro hz
  5. 0005have hdc : d=0 \/ ~(d=0)
  6. 0006specialize eq_decidable (d)
  7. 0007specialize eq_decidable (0)
  8. 0008apply eq_decidable
  9. 0009cases hdc
  10. 0010have hzc : z=0 \/ ~(z=0)
  11. 0011specialize eq_decidable (z)
  12. 0012specialize eq_decidable (0)
  13. 0013apply eq_decidable
  14. 0014cases hzc
  15. 0015left
  16. 0016exists (0)
  17. 0017rewrite hdc_left
  18. 0018rewrite hzc_left
  19. 0019specialize gaussian_multiply_zero_right (0)
  20. 0020apply gaussian_multiply_zero_right
  21. 0021exact gaussian_zero_valid
  22. 0022right
  23. 0023intro hdiv
  24. 0024apply hzc_right
  25. 0025specialize gaussian_zero_divides_only_zero (z)
  26. 0026apply gaussian_zero_divides_only_zero
  27. 0027rewrite hdc_left at hdiv
  28. 0028exact hdiv
  29. 0029have hex : exists q r U V. (((exists ge_real_positive_decision_actual_divisionquotient ge_real_negative_decision_actual_divisionquotient ge_imaginary_positive_decision_actual_divisionquotient ge_imaginary_negative_decision_actual_divisionquotient. (exists ge_real_code_decision_actual_divisionquotientdecode ge_imaginary_code_decision_actual_divisionquotientdecode. (((q) = ((ge_real_code_decision_actual_divisionquotientdecode) + (ge_imaginary_code_decision_actual_divisionquotientdecode)) * S ((ge_real_code_decision_actual_divisionquotientdecode) + (ge_imaginary_code_decision_actual_divisionquotientdecode)) + ((ge_imaginary_code_decision_actual_divisionquotientdecode) + (ge_imaginary_code_decision_actual_divisionquotientdecode))) /\ (((((ge_real_code_decision_actual_divisionquotientdecode) = 2 * (ge_real_positive_decision_actual_divisionquotient) /\ (ge_real_negative_decision_actual_divisionquotient) = 0) \/ exists ge_signed_half_ge_decision_actual_divisionquotientdecode_real. (((ge_real_code_decision_actual_divisionquotientdecode) = 2 * ge_signed_half_ge_decision_actual_divisionquotientdecode_real + 1 /\ (ge_real_positive_decision_actual_divisionquotient) = 0) /\ (ge_real_negative_decision_actual_divisionquotient) = S ge_signed_half_ge_decision_actual_divisionquotientdecode_real))) /\ ((((ge_imaginary_code_decision_actual_divisionquotientdecode) = 2 * (ge_imaginary_positive_decision_actual_divisionquotient) /\ (ge_imaginary_negative_decision_actual_divisionquotient) = 0) \/ exists ge_signed_half_ge_decision_actual_divisionquotientdecode_imaginary. (((ge_imaginary_code_decision_actual_divisionquotientdecode) = 2 * ge_signed_half_ge_decision_actual_divisionquotientdecode_imaginary + 1 /\ (ge_imaginary_positive_decision_actual_divisionquotient) = 0) /\ (ge_imaginary_negative_decision_actual_divisionquotient) = S ge_signed_half_ge_decision_actual_divisionquotientdecode_imaginary))))))) /\ ((exists ge_real_positive_decision_actual_divisionremainder ge_real_negative_decision_actual_divisionremainder ge_imaginary_positive_decision_actual_divisionremainder ge_imaginary_negative_decision_actual_divisionremainder. (exists ge_real_code_decision_actual_divisionremainderdecode ge_imaginary_code_decision_actual_divisionremainderdecode. (((r) = ((ge_real_code_decision_actual_divisionremainderdecode) + (ge_imaginary_code_decision_actual_divisionremainderdecode)) * S ((ge_real_code_decision_actual_divisionremainderdecode) + (ge_imaginary_code_decision_actual_divisionremainderdecode)) + ((ge_imaginary_code_decision_actual_divisionremainderdecode) + (ge_imaginary_code_decision_actual_divisionremainderdecode))) /\ (((((ge_real_code_decision_actual_divisionremainderdecode) = 2 * (ge_real_positive_decision_actual_divisionremainder) /\ (ge_real_negative_decision_actual_divisionremainder) = 0) \/ exists ge_signed_half_ge_decision_actual_divisionremainderdecode_real. (((ge_real_code_decision_actual_divisionremainderdecode) = 2 * ge_signed_half_ge_decision_actual_divisionremainderdecode_real + 1 /\ (ge_real_positive_decision_actual_divisionremainder) = 0) /\ (ge_real_negative_decision_actual_divisionremainder) = S ge_signed_half_ge_decision_actual_divisionremainderdecode_real))) /\ ((((ge_imaginary_code_decision_actual_divisionremainderdecode) = 2 * (ge_imaginary_positive_decision_actual_divisionremainder) /\ (ge_imaginary_negative_decision_actual_divisionremainder) = 0) \/ exists ge_signed_half_ge_decision_actual_divisionremainderdecode_imaginary. (((ge_imaginary_code_decision_actual_divisionremainderdecode) = 2 * ge_signed_half_ge_decision_actual_divisionremainderdecode_imaginary + 1 /\ (ge_imaginary_positive_decision_actual_divisionremainder) = 0) /\ (ge_imaginary_negative_decision_actual_divisionremainder) = S ge_signed_half_ge_decision_actual_divisionremainderdecode_imaginary))))))) /\ ((exists ge_division_product_decision_actual_divisionequation. ((exists ge_first_rp_decision_actual_divisionequationproduct ge_first_rn_decision_actual_divisionequationproduct ge_first_ip_decision_actual_divisionequationproduct ge_first_in_decision_actual_divisionequationproduct ge_second_rp_decision_actual_divisionequationproduct ge_second_rn_decision_actual_divisionequationproduct ge_second_ip_decision_actual_divisionequationproduct ge_second_in_decision_actual_divisionequationproduct. ((exists ge_representation_real_code_decision_actual_divisionequationproductfirst ge_representation_imaginary_code_decision_actual_divisionequationproductfirst. (((d) = ((ge_representation_real_code_decision_actual_divisionequationproductfirst) + (ge_representation_imaginary_code_decision_actual_divisionequationproductfirst)) * S ((ge_representation_real_code_decision_actual_divisionequationproductfirst) + (ge_representation_imaginary_code_decision_actual_divisionequationproductfirst)) + ((ge_representation_imaginary_code_decision_actual_divisionequationproductfirst) + (ge_representation_imaginary_code_decision_actual_divisionequationproductfirst))) /\ ((exists ge_balance_positive_decision_actual_divisionequationproductfirstreal ge_balance_negative_decision_actual_divisionequationproductfirstreal. (((((ge_representation_real_code_decision_actual_divisionequationproductfirst) = 2 * (ge_balance_positive_decision_actual_divisionequationproductfirstreal) /\ (ge_balance_negative_decision_actual_divisionequationproductfirstreal) = 0) \/ exists ge_signed_half_decision_actual_divisionequationproductfirstrealdecode. (((ge_representation_real_code_decision_actual_divisionequationproductfirst) = 2 * ge_signed_half_decision_actual_divisionequationproductfirstrealdecode + 1 /\ (ge_balance_positive_decision_actual_divisionequationproductfirstreal) = 0) /\ (ge_balance_negative_decision_actual_divisionequationproductfirstreal) = S ge_signed_half_decision_actual_divisionequationproductfirstrealdecode))) /\ ((ge_first_rp_decision_actual_divisionequationproduct) + ge_balance_negative_decision_actual_divisionequationproductfirstreal = (ge_first_rn_decision_actual_divisionequationproduct) + ge_balance_positive_decision_actual_divisionequationproductfirstreal))) /\ (exists ge_balance_positive_decision_actual_divisionequationproductfirstimaginary ge_balance_negative_decision_actual_divisionequationproductfirstimaginary. (((((ge_representation_imaginary_code_decision_actual_divisionequationproductfirst) = 2 * (ge_balance_positive_decision_actual_divisionequationproductfirstimaginary) /\ (ge_balance_negative_decision_actual_divisionequationproductfirstimaginary) = 0) \/ exists ge_signed_half_decision_actual_divisionequationproductfirstimaginarydecode. (((ge_representation_imaginary_code_decision_actual_divisionequationproductfirst) = 2 * ge_signed_half_decision_actual_divisionequationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_decision_actual_divisionequationproductfirstimaginary) = 0) /\ (ge_balance_negative_decision_actual_divisionequationproductfirstimaginary) = S ge_signed_half_decision_actual_divisionequationproductfirstimaginarydecode))) /\ ((ge_first_ip_decision_actual_divisionequationproduct) + ge_balance_negative_decision_actual_divisionequationproductfirstimaginary = (ge_first_in_decision_actual_divisionequationproduct) + ge_balance_positive_decision_actual_divisionequationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_decision_actual_divisionequationproductsecond ge_representation_imaginary_code_decision_actual_divisionequationproductsecond. (((q) = ((ge_representation_real_code_decision_actual_divisionequationproductsecond) + (ge_representation_imaginary_code_decision_actual_divisionequationproductsecond)) * S ((ge_representation_real_code_decision_actual_divisionequationproductsecond) + (ge_representation_imaginary_code_decision_actual_divisionequationproductsecond)) + ((ge_representation_imaginary_code_decision_actual_divisionequationproductsecond) + (ge_representation_imaginary_code_decision_actual_divisionequationproductsecond))) /\ ((exists ge_balance_positive_decision_actual_divisionequationproductsecondreal ge_balance_negative_decision_actual_divisionequationproductsecondreal. (((((ge_representation_real_code_decision_actual_divisionequationproductsecond) = 2 * (ge_balance_positive_decision_actual_divisionequationproductsecondreal) /\ (ge_balance_negative_decision_actual_divisionequationproductsecondreal) = 0) \/ exists ge_signed_half_decision_actual_divisionequationproductsecondrealdecode. (((ge_representation_real_code_decision_actual_divisionequationproductsecond) = 2 * ge_signed_half_decision_actual_divisionequationproductsecondrealdecode + 1 /\ (ge_balance_positive_decision_actual_divisionequationproductsecondreal) = 0) /\ (ge_balance_negative_decision_actual_divisionequationproductsecondreal) = S ge_signed_half_decision_actual_divisionequationproductsecondrealdecode))) /\ ((ge_second_rp_decision_actual_divisionequationproduct) + ge_balance_negative_decision_actual_divisionequationproductsecondreal = (ge_second_rn_decision_actual_divisionequationproduct) + ge_balance_positive_decision_actual_divisionequationproductsecondreal))) /\ (exists ge_balance_positive_decision_actual_divisionequationproductsecondimaginary ge_balance_negative_decision_actual_divisionequationproductsecondimaginary. (((((ge_representation_imaginary_code_decision_actual_divisionequationproductsecond) = 2 * (ge_balance_positive_decision_actual_divisionequationproductsecondimaginary) /\ (ge_balance_negative_decision_actual_divisionequationproductsecondimaginary) = 0) \/ exists ge_signed_half_decision_actual_divisionequationproductsecondimaginarydecode. (((ge_representation_imaginary_code_decision_actual_divisionequationproductsecond) = 2 * ge_signed_half_decision_actual_divisionequationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_decision_actual_divisionequationproductsecondimaginary) = 0) /\ (ge_balance_negative_decision_actual_divisionequationproductsecondimaginary) = S ge_signed_half_decision_actual_divisionequationproductsecondimaginarydecode))) /\ ((ge_second_ip_decision_actual_divisionequationproduct) + ge_balance_negative_decision_actual_divisionequationproductsecondimaginary = (ge_second_in_decision_actual_divisionequationproduct) + ge_balance_positive_decision_actual_divisionequationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_decision_actual_divisionequationproductoutput ge_representation_imaginary_code_decision_actual_divisionequationproductoutput. (((ge_division_product_decision_actual_divisionequation) = ((ge_representation_real_code_decision_actual_divisionequationproductoutput) + (ge_representation_imaginary_code_decision_actual_divisionequationproductoutput)) * S ((ge_representation_real_code_decision_actual_divisionequationproductoutput) + (ge_representation_imaginary_code_decision_actual_divisionequationproductoutput)) + ((ge_representation_imaginary_code_decision_actual_divisionequationproductoutput) + (ge_representation_imaginary_code_decision_actual_divisionequationproductoutput))) /\ ((exists ge_balance_positive_decision_actual_divisionequationproductoutputreal ge_balance_negative_decision_actual_divisionequationproductoutputreal. (((((ge_representation_real_code_decision_actual_divisionequationproductoutput) = 2 * (ge_balance_positive_decision_actual_divisionequationproductoutputreal) /\ (ge_balance_negative_decision_actual_divisionequationproductoutputreal) = 0) \/ exists ge_signed_half_decision_actual_divisionequationproductoutputrealdecode. (((ge_representation_real_code_decision_actual_divisionequationproductoutput) = 2 * ge_signed_half_decision_actual_divisionequationproductoutputrealdecode + 1 /\ (ge_balance_positive_decision_actual_divisionequationproductoutputreal) = 0) /\ (ge_balance_negative_decision_actual_divisionequationproductoutputreal) = S ge_signed_half_decision_actual_divisionequationproductoutputrealdecode))) /\ ((((((((ge_first_rp_decision_actual_divisionequationproduct) * (ge_second_rp_decision_actual_divisionequationproduct))) + (((ge_first_rn_decision_actual_divisionequationproduct) * (ge_second_rn_decision_actual_divisionequationproduct))))) + (((((ge_first_ip_decision_actual_divisionequationproduct) * (ge_second_in_decision_actual_divisionequationproduct))) + (((ge_first_in_decision_actual_divisionequationproduct) * (ge_second_ip_decision_actual_divisionequationproduct))))))) + ge_balance_negative_decision_actual_divisionequationproductoutputreal = (((((((ge_first_rp_decision_actual_divisionequationproduct) * (ge_second_rn_decision_actual_divisionequationproduct))) + (((ge_first_rn_decision_actual_divisionequationproduct) * (ge_second_rp_decision_actual_divisionequationproduct))))) + (((((ge_first_ip_decision_actual_divisionequationproduct) * (ge_second_ip_decision_actual_divisionequationproduct))) + (((ge_first_in_decision_actual_divisionequationproduct) * (ge_second_in_decision_actual_divisionequationproduct))))))) + ge_balance_positive_decision_actual_divisionequationproductoutputreal))) /\ (exists ge_balance_positive_decision_actual_divisionequationproductoutputimaginary ge_balance_negative_decision_actual_divisionequationproductoutputimaginary. (((((ge_representation_imaginary_code_decision_actual_divisionequationproductoutput) = 2 * (ge_balance_positive_decision_actual_divisionequationproductoutputimaginary) /\ (ge_balance_negative_decision_actual_divisionequationproductoutputimaginary) = 0) \/ exists ge_signed_half_decision_actual_divisionequationproductoutputimaginarydecode. (((ge_representation_imaginary_code_decision_actual_divisionequationproductoutput) = 2 * ge_signed_half_decision_actual_divisionequationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_decision_actual_divisionequationproductoutputimaginary) = 0) /\ (ge_balance_negative_decision_actual_divisionequationproductoutputimaginary) = S ge_signed_half_decision_actual_divisionequationproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_decision_actual_divisionequationproduct) * (ge_second_ip_decision_actual_divisionequationproduct))) + (((ge_first_rn_decision_actual_divisionequationproduct) * (ge_second_in_decision_actual_divisionequationproduct))))) + (((((ge_first_ip_decision_actual_divisionequationproduct) * (ge_second_rp_decision_actual_divisionequationproduct))) + (((ge_first_in_decision_actual_divisionequationproduct) * (ge_second_rn_decision_actual_divisionequationproduct))))))) + ge_balance_negative_decision_actual_divisionequationproductoutputimaginary = (((((((ge_first_rp_decision_actual_divisionequationproduct) * (ge_second_in_decision_actual_divisionequationproduct))) + (((ge_first_rn_decision_actual_divisionequationproduct) * (ge_second_ip_decision_actual_divisionequationproduct))))) + (((((ge_first_ip_decision_actual_divisionequationproduct) * (ge_second_rn_decision_actual_divisionequationproduct))) + (((ge_first_in_decision_actual_divisionequationproduct) * (ge_second_rp_decision_actual_divisionequationproduct))))))) + ge_balance_positive_decision_actual_divisionequationproductoutputimaginary))))))))) /\ (exists ge_first_rp_decision_actual_divisionequationsum ge_first_rn_decision_actual_divisionequationsum ge_first_ip_decision_actual_divisionequationsum ge_first_in_decision_actual_divisionequationsum ge_second_rp_decision_actual_divisionequationsum ge_second_rn_decision_actual_divisionequationsum ge_second_ip_decision_actual_divisionequationsum ge_second_in_decision_actual_divisionequationsum. ((exists ge_representation_real_code_decision_actual_divisionequationsumfirst ge_representation_imaginary_code_decision_actual_divisionequationsumfirst. (((ge_division_product_decision_actual_divisionequation) = ((ge_representation_real_code_decision_actual_divisionequationsumfirst) + (ge_representation_imaginary_code_decision_actual_divisionequationsumfirst)) * S ((ge_representation_real_code_decision_actual_divisionequationsumfirst) + (ge_representation_imaginary_code_decision_actual_divisionequationsumfirst)) + ((ge_representation_imaginary_code_decision_actual_divisionequationsumfirst) + (ge_representation_imaginary_code_decision_actual_divisionequationsumfirst))) /\ ((exists ge_balance_positive_decision_actual_divisionequationsumfirstreal ge_balance_negative_decision_actual_divisionequationsumfirstreal. (((((ge_representation_real_code_decision_actual_divisionequationsumfirst) = 2 * (ge_balance_positive_decision_actual_divisionequationsumfirstreal) /\ (ge_balance_negative_decision_actual_divisionequationsumfirstreal) = 0) \/ exists ge_signed_half_decision_actual_divisionequationsumfirstrealdecode. (((ge_representation_real_code_decision_actual_divisionequationsumfirst) = 2 * ge_signed_half_decision_actual_divisionequationsumfirstrealdecode + 1 /\ (ge_balance_positive_decision_actual_divisionequationsumfirstreal) = 0) /\ (ge_balance_negative_decision_actual_divisionequationsumfirstreal) = S ge_signed_half_decision_actual_divisionequationsumfirstrealdecode))) /\ ((ge_first_rp_decision_actual_divisionequationsum) + ge_balance_negative_decision_actual_divisionequationsumfirstreal = (ge_first_rn_decision_actual_divisionequationsum) + ge_balance_positive_decision_actual_divisionequationsumfirstreal))) /\ (exists ge_balance_positive_decision_actual_divisionequationsumfirstimaginary ge_balance_negative_decision_actual_divisionequationsumfirstimaginary. (((((ge_representation_imaginary_code_decision_actual_divisionequationsumfirst) = 2 * (ge_balance_positive_decision_actual_divisionequationsumfirstimaginary) /\ (ge_balance_negative_decision_actual_divisionequationsumfirstimaginary) = 0) \/ exists ge_signed_half_decision_actual_divisionequationsumfirstimaginarydecode. (((ge_representation_imaginary_code_decision_actual_divisionequationsumfirst) = 2 * ge_signed_half_decision_actual_divisionequationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_decision_actual_divisionequationsumfirstimaginary) = 0) /\ (ge_balance_negative_decision_actual_divisionequationsumfirstimaginary) = S ge_signed_half_decision_actual_divisionequationsumfirstimaginarydecode))) /\ ((ge_first_ip_decision_actual_divisionequationsum) + ge_balance_negative_decision_actual_divisionequationsumfirstimaginary = (ge_first_in_decision_actual_divisionequationsum) + ge_balance_positive_decision_actual_divisionequationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_decision_actual_divisionequationsumsecond ge_representation_imaginary_code_decision_actual_divisionequationsumsecond. (((r) = ((ge_representation_real_code_decision_actual_divisionequationsumsecond) + (ge_representation_imaginary_code_decision_actual_divisionequationsumsecond)) * S ((ge_representation_real_code_decision_actual_divisionequationsumsecond) + (ge_representation_imaginary_code_decision_actual_divisionequationsumsecond)) + ((ge_representation_imaginary_code_decision_actual_divisionequationsumsecond) + (ge_representation_imaginary_code_decision_actual_divisionequationsumsecond))) /\ ((exists ge_balance_positive_decision_actual_divisionequationsumsecondreal ge_balance_negative_decision_actual_divisionequationsumsecondreal. (((((ge_representation_real_code_decision_actual_divisionequationsumsecond) = 2 * (ge_balance_positive_decision_actual_divisionequationsumsecondreal) /\ (ge_balance_negative_decision_actual_divisionequationsumsecondreal) = 0) \/ exists ge_signed_half_decision_actual_divisionequationsumsecondrealdecode. (((ge_representation_real_code_decision_actual_divisionequationsumsecond) = 2 * ge_signed_half_decision_actual_divisionequationsumsecondrealdecode + 1 /\ (ge_balance_positive_decision_actual_divisionequationsumsecondreal) = 0) /\ (ge_balance_negative_decision_actual_divisionequationsumsecondreal) = S ge_signed_half_decision_actual_divisionequationsumsecondrealdecode))) /\ ((ge_second_rp_decision_actual_divisionequationsum) + ge_balance_negative_decision_actual_divisionequationsumsecondreal = (ge_second_rn_decision_actual_divisionequationsum) + ge_balance_positive_decision_actual_divisionequationsumsecondreal))) /\ (exists ge_balance_positive_decision_actual_divisionequationsumsecondimaginary ge_balance_negative_decision_actual_divisionequationsumsecondimaginary. (((((ge_representation_imaginary_code_decision_actual_divisionequationsumsecond) = 2 * (ge_balance_positive_decision_actual_divisionequationsumsecondimaginary) /\ (ge_balance_negative_decision_actual_divisionequationsumsecondimaginary) = 0) \/ exists ge_signed_half_decision_actual_divisionequationsumsecondimaginarydecode. (((ge_representation_imaginary_code_decision_actual_divisionequationsumsecond) = 2 * ge_signed_half_decision_actual_divisionequationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_decision_actual_divisionequationsumsecondimaginary) = 0) /\ (ge_balance_negative_decision_actual_divisionequationsumsecondimaginary) = S ge_signed_half_decision_actual_divisionequationsumsecondimaginarydecode))) /\ ((ge_second_ip_decision_actual_divisionequationsum) + ge_balance_negative_decision_actual_divisionequationsumsecondimaginary = (ge_second_in_decision_actual_divisionequationsum) + ge_balance_positive_decision_actual_divisionequationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_decision_actual_divisionequationsumoutput ge_representation_imaginary_code_decision_actual_divisionequationsumoutput. (((z) = ((ge_representation_real_code_decision_actual_divisionequationsumoutput) + (ge_representation_imaginary_code_decision_actual_divisionequationsumoutput)) * S ((ge_representation_real_code_decision_actual_divisionequationsumoutput) + (ge_representation_imaginary_code_decision_actual_divisionequationsumoutput)) + ((ge_representation_imaginary_code_decision_actual_divisionequationsumoutput) + (ge_representation_imaginary_code_decision_actual_divisionequationsumoutput))) /\ ((exists ge_balance_positive_decision_actual_divisionequationsumoutputreal ge_balance_negative_decision_actual_divisionequationsumoutputreal. (((((ge_representation_real_code_decision_actual_divisionequationsumoutput) = 2 * (ge_balance_positive_decision_actual_divisionequationsumoutputreal) /\ (ge_balance_negative_decision_actual_divisionequationsumoutputreal) = 0) \/ exists ge_signed_half_decision_actual_divisionequationsumoutputrealdecode. (((ge_representation_real_code_decision_actual_divisionequationsumoutput) = 2 * ge_signed_half_decision_actual_divisionequationsumoutputrealdecode + 1 /\ (ge_balance_positive_decision_actual_divisionequationsumoutputreal) = 0) /\ (ge_balance_negative_decision_actual_divisionequationsumoutputreal) = S ge_signed_half_decision_actual_divisionequationsumoutputrealdecode))) /\ ((((ge_first_rp_decision_actual_divisionequationsum) + (ge_second_rp_decision_actual_divisionequationsum))) + ge_balance_negative_decision_actual_divisionequationsumoutputreal = (((ge_first_rn_decision_actual_divisionequationsum) + (ge_second_rn_decision_actual_divisionequationsum))) + ge_balance_positive_decision_actual_divisionequationsumoutputreal))) /\ (exists ge_balance_positive_decision_actual_divisionequationsumoutputimaginary ge_balance_negative_decision_actual_divisionequationsumoutputimaginary. (((((ge_representation_imaginary_code_decision_actual_divisionequationsumoutput) = 2 * (ge_balance_positive_decision_actual_divisionequationsumoutputimaginary) /\ (ge_balance_negative_decision_actual_divisionequationsumoutputimaginary) = 0) \/ exists ge_signed_half_decision_actual_divisionequationsumoutputimaginarydecode. (((ge_representation_imaginary_code_decision_actual_divisionequationsumoutput) = 2 * ge_signed_half_decision_actual_divisionequationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_decision_actual_divisionequationsumoutputimaginary) = 0) /\ (ge_balance_negative_decision_actual_divisionequationsumoutputimaginary) = S ge_signed_half_decision_actual_divisionequationsumoutputimaginarydecode))) /\ ((((ge_first_ip_decision_actual_divisionequationsum) + (ge_second_ip_decision_actual_divisionequationsum))) + ge_balance_negative_decision_actual_divisionequationsumoutputimaginary = (((ge_first_in_decision_actual_divisionequationsum) + (ge_second_in_decision_actual_divisionequationsum))) + ge_balance_positive_decision_actual_divisionequationsumoutputimaginary))))))))))) /\ ((exists ge_norm_rp_decision_actual_divisionsmallnorm ge_norm_rn_decision_actual_divisionsmallnorm ge_norm_ip_decision_actual_divisionsmallnorm ge_norm_in_decision_actual_divisionsmallnorm. ((exists ge_representation_real_code_decision_actual_divisionsmallnormrepresentation ge_representation_imaginary_code_decision_actual_divisionsmallnormrepresentation. (((r) = ((ge_representation_real_code_decision_actual_divisionsmallnormrepresentation) + (ge_representation_imaginary_code_decision_actual_divisionsmallnormrepresentation)) * S ((ge_representation_real_code_decision_actual_divisionsmallnormrepresentation) + (ge_representation_imaginary_code_decision_actual_divisionsmallnormrepresentation)) + ((ge_representation_imaginary_code_decision_actual_divisionsmallnormrepresentation) + (ge_representation_imaginary_code_decision_actual_divisionsmallnormrepresentation))) /\ ((exists ge_balance_positive_decision_actual_divisionsmallnormrepresentationreal ge_balance_negative_decision_actual_divisionsmallnormrepresentationreal. (((((ge_representation_real_code_decision_actual_divisionsmallnormrepresentation) = 2 * (ge_balance_positive_decision_actual_divisionsmallnormrepresentationreal) /\ (ge_balance_negative_decision_actual_divisionsmallnormrepresentationreal) = 0) \/ exists ge_signed_half_decision_actual_divisionsmallnormrepresentationrealdecode. (((ge_representation_real_code_decision_actual_divisionsmallnormrepresentation) = 2 * ge_signed_half_decision_actual_divisionsmallnormrepresentationrealdecode + 1 /\ (ge_balance_positive_decision_actual_divisionsmallnormrepresentationreal) = 0) /\ (ge_balance_negative_decision_actual_divisionsmallnormrepresentationreal) = S ge_signed_half_decision_actual_divisionsmallnormrepresentationrealdecode))) /\ ((ge_norm_rp_decision_actual_divisionsmallnorm) + ge_balance_negative_decision_actual_divisionsmallnormrepresentationreal = (ge_norm_rn_decision_actual_divisionsmallnorm) + ge_balance_positive_decision_actual_divisionsmallnormrepresentationreal))) /\ (exists ge_balance_positive_decision_actual_divisionsmallnormrepresentationimaginary ge_balance_negative_decision_actual_divisionsmallnormrepresentationimaginary. (((((ge_representation_imaginary_code_decision_actual_divisionsmallnormrepresentation) = 2 * (ge_balance_positive_decision_actual_divisionsmallnormrepresentationimaginary) /\ (ge_balance_negative_decision_actual_divisionsmallnormrepresentationimaginary) = 0) \/ exists ge_signed_half_decision_actual_divisionsmallnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_decision_actual_divisionsmallnormrepresentation) = 2 * ge_signed_half_decision_actual_divisionsmallnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_decision_actual_divisionsmallnormrepresentationimaginary) = 0) /\ (ge_balance_negative_decision_actual_divisionsmallnormrepresentationimaginary) = S ge_signed_half_decision_actual_divisionsmallnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_decision_actual_divisionsmallnorm) + ge_balance_negative_decision_actual_divisionsmallnormrepresentationimaginary = (ge_norm_in_decision_actual_divisionsmallnorm) + ge_balance_positive_decision_actual_divisionsmallnormrepresentationimaginary)))))) /\ (exists ge_real_square_decision_actual_divisionsmallnormsquare ge_imaginary_square_decision_actual_divisionsmallnormsquare. ((((((ge_norm_rp_decision_actual_divisionsmallnorm) * (ge_norm_rp_decision_actual_divisionsmallnorm))) + (((ge_norm_rn_decision_actual_divisionsmallnorm) * (ge_norm_rn_decision_actual_divisionsmallnorm)))) = ((ge_real_square_decision_actual_divisionsmallnormsquare) + (((((ge_norm_rp_decision_actual_divisionsmallnorm) * (ge_norm_rn_decision_actual_divisionsmallnorm))) + (((ge_norm_rn_decision_actual_divisionsmallnorm) * (ge_norm_rp_decision_actual_divisionsmallnorm))))))) /\ ((((((ge_norm_ip_decision_actual_divisionsmallnorm) * (ge_norm_ip_decision_actual_divisionsmallnorm))) + (((ge_norm_in_decision_actual_divisionsmallnorm) * (ge_norm_in_decision_actual_divisionsmallnorm)))) = ((ge_imaginary_square_decision_actual_divisionsmallnormsquare) + (((((ge_norm_ip_decision_actual_divisionsmallnorm) * (ge_norm_in_decision_actual_divisionsmallnorm))) + (((ge_norm_in_decision_actual_divisionsmallnorm) * (ge_norm_ip_decision_actual_divisionsmallnorm))))))) /\ ((U) = ge_real_square_decision_actual_divisionsmallnormsquare + ge_imaginary_square_decision_actual_divisionsmallnormsquare)))))) /\ ((exists ge_norm_rp_decision_actual_divisionlargenorm ge_norm_rn_decision_actual_divisionlargenorm ge_norm_ip_decision_actual_divisionlargenorm ge_norm_in_decision_actual_divisionlargenorm. ((exists ge_representation_real_code_decision_actual_divisionlargenormrepresentation ge_representation_imaginary_code_decision_actual_divisionlargenormrepresentation. (((d) = ((ge_representation_real_code_decision_actual_divisionlargenormrepresentation) + (ge_representation_imaginary_code_decision_actual_divisionlargenormrepresentation)) * S ((ge_representation_real_code_decision_actual_divisionlargenormrepresentation) + (ge_representation_imaginary_code_decision_actual_divisionlargenormrepresentation)) + ((ge_representation_imaginary_code_decision_actual_divisionlargenormrepresentation) + (ge_representation_imaginary_code_decision_actual_divisionlargenormrepresentation))) /\ ((exists ge_balance_positive_decision_actual_divisionlargenormrepresentationreal ge_balance_negative_decision_actual_divisionlargenormrepresentationreal. (((((ge_representation_real_code_decision_actual_divisionlargenormrepresentation) = 2 * (ge_balance_positive_decision_actual_divisionlargenormrepresentationreal) /\ (ge_balance_negative_decision_actual_divisionlargenormrepresentationreal) = 0) \/ exists ge_signed_half_decision_actual_divisionlargenormrepresentationrealdecode. (((ge_representation_real_code_decision_actual_divisionlargenormrepresentation) = 2 * ge_signed_half_decision_actual_divisionlargenormrepresentationrealdecode + 1 /\ (ge_balance_positive_decision_actual_divisionlargenormrepresentationreal) = 0) /\ (ge_balance_negative_decision_actual_divisionlargenormrepresentationreal) = S ge_signed_half_decision_actual_divisionlargenormrepresentationrealdecode))) /\ ((ge_norm_rp_decision_actual_divisionlargenorm) + ge_balance_negative_decision_actual_divisionlargenormrepresentationreal = (ge_norm_rn_decision_actual_divisionlargenorm) + ge_balance_positive_decision_actual_divisionlargenormrepresentationreal))) /\ (exists ge_balance_positive_decision_actual_divisionlargenormrepresentationimaginary ge_balance_negative_decision_actual_divisionlargenormrepresentationimaginary. (((((ge_representation_imaginary_code_decision_actual_divisionlargenormrepresentation) = 2 * (ge_balance_positive_decision_actual_divisionlargenormrepresentationimaginary) /\ (ge_balance_negative_decision_actual_divisionlargenormrepresentationimaginary) = 0) \/ exists ge_signed_half_decision_actual_divisionlargenormrepresentationimaginarydecode. (((ge_representation_imaginary_code_decision_actual_divisionlargenormrepresentation) = 2 * ge_signed_half_decision_actual_divisionlargenormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_decision_actual_divisionlargenormrepresentationimaginary) = 0) /\ (ge_balance_negative_decision_actual_divisionlargenormrepresentationimaginary) = S ge_signed_half_decision_actual_divisionlargenormrepresentationimaginarydecode))) /\ ((ge_norm_ip_decision_actual_divisionlargenorm) + ge_balance_negative_decision_actual_divisionlargenormrepresentationimaginary = (ge_norm_in_decision_actual_divisionlargenorm) + ge_balance_positive_decision_actual_divisionlargenormrepresentationimaginary)))))) /\ (exists ge_real_square_decision_actual_divisionlargenormsquare ge_imaginary_square_decision_actual_divisionlargenormsquare. ((((((ge_norm_rp_decision_actual_divisionlargenorm) * (ge_norm_rp_decision_actual_divisionlargenorm))) + (((ge_norm_rn_decision_actual_divisionlargenorm) * (ge_norm_rn_decision_actual_divisionlargenorm)))) = ((ge_real_square_decision_actual_divisionlargenormsquare) + (((((ge_norm_rp_decision_actual_divisionlargenorm) * (ge_norm_rn_decision_actual_divisionlargenorm))) + (((ge_norm_rn_decision_actual_divisionlargenorm) * (ge_norm_rp_decision_actual_divisionlargenorm))))))) /\ ((((((ge_norm_ip_decision_actual_divisionlargenorm) * (ge_norm_ip_decision_actual_divisionlargenorm))) + (((ge_norm_in_decision_actual_divisionlargenorm) * (ge_norm_in_decision_actual_divisionlargenorm)))) = ((ge_imaginary_square_decision_actual_divisionlargenormsquare) + (((((ge_norm_ip_decision_actual_divisionlargenorm) * (ge_norm_in_decision_actual_divisionlargenorm))) + (((ge_norm_in_decision_actual_divisionlargenorm) * (ge_norm_ip_decision_actual_divisionlargenorm))))))) /\ ((V) = ge_real_square_decision_actual_divisionlargenormsquare + ge_imaginary_square_decision_actual_divisionlargenormsquare)))))) /\ (exists ge_gap_decision_actual_divisionstrict. ge_gap_decision_actual_divisionstrict + S (U) = (V))))))))
  30. 0030specialize gaussian_euclidean_division_exists (z)
  31. 0031specialize gaussian_euclidean_division_exists (d)
  32. 0032apply gaussian_euclidean_division_exists
  33. 0033exact hz
  34. 0034exact hd
  35. 0035exact hdc_right
  36. 0036cases hex
  37. 0037cases hex_witness
  38. 0038cases hex_witness_witness
  39. 0039cases hex_witness_witness_witness
  40. 0040cases hex_witness_witness_witness_witness
  41. 0041cases hex_witness_witness_witness_witness_right
  42. 0042cases hex_witness_witness_witness_witness_right_right
  43. 0043cases hex_witness_witness_witness_witness_right_right_right
  44. 0044cases hex_witness_witness_witness_witness_right_right_right_right
  45. 0045have hrc : x1=0 \/ ~(x1=0)
  46. 0046specialize eq_decidable (x1)
  47. 0047specialize eq_decidable (0)
  48. 0048apply eq_decidable
  49. 0049cases hrc
  50. 0050left
  51. 0051specialize gaussian_division_zero_remainder_divides (z)
  52. 0052specialize gaussian_division_zero_remainder_divides (d)
  53. 0053specialize gaussian_division_zero_remainder_divides (x)
  54. 0054specialize gaussian_division_zero_remainder_divides (x1)
  55. 0055apply gaussian_division_zero_remainder_divides
  56. 0056exact hex_witness_witness_witness_witness_right_right_left
  57. 0057exact hrc_left
  58. 0058right
  59. 0059intro hdiv
  60. 0060apply hrc_right
  61. 0061specialize gaussian_division_divisible_remainder_zero (z)
  62. 0062specialize gaussian_division_divisible_remainder_zero (d)
  63. 0063specialize gaussian_division_divisible_remainder_zero (x)
  64. 0064specialize gaussian_division_divisible_remainder_zero (x1)
  65. 0065specialize gaussian_division_divisible_remainder_zero (x2)
  66. 0066specialize gaussian_division_divisible_remainder_zero (x3)
  67. 0067apply gaussian_division_divisible_remainder_zero
  68. 0068exact hex_witness_witness_witness_witness_right_right_left
  69. 0069exact hex_witness_witness_witness_witness_right_right_right_left
  70. 0070exact hex_witness_witness_witness_witness_right_right_right_right_left
  71. 0071exact hex_witness_witness_witness_witness_right_right_right_right_right
  72. 0072exact hdiv