GF0076

gaussian_factor_search_coordinate_rectangle

Two ordinary finite inductions exhaust the actual signed-coordinate rectangle, with a witness or an explicit absence theorem.

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

∀ h. ∀ z. ∀ N. ∀ k. ZPairValid(z) → (∃ x. ∃ y. Lt(x,h) ∧ (Lt(y,k) ∧ GProperNormDivisor((x + y) · S (x + y) + (y + y),z,N))) ∨ (∀ x. ∀ y. Lt(x,h) → Lt(y,k) → ¬GProperNormDivisor((x + y) · S (x + y) + (y + y),z,N))

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

Definition DAG

ZPairValid(z) · 1GProperNormDivisor(d,z,N) · 6Lt(a,b) · 11

Actual proof prerequisites

gaussian_search_no_index_below_zerogaussian_factor_search_coordinate_rowfinite_lt_succ_eq_or_lt · checked external prerequisitelt_of_lt_of_le · checked external prerequisitele_succ_self · checked external prerequisitezero_add · checked external prerequisitegaussian_search_proper_divisor_code_transport
Original expanded first-order statement 
forall h z N k. (exists ge_real_positive_rectangle_target ge_real_negative_rectangle_target ge_imaginary_positive_rectangle_target ge_imaginary_negative_rectangle_target. (exists ge_real_code_rectangle_targetdecode ge_imaginary_code_rectangle_targetdecode. (((z) = ((ge_real_code_rectangle_targetdecode) + (ge_imaginary_code_rectangle_targetdecode)) * S ((ge_real_code_rectangle_targetdecode) + (ge_imaginary_code_rectangle_targetdecode)) + ((ge_imaginary_code_rectangle_targetdecode) + (ge_imaginary_code_rectangle_targetdecode))) /\ (((((ge_real_code_rectangle_targetdecode) = 2 * (ge_real_positive_rectangle_target) /\ (ge_real_negative_rectangle_target) = 0) \/ exists ge_signed_half_ge_rectangle_targetdecode_real. (((ge_real_code_rectangle_targetdecode) = 2 * ge_signed_half_ge_rectangle_targetdecode_real + 1 /\ (ge_real_positive_rectangle_target) = 0) /\ (ge_real_negative_rectangle_target) = S ge_signed_half_ge_rectangle_targetdecode_real))) /\ ((((ge_imaginary_code_rectangle_targetdecode) = 2 * (ge_imaginary_positive_rectangle_target) /\ (ge_imaginary_negative_rectangle_target) = 0) \/ exists ge_signed_half_ge_rectangle_targetdecode_imaginary. (((ge_imaginary_code_rectangle_targetdecode) = 2 * ge_signed_half_ge_rectangle_targetdecode_imaginary + 1 /\ (ge_imaginary_positive_rectangle_target) = 0) /\ (ge_imaginary_negative_rectangle_target) = S ge_signed_half_ge_rectangle_targetdecode_imaginary))))))) -> ((exists gr_rectangle_real_rectangle_scan gr_rectangle_imaginary_rectangle_scan. ((exists ge_gap_rectangle_scanfound_real. ge_gap_rectangle_scanfound_real + S (gr_rectangle_real_rectangle_scan) = (h)) /\ ((exists ge_gap_rectangle_scanfound_imaginary. ge_gap_rectangle_scanfound_imaginary + S (gr_rectangle_imaginary_rectangle_scan) = (k)) /\ (((~(exists gr_inverse_rectangle_scanfoundnonunit. (exists ge_first_rp_rectangle_scanfoundnonunitidentity ge_first_rn_rectangle_scanfoundnonunitidentity ge_first_ip_rectangle_scanfoundnonunitidentity ge_first_in_rectangle_scanfoundnonunitidentity ge_second_rp_rectangle_scanfoundnonunitidentity ge_second_rn_rectangle_scanfoundnonunitidentity ge_second_ip_rectangle_scanfoundnonunitidentity ge_second_in_rectangle_scanfoundnonunitidentity. ((exists ge_representation_real_code_rectangle_scanfoundnonunitidentityfirst ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst. (((((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) * S ((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) + ((gr_rectangle_imaginary_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan))) = ((ge_representation_real_code_rectangle_scanfoundnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst)) * S ((ge_representation_real_code_rectangle_scanfoundnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst)) + ((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst))) /\ ((exists ge_balance_positive_rectangle_scanfoundnonunitidentityfirstreal ge_balance_negative_rectangle_scanfoundnonunitidentityfirstreal. (((((ge_representation_real_code_rectangle_scanfoundnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_scanfoundnonunitidentityfirstreal) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundnonunitidentityfirstrealdecode. (((ge_representation_real_code_rectangle_scanfoundnonunitidentityfirst) = 2 * ge_signed_half_rectangle_scanfoundnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityfirstreal) = S ge_signed_half_rectangle_scanfoundnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_rectangle_scanfoundnonunitidentity) + ge_balance_negative_rectangle_scanfoundnonunitidentityfirstreal = (ge_first_rn_rectangle_scanfoundnonunitidentity) + ge_balance_positive_rectangle_scanfoundnonunitidentityfirstreal))) /\ (exists ge_balance_positive_rectangle_scanfoundnonunitidentityfirstimaginary ge_balance_negative_rectangle_scanfoundnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_scanfoundnonunitidentityfirstimaginary) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst) = 2 * ge_signed_half_rectangle_scanfoundnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityfirstimaginary) = S ge_signed_half_rectangle_scanfoundnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_scanfoundnonunitidentity) + ge_balance_negative_rectangle_scanfoundnonunitidentityfirstimaginary = (ge_first_in_rectangle_scanfoundnonunitidentity) + ge_balance_positive_rectangle_scanfoundnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_scanfoundnonunitidentitysecond ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond. (((gr_inverse_rectangle_scanfoundnonunit) = ((ge_representation_real_code_rectangle_scanfoundnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond)) * S ((ge_representation_real_code_rectangle_scanfoundnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond)) + ((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond))) /\ ((exists ge_balance_positive_rectangle_scanfoundnonunitidentitysecondreal ge_balance_negative_rectangle_scanfoundnonunitidentitysecondreal. (((((ge_representation_real_code_rectangle_scanfoundnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_scanfoundnonunitidentitysecondreal) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundnonunitidentitysecondrealdecode. (((ge_representation_real_code_rectangle_scanfoundnonunitidentitysecond) = 2 * ge_signed_half_rectangle_scanfoundnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentitysecondreal) = S ge_signed_half_rectangle_scanfoundnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_rectangle_scanfoundnonunitidentity) + ge_balance_negative_rectangle_scanfoundnonunitidentitysecondreal = (ge_second_rn_rectangle_scanfoundnonunitidentity) + ge_balance_positive_rectangle_scanfoundnonunitidentitysecondreal))) /\ (exists ge_balance_positive_rectangle_scanfoundnonunitidentitysecondimaginary ge_balance_negative_rectangle_scanfoundnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_scanfoundnonunitidentitysecondimaginary) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond) = 2 * ge_signed_half_rectangle_scanfoundnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentitysecondimaginary) = S ge_signed_half_rectangle_scanfoundnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_rectangle_scanfoundnonunitidentity) + ge_balance_negative_rectangle_scanfoundnonunitidentitysecondimaginary = (ge_second_in_rectangle_scanfoundnonunitidentity) + ge_balance_positive_rectangle_scanfoundnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_scanfoundnonunitidentityoutput ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput. (((6) = ((ge_representation_real_code_rectangle_scanfoundnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput)) * S ((ge_representation_real_code_rectangle_scanfoundnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput)) + ((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput))) /\ ((exists ge_balance_positive_rectangle_scanfoundnonunitidentityoutputreal ge_balance_negative_rectangle_scanfoundnonunitidentityoutputreal. (((((ge_representation_real_code_rectangle_scanfoundnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_scanfoundnonunitidentityoutputreal) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundnonunitidentityoutputrealdecode. (((ge_representation_real_code_rectangle_scanfoundnonunitidentityoutput) = 2 * ge_signed_half_rectangle_scanfoundnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityoutputreal) = S ge_signed_half_rectangle_scanfoundnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_scanfoundnonunitidentity) * (ge_second_rp_rectangle_scanfoundnonunitidentity))) + (((ge_first_rn_rectangle_scanfoundnonunitidentity) * (ge_second_rn_rectangle_scanfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_scanfoundnonunitidentity) * (ge_second_in_rectangle_scanfoundnonunitidentity))) + (((ge_first_in_rectangle_scanfoundnonunitidentity) * (ge_second_ip_rectangle_scanfoundnonunitidentity))))))) + ge_balance_negative_rectangle_scanfoundnonunitidentityoutputreal = (((((((ge_first_rp_rectangle_scanfoundnonunitidentity) * (ge_second_rn_rectangle_scanfoundnonunitidentity))) + (((ge_first_rn_rectangle_scanfoundnonunitidentity) * (ge_second_rp_rectangle_scanfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_scanfoundnonunitidentity) * (ge_second_ip_rectangle_scanfoundnonunitidentity))) + (((ge_first_in_rectangle_scanfoundnonunitidentity) * (ge_second_in_rectangle_scanfoundnonunitidentity))))))) + ge_balance_positive_rectangle_scanfoundnonunitidentityoutputreal))) /\ (exists ge_balance_positive_rectangle_scanfoundnonunitidentityoutputimaginary ge_balance_negative_rectangle_scanfoundnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_scanfoundnonunitidentityoutputimaginary) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput) = 2 * ge_signed_half_rectangle_scanfoundnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityoutputimaginary) = S ge_signed_half_rectangle_scanfoundnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_scanfoundnonunitidentity) * (ge_second_ip_rectangle_scanfoundnonunitidentity))) + (((ge_first_rn_rectangle_scanfoundnonunitidentity) * (ge_second_in_rectangle_scanfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_scanfoundnonunitidentity) * (ge_second_rp_rectangle_scanfoundnonunitidentity))) + (((ge_first_in_rectangle_scanfoundnonunitidentity) * (ge_second_rn_rectangle_scanfoundnonunitidentity))))))) + ge_balance_negative_rectangle_scanfoundnonunitidentityoutputimaginary = (((((((ge_first_rp_rectangle_scanfoundnonunitidentity) * (ge_second_in_rectangle_scanfoundnonunitidentity))) + (((ge_first_rn_rectangle_scanfoundnonunitidentity) * (ge_second_ip_rectangle_scanfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_scanfoundnonunitidentity) * (ge_second_rn_rectangle_scanfoundnonunitidentity))) + (((ge_first_in_rectangle_scanfoundnonunitidentity) * (ge_second_rp_rectangle_scanfoundnonunitidentity))))))) + ge_balance_positive_rectangle_scanfoundnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_rectangle_scanfoundquotient. (exists ge_first_rp_rectangle_scanfoundquotientproduct ge_first_rn_rectangle_scanfoundquotientproduct ge_first_ip_rectangle_scanfoundquotientproduct ge_first_in_rectangle_scanfoundquotientproduct ge_second_rp_rectangle_scanfoundquotientproduct ge_second_rn_rectangle_scanfoundquotientproduct ge_second_ip_rectangle_scanfoundquotientproduct ge_second_in_rectangle_scanfoundquotientproduct. ((exists ge_representation_real_code_rectangle_scanfoundquotientproductfirst ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst. (((((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) * S ((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) + ((gr_rectangle_imaginary_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan))) = ((ge_representation_real_code_rectangle_scanfoundquotientproductfirst) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst)) * S ((ge_representation_real_code_rectangle_scanfoundquotientproductfirst) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst)) + ((ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst))) /\ ((exists ge_balance_positive_rectangle_scanfoundquotientproductfirstreal ge_balance_negative_rectangle_scanfoundquotientproductfirstreal. (((((ge_representation_real_code_rectangle_scanfoundquotientproductfirst) = 2 * (ge_balance_positive_rectangle_scanfoundquotientproductfirstreal) /\ (ge_balance_negative_rectangle_scanfoundquotientproductfirstreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundquotientproductfirstrealdecode. (((ge_representation_real_code_rectangle_scanfoundquotientproductfirst) = 2 * ge_signed_half_rectangle_scanfoundquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundquotientproductfirstreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundquotientproductfirstreal) = S ge_signed_half_rectangle_scanfoundquotientproductfirstrealdecode))) /\ ((ge_first_rp_rectangle_scanfoundquotientproduct) + ge_balance_negative_rectangle_scanfoundquotientproductfirstreal = (ge_first_rn_rectangle_scanfoundquotientproduct) + ge_balance_positive_rectangle_scanfoundquotientproductfirstreal))) /\ (exists ge_balance_positive_rectangle_scanfoundquotientproductfirstimaginary ge_balance_negative_rectangle_scanfoundquotientproductfirstimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst) = 2 * (ge_balance_positive_rectangle_scanfoundquotientproductfirstimaginary) /\ (ge_balance_negative_rectangle_scanfoundquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst) = 2 * ge_signed_half_rectangle_scanfoundquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundquotientproductfirstimaginary) = S ge_signed_half_rectangle_scanfoundquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_scanfoundquotientproduct) + ge_balance_negative_rectangle_scanfoundquotientproductfirstimaginary = (ge_first_in_rectangle_scanfoundquotientproduct) + ge_balance_positive_rectangle_scanfoundquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_scanfoundquotientproductsecond ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond. (((gr_quotient_rectangle_scanfoundquotient) = ((ge_representation_real_code_rectangle_scanfoundquotientproductsecond) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond)) * S ((ge_representation_real_code_rectangle_scanfoundquotientproductsecond) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond)) + ((ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond))) /\ ((exists ge_balance_positive_rectangle_scanfoundquotientproductsecondreal ge_balance_negative_rectangle_scanfoundquotientproductsecondreal. (((((ge_representation_real_code_rectangle_scanfoundquotientproductsecond) = 2 * (ge_balance_positive_rectangle_scanfoundquotientproductsecondreal) /\ (ge_balance_negative_rectangle_scanfoundquotientproductsecondreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundquotientproductsecondrealdecode. (((ge_representation_real_code_rectangle_scanfoundquotientproductsecond) = 2 * ge_signed_half_rectangle_scanfoundquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundquotientproductsecondreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundquotientproductsecondreal) = S ge_signed_half_rectangle_scanfoundquotientproductsecondrealdecode))) /\ ((ge_second_rp_rectangle_scanfoundquotientproduct) + ge_balance_negative_rectangle_scanfoundquotientproductsecondreal = (ge_second_rn_rectangle_scanfoundquotientproduct) + ge_balance_positive_rectangle_scanfoundquotientproductsecondreal))) /\ (exists ge_balance_positive_rectangle_scanfoundquotientproductsecondimaginary ge_balance_negative_rectangle_scanfoundquotientproductsecondimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond) = 2 * (ge_balance_positive_rectangle_scanfoundquotientproductsecondimaginary) /\ (ge_balance_negative_rectangle_scanfoundquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond) = 2 * ge_signed_half_rectangle_scanfoundquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundquotientproductsecondimaginary) = S ge_signed_half_rectangle_scanfoundquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_rectangle_scanfoundquotientproduct) + ge_balance_negative_rectangle_scanfoundquotientproductsecondimaginary = (ge_second_in_rectangle_scanfoundquotientproduct) + ge_balance_positive_rectangle_scanfoundquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_scanfoundquotientproductoutput ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput. (((z) = ((ge_representation_real_code_rectangle_scanfoundquotientproductoutput) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput)) * S ((ge_representation_real_code_rectangle_scanfoundquotientproductoutput) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput)) + ((ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput))) /\ ((exists ge_balance_positive_rectangle_scanfoundquotientproductoutputreal ge_balance_negative_rectangle_scanfoundquotientproductoutputreal. (((((ge_representation_real_code_rectangle_scanfoundquotientproductoutput) = 2 * (ge_balance_positive_rectangle_scanfoundquotientproductoutputreal) /\ (ge_balance_negative_rectangle_scanfoundquotientproductoutputreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundquotientproductoutputrealdecode. (((ge_representation_real_code_rectangle_scanfoundquotientproductoutput) = 2 * ge_signed_half_rectangle_scanfoundquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundquotientproductoutputreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundquotientproductoutputreal) = S ge_signed_half_rectangle_scanfoundquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_scanfoundquotientproduct) * (ge_second_rp_rectangle_scanfoundquotientproduct))) + (((ge_first_rn_rectangle_scanfoundquotientproduct) * (ge_second_rn_rectangle_scanfoundquotientproduct))))) + (((((ge_first_ip_rectangle_scanfoundquotientproduct) * (ge_second_in_rectangle_scanfoundquotientproduct))) + (((ge_first_in_rectangle_scanfoundquotientproduct) * (ge_second_ip_rectangle_scanfoundquotientproduct))))))) + ge_balance_negative_rectangle_scanfoundquotientproductoutputreal = (((((((ge_first_rp_rectangle_scanfoundquotientproduct) * (ge_second_rn_rectangle_scanfoundquotientproduct))) + (((ge_first_rn_rectangle_scanfoundquotientproduct) * (ge_second_rp_rectangle_scanfoundquotientproduct))))) + (((((ge_first_ip_rectangle_scanfoundquotientproduct) * (ge_second_ip_rectangle_scanfoundquotientproduct))) + (((ge_first_in_rectangle_scanfoundquotientproduct) * (ge_second_in_rectangle_scanfoundquotientproduct))))))) + ge_balance_positive_rectangle_scanfoundquotientproductoutputreal))) /\ (exists ge_balance_positive_rectangle_scanfoundquotientproductoutputimaginary ge_balance_negative_rectangle_scanfoundquotientproductoutputimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput) = 2 * (ge_balance_positive_rectangle_scanfoundquotientproductoutputimaginary) /\ (ge_balance_negative_rectangle_scanfoundquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput) = 2 * ge_signed_half_rectangle_scanfoundquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundquotientproductoutputimaginary) = S ge_signed_half_rectangle_scanfoundquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_scanfoundquotientproduct) * (ge_second_ip_rectangle_scanfoundquotientproduct))) + (((ge_first_rn_rectangle_scanfoundquotientproduct) * (ge_second_in_rectangle_scanfoundquotientproduct))))) + (((((ge_first_ip_rectangle_scanfoundquotientproduct) * (ge_second_rp_rectangle_scanfoundquotientproduct))) + (((ge_first_in_rectangle_scanfoundquotientproduct) * (ge_second_rn_rectangle_scanfoundquotientproduct))))))) + ge_balance_negative_rectangle_scanfoundquotientproductoutputimaginary = (((((((ge_first_rp_rectangle_scanfoundquotientproduct) * (ge_second_in_rectangle_scanfoundquotientproduct))) + (((ge_first_rn_rectangle_scanfoundquotientproduct) * (ge_second_ip_rectangle_scanfoundquotientproduct))))) + (((((ge_first_ip_rectangle_scanfoundquotientproduct) * (ge_second_rn_rectangle_scanfoundquotientproduct))) + (((ge_first_in_rectangle_scanfoundquotientproduct) * (ge_second_rp_rectangle_scanfoundquotientproduct))))))) + ge_balance_positive_rectangle_scanfoundquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_rectangle_scanfound. ((exists ge_norm_rp_rectangle_scanfoundnorm ge_norm_rn_rectangle_scanfoundnorm ge_norm_ip_rectangle_scanfoundnorm ge_norm_in_rectangle_scanfoundnorm. ((exists ge_representation_real_code_rectangle_scanfoundnormrepresentation ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation. (((((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) * S ((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) + ((gr_rectangle_imaginary_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan))) = ((ge_representation_real_code_rectangle_scanfoundnormrepresentation) + (ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation)) * S ((ge_representation_real_code_rectangle_scanfoundnormrepresentation) + (ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation)) + ((ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation) + (ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation))) /\ ((exists ge_balance_positive_rectangle_scanfoundnormrepresentationreal ge_balance_negative_rectangle_scanfoundnormrepresentationreal. (((((ge_representation_real_code_rectangle_scanfoundnormrepresentation) = 2 * (ge_balance_positive_rectangle_scanfoundnormrepresentationreal) /\ (ge_balance_negative_rectangle_scanfoundnormrepresentationreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundnormrepresentationrealdecode. (((ge_representation_real_code_rectangle_scanfoundnormrepresentation) = 2 * ge_signed_half_rectangle_scanfoundnormrepresentationrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnormrepresentationreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundnormrepresentationreal) = S ge_signed_half_rectangle_scanfoundnormrepresentationrealdecode))) /\ ((ge_norm_rp_rectangle_scanfoundnorm) + ge_balance_negative_rectangle_scanfoundnormrepresentationreal = (ge_norm_rn_rectangle_scanfoundnorm) + ge_balance_positive_rectangle_scanfoundnormrepresentationreal))) /\ (exists ge_balance_positive_rectangle_scanfoundnormrepresentationimaginary ge_balance_negative_rectangle_scanfoundnormrepresentationimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation) = 2 * (ge_balance_positive_rectangle_scanfoundnormrepresentationimaginary) /\ (ge_balance_negative_rectangle_scanfoundnormrepresentationimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation) = 2 * ge_signed_half_rectangle_scanfoundnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnormrepresentationimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundnormrepresentationimaginary) = S ge_signed_half_rectangle_scanfoundnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_rectangle_scanfoundnorm) + ge_balance_negative_rectangle_scanfoundnormrepresentationimaginary = (ge_norm_in_rectangle_scanfoundnorm) + ge_balance_positive_rectangle_scanfoundnormrepresentationimaginary)))))) /\ (exists ge_real_square_rectangle_scanfoundnormsquare ge_imaginary_square_rectangle_scanfoundnormsquare. ((((((ge_norm_rp_rectangle_scanfoundnorm) * (ge_norm_rp_rectangle_scanfoundnorm))) + (((ge_norm_rn_rectangle_scanfoundnorm) * (ge_norm_rn_rectangle_scanfoundnorm)))) = ((ge_real_square_rectangle_scanfoundnormsquare) + (((((ge_norm_rp_rectangle_scanfoundnorm) * (ge_norm_rn_rectangle_scanfoundnorm))) + (((ge_norm_rn_rectangle_scanfoundnorm) * (ge_norm_rp_rectangle_scanfoundnorm))))))) /\ ((((((ge_norm_ip_rectangle_scanfoundnorm) * (ge_norm_ip_rectangle_scanfoundnorm))) + (((ge_norm_in_rectangle_scanfoundnorm) * (ge_norm_in_rectangle_scanfoundnorm)))) = ((ge_imaginary_square_rectangle_scanfoundnormsquare) + (((((ge_norm_ip_rectangle_scanfoundnorm) * (ge_norm_in_rectangle_scanfoundnorm))) + (((ge_norm_in_rectangle_scanfoundnorm) * (ge_norm_ip_rectangle_scanfoundnorm))))))) /\ ((gr_proper_divisor_norm_rectangle_scanfound) = ge_real_square_rectangle_scanfoundnormsquare + ge_imaginary_square_rectangle_scanfoundnormsquare)))))) /\ (exists ge_gap_rectangle_scanfoundstrict. ge_gap_rectangle_scanfoundstrict + S (gr_proper_divisor_norm_rectangle_scanfound) = (N)))))))))) \/ (forall gr_rectangle_real_rectangle_scan gr_rectangle_imaginary_rectangle_scan. (exists ge_gap_rectangle_scanabsent_real. ge_gap_rectangle_scanabsent_real + S (gr_rectangle_real_rectangle_scan) = (h)) -> (exists ge_gap_rectangle_scanabsent_imaginary. ge_gap_rectangle_scanabsent_imaginary + S (gr_rectangle_imaginary_rectangle_scan) = (k)) -> ~(((~(exists gr_inverse_rectangle_scanabsentnonunit. (exists ge_first_rp_rectangle_scanabsentnonunitidentity ge_first_rn_rectangle_scanabsentnonunitidentity ge_first_ip_rectangle_scanabsentnonunitidentity ge_first_in_rectangle_scanabsentnonunitidentity ge_second_rp_rectangle_scanabsentnonunitidentity ge_second_rn_rectangle_scanabsentnonunitidentity ge_second_ip_rectangle_scanabsentnonunitidentity ge_second_in_rectangle_scanabsentnonunitidentity. ((exists ge_representation_real_code_rectangle_scanabsentnonunitidentityfirst ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst. (((((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) * S ((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) + ((gr_rectangle_imaginary_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan))) = ((ge_representation_real_code_rectangle_scanabsentnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst)) * S ((ge_representation_real_code_rectangle_scanabsentnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst)) + ((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst))) /\ ((exists ge_balance_positive_rectangle_scanabsentnonunitidentityfirstreal ge_balance_negative_rectangle_scanabsentnonunitidentityfirstreal. (((((ge_representation_real_code_rectangle_scanabsentnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_scanabsentnonunitidentityfirstreal) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentnonunitidentityfirstrealdecode. (((ge_representation_real_code_rectangle_scanabsentnonunitidentityfirst) = 2 * ge_signed_half_rectangle_scanabsentnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityfirstreal) = S ge_signed_half_rectangle_scanabsentnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_rectangle_scanabsentnonunitidentity) + ge_balance_negative_rectangle_scanabsentnonunitidentityfirstreal = (ge_first_rn_rectangle_scanabsentnonunitidentity) + ge_balance_positive_rectangle_scanabsentnonunitidentityfirstreal))) /\ (exists ge_balance_positive_rectangle_scanabsentnonunitidentityfirstimaginary ge_balance_negative_rectangle_scanabsentnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_scanabsentnonunitidentityfirstimaginary) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst) = 2 * ge_signed_half_rectangle_scanabsentnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityfirstimaginary) = S ge_signed_half_rectangle_scanabsentnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_scanabsentnonunitidentity) + ge_balance_negative_rectangle_scanabsentnonunitidentityfirstimaginary = (ge_first_in_rectangle_scanabsentnonunitidentity) + ge_balance_positive_rectangle_scanabsentnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_scanabsentnonunitidentitysecond ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond. (((gr_inverse_rectangle_scanabsentnonunit) = ((ge_representation_real_code_rectangle_scanabsentnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond)) * S ((ge_representation_real_code_rectangle_scanabsentnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond)) + ((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond))) /\ ((exists ge_balance_positive_rectangle_scanabsentnonunitidentitysecondreal ge_balance_negative_rectangle_scanabsentnonunitidentitysecondreal. (((((ge_representation_real_code_rectangle_scanabsentnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_scanabsentnonunitidentitysecondreal) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentnonunitidentitysecondrealdecode. (((ge_representation_real_code_rectangle_scanabsentnonunitidentitysecond) = 2 * ge_signed_half_rectangle_scanabsentnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentitysecondreal) = S ge_signed_half_rectangle_scanabsentnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_rectangle_scanabsentnonunitidentity) + ge_balance_negative_rectangle_scanabsentnonunitidentitysecondreal = (ge_second_rn_rectangle_scanabsentnonunitidentity) + ge_balance_positive_rectangle_scanabsentnonunitidentitysecondreal))) /\ (exists ge_balance_positive_rectangle_scanabsentnonunitidentitysecondimaginary ge_balance_negative_rectangle_scanabsentnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_scanabsentnonunitidentitysecondimaginary) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond) = 2 * ge_signed_half_rectangle_scanabsentnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentitysecondimaginary) = S ge_signed_half_rectangle_scanabsentnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_rectangle_scanabsentnonunitidentity) + ge_balance_negative_rectangle_scanabsentnonunitidentitysecondimaginary = (ge_second_in_rectangle_scanabsentnonunitidentity) + ge_balance_positive_rectangle_scanabsentnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_scanabsentnonunitidentityoutput ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput. (((6) = ((ge_representation_real_code_rectangle_scanabsentnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput)) * S ((ge_representation_real_code_rectangle_scanabsentnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput)) + ((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput))) /\ ((exists ge_balance_positive_rectangle_scanabsentnonunitidentityoutputreal ge_balance_negative_rectangle_scanabsentnonunitidentityoutputreal. (((((ge_representation_real_code_rectangle_scanabsentnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_scanabsentnonunitidentityoutputreal) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentnonunitidentityoutputrealdecode. (((ge_representation_real_code_rectangle_scanabsentnonunitidentityoutput) = 2 * ge_signed_half_rectangle_scanabsentnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityoutputreal) = S ge_signed_half_rectangle_scanabsentnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_scanabsentnonunitidentity) * (ge_second_rp_rectangle_scanabsentnonunitidentity))) + (((ge_first_rn_rectangle_scanabsentnonunitidentity) * (ge_second_rn_rectangle_scanabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_scanabsentnonunitidentity) * (ge_second_in_rectangle_scanabsentnonunitidentity))) + (((ge_first_in_rectangle_scanabsentnonunitidentity) * (ge_second_ip_rectangle_scanabsentnonunitidentity))))))) + ge_balance_negative_rectangle_scanabsentnonunitidentityoutputreal = (((((((ge_first_rp_rectangle_scanabsentnonunitidentity) * (ge_second_rn_rectangle_scanabsentnonunitidentity))) + (((ge_first_rn_rectangle_scanabsentnonunitidentity) * (ge_second_rp_rectangle_scanabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_scanabsentnonunitidentity) * (ge_second_ip_rectangle_scanabsentnonunitidentity))) + (((ge_first_in_rectangle_scanabsentnonunitidentity) * (ge_second_in_rectangle_scanabsentnonunitidentity))))))) + ge_balance_positive_rectangle_scanabsentnonunitidentityoutputreal))) /\ (exists ge_balance_positive_rectangle_scanabsentnonunitidentityoutputimaginary ge_balance_negative_rectangle_scanabsentnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_scanabsentnonunitidentityoutputimaginary) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput) = 2 * ge_signed_half_rectangle_scanabsentnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityoutputimaginary) = S ge_signed_half_rectangle_scanabsentnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_scanabsentnonunitidentity) * (ge_second_ip_rectangle_scanabsentnonunitidentity))) + (((ge_first_rn_rectangle_scanabsentnonunitidentity) * (ge_second_in_rectangle_scanabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_scanabsentnonunitidentity) * (ge_second_rp_rectangle_scanabsentnonunitidentity))) + (((ge_first_in_rectangle_scanabsentnonunitidentity) * (ge_second_rn_rectangle_scanabsentnonunitidentity))))))) + ge_balance_negative_rectangle_scanabsentnonunitidentityoutputimaginary = (((((((ge_first_rp_rectangle_scanabsentnonunitidentity) * (ge_second_in_rectangle_scanabsentnonunitidentity))) + (((ge_first_rn_rectangle_scanabsentnonunitidentity) * (ge_second_ip_rectangle_scanabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_scanabsentnonunitidentity) * (ge_second_rn_rectangle_scanabsentnonunitidentity))) + (((ge_first_in_rectangle_scanabsentnonunitidentity) * (ge_second_rp_rectangle_scanabsentnonunitidentity))))))) + ge_balance_positive_rectangle_scanabsentnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_rectangle_scanabsentquotient. (exists ge_first_rp_rectangle_scanabsentquotientproduct ge_first_rn_rectangle_scanabsentquotientproduct ge_first_ip_rectangle_scanabsentquotientproduct ge_first_in_rectangle_scanabsentquotientproduct ge_second_rp_rectangle_scanabsentquotientproduct ge_second_rn_rectangle_scanabsentquotientproduct ge_second_ip_rectangle_scanabsentquotientproduct ge_second_in_rectangle_scanabsentquotientproduct. ((exists ge_representation_real_code_rectangle_scanabsentquotientproductfirst ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst. (((((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) * S ((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) + ((gr_rectangle_imaginary_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan))) = ((ge_representation_real_code_rectangle_scanabsentquotientproductfirst) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst)) * S ((ge_representation_real_code_rectangle_scanabsentquotientproductfirst) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst)) + ((ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst))) /\ ((exists ge_balance_positive_rectangle_scanabsentquotientproductfirstreal ge_balance_negative_rectangle_scanabsentquotientproductfirstreal. (((((ge_representation_real_code_rectangle_scanabsentquotientproductfirst) = 2 * (ge_balance_positive_rectangle_scanabsentquotientproductfirstreal) /\ (ge_balance_negative_rectangle_scanabsentquotientproductfirstreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentquotientproductfirstrealdecode. (((ge_representation_real_code_rectangle_scanabsentquotientproductfirst) = 2 * ge_signed_half_rectangle_scanabsentquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentquotientproductfirstreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentquotientproductfirstreal) = S ge_signed_half_rectangle_scanabsentquotientproductfirstrealdecode))) /\ ((ge_first_rp_rectangle_scanabsentquotientproduct) + ge_balance_negative_rectangle_scanabsentquotientproductfirstreal = (ge_first_rn_rectangle_scanabsentquotientproduct) + ge_balance_positive_rectangle_scanabsentquotientproductfirstreal))) /\ (exists ge_balance_positive_rectangle_scanabsentquotientproductfirstimaginary ge_balance_negative_rectangle_scanabsentquotientproductfirstimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst) = 2 * (ge_balance_positive_rectangle_scanabsentquotientproductfirstimaginary) /\ (ge_balance_negative_rectangle_scanabsentquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst) = 2 * ge_signed_half_rectangle_scanabsentquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentquotientproductfirstimaginary) = S ge_signed_half_rectangle_scanabsentquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_scanabsentquotientproduct) + ge_balance_negative_rectangle_scanabsentquotientproductfirstimaginary = (ge_first_in_rectangle_scanabsentquotientproduct) + ge_balance_positive_rectangle_scanabsentquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_scanabsentquotientproductsecond ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond. (((gr_quotient_rectangle_scanabsentquotient) = ((ge_representation_real_code_rectangle_scanabsentquotientproductsecond) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond)) * S ((ge_representation_real_code_rectangle_scanabsentquotientproductsecond) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond)) + ((ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond))) /\ ((exists ge_balance_positive_rectangle_scanabsentquotientproductsecondreal ge_balance_negative_rectangle_scanabsentquotientproductsecondreal. (((((ge_representation_real_code_rectangle_scanabsentquotientproductsecond) = 2 * (ge_balance_positive_rectangle_scanabsentquotientproductsecondreal) /\ (ge_balance_negative_rectangle_scanabsentquotientproductsecondreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentquotientproductsecondrealdecode. (((ge_representation_real_code_rectangle_scanabsentquotientproductsecond) = 2 * ge_signed_half_rectangle_scanabsentquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentquotientproductsecondreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentquotientproductsecondreal) = S ge_signed_half_rectangle_scanabsentquotientproductsecondrealdecode))) /\ ((ge_second_rp_rectangle_scanabsentquotientproduct) + ge_balance_negative_rectangle_scanabsentquotientproductsecondreal = (ge_second_rn_rectangle_scanabsentquotientproduct) + ge_balance_positive_rectangle_scanabsentquotientproductsecondreal))) /\ (exists ge_balance_positive_rectangle_scanabsentquotientproductsecondimaginary ge_balance_negative_rectangle_scanabsentquotientproductsecondimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond) = 2 * (ge_balance_positive_rectangle_scanabsentquotientproductsecondimaginary) /\ (ge_balance_negative_rectangle_scanabsentquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond) = 2 * ge_signed_half_rectangle_scanabsentquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentquotientproductsecondimaginary) = S ge_signed_half_rectangle_scanabsentquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_rectangle_scanabsentquotientproduct) + ge_balance_negative_rectangle_scanabsentquotientproductsecondimaginary = (ge_second_in_rectangle_scanabsentquotientproduct) + ge_balance_positive_rectangle_scanabsentquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_scanabsentquotientproductoutput ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput. (((z) = ((ge_representation_real_code_rectangle_scanabsentquotientproductoutput) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput)) * S ((ge_representation_real_code_rectangle_scanabsentquotientproductoutput) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput)) + ((ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput))) /\ ((exists ge_balance_positive_rectangle_scanabsentquotientproductoutputreal ge_balance_negative_rectangle_scanabsentquotientproductoutputreal. (((((ge_representation_real_code_rectangle_scanabsentquotientproductoutput) = 2 * (ge_balance_positive_rectangle_scanabsentquotientproductoutputreal) /\ (ge_balance_negative_rectangle_scanabsentquotientproductoutputreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentquotientproductoutputrealdecode. (((ge_representation_real_code_rectangle_scanabsentquotientproductoutput) = 2 * ge_signed_half_rectangle_scanabsentquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentquotientproductoutputreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentquotientproductoutputreal) = S ge_signed_half_rectangle_scanabsentquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_scanabsentquotientproduct) * (ge_second_rp_rectangle_scanabsentquotientproduct))) + (((ge_first_rn_rectangle_scanabsentquotientproduct) * (ge_second_rn_rectangle_scanabsentquotientproduct))))) + (((((ge_first_ip_rectangle_scanabsentquotientproduct) * (ge_second_in_rectangle_scanabsentquotientproduct))) + (((ge_first_in_rectangle_scanabsentquotientproduct) * (ge_second_ip_rectangle_scanabsentquotientproduct))))))) + ge_balance_negative_rectangle_scanabsentquotientproductoutputreal = (((((((ge_first_rp_rectangle_scanabsentquotientproduct) * (ge_second_rn_rectangle_scanabsentquotientproduct))) + (((ge_first_rn_rectangle_scanabsentquotientproduct) * (ge_second_rp_rectangle_scanabsentquotientproduct))))) + (((((ge_first_ip_rectangle_scanabsentquotientproduct) * (ge_second_ip_rectangle_scanabsentquotientproduct))) + (((ge_first_in_rectangle_scanabsentquotientproduct) * (ge_second_in_rectangle_scanabsentquotientproduct))))))) + ge_balance_positive_rectangle_scanabsentquotientproductoutputreal))) /\ (exists ge_balance_positive_rectangle_scanabsentquotientproductoutputimaginary ge_balance_negative_rectangle_scanabsentquotientproductoutputimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput) = 2 * (ge_balance_positive_rectangle_scanabsentquotientproductoutputimaginary) /\ (ge_balance_negative_rectangle_scanabsentquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput) = 2 * ge_signed_half_rectangle_scanabsentquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentquotientproductoutputimaginary) = S ge_signed_half_rectangle_scanabsentquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_scanabsentquotientproduct) * (ge_second_ip_rectangle_scanabsentquotientproduct))) + (((ge_first_rn_rectangle_scanabsentquotientproduct) * (ge_second_in_rectangle_scanabsentquotientproduct))))) + (((((ge_first_ip_rectangle_scanabsentquotientproduct) * (ge_second_rp_rectangle_scanabsentquotientproduct))) + (((ge_first_in_rectangle_scanabsentquotientproduct) * (ge_second_rn_rectangle_scanabsentquotientproduct))))))) + ge_balance_negative_rectangle_scanabsentquotientproductoutputimaginary = (((((((ge_first_rp_rectangle_scanabsentquotientproduct) * (ge_second_in_rectangle_scanabsentquotientproduct))) + (((ge_first_rn_rectangle_scanabsentquotientproduct) * (ge_second_ip_rectangle_scanabsentquotientproduct))))) + (((((ge_first_ip_rectangle_scanabsentquotientproduct) * (ge_second_rn_rectangle_scanabsentquotientproduct))) + (((ge_first_in_rectangle_scanabsentquotientproduct) * (ge_second_rp_rectangle_scanabsentquotientproduct))))))) + ge_balance_positive_rectangle_scanabsentquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_rectangle_scanabsent. ((exists ge_norm_rp_rectangle_scanabsentnorm ge_norm_rn_rectangle_scanabsentnorm ge_norm_ip_rectangle_scanabsentnorm ge_norm_in_rectangle_scanabsentnorm. ((exists ge_representation_real_code_rectangle_scanabsentnormrepresentation ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation. (((((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) * S ((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) + ((gr_rectangle_imaginary_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan))) = ((ge_representation_real_code_rectangle_scanabsentnormrepresentation) + (ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation)) * S ((ge_representation_real_code_rectangle_scanabsentnormrepresentation) + (ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation)) + ((ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation) + (ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation))) /\ ((exists ge_balance_positive_rectangle_scanabsentnormrepresentationreal ge_balance_negative_rectangle_scanabsentnormrepresentationreal. (((((ge_representation_real_code_rectangle_scanabsentnormrepresentation) = 2 * (ge_balance_positive_rectangle_scanabsentnormrepresentationreal) /\ (ge_balance_negative_rectangle_scanabsentnormrepresentationreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentnormrepresentationrealdecode. (((ge_representation_real_code_rectangle_scanabsentnormrepresentation) = 2 * ge_signed_half_rectangle_scanabsentnormrepresentationrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnormrepresentationreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentnormrepresentationreal) = S ge_signed_half_rectangle_scanabsentnormrepresentationrealdecode))) /\ ((ge_norm_rp_rectangle_scanabsentnorm) + ge_balance_negative_rectangle_scanabsentnormrepresentationreal = (ge_norm_rn_rectangle_scanabsentnorm) + ge_balance_positive_rectangle_scanabsentnormrepresentationreal))) /\ (exists ge_balance_positive_rectangle_scanabsentnormrepresentationimaginary ge_balance_negative_rectangle_scanabsentnormrepresentationimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation) = 2 * (ge_balance_positive_rectangle_scanabsentnormrepresentationimaginary) /\ (ge_balance_negative_rectangle_scanabsentnormrepresentationimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation) = 2 * ge_signed_half_rectangle_scanabsentnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnormrepresentationimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentnormrepresentationimaginary) = S ge_signed_half_rectangle_scanabsentnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_rectangle_scanabsentnorm) + ge_balance_negative_rectangle_scanabsentnormrepresentationimaginary = (ge_norm_in_rectangle_scanabsentnorm) + ge_balance_positive_rectangle_scanabsentnormrepresentationimaginary)))))) /\ (exists ge_real_square_rectangle_scanabsentnormsquare ge_imaginary_square_rectangle_scanabsentnormsquare. ((((((ge_norm_rp_rectangle_scanabsentnorm) * (ge_norm_rp_rectangle_scanabsentnorm))) + (((ge_norm_rn_rectangle_scanabsentnorm) * (ge_norm_rn_rectangle_scanabsentnorm)))) = ((ge_real_square_rectangle_scanabsentnormsquare) + (((((ge_norm_rp_rectangle_scanabsentnorm) * (ge_norm_rn_rectangle_scanabsentnorm))) + (((ge_norm_rn_rectangle_scanabsentnorm) * (ge_norm_rp_rectangle_scanabsentnorm))))))) /\ ((((((ge_norm_ip_rectangle_scanabsentnorm) * (ge_norm_ip_rectangle_scanabsentnorm))) + (((ge_norm_in_rectangle_scanabsentnorm) * (ge_norm_in_rectangle_scanabsentnorm)))) = ((ge_imaginary_square_rectangle_scanabsentnormsquare) + (((((ge_norm_ip_rectangle_scanabsentnorm) * (ge_norm_in_rectangle_scanabsentnorm))) + (((ge_norm_in_rectangle_scanabsentnorm) * (ge_norm_ip_rectangle_scanabsentnorm))))))) /\ ((gr_proper_divisor_norm_rectangle_scanabsent) = ge_real_square_rectangle_scanabsentnormsquare + ge_imaginary_square_rectangle_scanabsentnormsquare)))))) /\ (exists ge_gap_rectangle_scanabsentstrict. ge_gap_rectangle_scanabsentstrict + S (gr_proper_divisor_norm_rectangle_scanabsent) = (N)))))))))

