GF0088

gaussian_product_prefix_recode

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

Preserving actual factor entries preserves the same genuinely multiplied Gaussian product trace.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall b c d e l P. (exists gr_product_trace_recode_source gr_product_scale_recode_source. ((((exists ff_h_gprod_recode_sourcestart. ff_h_gprod_recode_sourcestart + S (6) = S ((S (0)) * gr_product_scale_recode_source)) /\ exists ff_q_gprod_recode_sourcestart. gr_product_trace_recode_source = ff_q_gprod_recode_sourcestart * S ((S (0)) * gr_product_scale_recode_source) + (6))) /\ ((((exists ff_h_gprod_recode_sourceend. ff_h_gprod_recode_sourceend + S (P) = S ((S (l)) * gr_product_scale_recode_source)) /\ exists ff_q_gprod_recode_sourceend. gr_product_trace_recode_source = ff_q_gprod_recode_sourceend * S ((S (l)) * gr_product_scale_recode_source) + (P))) /\ (forall gr_product_index_recode_sourcesteps. (exists ge_gap_recode_sourcestepsindex_bound. ge_gap_recode_sourcestepsindex_bound + S (gr_product_index_recode_sourcesteps) = (l)) -> exists gr_product_factor_recode_sourcesteps gr_product_before_recode_sourcesteps gr_product_after_recode_sourcesteps. ((((exists ff_h_gprod_recode_sourcestepsfactor. ff_h_gprod_recode_sourcestepsfactor + S (gr_product_factor_recode_sourcesteps) = S ((S (gr_product_index_recode_sourcesteps)) * c)) /\ exists ff_q_gprod_recode_sourcestepsfactor. b = ff_q_gprod_recode_sourcestepsfactor * S ((S (gr_product_index_recode_sourcesteps)) * c) + (gr_product_factor_recode_sourcesteps))) /\ ((((exists ff_h_gprod_recode_sourcestepsbefore. ff_h_gprod_recode_sourcestepsbefore + S (gr_product_before_recode_sourcesteps) = S ((S (gr_product_index_recode_sourcesteps)) * gr_product_scale_recode_source)) /\ exists ff_q_gprod_recode_sourcestepsbefore. gr_product_trace_recode_source = ff_q_gprod_recode_sourcestepsbefore * S ((S (gr_product_index_recode_sourcesteps)) * gr_product_scale_recode_source) + (gr_product_before_recode_sourcesteps))) /\ ((((exists ff_h_gprod_recode_sourcestepsafter. ff_h_gprod_recode_sourcestepsafter + S (gr_product_after_recode_sourcesteps) = S ((S (S (gr_product_index_recode_sourcesteps))) * gr_product_scale_recode_source)) /\ exists ff_q_gprod_recode_sourcestepsafter. gr_product_trace_recode_source = ff_q_gprod_recode_sourcestepsafter * S ((S (S (gr_product_index_recode_sourcesteps))) * gr_product_scale_recode_source) + (gr_product_after_recode_sourcesteps))) /\ (exists ge_first_rp_recode_sourcestepsmultiply ge_first_rn_recode_sourcestepsmultiply ge_first_ip_recode_sourcestepsmultiply ge_first_in_recode_sourcestepsmultiply ge_second_rp_recode_sourcestepsmultiply ge_second_rn_recode_sourcestepsmultiply ge_second_ip_recode_sourcestepsmultiply ge_second_in_recode_sourcestepsmultiply. ((exists ge_representation_real_code_recode_sourcestepsmultiplyfirst ge_representation_imaginary_code_recode_sourcestepsmultiplyfirst. (((gr_product_before_recode_sourcesteps) = ((ge_representation_real_code_recode_sourcestepsmultiplyfirst) + (ge_representation_imaginary_code_recode_sourcestepsmultiplyfirst)) * S ((ge_representation_real_code_recode_sourcestepsmultiplyfirst) + (ge_representation_imaginary_code_recode_sourcestepsmultiplyfirst)) + ((ge_representation_imaginary_code_recode_sourcestepsmultiplyfirst) + (ge_representation_imaginary_code_recode_sourcestepsmultiplyfirst))) /\ ((exists ge_balance_positive_recode_sourcestepsmultiplyfirstreal ge_balance_negative_recode_sourcestepsmultiplyfirstreal. (((((ge_representation_real_code_recode_sourcestepsmultiplyfirst) = 2 * (ge_balance_positive_recode_sourcestepsmultiplyfirstreal) /\ (ge_balance_negative_recode_sourcestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_recode_sourcestepsmultiplyfirstrealdecode. (((ge_representation_real_code_recode_sourcestepsmultiplyfirst) = 2 * ge_signed_half_recode_sourcestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_recode_sourcestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_recode_sourcestepsmultiplyfirstreal) = S ge_signed_half_recode_sourcestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_recode_sourcestepsmultiply) + ge_balance_negative_recode_sourcestepsmultiplyfirstreal = (ge_first_rn_recode_sourcestepsmultiply) + ge_balance_positive_recode_sourcestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_recode_sourcestepsmultiplyfirstimaginary ge_balance_negative_recode_sourcestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_recode_sourcestepsmultiplyfirst) = 2 * (ge_balance_positive_recode_sourcestepsmultiplyfirstimaginary) /\ (ge_balance_negative_recode_sourcestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_recode_sourcestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_recode_sourcestepsmultiplyfirst) = 2 * ge_signed_half_recode_sourcestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_recode_sourcestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_recode_sourcestepsmultiplyfirstimaginary) = S ge_signed_half_recode_sourcestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_recode_sourcestepsmultiply) + ge_balance_negative_recode_sourcestepsmultiplyfirstimaginary = (ge_first_in_recode_sourcestepsmultiply) + ge_balance_positive_recode_sourcestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_recode_sourcestepsmultiplysecond ge_representation_imaginary_code_recode_sourcestepsmultiplysecond. (((gr_product_factor_recode_sourcesteps) = ((ge_representation_real_code_recode_sourcestepsmultiplysecond) + (ge_representation_imaginary_code_recode_sourcestepsmultiplysecond)) * S ((ge_representation_real_code_recode_sourcestepsmultiplysecond) + (ge_representation_imaginary_code_recode_sourcestepsmultiplysecond)) + ((ge_representation_imaginary_code_recode_sourcestepsmultiplysecond) + (ge_representation_imaginary_code_recode_sourcestepsmultiplysecond))) /\ ((exists ge_balance_positive_recode_sourcestepsmultiplysecondreal ge_balance_negative_recode_sourcestepsmultiplysecondreal. (((((ge_representation_real_code_recode_sourcestepsmultiplysecond) = 2 * (ge_balance_positive_recode_sourcestepsmultiplysecondreal) /\ (ge_balance_negative_recode_sourcestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_recode_sourcestepsmultiplysecondrealdecode. (((ge_representation_real_code_recode_sourcestepsmultiplysecond) = 2 * ge_signed_half_recode_sourcestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_recode_sourcestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_recode_sourcestepsmultiplysecondreal) = S ge_signed_half_recode_sourcestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_recode_sourcestepsmultiply) + ge_balance_negative_recode_sourcestepsmultiplysecondreal = (ge_second_rn_recode_sourcestepsmultiply) + ge_balance_positive_recode_sourcestepsmultiplysecondreal))) /\ (exists ge_balance_positive_recode_sourcestepsmultiplysecondimaginary ge_balance_negative_recode_sourcestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_recode_sourcestepsmultiplysecond) = 2 * (ge_balance_positive_recode_sourcestepsmultiplysecondimaginary) /\ (ge_balance_negative_recode_sourcestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_recode_sourcestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_recode_sourcestepsmultiplysecond) = 2 * ge_signed_half_recode_sourcestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_recode_sourcestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_recode_sourcestepsmultiplysecondimaginary) = S ge_signed_half_recode_sourcestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_recode_sourcestepsmultiply) + ge_balance_negative_recode_sourcestepsmultiplysecondimaginary = (ge_second_in_recode_sourcestepsmultiply) + ge_balance_positive_recode_sourcestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_recode_sourcestepsmultiplyoutput ge_representation_imaginary_code_recode_sourcestepsmultiplyoutput. (((gr_product_after_recode_sourcesteps) = ((ge_representation_real_code_recode_sourcestepsmultiplyoutput) + (ge_representation_imaginary_code_recode_sourcestepsmultiplyoutput)) * S ((ge_representation_real_code_recode_sourcestepsmultiplyoutput) + (ge_representation_imaginary_code_recode_sourcestepsmultiplyoutput)) + ((ge_representation_imaginary_code_recode_sourcestepsmultiplyoutput) + (ge_representation_imaginary_code_recode_sourcestepsmultiplyoutput))) /\ ((exists ge_balance_positive_recode_sourcestepsmultiplyoutputreal ge_balance_negative_recode_sourcestepsmultiplyoutputreal. (((((ge_representation_real_code_recode_sourcestepsmultiplyoutput) = 2 * (ge_balance_positive_recode_sourcestepsmultiplyoutputreal) /\ (ge_balance_negative_recode_sourcestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_recode_sourcestepsmultiplyoutputrealdecode. (((ge_representation_real_code_recode_sourcestepsmultiplyoutput) = 2 * ge_signed_half_recode_sourcestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_recode_sourcestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_recode_sourcestepsmultiplyoutputreal) = S ge_signed_half_recode_sourcestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_recode_sourcestepsmultiply) * (ge_second_rp_recode_sourcestepsmultiply))) + (((ge_first_rn_recode_sourcestepsmultiply) * (ge_second_rn_recode_sourcestepsmultiply))))) + (((((ge_first_ip_recode_sourcestepsmultiply) * (ge_second_in_recode_sourcestepsmultiply))) + (((ge_first_in_recode_sourcestepsmultiply) * (ge_second_ip_recode_sourcestepsmultiply))))))) + ge_balance_negative_recode_sourcestepsmultiplyoutputreal = (((((((ge_first_rp_recode_sourcestepsmultiply) * (ge_second_rn_recode_sourcestepsmultiply))) + (((ge_first_rn_recode_sourcestepsmultiply) * (ge_second_rp_recode_sourcestepsmultiply))))) + (((((ge_first_ip_recode_sourcestepsmultiply) * (ge_second_ip_recode_sourcestepsmultiply))) + (((ge_first_in_recode_sourcestepsmultiply) * (ge_second_in_recode_sourcestepsmultiply))))))) + ge_balance_positive_recode_sourcestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_recode_sourcestepsmultiplyoutputimaginary ge_balance_negative_recode_sourcestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_recode_sourcestepsmultiplyoutput) = 2 * (ge_balance_positive_recode_sourcestepsmultiplyoutputimaginary) /\ (ge_balance_negative_recode_sourcestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_recode_sourcestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_recode_sourcestepsmultiplyoutput) = 2 * ge_signed_half_recode_sourcestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_recode_sourcestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_recode_sourcestepsmultiplyoutputimaginary) = S ge_signed_half_recode_sourcestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_recode_sourcestepsmultiply) * (ge_second_ip_recode_sourcestepsmultiply))) + (((ge_first_rn_recode_sourcestepsmultiply) * (ge_second_in_recode_sourcestepsmultiply))))) + (((((ge_first_ip_recode_sourcestepsmultiply) * (ge_second_rp_recode_sourcestepsmultiply))) + (((ge_first_in_recode_sourcestepsmultiply) * (ge_second_rn_recode_sourcestepsmultiply))))))) + ge_balance_negative_recode_sourcestepsmultiplyoutputimaginary = (((((((ge_first_rp_recode_sourcestepsmultiply) * (ge_second_in_recode_sourcestepsmultiply))) + (((ge_first_rn_recode_sourcestepsmultiply) * (ge_second_ip_recode_sourcestepsmultiply))))) + (((((ge_first_ip_recode_sourcestepsmultiply) * (ge_second_rn_recode_sourcestepsmultiply))) + (((ge_first_in_recode_sourcestepsmultiply) * (ge_second_rp_recode_sourcestepsmultiply))))))) + ge_balance_positive_recode_sourcestepsmultiplyoutputimaginary)))))))))))))))) -> (forall pfp_i_recode_entries pfp_a_recode_entries. (exists pfp_gap_recode_entriesbound. pfp_gap_recode_entriesbound + S (pfp_i_recode_entries) = (l)) -> (((exists ff_h_pfp_recode_entriesold. ff_h_pfp_recode_entriesold + S (pfp_a_recode_entries) = S ((S (pfp_i_recode_entries)) * c)) /\ exists ff_q_pfp_recode_entriesold. b = ff_q_pfp_recode_entriesold * S ((S (pfp_i_recode_entries)) * c) + (pfp_a_recode_entries))) -> (((exists ff_h_pfp_recode_entriesnew. ff_h_pfp_recode_entriesnew + S (pfp_a_recode_entries) = S ((S (pfp_i_recode_entries)) * e)) /\ exists ff_q_pfp_recode_entriesnew. d = ff_q_pfp_recode_entriesnew * S ((S (pfp_i_recode_entries)) * e) + (pfp_a_recode_entries)))) -> (exists gr_product_trace_recode_target gr_product_scale_recode_target. ((((exists ff_h_gprod_recode_targetstart. ff_h_gprod_recode_targetstart + S (6) = S ((S (0)) * gr_product_scale_recode_target)) /\ exists ff_q_gprod_recode_targetstart. gr_product_trace_recode_target = ff_q_gprod_recode_targetstart * S ((S (0)) * gr_product_scale_recode_target) + (6))) /\ ((((exists ff_h_gprod_recode_targetend. ff_h_gprod_recode_targetend + S (P) = S ((S (l)) * gr_product_scale_recode_target)) /\ exists ff_q_gprod_recode_targetend. gr_product_trace_recode_target = ff_q_gprod_recode_targetend * S ((S (l)) * gr_product_scale_recode_target) + (P))) /\ (forall gr_product_index_recode_targetsteps. (exists ge_gap_recode_targetstepsindex_bound. ge_gap_recode_targetstepsindex_bound + S (gr_product_index_recode_targetsteps) = (l)) -> exists gr_product_factor_recode_targetsteps gr_product_before_recode_targetsteps gr_product_after_recode_targetsteps. ((((exists ff_h_gprod_recode_targetstepsfactor. ff_h_gprod_recode_targetstepsfactor + S (gr_product_factor_recode_targetsteps) = S ((S (gr_product_index_recode_targetsteps)) * e)) /\ exists ff_q_gprod_recode_targetstepsfactor. d = ff_q_gprod_recode_targetstepsfactor * S ((S (gr_product_index_recode_targetsteps)) * e) + (gr_product_factor_recode_targetsteps))) /\ ((((exists ff_h_gprod_recode_targetstepsbefore. ff_h_gprod_recode_targetstepsbefore + S (gr_product_before_recode_targetsteps) = S ((S (gr_product_index_recode_targetsteps)) * gr_product_scale_recode_target)) /\ exists ff_q_gprod_recode_targetstepsbefore. gr_product_trace_recode_target = ff_q_gprod_recode_targetstepsbefore * S ((S (gr_product_index_recode_targetsteps)) * gr_product_scale_recode_target) + (gr_product_before_recode_targetsteps))) /\ ((((exists ff_h_gprod_recode_targetstepsafter. ff_h_gprod_recode_targetstepsafter + S (gr_product_after_recode_targetsteps) = S ((S (S (gr_product_index_recode_targetsteps))) * gr_product_scale_recode_target)) /\ exists ff_q_gprod_recode_targetstepsafter. gr_product_trace_recode_target = ff_q_gprod_recode_targetstepsafter * S ((S (S (gr_product_index_recode_targetsteps))) * gr_product_scale_recode_target) + (gr_product_after_recode_targetsteps))) /\ (exists ge_first_rp_recode_targetstepsmultiply ge_first_rn_recode_targetstepsmultiply ge_first_ip_recode_targetstepsmultiply ge_first_in_recode_targetstepsmultiply ge_second_rp_recode_targetstepsmultiply ge_second_rn_recode_targetstepsmultiply ge_second_ip_recode_targetstepsmultiply ge_second_in_recode_targetstepsmultiply. ((exists ge_representation_real_code_recode_targetstepsmultiplyfirst ge_representation_imaginary_code_recode_targetstepsmultiplyfirst. (((gr_product_before_recode_targetsteps) = ((ge_representation_real_code_recode_targetstepsmultiplyfirst) + (ge_representation_imaginary_code_recode_targetstepsmultiplyfirst)) * S ((ge_representation_real_code_recode_targetstepsmultiplyfirst) + (ge_representation_imaginary_code_recode_targetstepsmultiplyfirst)) + ((ge_representation_imaginary_code_recode_targetstepsmultiplyfirst) + (ge_representation_imaginary_code_recode_targetstepsmultiplyfirst))) /\ ((exists ge_balance_positive_recode_targetstepsmultiplyfirstreal ge_balance_negative_recode_targetstepsmultiplyfirstreal. (((((ge_representation_real_code_recode_targetstepsmultiplyfirst) = 2 * (ge_balance_positive_recode_targetstepsmultiplyfirstreal) /\ (ge_balance_negative_recode_targetstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_recode_targetstepsmultiplyfirstrealdecode. (((ge_representation_real_code_recode_targetstepsmultiplyfirst) = 2 * ge_signed_half_recode_targetstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_recode_targetstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_recode_targetstepsmultiplyfirstreal) = S ge_signed_half_recode_targetstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_recode_targetstepsmultiply) + ge_balance_negative_recode_targetstepsmultiplyfirstreal = (ge_first_rn_recode_targetstepsmultiply) + ge_balance_positive_recode_targetstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_recode_targetstepsmultiplyfirstimaginary ge_balance_negative_recode_targetstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_recode_targetstepsmultiplyfirst) = 2 * (ge_balance_positive_recode_targetstepsmultiplyfirstimaginary) /\ (ge_balance_negative_recode_targetstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_recode_targetstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_recode_targetstepsmultiplyfirst) = 2 * ge_signed_half_recode_targetstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_recode_targetstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_recode_targetstepsmultiplyfirstimaginary) = S ge_signed_half_recode_targetstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_recode_targetstepsmultiply) + ge_balance_negative_recode_targetstepsmultiplyfirstimaginary = (ge_first_in_recode_targetstepsmultiply) + ge_balance_positive_recode_targetstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_recode_targetstepsmultiplysecond ge_representation_imaginary_code_recode_targetstepsmultiplysecond. (((gr_product_factor_recode_targetsteps) = ((ge_representation_real_code_recode_targetstepsmultiplysecond) + (ge_representation_imaginary_code_recode_targetstepsmultiplysecond)) * S ((ge_representation_real_code_recode_targetstepsmultiplysecond) + (ge_representation_imaginary_code_recode_targetstepsmultiplysecond)) + ((ge_representation_imaginary_code_recode_targetstepsmultiplysecond) + (ge_representation_imaginary_code_recode_targetstepsmultiplysecond))) /\ ((exists ge_balance_positive_recode_targetstepsmultiplysecondreal ge_balance_negative_recode_targetstepsmultiplysecondreal. (((((ge_representation_real_code_recode_targetstepsmultiplysecond) = 2 * (ge_balance_positive_recode_targetstepsmultiplysecondreal) /\ (ge_balance_negative_recode_targetstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_recode_targetstepsmultiplysecondrealdecode. (((ge_representation_real_code_recode_targetstepsmultiplysecond) = 2 * ge_signed_half_recode_targetstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_recode_targetstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_recode_targetstepsmultiplysecondreal) = S ge_signed_half_recode_targetstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_recode_targetstepsmultiply) + ge_balance_negative_recode_targetstepsmultiplysecondreal = (ge_second_rn_recode_targetstepsmultiply) + ge_balance_positive_recode_targetstepsmultiplysecondreal))) /\ (exists ge_balance_positive_recode_targetstepsmultiplysecondimaginary ge_balance_negative_recode_targetstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_recode_targetstepsmultiplysecond) = 2 * (ge_balance_positive_recode_targetstepsmultiplysecondimaginary) /\ (ge_balance_negative_recode_targetstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_recode_targetstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_recode_targetstepsmultiplysecond) = 2 * ge_signed_half_recode_targetstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_recode_targetstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_recode_targetstepsmultiplysecondimaginary) = S ge_signed_half_recode_targetstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_recode_targetstepsmultiply) + ge_balance_negative_recode_targetstepsmultiplysecondimaginary = (ge_second_in_recode_targetstepsmultiply) + ge_balance_positive_recode_targetstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_recode_targetstepsmultiplyoutput ge_representation_imaginary_code_recode_targetstepsmultiplyoutput. (((gr_product_after_recode_targetsteps) = ((ge_representation_real_code_recode_targetstepsmultiplyoutput) + (ge_representation_imaginary_code_recode_targetstepsmultiplyoutput)) * S ((ge_representation_real_code_recode_targetstepsmultiplyoutput) + (ge_representation_imaginary_code_recode_targetstepsmultiplyoutput)) + ((ge_representation_imaginary_code_recode_targetstepsmultiplyoutput) + (ge_representation_imaginary_code_recode_targetstepsmultiplyoutput))) /\ ((exists ge_balance_positive_recode_targetstepsmultiplyoutputreal ge_balance_negative_recode_targetstepsmultiplyoutputreal. (((((ge_representation_real_code_recode_targetstepsmultiplyoutput) = 2 * (ge_balance_positive_recode_targetstepsmultiplyoutputreal) /\ (ge_balance_negative_recode_targetstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_recode_targetstepsmultiplyoutputrealdecode. (((ge_representation_real_code_recode_targetstepsmultiplyoutput) = 2 * ge_signed_half_recode_targetstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_recode_targetstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_recode_targetstepsmultiplyoutputreal) = S ge_signed_half_recode_targetstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_recode_targetstepsmultiply) * (ge_second_rp_recode_targetstepsmultiply))) + (((ge_first_rn_recode_targetstepsmultiply) * (ge_second_rn_recode_targetstepsmultiply))))) + (((((ge_first_ip_recode_targetstepsmultiply) * (ge_second_in_recode_targetstepsmultiply))) + (((ge_first_in_recode_targetstepsmultiply) * (ge_second_ip_recode_targetstepsmultiply))))))) + ge_balance_negative_recode_targetstepsmultiplyoutputreal = (((((((ge_first_rp_recode_targetstepsmultiply) * (ge_second_rn_recode_targetstepsmultiply))) + (((ge_first_rn_recode_targetstepsmultiply) * (ge_second_rp_recode_targetstepsmultiply))))) + (((((ge_first_ip_recode_targetstepsmultiply) * (ge_second_ip_recode_targetstepsmultiply))) + (((ge_first_in_recode_targetstepsmultiply) * (ge_second_in_recode_targetstepsmultiply))))))) + ge_balance_positive_recode_targetstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_recode_targetstepsmultiplyoutputimaginary ge_balance_negative_recode_targetstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_recode_targetstepsmultiplyoutput) = 2 * (ge_balance_positive_recode_targetstepsmultiplyoutputimaginary) /\ (ge_balance_negative_recode_targetstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_recode_targetstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_recode_targetstepsmultiplyoutput) = 2 * ge_signed_half_recode_targetstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_recode_targetstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_recode_targetstepsmultiplyoutputimaginary) = S ge_signed_half_recode_targetstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_recode_targetstepsmultiply) * (ge_second_ip_recode_targetstepsmultiply))) + (((ge_first_rn_recode_targetstepsmultiply) * (ge_second_in_recode_targetstepsmultiply))))) + (((((ge_first_ip_recode_targetstepsmultiply) * (ge_second_rp_recode_targetstepsmultiply))) + (((ge_first_in_recode_targetstepsmultiply) * (ge_second_rn_recode_targetstepsmultiply))))))) + ge_balance_negative_recode_targetstepsmultiplyoutputimaginary = (((((((ge_first_rp_recode_targetstepsmultiply) * (ge_second_in_recode_targetstepsmultiply))) + (((ge_first_rn_recode_targetstepsmultiply) * (ge_second_ip_recode_targetstepsmultiply))))) + (((((ge_first_ip_recode_targetstepsmultiply) * (ge_second_rn_recode_targetstepsmultiply))) + (((ge_first_in_recode_targetstepsmultiply) * (ge_second_rp_recode_targetstepsmultiply))))))) + ge_balance_positive_recode_targetstepsmultiplyoutputimaginary))))))))))))))))

