GF00A7

gaussian_factor_empty_matching

The actual zero beta map is a bounded, injective, surjective unit-matching bijection between any two empty factor prefixes.

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

∀ b. ∀ c. ∀ d. ∀ e. GMatchedFactors(b,c,d,e,0,0,0)

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

Definition DAG

GMatchedFactors(b,c,d,e,u,v,l) · 1

Actual proof prerequisites

gaussian_search_no_index_below_zero
Original expanded first-order statement 
forall b c d e. (((((forall pfp_i_empty_matchingbijectionbounded. (exists pfp_gap_empty_matchingbijectionboundedindex. pfp_gap_empty_matchingbijectionboundedindex + S (pfp_i_empty_matchingbijectionbounded) = (0)) -> exists pfp_a_empty_matchingbijectionbounded. (((exists ff_h_pfp_empty_matchingbijectionboundedentry. ff_h_pfp_empty_matchingbijectionboundedentry + S (pfp_a_empty_matchingbijectionbounded) = S ((S (pfp_i_empty_matchingbijectionbounded)) * 0)) /\ exists ff_q_pfp_empty_matchingbijectionboundedentry. 0 = ff_q_pfp_empty_matchingbijectionboundedentry * S ((S (pfp_i_empty_matchingbijectionbounded)) * 0) + (pfp_a_empty_matchingbijectionbounded))) /\ (exists pfp_gap_empty_matchingbijectionboundedvalue. pfp_gap_empty_matchingbijectionboundedvalue + S (pfp_a_empty_matchingbijectionbounded) = (0))) /\ (((forall pfp_i_empty_matchingbijectioninjective pfp_j_empty_matchingbijectioninjective pfp_a_empty_matchingbijectioninjective. (exists pfp_gap_empty_matchingbijectioninjectivefirst. pfp_gap_empty_matchingbijectioninjectivefirst + S (pfp_i_empty_matchingbijectioninjective) = (0)) -> (exists pfp_gap_empty_matchingbijectioninjectivesecond. pfp_gap_empty_matchingbijectioninjectivesecond + S (pfp_j_empty_matchingbijectioninjective) = (0)) -> (((exists ff_h_pfp_empty_matchingbijectioninjectiveleft. ff_h_pfp_empty_matchingbijectioninjectiveleft + S (pfp_a_empty_matchingbijectioninjective) = S ((S (pfp_i_empty_matchingbijectioninjective)) * 0)) /\ exists ff_q_pfp_empty_matchingbijectioninjectiveleft. 0 = ff_q_pfp_empty_matchingbijectioninjectiveleft * S ((S (pfp_i_empty_matchingbijectioninjective)) * 0) + (pfp_a_empty_matchingbijectioninjective))) -> (((exists ff_h_pfp_empty_matchingbijectioninjectiveright. ff_h_pfp_empty_matchingbijectioninjectiveright + S (pfp_a_empty_matchingbijectioninjective) = S ((S (pfp_j_empty_matchingbijectioninjective)) * 0)) /\ exists ff_q_pfp_empty_matchingbijectioninjectiveright. 0 = ff_q_pfp_empty_matchingbijectioninjectiveright * S ((S (pfp_j_empty_matchingbijectioninjective)) * 0) + (pfp_a_empty_matchingbijectioninjective))) -> pfp_i_empty_matchingbijectioninjective = pfp_j_empty_matchingbijectioninjective) /\ (forall pfp_a_empty_matchingbijectionsurjective. (exists pfp_gap_empty_matchingbijectionsurjectivevalue. pfp_gap_empty_matchingbijectionsurjectivevalue + S (pfp_a_empty_matchingbijectionsurjective) = (0)) -> exists pfp_i_empty_matchingbijectionsurjective. (exists pfp_gap_empty_matchingbijectionsurjectiveindex. pfp_gap_empty_matchingbijectionsurjectiveindex + S (pfp_i_empty_matchingbijectionsurjective) = (0)) /\ (((exists ff_h_pfp_empty_matchingbijectionsurjectiveentry. ff_h_pfp_empty_matchingbijectionsurjectiveentry + S (pfp_a_empty_matchingbijectionsurjective) = S ((S (pfp_i_empty_matchingbijectionsurjective)) * 0)) /\ exists ff_q_pfp_empty_matchingbijectionsurjectiveentry. 0 = ff_q_pfp_empty_matchingbijectionsurjectiveentry * S ((S (pfp_i_empty_matchingbijectionsurjective)) * 0) + (pfp_a_empty_matchingbijectionsurjective)))))))) /\ (forall gr_match_index_empty_matchingmatching gr_match_image_empty_matchingmatching gr_match_source_empty_matchingmatching gr_match_target_empty_matchingmatching. (exists ge_gap_empty_matchingmatchingindex. ge_gap_empty_matchingmatchingindex + S (gr_match_index_empty_matchingmatching) = (0)) -> (((exists ff_h_gprod_empty_matchingmatchingmap. ff_h_gprod_empty_matchingmatchingmap + S (gr_match_image_empty_matchingmatching) = S ((S (gr_match_index_empty_matchingmatching)) * 0)) /\ exists ff_q_gprod_empty_matchingmatchingmap. 0 = ff_q_gprod_empty_matchingmatchingmap * S ((S (gr_match_index_empty_matchingmatching)) * 0) + (gr_match_image_empty_matchingmatching))) -> (((exists ff_h_gprod_empty_matchingmatchingsource. ff_h_gprod_empty_matchingmatchingsource + S (gr_match_source_empty_matchingmatching) = S ((S (gr_match_index_empty_matchingmatching)) * c)) /\ exists ff_q_gprod_empty_matchingmatchingsource. b = ff_q_gprod_empty_matchingmatchingsource * S ((S (gr_match_index_empty_matchingmatching)) * c) + (gr_match_source_empty_matchingmatching))) -> (((exists ff_h_gprod_empty_matchingmatchingtarget. ff_h_gprod_empty_matchingmatchingtarget + S (gr_match_target_empty_matchingmatching) = S ((S (gr_match_image_empty_matchingmatching)) * e)) /\ exists ff_q_gprod_empty_matchingmatchingtarget. d = ff_q_gprod_empty_matchingmatchingtarget * S ((S (gr_match_image_empty_matchingmatching)) * e) + (gr_match_target_empty_matchingmatching))) -> (exists gr_unit_empty_matchingmatchingunit_witness. ((exists gr_inverse_empty_matchingmatchingunit_witnessunit. (exists ge_first_rp_empty_matchingmatchingunit_witnessunitidentity ge_first_rn_empty_matchingmatchingunit_witnessunitidentity ge_first_ip_empty_matchingmatchingunit_witnessunitidentity ge_first_in_empty_matchingmatchingunit_witnessunitidentity ge_second_rp_empty_matchingmatchingunit_witnessunitidentity ge_second_rn_empty_matchingmatchingunit_witnessunitidentity ge_second_ip_empty_matchingmatchingunit_witnessunitidentity ge_second_in_empty_matchingmatchingunit_witnessunitidentity. ((exists ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityfirst ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst. (((gr_unit_empty_matchingmatchingunit_witness) = ((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstreal ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_empty_matchingmatchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstreal) = S ge_signed_half_empty_matchingmatchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstreal = (ge_first_rn_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstimaginary ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_empty_matchingmatchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_empty_matchingmatchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstimaginary = (ge_first_in_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentitysecond ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond. (((gr_inverse_empty_matchingmatchingunit_witnessunit) = ((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondreal ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_empty_matchingmatchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondreal) = S ge_signed_half_empty_matchingmatchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondreal = (ge_second_rn_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondimaginary ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_empty_matchingmatchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_empty_matchingmatchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondimaginary = (ge_second_in_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityoutput ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputreal ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_empty_matchingmatchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputreal) = S ge_signed_half_empty_matchingmatchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rp_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rn_empty_matchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_in_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_in_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_ip_empty_matchingmatchingunit_witnessunitidentity))))))) + ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rn_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rp_empty_matchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_ip_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_in_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_in_empty_matchingmatchingunit_witnessunitidentity))))))) + ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputimaginary ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_empty_matchingmatchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_empty_matchingmatchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_ip_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_in_empty_matchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rp_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_in_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rn_empty_matchingmatchingunit_witnessunitidentity))))))) + ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_in_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_ip_empty_matchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rn_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_in_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rp_empty_matchingmatchingunit_witnessunitidentity))))))) + ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_empty_matchingmatchingunit_witnesstransport ge_first_rn_empty_matchingmatchingunit_witnesstransport ge_first_ip_empty_matchingmatchingunit_witnesstransport ge_first_in_empty_matchingmatchingunit_witnesstransport ge_second_rp_empty_matchingmatchingunit_witnesstransport ge_second_rn_empty_matchingmatchingunit_witnesstransport ge_second_ip_empty_matchingmatchingunit_witnesstransport ge_second_in_empty_matchingmatchingunit_witnesstransport. ((exists ge_representation_real_code_empty_matchingmatchingunit_witnesstransportfirst ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst. (((gr_unit_empty_matchingmatchingunit_witness) = ((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstreal ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_empty_matchingmatchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstreal) = S ge_signed_half_empty_matchingmatchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_empty_matchingmatchingunit_witnesstransport) + ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstreal = (ge_first_rn_empty_matchingmatchingunit_witnesstransport) + ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstimaginary ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_empty_matchingmatchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstimaginary) = S ge_signed_half_empty_matchingmatchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_empty_matchingmatchingunit_witnesstransport) + ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstimaginary = (ge_first_in_empty_matchingmatchingunit_witnesstransport) + ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_empty_matchingmatchingunit_witnesstransportsecond ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond. (((gr_match_source_empty_matchingmatching) = ((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondreal ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_empty_matchingmatchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondreal) = S ge_signed_half_empty_matchingmatchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_empty_matchingmatchingunit_witnesstransport) + ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondreal = (ge_second_rn_empty_matchingmatchingunit_witnesstransport) + ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondimaginary ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_empty_matchingmatchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondimaginary) = S ge_signed_half_empty_matchingmatchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_empty_matchingmatchingunit_witnesstransport) + ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondimaginary = (ge_second_in_empty_matchingmatchingunit_witnesstransport) + ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_empty_matchingmatchingunit_witnesstransportoutput ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput. (((gr_match_target_empty_matchingmatching) = ((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputreal ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_empty_matchingmatchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputreal) = S ge_signed_half_empty_matchingmatchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_empty_matchingmatchingunit_witnesstransport) * (ge_second_rp_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_rn_empty_matchingmatchingunit_witnesstransport) * (ge_second_rn_empty_matchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnesstransport) * (ge_second_in_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_in_empty_matchingmatchingunit_witnesstransport) * (ge_second_ip_empty_matchingmatchingunit_witnesstransport))))))) + ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputreal = (((((((ge_first_rp_empty_matchingmatchingunit_witnesstransport) * (ge_second_rn_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_rn_empty_matchingmatchingunit_witnesstransport) * (ge_second_rp_empty_matchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnesstransport) * (ge_second_ip_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_in_empty_matchingmatchingunit_witnesstransport) * (ge_second_in_empty_matchingmatchingunit_witnesstransport))))))) + ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputimaginary ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_empty_matchingmatchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputimaginary) = S ge_signed_half_empty_matchingmatchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_empty_matchingmatchingunit_witnesstransport) * (ge_second_ip_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_rn_empty_matchingmatchingunit_witnesstransport) * (ge_second_in_empty_matchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnesstransport) * (ge_second_rp_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_in_empty_matchingmatchingunit_witnesstransport) * (ge_second_rn_empty_matchingmatchingunit_witnesstransport))))))) + ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_empty_matchingmatchingunit_witnesstransport) * (ge_second_in_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_rn_empty_matchingmatchingunit_witnesstransport) * (ge_second_ip_empty_matchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnesstransport) * (ge_second_rn_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_in_empty_matchingmatchingunit_witnesstransport) * (ge_second_rp_empty_matchingmatchingunit_witnesstransport))))))) + ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputimaginary))))))))))))))

