GF0088

gaussian_product_prefix_recode

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

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. ∀ l. ∀ P. GProduct(b,c,l,P) → (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(d,e,x,y)) → GProduct(d,e,l,P)

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

Definition DAG

GProductStep(b,c,h,e,i) · 1GProduct(b,c,l,P) · 2Lt(a,b) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

none
Original expanded first-order 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))))))))))))))))

Complete tactic proof in conservative notation

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

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.

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

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(b,c,x,x1,i)Original native command in the exact edition
  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 defined 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 : GProductStep(b,c,x,x1,i)
  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