Constructive proof overview

Generated structural guide

Preserving actual factor entries preserves the same genuinely multiplied Gaussian product trace.

The unchanged tactic script uses 0 declared prerequisites and contains 44 exact native proof lines.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

GF0093 gaussian_factorization_append_irreducible GF00A0 gaussian_product_replace_balance

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

44 script commands · 17 reading checkpoints · 1 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–8

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
  5. L5
    intro l
  6. L6
    intro P
  7. L7
    intro hp
  8. L8
    intro hpreserve
02Separate the logical casesL9–12

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

  1. L9
    cases hp
  2. L10
    cases hp_witness
  3. L11
    cases hp_witness_witness
  4. L12
    cases hp_witness_witness_right
03Construct an explicit witnessL13–14

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

  1. L13
    exists (x)
  2. L14
    exists (x1)
04Separate the logical casesL15–15

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

  1. L15
    split
05Use earlier factsL16–16

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

  1. L16
    exact hp_witness_witness_left
06Separate the logical casesL17–17

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

  1. L17
    split
07Use earlier factsL18–18

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

  1. L18
    exact hp_witness_witness_right_left
08Fix variables and assumptionsL19–20

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

  1. L19
    intro i
  2. L20
    intro hi
09Establish hsL21–24

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

  1. L21
    have hs : GProductStep(b,c,x,x1,i)Definitions: GProductStep
  2. L22
    specialize hp_witness_witness_right_right (i)
  3. L23
    apply hp_witness_witness_right_right
  4. L24
    exact hi
