GF0089

gaussian_product_successor_decompose

Every nonempty actual Gaussian product exposes its final factor, the actual shorter prefix product, and the genuine final multiplication.

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. ∀ l. ∀ Q. GProduct(b,c,S l,Q) → ∃ x. ∃ y. BetaAt(b,c,l,x) ∧ (GProduct(b,c,l,y) ∧ GMul(y,x,Q))

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

Definition DAG

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

Actual proof prerequisites

le_refl · checked external prerequisitebeta_at_unique · checked external prerequisitegaussian_multiply_output_transportlt_of_lt_of_le · checked external prerequisitele_succ_self · checked external prerequisite
Original expanded first-order statement 
forall b c l Q. (exists gr_product_trace_successor_product gr_product_scale_successor_product. ((((exists ff_h_gprod_successor_productstart. ff_h_gprod_successor_productstart + S (6) = S ((S (0)) * gr_product_scale_successor_product)) /\ exists ff_q_gprod_successor_productstart. gr_product_trace_successor_product = ff_q_gprod_successor_productstart * S ((S (0)) * gr_product_scale_successor_product) + (6))) /\ ((((exists ff_h_gprod_successor_productend. ff_h_gprod_successor_productend + S (Q) = S ((S (S l)) * gr_product_scale_successor_product)) /\ exists ff_q_gprod_successor_productend. gr_product_trace_successor_product = ff_q_gprod_successor_productend * S ((S (S l)) * gr_product_scale_successor_product) + (Q))) /\ (forall gr_product_index_successor_productsteps. (exists ge_gap_successor_productstepsindex_bound. ge_gap_successor_productstepsindex_bound + S (gr_product_index_successor_productsteps) = (S l)) -> exists gr_product_factor_successor_productsteps gr_product_before_successor_productsteps gr_product_after_successor_productsteps. ((((exists ff_h_gprod_successor_productstepsfactor. ff_h_gprod_successor_productstepsfactor + S (gr_product_factor_successor_productsteps) = S ((S (gr_product_index_successor_productsteps)) * c)) /\ exists ff_q_gprod_successor_productstepsfactor. b = ff_q_gprod_successor_productstepsfactor * S ((S (gr_product_index_successor_productsteps)) * c) + (gr_product_factor_successor_productsteps))) /\ ((((exists ff_h_gprod_successor_productstepsbefore. ff_h_gprod_successor_productstepsbefore + S (gr_product_before_successor_productsteps) = S ((S (gr_product_index_successor_productsteps)) * gr_product_scale_successor_product)) /\ exists ff_q_gprod_successor_productstepsbefore. gr_product_trace_successor_product = ff_q_gprod_successor_productstepsbefore * S ((S (gr_product_index_successor_productsteps)) * gr_product_scale_successor_product) + (gr_product_before_successor_productsteps))) /\ ((((exists ff_h_gprod_successor_productstepsafter. ff_h_gprod_successor_productstepsafter + S (gr_product_after_successor_productsteps) = S ((S (S (gr_product_index_successor_productsteps))) * gr_product_scale_successor_product)) /\ exists ff_q_gprod_successor_productstepsafter. gr_product_trace_successor_product = ff_q_gprod_successor_productstepsafter * S ((S (S (gr_product_index_successor_productsteps))) * gr_product_scale_successor_product) + (gr_product_after_successor_productsteps))) /\ (exists ge_first_rp_successor_productstepsmultiply ge_first_rn_successor_productstepsmultiply ge_first_ip_successor_productstepsmultiply ge_first_in_successor_productstepsmultiply ge_second_rp_successor_productstepsmultiply ge_second_rn_successor_productstepsmultiply ge_second_ip_successor_productstepsmultiply ge_second_in_successor_productstepsmultiply. ((exists ge_representation_real_code_successor_productstepsmultiplyfirst ge_representation_imaginary_code_successor_productstepsmultiplyfirst. (((gr_product_before_successor_productsteps) = ((ge_representation_real_code_successor_productstepsmultiplyfirst) + (ge_representation_imaginary_code_successor_productstepsmultiplyfirst)) * S ((ge_representation_real_code_successor_productstepsmultiplyfirst) + (ge_representation_imaginary_code_successor_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_successor_productstepsmultiplyfirst) + (ge_representation_imaginary_code_successor_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_successor_productstepsmultiplyfirstreal ge_balance_negative_successor_productstepsmultiplyfirstreal. (((((ge_representation_real_code_successor_productstepsmultiplyfirst) = 2 * (ge_balance_positive_successor_productstepsmultiplyfirstreal) /\ (ge_balance_negative_successor_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_successor_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_successor_productstepsmultiplyfirst) = 2 * ge_signed_half_successor_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_successor_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_successor_productstepsmultiplyfirstreal) = S ge_signed_half_successor_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_successor_productstepsmultiply) + ge_balance_negative_successor_productstepsmultiplyfirstreal = (ge_first_rn_successor_productstepsmultiply) + ge_balance_positive_successor_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_successor_productstepsmultiplyfirstimaginary ge_balance_negative_successor_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_successor_productstepsmultiplyfirst) = 2 * (ge_balance_positive_successor_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_successor_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_successor_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_successor_productstepsmultiplyfirst) = 2 * ge_signed_half_successor_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_successor_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_successor_productstepsmultiplyfirstimaginary) = S ge_signed_half_successor_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_successor_productstepsmultiply) + ge_balance_negative_successor_productstepsmultiplyfirstimaginary = (ge_first_in_successor_productstepsmultiply) + ge_balance_positive_successor_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_successor_productstepsmultiplysecond ge_representation_imaginary_code_successor_productstepsmultiplysecond. (((gr_product_factor_successor_productsteps) = ((ge_representation_real_code_successor_productstepsmultiplysecond) + (ge_representation_imaginary_code_successor_productstepsmultiplysecond)) * S ((ge_representation_real_code_successor_productstepsmultiplysecond) + (ge_representation_imaginary_code_successor_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_successor_productstepsmultiplysecond) + (ge_representation_imaginary_code_successor_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_successor_productstepsmultiplysecondreal ge_balance_negative_successor_productstepsmultiplysecondreal. (((((ge_representation_real_code_successor_productstepsmultiplysecond) = 2 * (ge_balance_positive_successor_productstepsmultiplysecondreal) /\ (ge_balance_negative_successor_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_successor_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_successor_productstepsmultiplysecond) = 2 * ge_signed_half_successor_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_successor_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_successor_productstepsmultiplysecondreal) = S ge_signed_half_successor_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_successor_productstepsmultiply) + ge_balance_negative_successor_productstepsmultiplysecondreal = (ge_second_rn_successor_productstepsmultiply) + ge_balance_positive_successor_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_successor_productstepsmultiplysecondimaginary ge_balance_negative_successor_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_successor_productstepsmultiplysecond) = 2 * (ge_balance_positive_successor_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_successor_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_successor_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_successor_productstepsmultiplysecond) = 2 * ge_signed_half_successor_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_successor_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_successor_productstepsmultiplysecondimaginary) = S ge_signed_half_successor_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_successor_productstepsmultiply) + ge_balance_negative_successor_productstepsmultiplysecondimaginary = (ge_second_in_successor_productstepsmultiply) + ge_balance_positive_successor_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_successor_productstepsmultiplyoutput ge_representation_imaginary_code_successor_productstepsmultiplyoutput. (((gr_product_after_successor_productsteps) = ((ge_representation_real_code_successor_productstepsmultiplyoutput) + (ge_representation_imaginary_code_successor_productstepsmultiplyoutput)) * S ((ge_representation_real_code_successor_productstepsmultiplyoutput) + (ge_representation_imaginary_code_successor_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_successor_productstepsmultiplyoutput) + (ge_representation_imaginary_code_successor_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_successor_productstepsmultiplyoutputreal ge_balance_negative_successor_productstepsmultiplyoutputreal. (((((ge_representation_real_code_successor_productstepsmultiplyoutput) = 2 * (ge_balance_positive_successor_productstepsmultiplyoutputreal) /\ (ge_balance_negative_successor_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_successor_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_successor_productstepsmultiplyoutput) = 2 * ge_signed_half_successor_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_successor_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_successor_productstepsmultiplyoutputreal) = S ge_signed_half_successor_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_successor_productstepsmultiply) * (ge_second_rp_successor_productstepsmultiply))) + (((ge_first_rn_successor_productstepsmultiply) * (ge_second_rn_successor_productstepsmultiply))))) + (((((ge_first_ip_successor_productstepsmultiply) * (ge_second_in_successor_productstepsmultiply))) + (((ge_first_in_successor_productstepsmultiply) * (ge_second_ip_successor_productstepsmultiply))))))) + ge_balance_negative_successor_productstepsmultiplyoutputreal = (((((((ge_first_rp_successor_productstepsmultiply) * (ge_second_rn_successor_productstepsmultiply))) + (((ge_first_rn_successor_productstepsmultiply) * (ge_second_rp_successor_productstepsmultiply))))) + (((((ge_first_ip_successor_productstepsmultiply) * (ge_second_ip_successor_productstepsmultiply))) + (((ge_first_in_successor_productstepsmultiply) * (ge_second_in_successor_productstepsmultiply))))))) + ge_balance_positive_successor_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_successor_productstepsmultiplyoutputimaginary ge_balance_negative_successor_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_successor_productstepsmultiplyoutput) = 2 * (ge_balance_positive_successor_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_successor_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_successor_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_successor_productstepsmultiplyoutput) = 2 * ge_signed_half_successor_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_successor_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_successor_productstepsmultiplyoutputimaginary) = S ge_signed_half_successor_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_successor_productstepsmultiply) * (ge_second_ip_successor_productstepsmultiply))) + (((ge_first_rn_successor_productstepsmultiply) * (ge_second_in_successor_productstepsmultiply))))) + (((((ge_first_ip_successor_productstepsmultiply) * (ge_second_rp_successor_productstepsmultiply))) + (((ge_first_in_successor_productstepsmultiply) * (ge_second_rn_successor_productstepsmultiply))))))) + ge_balance_negative_successor_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_successor_productstepsmultiply) * (ge_second_in_successor_productstepsmultiply))) + (((ge_first_rn_successor_productstepsmultiply) * (ge_second_ip_successor_productstepsmultiply))))) + (((((ge_first_ip_successor_productstepsmultiply) * (ge_second_rn_successor_productstepsmultiply))) + (((ge_first_in_successor_productstepsmultiply) * (ge_second_rp_successor_productstepsmultiply))))))) + ge_balance_positive_successor_productstepsmultiplyoutputimaginary)))))))))))))))) -> exists a P. ((((exists ff_h_gprod_successor_factor. ff_h_gprod_successor_factor + S (a) = S ((S (l)) * c)) /\ exists ff_q_gprod_successor_factor. b = ff_q_gprod_successor_factor * S ((S (l)) * c) + (a))) /\ ((exists gr_product_trace_successor_prefix gr_product_scale_successor_prefix. ((((exists ff_h_gprod_successor_prefixstart. ff_h_gprod_successor_prefixstart + S (6) = S ((S (0)) * gr_product_scale_successor_prefix)) /\ exists ff_q_gprod_successor_prefixstart. gr_product_trace_successor_prefix = ff_q_gprod_successor_prefixstart * S ((S (0)) * gr_product_scale_successor_prefix) + (6))) /\ ((((exists ff_h_gprod_successor_prefixend. ff_h_gprod_successor_prefixend + S (P) = S ((S (l)) * gr_product_scale_successor_prefix)) /\ exists ff_q_gprod_successor_prefixend. gr_product_trace_successor_prefix = ff_q_gprod_successor_prefixend * S ((S (l)) * gr_product_scale_successor_prefix) + (P))) /\ (forall gr_product_index_successor_prefixsteps. (exists ge_gap_successor_prefixstepsindex_bound. ge_gap_successor_prefixstepsindex_bound + S (gr_product_index_successor_prefixsteps) = (l)) -> exists gr_product_factor_successor_prefixsteps gr_product_before_successor_prefixsteps gr_product_after_successor_prefixsteps. ((((exists ff_h_gprod_successor_prefixstepsfactor. ff_h_gprod_successor_prefixstepsfactor + S (gr_product_factor_successor_prefixsteps) = S ((S (gr_product_index_successor_prefixsteps)) * c)) /\ exists ff_q_gprod_successor_prefixstepsfactor. b = ff_q_gprod_successor_prefixstepsfactor * S ((S (gr_product_index_successor_prefixsteps)) * c) + (gr_product_factor_successor_prefixsteps))) /\ ((((exists ff_h_gprod_successor_prefixstepsbefore. ff_h_gprod_successor_prefixstepsbefore + S (gr_product_before_successor_prefixsteps) = S ((S (gr_product_index_successor_prefixsteps)) * gr_product_scale_successor_prefix)) /\ exists ff_q_gprod_successor_prefixstepsbefore. gr_product_trace_successor_prefix = ff_q_gprod_successor_prefixstepsbefore * S ((S (gr_product_index_successor_prefixsteps)) * gr_product_scale_successor_prefix) + (gr_product_before_successor_prefixsteps))) /\ ((((exists ff_h_gprod_successor_prefixstepsafter. ff_h_gprod_successor_prefixstepsafter + S (gr_product_after_successor_prefixsteps) = S ((S (S (gr_product_index_successor_prefixsteps))) * gr_product_scale_successor_prefix)) /\ exists ff_q_gprod_successor_prefixstepsafter. gr_product_trace_successor_prefix = ff_q_gprod_successor_prefixstepsafter * S ((S (S (gr_product_index_successor_prefixsteps))) * gr_product_scale_successor_prefix) + (gr_product_after_successor_prefixsteps))) /\ (exists ge_first_rp_successor_prefixstepsmultiply ge_first_rn_successor_prefixstepsmultiply ge_first_ip_successor_prefixstepsmultiply ge_first_in_successor_prefixstepsmultiply ge_second_rp_successor_prefixstepsmultiply ge_second_rn_successor_prefixstepsmultiply ge_second_ip_successor_prefixstepsmultiply ge_second_in_successor_prefixstepsmultiply. ((exists ge_representation_real_code_successor_prefixstepsmultiplyfirst ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst. (((gr_product_before_successor_prefixsteps) = ((ge_representation_real_code_successor_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst)) * S ((ge_representation_real_code_successor_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst)) + ((ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst))) /\ ((exists ge_balance_positive_successor_prefixstepsmultiplyfirstreal ge_balance_negative_successor_prefixstepsmultiplyfirstreal. (((((ge_representation_real_code_successor_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_successor_prefixstepsmultiplyfirstreal) /\ (ge_balance_negative_successor_prefixstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_successor_prefixstepsmultiplyfirstrealdecode. (((ge_representation_real_code_successor_prefixstepsmultiplyfirst) = 2 * ge_signed_half_successor_prefixstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_successor_prefixstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_successor_prefixstepsmultiplyfirstreal) = S ge_signed_half_successor_prefixstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_successor_prefixstepsmultiply) + ge_balance_negative_successor_prefixstepsmultiplyfirstreal = (ge_first_rn_successor_prefixstepsmultiply) + ge_balance_positive_successor_prefixstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_successor_prefixstepsmultiplyfirstimaginary ge_balance_negative_successor_prefixstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_successor_prefixstepsmultiplyfirstimaginary) /\ (ge_balance_negative_successor_prefixstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_successor_prefixstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst) = 2 * ge_signed_half_successor_prefixstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_successor_prefixstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_successor_prefixstepsmultiplyfirstimaginary) = S ge_signed_half_successor_prefixstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_successor_prefixstepsmultiply) + ge_balance_negative_successor_prefixstepsmultiplyfirstimaginary = (ge_first_in_successor_prefixstepsmultiply) + ge_balance_positive_successor_prefixstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_successor_prefixstepsmultiplysecond ge_representation_imaginary_code_successor_prefixstepsmultiplysecond. (((gr_product_factor_successor_prefixsteps) = ((ge_representation_real_code_successor_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_successor_prefixstepsmultiplysecond)) * S ((ge_representation_real_code_successor_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_successor_prefixstepsmultiplysecond)) + ((ge_representation_imaginary_code_successor_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_successor_prefixstepsmultiplysecond))) /\ ((exists ge_balance_positive_successor_prefixstepsmultiplysecondreal ge_balance_negative_successor_prefixstepsmultiplysecondreal. (((((ge_representation_real_code_successor_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_successor_prefixstepsmultiplysecondreal) /\ (ge_balance_negative_successor_prefixstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_successor_prefixstepsmultiplysecondrealdecode. (((ge_representation_real_code_successor_prefixstepsmultiplysecond) = 2 * ge_signed_half_successor_prefixstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_successor_prefixstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_successor_prefixstepsmultiplysecondreal) = S ge_signed_half_successor_prefixstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_successor_prefixstepsmultiply) + ge_balance_negative_successor_prefixstepsmultiplysecondreal = (ge_second_rn_successor_prefixstepsmultiply) + ge_balance_positive_successor_prefixstepsmultiplysecondreal))) /\ (exists ge_balance_positive_successor_prefixstepsmultiplysecondimaginary ge_balance_negative_successor_prefixstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_successor_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_successor_prefixstepsmultiplysecondimaginary) /\ (ge_balance_negative_successor_prefixstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_successor_prefixstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_successor_prefixstepsmultiplysecond) = 2 * ge_signed_half_successor_prefixstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_successor_prefixstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_successor_prefixstepsmultiplysecondimaginary) = S ge_signed_half_successor_prefixstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_successor_prefixstepsmultiply) + ge_balance_negative_successor_prefixstepsmultiplysecondimaginary = (ge_second_in_successor_prefixstepsmultiply) + ge_balance_positive_successor_prefixstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_successor_prefixstepsmultiplyoutput ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput. (((gr_product_after_successor_prefixsteps) = ((ge_representation_real_code_successor_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput)) * S ((ge_representation_real_code_successor_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput)) + ((ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput))) /\ ((exists ge_balance_positive_successor_prefixstepsmultiplyoutputreal ge_balance_negative_successor_prefixstepsmultiplyoutputreal. (((((ge_representation_real_code_successor_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_successor_prefixstepsmultiplyoutputreal) /\ (ge_balance_negative_successor_prefixstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_successor_prefixstepsmultiplyoutputrealdecode. (((ge_representation_real_code_successor_prefixstepsmultiplyoutput) = 2 * ge_signed_half_successor_prefixstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_successor_prefixstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_successor_prefixstepsmultiplyoutputreal) = S ge_signed_half_successor_prefixstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_successor_prefixstepsmultiply) * (ge_second_rp_successor_prefixstepsmultiply))) + (((ge_first_rn_successor_prefixstepsmultiply) * (ge_second_rn_successor_prefixstepsmultiply))))) + (((((ge_first_ip_successor_prefixstepsmultiply) * (ge_second_in_successor_prefixstepsmultiply))) + (((ge_first_in_successor_prefixstepsmultiply) * (ge_second_ip_successor_prefixstepsmultiply))))))) + ge_balance_negative_successor_prefixstepsmultiplyoutputreal = (((((((ge_first_rp_successor_prefixstepsmultiply) * (ge_second_rn_successor_prefixstepsmultiply))) + (((ge_first_rn_successor_prefixstepsmultiply) * (ge_second_rp_successor_prefixstepsmultiply))))) + (((((ge_first_ip_successor_prefixstepsmultiply) * (ge_second_ip_successor_prefixstepsmultiply))) + (((ge_first_in_successor_prefixstepsmultiply) * (ge_second_in_successor_prefixstepsmultiply))))))) + ge_balance_positive_successor_prefixstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_successor_prefixstepsmultiplyoutputimaginary ge_balance_negative_successor_prefixstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_successor_prefixstepsmultiplyoutputimaginary) /\ (ge_balance_negative_successor_prefixstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_successor_prefixstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput) = 2 * ge_signed_half_successor_prefixstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_successor_prefixstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_successor_prefixstepsmultiplyoutputimaginary) = S ge_signed_half_successor_prefixstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_successor_prefixstepsmultiply) * (ge_second_ip_successor_prefixstepsmultiply))) + (((ge_first_rn_successor_prefixstepsmultiply) * (ge_second_in_successor_prefixstepsmultiply))))) + (((((ge_first_ip_successor_prefixstepsmultiply) * (ge_second_rp_successor_prefixstepsmultiply))) + (((ge_first_in_successor_prefixstepsmultiply) * (ge_second_rn_successor_prefixstepsmultiply))))))) + ge_balance_negative_successor_prefixstepsmultiplyoutputimaginary = (((((((ge_first_rp_successor_prefixstepsmultiply) * (ge_second_in_successor_prefixstepsmultiply))) + (((ge_first_rn_successor_prefixstepsmultiply) * (ge_second_ip_successor_prefixstepsmultiply))))) + (((((ge_first_ip_successor_prefixstepsmultiply) * (ge_second_rn_successor_prefixstepsmultiply))) + (((ge_first_in_successor_prefixstepsmultiply) * (ge_second_rp_successor_prefixstepsmultiply))))))) + ge_balance_positive_successor_prefixstepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_successor_multiply ge_first_rn_successor_multiply ge_first_ip_successor_multiply ge_first_in_successor_multiply ge_second_rp_successor_multiply ge_second_rn_successor_multiply ge_second_ip_successor_multiply ge_second_in_successor_multiply. ((exists ge_representation_real_code_successor_multiplyfirst ge_representation_imaginary_code_successor_multiplyfirst. (((P) = ((ge_representation_real_code_successor_multiplyfirst) + (ge_representation_imaginary_code_successor_multiplyfirst)) * S ((ge_representation_real_code_successor_multiplyfirst) + (ge_representation_imaginary_code_successor_multiplyfirst)) + ((ge_representation_imaginary_code_successor_multiplyfirst) + (ge_representation_imaginary_code_successor_multiplyfirst))) /\ ((exists ge_balance_positive_successor_multiplyfirstreal ge_balance_negative_successor_multiplyfirstreal. (((((ge_representation_real_code_successor_multiplyfirst) = 2 * (ge_balance_positive_successor_multiplyfirstreal) /\ (ge_balance_negative_successor_multiplyfirstreal) = 0) \/ exists ge_signed_half_successor_multiplyfirstrealdecode. (((ge_representation_real_code_successor_multiplyfirst) = 2 * ge_signed_half_successor_multiplyfirstrealdecode + 1 /\ (ge_balance_positive_successor_multiplyfirstreal) = 0) /\ (ge_balance_negative_successor_multiplyfirstreal) = S ge_signed_half_successor_multiplyfirstrealdecode))) /\ ((ge_first_rp_successor_multiply) + ge_balance_negative_successor_multiplyfirstreal = (ge_first_rn_successor_multiply) + ge_balance_positive_successor_multiplyfirstreal))) /\ (exists ge_balance_positive_successor_multiplyfirstimaginary ge_balance_negative_successor_multiplyfirstimaginary. (((((ge_representation_imaginary_code_successor_multiplyfirst) = 2 * (ge_balance_positive_successor_multiplyfirstimaginary) /\ (ge_balance_negative_successor_multiplyfirstimaginary) = 0) \/ exists ge_signed_half_successor_multiplyfirstimaginarydecode. (((ge_representation_imaginary_code_successor_multiplyfirst) = 2 * ge_signed_half_successor_multiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_successor_multiplyfirstimaginary) = 0) /\ (ge_balance_negative_successor_multiplyfirstimaginary) = S ge_signed_half_successor_multiplyfirstimaginarydecode))) /\ ((ge_first_ip_successor_multiply) + ge_balance_negative_successor_multiplyfirstimaginary = (ge_first_in_successor_multiply) + ge_balance_positive_successor_multiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_successor_multiplysecond ge_representation_imaginary_code_successor_multiplysecond. (((a) = ((ge_representation_real_code_successor_multiplysecond) + (ge_representation_imaginary_code_successor_multiplysecond)) * S ((ge_representation_real_code_successor_multiplysecond) + (ge_representation_imaginary_code_successor_multiplysecond)) + ((ge_representation_imaginary_code_successor_multiplysecond) + (ge_representation_imaginary_code_successor_multiplysecond))) /\ ((exists ge_balance_positive_successor_multiplysecondreal ge_balance_negative_successor_multiplysecondreal. (((((ge_representation_real_code_successor_multiplysecond) = 2 * (ge_balance_positive_successor_multiplysecondreal) /\ (ge_balance_negative_successor_multiplysecondreal) = 0) \/ exists ge_signed_half_successor_multiplysecondrealdecode. (((ge_representation_real_code_successor_multiplysecond) = 2 * ge_signed_half_successor_multiplysecondrealdecode + 1 /\ (ge_balance_positive_successor_multiplysecondreal) = 0) /\ (ge_balance_negative_successor_multiplysecondreal) = S ge_signed_half_successor_multiplysecondrealdecode))) /\ ((ge_second_rp_successor_multiply) + ge_balance_negative_successor_multiplysecondreal = (ge_second_rn_successor_multiply) + ge_balance_positive_successor_multiplysecondreal))) /\ (exists ge_balance_positive_successor_multiplysecondimaginary ge_balance_negative_successor_multiplysecondimaginary. (((((ge_representation_imaginary_code_successor_multiplysecond) = 2 * (ge_balance_positive_successor_multiplysecondimaginary) /\ (ge_balance_negative_successor_multiplysecondimaginary) = 0) \/ exists ge_signed_half_successor_multiplysecondimaginarydecode. (((ge_representation_imaginary_code_successor_multiplysecond) = 2 * ge_signed_half_successor_multiplysecondimaginarydecode + 1 /\ (ge_balance_positive_successor_multiplysecondimaginary) = 0) /\ (ge_balance_negative_successor_multiplysecondimaginary) = S ge_signed_half_successor_multiplysecondimaginarydecode))) /\ ((ge_second_ip_successor_multiply) + ge_balance_negative_successor_multiplysecondimaginary = (ge_second_in_successor_multiply) + ge_balance_positive_successor_multiplysecondimaginary)))))) /\ (exists ge_representation_real_code_successor_multiplyoutput ge_representation_imaginary_code_successor_multiplyoutput. (((Q) = ((ge_representation_real_code_successor_multiplyoutput) + (ge_representation_imaginary_code_successor_multiplyoutput)) * S ((ge_representation_real_code_successor_multiplyoutput) + (ge_representation_imaginary_code_successor_multiplyoutput)) + ((ge_representation_imaginary_code_successor_multiplyoutput) + (ge_representation_imaginary_code_successor_multiplyoutput))) /\ ((exists ge_balance_positive_successor_multiplyoutputreal ge_balance_negative_successor_multiplyoutputreal. (((((ge_representation_real_code_successor_multiplyoutput) = 2 * (ge_balance_positive_successor_multiplyoutputreal) /\ (ge_balance_negative_successor_multiplyoutputreal) = 0) \/ exists ge_signed_half_successor_multiplyoutputrealdecode. (((ge_representation_real_code_successor_multiplyoutput) = 2 * ge_signed_half_successor_multiplyoutputrealdecode + 1 /\ (ge_balance_positive_successor_multiplyoutputreal) = 0) /\ (ge_balance_negative_successor_multiplyoutputreal) = S ge_signed_half_successor_multiplyoutputrealdecode))) /\ ((((((((ge_first_rp_successor_multiply) * (ge_second_rp_successor_multiply))) + (((ge_first_rn_successor_multiply) * (ge_second_rn_successor_multiply))))) + (((((ge_first_ip_successor_multiply) * (ge_second_in_successor_multiply))) + (((ge_first_in_successor_multiply) * (ge_second_ip_successor_multiply))))))) + ge_balance_negative_successor_multiplyoutputreal = (((((((ge_first_rp_successor_multiply) * (ge_second_rn_successor_multiply))) + (((ge_first_rn_successor_multiply) * (ge_second_rp_successor_multiply))))) + (((((ge_first_ip_successor_multiply) * (ge_second_ip_successor_multiply))) + (((ge_first_in_successor_multiply) * (ge_second_in_successor_multiply))))))) + ge_balance_positive_successor_multiplyoutputreal))) /\ (exists ge_balance_positive_successor_multiplyoutputimaginary ge_balance_negative_successor_multiplyoutputimaginary. (((((ge_representation_imaginary_code_successor_multiplyoutput) = 2 * (ge_balance_positive_successor_multiplyoutputimaginary) /\ (ge_balance_negative_successor_multiplyoutputimaginary) = 0) \/ exists ge_signed_half_successor_multiplyoutputimaginarydecode. (((ge_representation_imaginary_code_successor_multiplyoutput) = 2 * ge_signed_half_successor_multiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_successor_multiplyoutputimaginary) = 0) /\ (ge_balance_negative_successor_multiplyoutputimaginary) = S ge_signed_half_successor_multiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_successor_multiply) * (ge_second_ip_successor_multiply))) + (((ge_first_rn_successor_multiply) * (ge_second_in_successor_multiply))))) + (((((ge_first_ip_successor_multiply) * (ge_second_rp_successor_multiply))) + (((ge_first_in_successor_multiply) * (ge_second_rn_successor_multiply))))))) + ge_balance_negative_successor_multiplyoutputimaginary = (((((((ge_first_rp_successor_multiply) * (ge_second_in_successor_multiply))) + (((ge_first_rn_successor_multiply) * (ge_second_ip_successor_multiply))))) + (((((ge_first_ip_successor_multiply) * (ge_second_rn_successor_multiply))) + (((ge_first_in_successor_multiply) * (ge_second_rp_successor_multiply))))))) + ge_balance_positive_successor_multiplyoutputimaginary)))))))))))

Complete tactic proof in conservative notation

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

58 script commands · 17 reading checkpoints · 2 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 multiply output transport
01Fix variables and assumptionsL1–5

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro Q
  5. L5
    intro hp
02Separate the logical casesL6–9

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

  1. L6
    cases hp
  2. L7
    cases hp_witness
  3. L8
    cases hp_witness_witness
  4. L9
    cases hp_witness_witness_right
03Establish hsL10–14

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

  1. L10
    have hs : GProductStep(b,c,x,x1,l)Definitions: GProductStep(b,c,x,x1,l)Original native command in the exact edition
  2. L11
    specialize hp_witness_witness_right_right (l)
  3. L12
    apply hp_witness_witness_right_right
  4. L13
    specialize le_refl (S l)
  5. L14
    apply le_refl
04Separate the logical casesL15–20

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

  1. L15
    cases hs
  2. L16
    cases hs_witness
  3. L17
    cases hs_witness_witness
  4. L18
    cases hs_witness_witness_witness
  5. L19
    cases hs_witness_witness_witness_right
  6. L20
    cases hs_witness_witness_witness_right_right
05Establish heqL21–29

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

  1. L21
    have heq : x4=Q
  2. L22
    specialize beta_at_unique (x)
  3. L23
    specialize beta_at_unique (x1)
  4. L24
    specialize beta_at_unique (S l)
  5. L25
    specialize beta_at_unique (x4)
  6. L26
    specialize beta_at_unique (Q)
  7. L27
    apply beta_at_unique
  8. L28
    exact hs_witness_witness_witness_right_right_left
  9. L29
    exact hp_witness_witness_right_left
06Construct an explicit witnessL30–31

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

  1. L30
    exists (x2)
  2. L31
    exists (x3)
07Separate the logical casesL32–32

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

  1. L32
    split
08Use earlier factsL33–33

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

  1. L33
    exact hs_witness_witness_witness_left
09Separate the logical casesL34–34

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

  1. L34
    split
10Construct an explicit witnessL35–36

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

  1. L35
    exists (x)
  2. L36
    exists (x1)
11Separate the logical casesL37–37

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

  1. L37
    split
12Use earlier factsL38–38

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

  1. L38
    exact hp_witness_witness_left
13Separate the logical casesL39–39

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

  1. L39
    split
14Use earlier factsL40–40

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

  1. L40
    exact hs_witness_witness_witness_right_left
15Fix variables and assumptionsL41–42

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

  1. L41
    intro i
  2. L42
    intro hi
16Use earlier factsL43–52

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

  1. L43
    specialize hp_witness_witness_right_right (i)
  2. L44
    apply hp_witness_witness_right_right
  3. L45
    specialize lt_of_lt_of_le (i)
  4. L46
    specialize lt_of_lt_of_le (l)
  5. L47
    specialize lt_of_lt_of_le (S l)
  6. L48
    apply lt_of_lt_of_le
  7. L49
    exact hi
  8. L50
    specialize le_succ_self (l)
  9. L51
    apply le_succ_self
  10. L52
    specialize gaussian_multiply_output_transport (x3)
17Use earlier factsL53–58

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

  1. L53
    specialize gaussian_multiply_output_transport (x2)
  2. L54
    specialize gaussian_multiply_output_transport (x4)
  3. L55
    specialize gaussian_multiply_output_transport (Q)
  4. L56
    apply gaussian_multiply_output_transport
  5. L57
    exact heq
  6. L58
    exact hs_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 58 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro Q
  5. 0005intro hp
  6. 0006cases hp
  7. 0007cases hp_witness
  8. 0008cases hp_witness_witness
  9. 0009cases hp_witness_witness_right
  10. 0010have hs : GProductStep(b,c,x,x1,l)
  11. 0011specialize hp_witness_witness_right_right (l)
  12. 0012apply hp_witness_witness_right_right
  13. 0013specialize le_refl (S l)
  14. 0014apply le_refl
  15. 0015cases hs
  16. 0016cases hs_witness
  17. 0017cases hs_witness_witness
  18. 0018cases hs_witness_witness_witness
  19. 0019cases hs_witness_witness_witness_right
  20. 0020cases hs_witness_witness_witness_right_right
  21. 0021have heq : x4=Q
  22. 0022specialize beta_at_unique (x)
  23. 0023specialize beta_at_unique (x1)
  24. 0024specialize beta_at_unique (S l)
  25. 0025specialize beta_at_unique (x4)
  26. 0026specialize beta_at_unique (Q)
  27. 0027apply beta_at_unique
  28. 0028exact hs_witness_witness_witness_right_right_left
  29. 0029exact hp_witness_witness_right_left
  30. 0030exists (x2)
  31. 0031exists (x3)
  32. 0032split
  33. 0033exact hs_witness_witness_witness_left
  34. 0034split
  35. 0035exists (x)
  36. 0036exists (x1)
  37. 0037split
  38. 0038exact hp_witness_witness_left
  39. 0039split
  40. 0040exact hs_witness_witness_witness_right_left
  41. 0041intro i
  42. 0042intro hi
  43. 0043specialize hp_witness_witness_right_right (i)
  44. 0044apply hp_witness_witness_right_right
  45. 0045specialize lt_of_lt_of_le (i)
  46. 0046specialize lt_of_lt_of_le (l)
  47. 0047specialize lt_of_lt_of_le (S l)
  48. 0048apply lt_of_lt_of_le
  49. 0049exact hi
  50. 0050specialize le_succ_self (l)
  51. 0051apply le_succ_self
  52. 0052specialize gaussian_multiply_output_transport (x3)
  53. 0053specialize gaussian_multiply_output_transport (x2)
  54. 0054specialize gaussian_multiply_output_transport (x4)
  55. 0055specialize gaussian_multiply_output_transport (Q)
  56. 0056apply gaussian_multiply_output_transport
  57. 0057exact heq
  58. 0058exact hs_witness_witness_witness_right_right_right