Complete tactic proof in conservative notation

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

42 script commands · 15 reading checkpoints · 0 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 (1)
gaussian search no index below zero
01Fix variables and assumptionsL1–4

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
02Separate the logical casesL5–6

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

  1. L5
    split
  2. L6
    split
03Fix variables and assumptionsL7–8

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

  1. L7
    intro i
  2. L8
    intro hi
04Separate the logical casesL9–9

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

  1. L9
    exfalso
05Use earlier factsL10–12

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

  1. L10
    specialize gaussian_search_no_index_below_zero (i)
  2. L11
    apply gaussian_search_no_index_below_zero
  3. L12
    exact hi
06Separate the logical casesL13–13

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

  1. L13
    split
07Fix variables and assumptionsL14–20

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

  1. L14
    intro i
  2. L15
    intro j
  3. L16
    intro a
  4. L17
    intro hi
  5. L18
    intro hj
  6. L19
    intro hfirst
  7. L20
    intro hsecond
08Separate the logical casesL21–21

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

  1. L21
    exfalso
09Use earlier factsL22–24

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

  1. L22
    specialize gaussian_search_no_index_below_zero (i)
  2. L23
    apply gaussian_search_no_index_below_zero
  3. L24
    exact hi
10Fix variables and assumptionsL25–26

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

  1. L25
    intro a
  2. L26
    intro ha