Complete tactic proof in conservative notation

All 92 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

92 script commands · 27 reading checkpoints · 3 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 (3)
gaussian search no index below zerogaussian factor search coordinate rowgaussian search proper divisor code transport
01Induction on hL1–5

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

  1. L1
    induction h
  2. L2
    intro z
  3. L3
    intro N
  4. L4
    intro k
  5. L5
    intro hz
02Separate the logical casesL6–6

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

  1. L6
    right
03Fix variables and assumptionsL7–11

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

  1. L7
    intro rc
  2. L8
    intro ic
  3. L9
    intro hr
  4. L10
    intro hi
  5. L11
    intro hp
04Use earlier factsL12–14

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

  1. L12
    specialize gaussian_search_no_index_below_zero (rc)
  2. L13
    apply gaussian_search_no_index_below_zero
  3. L14
    exact hr
05Fix variables and assumptionsL15–18

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

  1. L15
    intro z
  2. L16
    intro N
  3. L17
    intro k
  4. L18
    intro hz
06Establish hpreviousL19–24

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

  1. L19
    have hprevious : (∃ x. ∃ y. Lt(x,h) ∧ (Lt(y,k) ∧ GProperNormDivisor((x + y) · S (x + y) + (y + y),z,N))) ∨ (∀ x. ∀ y. Lt(x,h) → Lt(y,k) → ¬GProperNormDivisor((x + y) · S (x + y) + (y + y),z,N))Definitions: Lt(x,h)Lt(y,k)GProperNormDivisor((x + y) · S (x + y) + (y + y),z,N)Original native command in the exact edition
  2. L20
    specialize IH (z)
  3. L21
    specialize IH (N)
  4. L22
    specialize IH (k)
  5. L23
    apply IH
  6. L24
    exact hz
