GF0053

gaussian_divides_decidable

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

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

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.

Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.

Exact theorem in conservative defined notation

∀ d. ∀ z. ZPairValid(d) → ZPairValid(z) → GDvd(d,z) ∨ ¬GDvd(d,z)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ZPairValid(z) · 4GNorm(z,n) · 2ZPairAdd(a,b,c) · 1GMul(a,b,c) · 1GDvd(d,z) · 2Lt(a,b) · 1

Actual proof prerequisites

eq_decidable · checked external prerequisitegaussian_multiply_zero_rightgaussian_zero_validgaussian_zero_divides_only_zerogaussian_euclidean_division_exists · checked external prerequisitegaussian_division_zero_remainder_dividesgaussian_division_divisible_remainder_zero
Original expanded first-order 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))))))))))

Complete tactic proof in conservative notation

All 72 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (5)
gaussian multiply zero rightgaussian zero validgaussian zero divides only zerogaussian division zero remainder dividesgaussian division divisible remainder zero
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: ZPairValid(q)ZPairValid(r)GMul(d,q,x)ZPairAdd(x,r,z)GNorm(r,U)GNorm(d,V)Lt(U,V)Original native command in the exact edition
  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 defined 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 : ∃ 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)))))
  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