11Separate the logical casesL27–27

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

  1. L27
    exfalso
12Use earlier factsL28–30

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

  1. L28
    specialize gaussian_search_no_index_below_zero (a)
  2. L29
    apply gaussian_search_no_index_below_zero
  3. L30
    exact ha
13Fix variables and assumptionsL31–38

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

  1. L31
    intro i
  2. L32
    intro j
  3. L33
    intro a
  4. L34
    intro t
  5. L35
    intro hi
  6. L36
    intro hmap
  7. L37
    intro hsource
  8. L38
    intro htarget
14Separate the logical casesL39–39

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

  1. L39
    exfalso
15Use earlier factsL40–42

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

  1. L40
    specialize gaussian_search_no_index_below_zero (i)
  2. L41
    apply gaussian_search_no_index_below_zero
  3. L42
    exact hi

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005split
  6. 0006split
  7. 0007intro i
  8. 0008intro hi
  9. 0009exfalso
  10. 0010specialize gaussian_search_no_index_below_zero (i)
  11. 0011apply gaussian_search_no_index_below_zero
  12. 0012exact hi
  13. 0013split
  14. 0014intro i
  15. 0015intro j
  16. 0016intro a
  17. 0017intro hi
  18. 0018intro hj
  19. 0019intro hfirst
  20. 0020intro hsecond
  21. 0021exfalso
  22. 0022specialize gaussian_search_no_index_below_zero (i)
  23. 0023apply gaussian_search_no_index_below_zero
  24. 0024exact hi
  25. 0025intro a
  26. 0026intro ha
  27. 0027exfalso
  28. 0028specialize gaussian_search_no_index_below_zero (a)
  29. 0029apply gaussian_search_no_index_below_zero
  30. 0030exact ha
  31. 0031intro i
  32. 0032intro j
  33. 0033intro a
  34. 0034intro t
  35. 0035intro hi
  36. 0036intro hmap
  37. 0037intro hsource
  38. 0038intro htarget
  39. 0039exfalso
  40. 0040specialize gaussian_search_no_index_below_zero (i)
  41. 0041apply gaussian_search_no_index_below_zero
  42. 0042exact hi