07Separate the logical casesL25–30

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

  1. L25
    cases hprevious
  2. L26
    cases hprevious_left
  3. L27
    cases hprevious_left_witness
  4. L28
    cases hprevious_left_witness_witness
  5. L29
    cases hprevious_left_witness_witness_right
  6. L30
    left
08Construct an explicit witnessL31–32

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

  1. L31
    exists (x)
  2. L32
    exists (x1)
09Separate the logical casesL33–33

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

  1. L33
    split
10Use earlier factsL34–40

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

  1. L34
    specialize lt_of_lt_of_le (x)
  2. L35
    specialize lt_of_lt_of_le (h)
  3. L36
    specialize lt_of_lt_of_le (S h)
  4. L37
    apply lt_of_lt_of_le
  5. L38
    exact hprevious_left_witness_witness_left
  6. L39
    specialize le_succ_self (h)
  7. L40
    apply le_succ_self
11Separate the logical casesL41–41

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

  1. L41
    split
12Use earlier factsL42–43

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

  1. L42
    exact hprevious_left_witness_witness_right_left
  2. L43
    exact hprevious_left_witness_witness_right_right
13Establish hlastL44–50

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian factor search coordinate row.

  1. L44
    have hlast : (∃ x. Lt(x,k) ∧ GProperNormDivisor((h + x) · S (h + x) + (x + x),z,N)) ∨ (∀ x. Lt(x,k) → ¬GProperNormDivisor((h + x) · S (h + x) + (x + x),z,N))Definitions: Lt(x,k)GProperNormDivisor((h + x) · S (h + x) + (x + x),z,N)Original native command in the exact edition
  2. L45
    specialize gaussian_factor_search_coordinate_row (k)
  3. L46
    specialize gaussian_factor_search_coordinate_row (z)
  4. L47
    specialize gaussian_factor_search_coordinate_row (N)
  5. L48
    specialize gaussian_factor_search_coordinate_row (h)
  6. L49
    apply gaussian_factor_search_coordinate_row
  7. L50
    exact hz