10Separate the logical casesL25–30

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

  1. L25
    cases hs
  2. L26
    cases hs_witness
  3. L27
    cases hs_witness_witness
  4. L28
    cases hs_witness_witness_witness
  5. L29
    cases hs_witness_witness_witness_right
  6. L30
    cases hs_witness_witness_witness_right_right
11Construct an explicit witnessL31–33

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

  1. L31
    exists (x2)
  2. L32
    exists (x3)
  3. L33
    exists (x4)
12Separate the logical casesL34–34

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

  1. L34
    split
13Use earlier factsL35–39

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

  1. L35
    specialize hpreserve (i)
  2. L36
    specialize hpreserve (x2)
  3. L37
    apply hpreserve
  4. L38
    exact hi
  5. L39
    exact hs_witness_witness_witness_left
14Separate the logical casesL40–40

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

  1. L40
    split
15Use earlier factsL41–41

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

  1. L41
    exact hs_witness_witness_witness_right_left
16Separate the logical casesL42–42

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

  1. L42
    split
17Use earlier factsL43–44

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

  1. L43
    exact hs_witness_witness_witness_right_right_left
  2. L44
    exact hs_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 44 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro l
  6. 0006intro P
  7. 0007intro hp
  8. 0008intro hpreserve
  9. 0009cases hp
  10. 0010cases hp_witness
  11. 0011cases hp_witness_witness
  12. 0012cases hp_witness_witness_right
  13. 0013exists (x)
  14. 0014exists (x1)
  15. 0015split
  16. 0016exact hp_witness_witness_left
  17. 0017split
  18. 0018exact hp_witness_witness_right_left
  19. 0019intro i
  20. 0020intro hi
  21. 0021have hs : exists a R T. ((((exists ff_h_gprod_recode_old_factor. ff_h_gprod_recode_old_factor + S (a) = S ((S (i)) * c)) /\ exists ff_q_gprod_recode_old_factor. b = ff_q_gprod_recode_old_factor * S ((S (i)) * c) + (a))) /\ ((((exists ff_h_gprod_recode_old_before. ff_h_gprod_recode_old_before + S (R) = S ((S (i)) * x1)) /\ exists ff_q_gprod_recode_old_before. x = ff_q_gprod_recode_old_before * S ((S (i)) * x1) + (R))) /\ ((((exists ff_h_gprod_recode_old_after. ff_h_gprod_recode_old_after + S (T) = S ((S (S i)) * x1)) /\ exists ff_q_gprod_recode_old_after. x = ff_q_gprod_recode_old_after * S ((S (S i)) * x1) + (T))) /\ (exists ge_first_rp_recode_old_multiply ge_first_rn_recode_old_multiply ge_first_ip_recode_old_multiply ge_first_in_recode_old_multiply ge_second_rp_recode_old_multiply ge_second_rn_recode_old_multiply ge_second_ip_recode_old_multiply ge_second_in_recode_old_multiply. ((exists ge_representation_real_code_recode_old_multiplyfirst ge_representation_imaginary_code_recode_old_multiplyfirst. (((R) = ((ge_representation_real_code_recode_old_multiplyfirst) + (ge_representation_imaginary_code_recode_old_multiplyfirst)) * S ((ge_representation_real_code_recode_old_multiplyfirst) + (ge_representation_imaginary_code_recode_old_multiplyfirst)) + ((ge_representation_imaginary_code_recode_old_multiplyfirst) + (ge_representation_imaginary_code_recode_old_multiplyfirst))) /\ ((exists ge_balance_positive_recode_old_multiplyfirstreal ge_balance_negative_recode_old_multiplyfirstreal. (((((ge_representation_real_code_recode_old_multiplyfirst) = 2 * (ge_balance_positive_recode_old_multiplyfirstreal) /\ (ge_balance_negative_recode_old_multiplyfirstreal) = 0) \/ exists ge_signed_half_recode_old_multiplyfirstrealdecode. (((ge_representation_real_code_recode_old_multiplyfirst) = 2 * ge_signed_half_recode_old_multiplyfirstrealdecode + 1 /\ (ge_balance_positive_recode_old_multiplyfirstreal) = 0) /\ (ge_balance_negative_recode_old_multiplyfirstreal) = S ge_signed_half_recode_old_multiplyfirstrealdecode))) /\ ((ge_first_rp_recode_old_multiply) + ge_balance_negative_recode_old_multiplyfirstreal = (ge_first_rn_recode_old_multiply) + ge_balance_positive_recode_old_multiplyfirstreal))) /\ (exists ge_balance_positive_recode_old_multiplyfirstimaginary ge_balance_negative_recode_old_multiplyfirstimaginary. (((((ge_representation_imaginary_code_recode_old_multiplyfirst) = 2 * (ge_balance_positive_recode_old_multiplyfirstimaginary) /\ (ge_balance_negative_recode_old_multiplyfirstimaginary) = 0) \/ exists ge_signed_half_recode_old_multiplyfirstimaginarydecode. (((ge_representation_imaginary_code_recode_old_multiplyfirst) = 2 * ge_signed_half_recode_old_multiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_recode_old_multiplyfirstimaginary) = 0) /\ (ge_balance_negative_recode_old_multiplyfirstimaginary) = S ge_signed_half_recode_old_multiplyfirstimaginarydecode))) /\ ((ge_first_ip_recode_old_multiply) + ge_balance_negative_recode_old_multiplyfirstimaginary = (ge_first_in_recode_old_multiply) + ge_balance_positive_recode_old_multiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_recode_old_multiplysecond ge_representation_imaginary_code_recode_old_multiplysecond. (((a) = ((ge_representation_real_code_recode_old_multiplysecond) + (ge_representation_imaginary_code_recode_old_multiplysecond)) * S ((ge_representation_real_code_recode_old_multiplysecond) + (ge_representation_imaginary_code_recode_old_multiplysecond)) + ((ge_representation_imaginary_code_recode_old_multiplysecond) + (ge_representation_imaginary_code_recode_old_multiplysecond))) /\ ((exists ge_balance_positive_recode_old_multiplysecondreal ge_balance_negative_recode_old_multiplysecondreal. (((((ge_representation_real_code_recode_old_multiplysecond) = 2 * (ge_balance_positive_recode_old_multiplysecondreal) /\ (ge_balance_negative_recode_old_multiplysecondreal) = 0) \/ exists ge_signed_half_recode_old_multiplysecondrealdecode. (((ge_representation_real_code_recode_old_multiplysecond) = 2 * ge_signed_half_recode_old_multiplysecondrealdecode + 1 /\ (ge_balance_positive_recode_old_multiplysecondreal) = 0) /\ (ge_balance_negative_recode_old_multiplysecondreal) = S ge_signed_half_recode_old_multiplysecondrealdecode))) /\ ((ge_second_rp_recode_old_multiply) + ge_balance_negative_recode_old_multiplysecondreal = (ge_second_rn_recode_old_multiply) + ge_balance_positive_recode_old_multiplysecondreal))) /\ (exists ge_balance_positive_recode_old_multiplysecondimaginary ge_balance_negative_recode_old_multiplysecondimaginary. (((((ge_representation_imaginary_code_recode_old_multiplysecond) = 2 * (ge_balance_positive_recode_old_multiplysecondimaginary) /\ (ge_balance_negative_recode_old_multiplysecondimaginary) = 0) \/ exists ge_signed_half_recode_old_multiplysecondimaginarydecode. (((ge_representation_imaginary_code_recode_old_multiplysecond) = 2 * ge_signed_half_recode_old_multiplysecondimaginarydecode + 1 /\ (ge_balance_positive_recode_old_multiplysecondimaginary) = 0) /\ (ge_balance_negative_recode_old_multiplysecondimaginary) = S ge_signed_half_recode_old_multiplysecondimaginarydecode))) /\ ((ge_second_ip_recode_old_multiply) + ge_balance_negative_recode_old_multiplysecondimaginary = (ge_second_in_recode_old_multiply) + ge_balance_positive_recode_old_multiplysecondimaginary)))))) /\ (exists ge_representation_real_code_recode_old_multiplyoutput ge_representation_imaginary_code_recode_old_multiplyoutput. (((T) = ((ge_representation_real_code_recode_old_multiplyoutput) + (ge_representation_imaginary_code_recode_old_multiplyoutput)) * S ((ge_representation_real_code_recode_old_multiplyoutput) + (ge_representation_imaginary_code_recode_old_multiplyoutput)) + ((ge_representation_imaginary_code_recode_old_multiplyoutput) + (ge_representation_imaginary_code_recode_old_multiplyoutput))) /\ ((exists ge_balance_positive_recode_old_multiplyoutputreal ge_balance_negative_recode_old_multiplyoutputreal. (((((ge_representation_real_code_recode_old_multiplyoutput) = 2 * (ge_balance_positive_recode_old_multiplyoutputreal) /\ (ge_balance_negative_recode_old_multiplyoutputreal) = 0) \/ exists ge_signed_half_recode_old_multiplyoutputrealdecode. (((ge_representation_real_code_recode_old_multiplyoutput) = 2 * ge_signed_half_recode_old_multiplyoutputrealdecode + 1 /\ (ge_balance_positive_recode_old_multiplyoutputreal) = 0) /\ (ge_balance_negative_recode_old_multiplyoutputreal) = S ge_signed_half_recode_old_multiplyoutputrealdecode))) /\ ((((((((ge_first_rp_recode_old_multiply) * (ge_second_rp_recode_old_multiply))) + (((ge_first_rn_recode_old_multiply) * (ge_second_rn_recode_old_multiply))))) + (((((ge_first_ip_recode_old_multiply) * (ge_second_in_recode_old_multiply))) + (((ge_first_in_recode_old_multiply) * (ge_second_ip_recode_old_multiply))))))) + ge_balance_negative_recode_old_multiplyoutputreal = (((((((ge_first_rp_recode_old_multiply) * (ge_second_rn_recode_old_multiply))) + (((ge_first_rn_recode_old_multiply) * (ge_second_rp_recode_old_multiply))))) + (((((ge_first_ip_recode_old_multiply) * (ge_second_ip_recode_old_multiply))) + (((ge_first_in_recode_old_multiply) * (ge_second_in_recode_old_multiply))))))) + ge_balance_positive_recode_old_multiplyoutputreal))) /\ (exists ge_balance_positive_recode_old_multiplyoutputimaginary ge_balance_negative_recode_old_multiplyoutputimaginary. (((((ge_representation_imaginary_code_recode_old_multiplyoutput) = 2 * (ge_balance_positive_recode_old_multiplyoutputimaginary) /\ (ge_balance_negative_recode_old_multiplyoutputimaginary) = 0) \/ exists ge_signed_half_recode_old_multiplyoutputimaginarydecode. (((ge_representation_imaginary_code_recode_old_multiplyoutput) = 2 * ge_signed_half_recode_old_multiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_recode_old_multiplyoutputimaginary) = 0) /\ (ge_balance_negative_recode_old_multiplyoutputimaginary) = S ge_signed_half_recode_old_multiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_recode_old_multiply) * (ge_second_ip_recode_old_multiply))) + (((ge_first_rn_recode_old_multiply) * (ge_second_in_recode_old_multiply))))) + (((((ge_first_ip_recode_old_multiply) * (ge_second_rp_recode_old_multiply))) + (((ge_first_in_recode_old_multiply) * (ge_second_rn_recode_old_multiply))))))) + ge_balance_negative_recode_old_multiplyoutputimaginary = (((((((ge_first_rp_recode_old_multiply) * (ge_second_in_recode_old_multiply))) + (((ge_first_rn_recode_old_multiply) * (ge_second_ip_recode_old_multiply))))) + (((((ge_first_ip_recode_old_multiply) * (ge_second_rn_recode_old_multiply))) + (((ge_first_in_recode_old_multiply) * (ge_second_rp_recode_old_multiply))))))) + ge_balance_positive_recode_old_multiplyoutputimaginary))))))))))))
  22. 0022specialize hp_witness_witness_right_right (i)
  23. 0023apply hp_witness_witness_right_right
  24. 0024exact hi
  25. 0025cases hs
  26. 0026cases hs_witness
  27. 0027cases hs_witness_witness
  28. 0028cases hs_witness_witness_witness
  29. 0029cases hs_witness_witness_witness_right
  30. 0030cases hs_witness_witness_witness_right_right
  31. 0031exists (x2)
  32. 0032exists (x3)
  33. 0033exists (x4)
  34. 0034split
  35. 0035specialize hpreserve (i)
  36. 0036specialize hpreserve (x2)
  37. 0037apply hpreserve
  38. 0038exact hi
  39. 0039exact hs_witness_witness_witness_left
  40. 0040split
  41. 0041exact hs_witness_witness_witness_right_left
  42. 0042split
  43. 0043exact hs_witness_witness_witness_right_right_left
  44. 0044exact hs_witness_witness_witness_right_right_right