14Separate the logical casesL51–54

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

  1. L51
    cases hlast
  2. L52
    cases hlast_left
  3. L53
    cases hlast_left_witness
  4. L54
    left
15Construct an explicit witnessL55–56

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

  1. L55
    exists (h)
  2. L56
    exists (x)
16Separate the logical casesL57–57

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

  1. L57
    split
17Construct an explicit witnessL58–58

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

  1. L58
    exists 0
18Use earlier factsL59–59

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

  1. L59
    apply zero_add
19Separate the logical casesL60–60

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

  1. L60
    split
20Use earlier factsL61–62

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

  1. L61
    exact hlast_left_witness_left
  2. L62
    exact hlast_left_witness_right
21Separate the logical casesL63–63

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

  1. L63
    right
22Fix variables and assumptionsL64–68

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

  1. L64
    intro rc
  2. L65
    intro ic
  3. L66
    intro hr
  4. L67
    intro hi
  5. L68
    intro hp
23Establish hcL69–73

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

  1. L69
    have hc : rc = h ∨ Lt(rc,h)Definitions: Lt(rc,h)Original native command in the exact edition
  2. L70
    specialize finite_lt_succ_eq_or_lt (h)
  3. L71
    specialize finite_lt_succ_eq_or_lt (rc)
  4. L72
    apply finite_lt_succ_eq_or_lt
  5. L73
    exact hr
24Separate the logical casesL74–74

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

  1. L74
    cases hc
25Use earlier factsL75–82

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

  1. L75
    specialize hlast_right (ic)
  2. L76
    apply hlast_right
  3. L77
    exact hi
  4. L78
    specialize gaussian_search_proper_divisor_code_transport (((rc) + (ic)) * S ((rc) + (ic)) + ((ic) + (ic)))
  5. L79
    specialize gaussian_search_proper_divisor_code_transport (((h) + (ic)) * S ((h) + (ic)) + ((ic) + (ic)))
  6. L80
    specialize gaussian_search_proper_divisor_code_transport (z)
  7. L81
    specialize gaussian_search_proper_divisor_code_transport (N)
  8. L82
    apply gaussian_search_proper_divisor_code_transport
26Calculate and transport equalitiesL83–85

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

  1. L83
    rewrite hc_left
  2. L84
    rewrite hc_left
  3. L85
    refl
27Use earlier factsL86–92

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

  1. L86
    exact hp
  2. L87
    specialize hprevious_right (rc)
  3. L88
    specialize hprevious_right (ic)
  4. L89
    apply hprevious_right
  5. L90
    exact hc_right
  6. L91
    exact hi
  7. L92
    exact hp

Library-wide reading audit

Original defined command ledger · 92 lines
  1. 0001induction h
  2. 0002intro z
  3. 0003intro N
  4. 0004intro k
  5. 0005intro hz
  6. 0006right
  7. 0007intro rc
  8. 0008intro ic
  9. 0009intro hr
  10. 0010intro hi
  11. 0011intro hp
  12. 0012specialize gaussian_search_no_index_below_zero (rc)
  13. 0013apply gaussian_search_no_index_below_zero
  14. 0014exact hr
  15. 0015intro z
  16. 0016intro N
  17. 0017intro k
  18. 0018intro hz
  19. 0019have hprevious : (∃ x. ∃ y. Lt(x,h) ∧ (Lt(y,k) ∧ GProperNormDivisor((x + y) · S (x + y) + (y + y),z,N))) ∨ (∀ x. ∀ y. Lt(x,h) → Lt(y,k) → ¬GProperNormDivisor((x + y) · S (x + y) + (y + y),z,N))
  20. 0020specialize IH (z)
  21. 0021specialize IH (N)
  22. 0022specialize IH (k)
  23. 0023apply IH
  24. 0024exact hz
  25. 0025cases hprevious
  26. 0026cases hprevious_left
  27. 0027cases hprevious_left_witness
  28. 0028cases hprevious_left_witness_witness
  29. 0029cases hprevious_left_witness_witness_right
  30. 0030left
  31. 0031exists (x)
  32. 0032exists (x1)
  33. 0033split
  34. 0034specialize lt_of_lt_of_le (x)
  35. 0035specialize lt_of_lt_of_le (h)
  36. 0036specialize lt_of_lt_of_le (S h)
  37. 0037apply lt_of_lt_of_le
  38. 0038exact hprevious_left_witness_witness_left
  39. 0039specialize le_succ_self (h)
  40. 0040apply le_succ_self
  41. 0041split
  42. 0042exact hprevious_left_witness_witness_right_left
  43. 0043exact hprevious_left_witness_witness_right_right
  44. 0044have hlast : (∃ x. Lt(x,k) ∧ GProperNormDivisor((h + x) · S (h + x) + (x + x),z,N)) ∨ (∀ x. Lt(x,k) → ¬GProperNormDivisor((h + x) · S (h + x) + (x + x),z,N))
  45. 0045specialize gaussian_factor_search_coordinate_row (k)
  46. 0046specialize gaussian_factor_search_coordinate_row (z)
  47. 0047specialize gaussian_factor_search_coordinate_row (N)
  48. 0048specialize gaussian_factor_search_coordinate_row (h)
  49. 0049apply gaussian_factor_search_coordinate_row
  50. 0050exact hz
  51. 0051cases hlast
  52. 0052cases hlast_left
  53. 0053cases hlast_left_witness
  54. 0054left
  55. 0055exists (h)
  56. 0056exists (x)
  57. 0057split
  58. 0058exists 0
  59. 0059apply zero_add
  60. 0060split
  61. 0061exact hlast_left_witness_left
  62. 0062exact hlast_left_witness_right
  63. 0063right
  64. 0064intro rc
  65. 0065intro ic
  66. 0066intro hr
  67. 0067intro hi
  68. 0068intro hp
  69. 0069have hc : rc = h ∨ Lt(rc,h)
  70. 0070specialize finite_lt_succ_eq_or_lt (h)
  71. 0071specialize finite_lt_succ_eq_or_lt (rc)
  72. 0072apply finite_lt_succ_eq_or_lt
  73. 0073exact hr
  74. 0074cases hc
  75. 0075specialize hlast_right (ic)
  76. 0076apply hlast_right
  77. 0077exact hi
  78. 0078specialize gaussian_search_proper_divisor_code_transport (((rc) + (ic)) * S ((rc) + (ic)) + ((ic) + (ic)))
  79. 0079specialize gaussian_search_proper_divisor_code_transport (((h) + (ic)) * S ((h) + (ic)) + ((ic) + (ic)))
  80. 0080specialize gaussian_search_proper_divisor_code_transport (z)
  81. 0081specialize gaussian_search_proper_divisor_code_transport (N)
  82. 0082apply gaussian_search_proper_divisor_code_transport
  83. 0083rewrite hc_left
  84. 0084rewrite hc_left
  85. 0085refl
  86. 0086exact hp
  87. 0087specialize hprevious_right (rc)
  88. 0088specialize hprevious_right (ic)
  89. 0089apply hprevious_right
  90. 0090exact hc_right
  91. 0091exact hi
  92. 0092exact hp