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. ∀ P. ∀ p. GProduct(b,c,S l,P) → BetaAt(b,c,l,p) → ∃ x. GProduct(b,c,l,x) ∧ GMul(x,p,P)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
gaussian_product_successor_decomposebeta_at_unique · checked external prerequisite
Original expanded first-order statement
forall b c l P p. (exists gr_product_trace_last_fixed_product gr_product_scale_last_fixed_product. ((((exists ff_h_gprod_last_fixed_productstart. ff_h_gprod_last_fixed_productstart + S (6) = S ((S (0)) * gr_product_scale_last_fixed_product)) /\ exists ff_q_gprod_last_fixed_productstart. gr_product_trace_last_fixed_product = ff_q_gprod_last_fixed_productstart * S ((S (0)) * gr_product_scale_last_fixed_product) + (6))) /\ ((((exists ff_h_gprod_last_fixed_productend. ff_h_gprod_last_fixed_productend + S (P) = S ((S (S l)) * gr_product_scale_last_fixed_product)) /\ exists ff_q_gprod_last_fixed_productend. gr_product_trace_last_fixed_product = ff_q_gprod_last_fixed_productend * S ((S (S l)) * gr_product_scale_last_fixed_product) + (P))) /\ (forall gr_product_index_last_fixed_productsteps. (exists ge_gap_last_fixed_productstepsindex_bound. ge_gap_last_fixed_productstepsindex_bound + S (gr_product_index_last_fixed_productsteps) = (S l)) -> exists gr_product_factor_last_fixed_productsteps gr_product_before_last_fixed_productsteps gr_product_after_last_fixed_productsteps. ((((exists ff_h_gprod_last_fixed_productstepsfactor. ff_h_gprod_last_fixed_productstepsfactor + S (gr_product_factor_last_fixed_productsteps) = S ((S (gr_product_index_last_fixed_productsteps)) * c)) /\ exists ff_q_gprod_last_fixed_productstepsfactor. b = ff_q_gprod_last_fixed_productstepsfactor * S ((S (gr_product_index_last_fixed_productsteps)) * c) + (gr_product_factor_last_fixed_productsteps))) /\ ((((exists ff_h_gprod_last_fixed_productstepsbefore. ff_h_gprod_last_fixed_productstepsbefore + S (gr_product_before_last_fixed_productsteps) = S ((S (gr_product_index_last_fixed_productsteps)) * gr_product_scale_last_fixed_product)) /\ exists ff_q_gprod_last_fixed_productstepsbefore. gr_product_trace_last_fixed_product = ff_q_gprod_last_fixed_productstepsbefore * S ((S (gr_product_index_last_fixed_productsteps)) * gr_product_scale_last_fixed_product) + (gr_product_before_last_fixed_productsteps))) /\ ((((exists ff_h_gprod_last_fixed_productstepsafter. ff_h_gprod_last_fixed_productstepsafter + S (gr_product_after_last_fixed_productsteps) = S ((S (S (gr_product_index_last_fixed_productsteps))) * gr_product_scale_last_fixed_product)) /\ exists ff_q_gprod_last_fixed_productstepsafter. gr_product_trace_last_fixed_product = ff_q_gprod_last_fixed_productstepsafter * S ((S (S (gr_product_index_last_fixed_productsteps))) * gr_product_scale_last_fixed_product) + (gr_product_after_last_fixed_productsteps))) /\ (exists ge_first_rp_last_fixed_productstepsmultiply ge_first_rn_last_fixed_productstepsmultiply ge_first_ip_last_fixed_productstepsmultiply ge_first_in_last_fixed_productstepsmultiply ge_second_rp_last_fixed_productstepsmultiply ge_second_rn_last_fixed_productstepsmultiply ge_second_ip_last_fixed_productstepsmultiply ge_second_in_last_fixed_productstepsmultiply. ((exists ge_representation_real_code_last_fixed_productstepsmultiplyfirst ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst. (((gr_product_before_last_fixed_productsteps) = ((ge_representation_real_code_last_fixed_productstepsmultiplyfirst) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst)) * S ((ge_representation_real_code_last_fixed_productstepsmultiplyfirst) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_last_fixed_productstepsmultiplyfirstreal ge_balance_negative_last_fixed_productstepsmultiplyfirstreal. (((((ge_representation_real_code_last_fixed_productstepsmultiplyfirst) = 2 * (ge_balance_positive_last_fixed_productstepsmultiplyfirstreal) /\ (ge_balance_negative_last_fixed_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_last_fixed_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_last_fixed_productstepsmultiplyfirst) = 2 * ge_signed_half_last_fixed_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_last_fixed_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_last_fixed_productstepsmultiplyfirstreal) = S ge_signed_half_last_fixed_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_last_fixed_productstepsmultiply) + ge_balance_negative_last_fixed_productstepsmultiplyfirstreal = (ge_first_rn_last_fixed_productstepsmultiply) + ge_balance_positive_last_fixed_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_last_fixed_productstepsmultiplyfirstimaginary ge_balance_negative_last_fixed_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst) = 2 * (ge_balance_positive_last_fixed_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_last_fixed_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_last_fixed_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst) = 2 * ge_signed_half_last_fixed_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_last_fixed_productstepsmultiplyfirstimaginary) = S ge_signed_half_last_fixed_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_last_fixed_productstepsmultiply) + ge_balance_negative_last_fixed_productstepsmultiplyfirstimaginary = (ge_first_in_last_fixed_productstepsmultiply) + ge_balance_positive_last_fixed_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_last_fixed_productstepsmultiplysecond ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond. (((gr_product_factor_last_fixed_productsteps) = ((ge_representation_real_code_last_fixed_productstepsmultiplysecond) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond)) * S ((ge_representation_real_code_last_fixed_productstepsmultiplysecond) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_last_fixed_productstepsmultiplysecondreal ge_balance_negative_last_fixed_productstepsmultiplysecondreal. (((((ge_representation_real_code_last_fixed_productstepsmultiplysecond) = 2 * (ge_balance_positive_last_fixed_productstepsmultiplysecondreal) /\ (ge_balance_negative_last_fixed_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_last_fixed_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_last_fixed_productstepsmultiplysecond) = 2 * ge_signed_half_last_fixed_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_last_fixed_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_last_fixed_productstepsmultiplysecondreal) = S ge_signed_half_last_fixed_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_last_fixed_productstepsmultiply) + ge_balance_negative_last_fixed_productstepsmultiplysecondreal = (ge_second_rn_last_fixed_productstepsmultiply) + ge_balance_positive_last_fixed_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_last_fixed_productstepsmultiplysecondimaginary ge_balance_negative_last_fixed_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond) = 2 * (ge_balance_positive_last_fixed_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_last_fixed_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_last_fixed_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond) = 2 * ge_signed_half_last_fixed_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_last_fixed_productstepsmultiplysecondimaginary) = S ge_signed_half_last_fixed_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_last_fixed_productstepsmultiply) + ge_balance_negative_last_fixed_productstepsmultiplysecondimaginary = (ge_second_in_last_fixed_productstepsmultiply) + ge_balance_positive_last_fixed_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_last_fixed_productstepsmultiplyoutput ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput. (((gr_product_after_last_fixed_productsteps) = ((ge_representation_real_code_last_fixed_productstepsmultiplyoutput) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput)) * S ((ge_representation_real_code_last_fixed_productstepsmultiplyoutput) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_last_fixed_productstepsmultiplyoutputreal ge_balance_negative_last_fixed_productstepsmultiplyoutputreal. (((((ge_representation_real_code_last_fixed_productstepsmultiplyoutput) = 2 * (ge_balance_positive_last_fixed_productstepsmultiplyoutputreal) /\ (ge_balance_negative_last_fixed_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_last_fixed_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_last_fixed_productstepsmultiplyoutput) = 2 * ge_signed_half_last_fixed_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_last_fixed_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_last_fixed_productstepsmultiplyoutputreal) = S ge_signed_half_last_fixed_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_last_fixed_productstepsmultiply) * (ge_second_rp_last_fixed_productstepsmultiply))) + (((ge_first_rn_last_fixed_productstepsmultiply) * (ge_second_rn_last_fixed_productstepsmultiply))))) + (((((ge_first_ip_last_fixed_productstepsmultiply) * (ge_second_in_last_fixed_productstepsmultiply))) + (((ge_first_in_last_fixed_productstepsmultiply) * (ge_second_ip_last_fixed_productstepsmultiply))))))) + ge_balance_negative_last_fixed_productstepsmultiplyoutputreal = (((((((ge_first_rp_last_fixed_productstepsmultiply) * (ge_second_rn_last_fixed_productstepsmultiply))) + (((ge_first_rn_last_fixed_productstepsmultiply) * (ge_second_rp_last_fixed_productstepsmultiply))))) + (((((ge_first_ip_last_fixed_productstepsmultiply) * (ge_second_ip_last_fixed_productstepsmultiply))) + (((ge_first_in_last_fixed_productstepsmultiply) * (ge_second_in_last_fixed_productstepsmultiply))))))) + ge_balance_positive_last_fixed_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_last_fixed_productstepsmultiplyoutputimaginary ge_balance_negative_last_fixed_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput) = 2 * (ge_balance_positive_last_fixed_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_last_fixed_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_last_fixed_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput) = 2 * ge_signed_half_last_fixed_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_last_fixed_productstepsmultiplyoutputimaginary) = S ge_signed_half_last_fixed_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_last_fixed_productstepsmultiply) * (ge_second_ip_last_fixed_productstepsmultiply))) + (((ge_first_rn_last_fixed_productstepsmultiply) * (ge_second_in_last_fixed_productstepsmultiply))))) + (((((ge_first_ip_last_fixed_productstepsmultiply) * (ge_second_rp_last_fixed_productstepsmultiply))) + (((ge_first_in_last_fixed_productstepsmultiply) * (ge_second_rn_last_fixed_productstepsmultiply))))))) + ge_balance_negative_last_fixed_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_last_fixed_productstepsmultiply) * (ge_second_in_last_fixed_productstepsmultiply))) + (((ge_first_rn_last_fixed_productstepsmultiply) * (ge_second_ip_last_fixed_productstepsmultiply))))) + (((((ge_first_ip_last_fixed_productstepsmultiply) * (ge_second_rn_last_fixed_productstepsmultiply))) + (((ge_first_in_last_fixed_productstepsmultiply) * (ge_second_rp_last_fixed_productstepsmultiply))))))) + ge_balance_positive_last_fixed_productstepsmultiplyoutputimaginary)))))))))))))))) -> (((exists ff_h_gprod_last_fixed_factor. ff_h_gprod_last_fixed_factor + S (p) = S ((S (l)) * c)) /\ exists ff_q_gprod_last_fixed_factor. b = ff_q_gprod_last_fixed_factor * S ((S (l)) * c) + (p))) -> exists R. ((exists gr_product_trace_last_fixed_prefix gr_product_scale_last_fixed_prefix. ((((exists ff_h_gprod_last_fixed_prefixstart. ff_h_gprod_last_fixed_prefixstart + S (6) = S ((S (0)) * gr_product_scale_last_fixed_prefix)) /\ exists ff_q_gprod_last_fixed_prefixstart. gr_product_trace_last_fixed_prefix = ff_q_gprod_last_fixed_prefixstart * S ((S (0)) * gr_product_scale_last_fixed_prefix) + (6))) /\ ((((exists ff_h_gprod_last_fixed_prefixend. ff_h_gprod_last_fixed_prefixend + S (R) = S ((S (l)) * gr_product_scale_last_fixed_prefix)) /\ exists ff_q_gprod_last_fixed_prefixend. gr_product_trace_last_fixed_prefix = ff_q_gprod_last_fixed_prefixend * S ((S (l)) * gr_product_scale_last_fixed_prefix) + (R))) /\ (forall gr_product_index_last_fixed_prefixsteps. (exists ge_gap_last_fixed_prefixstepsindex_bound. ge_gap_last_fixed_prefixstepsindex_bound + S (gr_product_index_last_fixed_prefixsteps) = (l)) -> exists gr_product_factor_last_fixed_prefixsteps gr_product_before_last_fixed_prefixsteps gr_product_after_last_fixed_prefixsteps. ((((exists ff_h_gprod_last_fixed_prefixstepsfactor. ff_h_gprod_last_fixed_prefixstepsfactor + S (gr_product_factor_last_fixed_prefixsteps) = S ((S (gr_product_index_last_fixed_prefixsteps)) * c)) /\ exists ff_q_gprod_last_fixed_prefixstepsfactor. b = ff_q_gprod_last_fixed_prefixstepsfactor * S ((S (gr_product_index_last_fixed_prefixsteps)) * c) + (gr_product_factor_last_fixed_prefixsteps))) /\ ((((exists ff_h_gprod_last_fixed_prefixstepsbefore. ff_h_gprod_last_fixed_prefixstepsbefore + S (gr_product_before_last_fixed_prefixsteps) = S ((S (gr_product_index_last_fixed_prefixsteps)) * gr_product_scale_last_fixed_prefix)) /\ exists ff_q_gprod_last_fixed_prefixstepsbefore. gr_product_trace_last_fixed_prefix = ff_q_gprod_last_fixed_prefixstepsbefore * S ((S (gr_product_index_last_fixed_prefixsteps)) * gr_product_scale_last_fixed_prefix) + (gr_product_before_last_fixed_prefixsteps))) /\ ((((exists ff_h_gprod_last_fixed_prefixstepsafter. ff_h_gprod_last_fixed_prefixstepsafter + S (gr_product_after_last_fixed_prefixsteps) = S ((S (S (gr_product_index_last_fixed_prefixsteps))) * gr_product_scale_last_fixed_prefix)) /\ exists ff_q_gprod_last_fixed_prefixstepsafter. gr_product_trace_last_fixed_prefix = ff_q_gprod_last_fixed_prefixstepsafter * S ((S (S (gr_product_index_last_fixed_prefixsteps))) * gr_product_scale_last_fixed_prefix) + (gr_product_after_last_fixed_prefixsteps))) /\ (exists ge_first_rp_last_fixed_prefixstepsmultiply ge_first_rn_last_fixed_prefixstepsmultiply ge_first_ip_last_fixed_prefixstepsmultiply ge_first_in_last_fixed_prefixstepsmultiply ge_second_rp_last_fixed_prefixstepsmultiply ge_second_rn_last_fixed_prefixstepsmultiply ge_second_ip_last_fixed_prefixstepsmultiply ge_second_in_last_fixed_prefixstepsmultiply. ((exists ge_representation_real_code_last_fixed_prefixstepsmultiplyfirst ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst. (((gr_product_before_last_fixed_prefixsteps) = ((ge_representation_real_code_last_fixed_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst)) * S ((ge_representation_real_code_last_fixed_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst)) + ((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst))) /\ ((exists ge_balance_positive_last_fixed_prefixstepsmultiplyfirstreal ge_balance_negative_last_fixed_prefixstepsmultiplyfirstreal. (((((ge_representation_real_code_last_fixed_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_last_fixed_prefixstepsmultiplyfirstreal) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_last_fixed_prefixstepsmultiplyfirstrealdecode. (((ge_representation_real_code_last_fixed_prefixstepsmultiplyfirst) = 2 * ge_signed_half_last_fixed_prefixstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_last_fixed_prefixstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyfirstreal) = S ge_signed_half_last_fixed_prefixstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_last_fixed_prefixstepsmultiply) + ge_balance_negative_last_fixed_prefixstepsmultiplyfirstreal = (ge_first_rn_last_fixed_prefixstepsmultiply) + ge_balance_positive_last_fixed_prefixstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_last_fixed_prefixstepsmultiplyfirstimaginary ge_balance_negative_last_fixed_prefixstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_last_fixed_prefixstepsmultiplyfirstimaginary) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_last_fixed_prefixstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst) = 2 * ge_signed_half_last_fixed_prefixstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_prefixstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyfirstimaginary) = S ge_signed_half_last_fixed_prefixstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_last_fixed_prefixstepsmultiply) + ge_balance_negative_last_fixed_prefixstepsmultiplyfirstimaginary = (ge_first_in_last_fixed_prefixstepsmultiply) + ge_balance_positive_last_fixed_prefixstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_last_fixed_prefixstepsmultiplysecond ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond. (((gr_product_factor_last_fixed_prefixsteps) = ((ge_representation_real_code_last_fixed_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond)) * S ((ge_representation_real_code_last_fixed_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond)) + ((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond))) /\ ((exists ge_balance_positive_last_fixed_prefixstepsmultiplysecondreal ge_balance_negative_last_fixed_prefixstepsmultiplysecondreal. (((((ge_representation_real_code_last_fixed_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_last_fixed_prefixstepsmultiplysecondreal) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_last_fixed_prefixstepsmultiplysecondrealdecode. (((ge_representation_real_code_last_fixed_prefixstepsmultiplysecond) = 2 * ge_signed_half_last_fixed_prefixstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_last_fixed_prefixstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplysecondreal) = S ge_signed_half_last_fixed_prefixstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_last_fixed_prefixstepsmultiply) + ge_balance_negative_last_fixed_prefixstepsmultiplysecondreal = (ge_second_rn_last_fixed_prefixstepsmultiply) + ge_balance_positive_last_fixed_prefixstepsmultiplysecondreal))) /\ (exists ge_balance_positive_last_fixed_prefixstepsmultiplysecondimaginary ge_balance_negative_last_fixed_prefixstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_last_fixed_prefixstepsmultiplysecondimaginary) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_last_fixed_prefixstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond) = 2 * ge_signed_half_last_fixed_prefixstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_prefixstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplysecondimaginary) = S ge_signed_half_last_fixed_prefixstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_last_fixed_prefixstepsmultiply) + ge_balance_negative_last_fixed_prefixstepsmultiplysecondimaginary = (ge_second_in_last_fixed_prefixstepsmultiply) + ge_balance_positive_last_fixed_prefixstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_last_fixed_prefixstepsmultiplyoutput ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput. (((gr_product_after_last_fixed_prefixsteps) = ((ge_representation_real_code_last_fixed_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput)) * S ((ge_representation_real_code_last_fixed_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput)) + ((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput))) /\ ((exists ge_balance_positive_last_fixed_prefixstepsmultiplyoutputreal ge_balance_negative_last_fixed_prefixstepsmultiplyoutputreal. (((((ge_representation_real_code_last_fixed_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_last_fixed_prefixstepsmultiplyoutputreal) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_last_fixed_prefixstepsmultiplyoutputrealdecode. (((ge_representation_real_code_last_fixed_prefixstepsmultiplyoutput) = 2 * ge_signed_half_last_fixed_prefixstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_last_fixed_prefixstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyoutputreal) = S ge_signed_half_last_fixed_prefixstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_last_fixed_prefixstepsmultiply) * (ge_second_rp_last_fixed_prefixstepsmultiply))) + (((ge_first_rn_last_fixed_prefixstepsmultiply) * (ge_second_rn_last_fixed_prefixstepsmultiply))))) + (((((ge_first_ip_last_fixed_prefixstepsmultiply) * (ge_second_in_last_fixed_prefixstepsmultiply))) + (((ge_first_in_last_fixed_prefixstepsmultiply) * (ge_second_ip_last_fixed_prefixstepsmultiply))))))) + ge_balance_negative_last_fixed_prefixstepsmultiplyoutputreal = (((((((ge_first_rp_last_fixed_prefixstepsmultiply) * (ge_second_rn_last_fixed_prefixstepsmultiply))) + (((ge_first_rn_last_fixed_prefixstepsmultiply) * (ge_second_rp_last_fixed_prefixstepsmultiply))))) + (((((ge_first_ip_last_fixed_prefixstepsmultiply) * (ge_second_ip_last_fixed_prefixstepsmultiply))) + (((ge_first_in_last_fixed_prefixstepsmultiply) * (ge_second_in_last_fixed_prefixstepsmultiply))))))) + ge_balance_positive_last_fixed_prefixstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_last_fixed_prefixstepsmultiplyoutputimaginary ge_balance_negative_last_fixed_prefixstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_last_fixed_prefixstepsmultiplyoutputimaginary) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_last_fixed_prefixstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput) = 2 * ge_signed_half_last_fixed_prefixstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_prefixstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyoutputimaginary) = S ge_signed_half_last_fixed_prefixstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_last_fixed_prefixstepsmultiply) * (ge_second_ip_last_fixed_prefixstepsmultiply))) + (((ge_first_rn_last_fixed_prefixstepsmultiply) * (ge_second_in_last_fixed_prefixstepsmultiply))))) + (((((ge_first_ip_last_fixed_prefixstepsmultiply) * (ge_second_rp_last_fixed_prefixstepsmultiply))) + (((ge_first_in_last_fixed_prefixstepsmultiply) * (ge_second_rn_last_fixed_prefixstepsmultiply))))))) + ge_balance_negative_last_fixed_prefixstepsmultiplyoutputimaginary = (((((((ge_first_rp_last_fixed_prefixstepsmultiply) * (ge_second_in_last_fixed_prefixstepsmultiply))) + (((ge_first_rn_last_fixed_prefixstepsmultiply) * (ge_second_ip_last_fixed_prefixstepsmultiply))))) + (((((ge_first_ip_last_fixed_prefixstepsmultiply) * (ge_second_rn_last_fixed_prefixstepsmultiply))) + (((ge_first_in_last_fixed_prefixstepsmultiply) * (ge_second_rp_last_fixed_prefixstepsmultiply))))))) + ge_balance_positive_last_fixed_prefixstepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_last_fixed_multiply ge_first_rn_last_fixed_multiply ge_first_ip_last_fixed_multiply ge_first_in_last_fixed_multiply ge_second_rp_last_fixed_multiply ge_second_rn_last_fixed_multiply ge_second_ip_last_fixed_multiply ge_second_in_last_fixed_multiply. ((exists ge_representation_real_code_last_fixed_multiplyfirst ge_representation_imaginary_code_last_fixed_multiplyfirst. (((R) = ((ge_representation_real_code_last_fixed_multiplyfirst) + (ge_representation_imaginary_code_last_fixed_multiplyfirst)) * S ((ge_representation_real_code_last_fixed_multiplyfirst) + (ge_representation_imaginary_code_last_fixed_multiplyfirst)) + ((ge_representation_imaginary_code_last_fixed_multiplyfirst) + (ge_representation_imaginary_code_last_fixed_multiplyfirst))) /\ ((exists ge_balance_positive_last_fixed_multiplyfirstreal ge_balance_negative_last_fixed_multiplyfirstreal. (((((ge_representation_real_code_last_fixed_multiplyfirst) = 2 * (ge_balance_positive_last_fixed_multiplyfirstreal) /\ (ge_balance_negative_last_fixed_multiplyfirstreal) = 0) \/ exists ge_signed_half_last_fixed_multiplyfirstrealdecode. (((ge_representation_real_code_last_fixed_multiplyfirst) = 2 * ge_signed_half_last_fixed_multiplyfirstrealdecode + 1 /\ (ge_balance_positive_last_fixed_multiplyfirstreal) = 0) /\ (ge_balance_negative_last_fixed_multiplyfirstreal) = S ge_signed_half_last_fixed_multiplyfirstrealdecode))) /\ ((ge_first_rp_last_fixed_multiply) + ge_balance_negative_last_fixed_multiplyfirstreal = (ge_first_rn_last_fixed_multiply) + ge_balance_positive_last_fixed_multiplyfirstreal))) /\ (exists ge_balance_positive_last_fixed_multiplyfirstimaginary ge_balance_negative_last_fixed_multiplyfirstimaginary. (((((ge_representation_imaginary_code_last_fixed_multiplyfirst) = 2 * (ge_balance_positive_last_fixed_multiplyfirstimaginary) /\ (ge_balance_negative_last_fixed_multiplyfirstimaginary) = 0) \/ exists ge_signed_half_last_fixed_multiplyfirstimaginarydecode. (((ge_representation_imaginary_code_last_fixed_multiplyfirst) = 2 * ge_signed_half_last_fixed_multiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_multiplyfirstimaginary) = 0) /\ (ge_balance_negative_last_fixed_multiplyfirstimaginary) = S ge_signed_half_last_fixed_multiplyfirstimaginarydecode))) /\ ((ge_first_ip_last_fixed_multiply) + ge_balance_negative_last_fixed_multiplyfirstimaginary = (ge_first_in_last_fixed_multiply) + ge_balance_positive_last_fixed_multiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_last_fixed_multiplysecond ge_representation_imaginary_code_last_fixed_multiplysecond. (((p) = ((ge_representation_real_code_last_fixed_multiplysecond) + (ge_representation_imaginary_code_last_fixed_multiplysecond)) * S ((ge_representation_real_code_last_fixed_multiplysecond) + (ge_representation_imaginary_code_last_fixed_multiplysecond)) + ((ge_representation_imaginary_code_last_fixed_multiplysecond) + (ge_representation_imaginary_code_last_fixed_multiplysecond))) /\ ((exists ge_balance_positive_last_fixed_multiplysecondreal ge_balance_negative_last_fixed_multiplysecondreal. (((((ge_representation_real_code_last_fixed_multiplysecond) = 2 * (ge_balance_positive_last_fixed_multiplysecondreal) /\ (ge_balance_negative_last_fixed_multiplysecondreal) = 0) \/ exists ge_signed_half_last_fixed_multiplysecondrealdecode. (((ge_representation_real_code_last_fixed_multiplysecond) = 2 * ge_signed_half_last_fixed_multiplysecondrealdecode + 1 /\ (ge_balance_positive_last_fixed_multiplysecondreal) = 0) /\ (ge_balance_negative_last_fixed_multiplysecondreal) = S ge_signed_half_last_fixed_multiplysecondrealdecode))) /\ ((ge_second_rp_last_fixed_multiply) + ge_balance_negative_last_fixed_multiplysecondreal = (ge_second_rn_last_fixed_multiply) + ge_balance_positive_last_fixed_multiplysecondreal))) /\ (exists ge_balance_positive_last_fixed_multiplysecondimaginary ge_balance_negative_last_fixed_multiplysecondimaginary. (((((ge_representation_imaginary_code_last_fixed_multiplysecond) = 2 * (ge_balance_positive_last_fixed_multiplysecondimaginary) /\ (ge_balance_negative_last_fixed_multiplysecondimaginary) = 0) \/ exists ge_signed_half_last_fixed_multiplysecondimaginarydecode. (((ge_representation_imaginary_code_last_fixed_multiplysecond) = 2 * ge_signed_half_last_fixed_multiplysecondimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_multiplysecondimaginary) = 0) /\ (ge_balance_negative_last_fixed_multiplysecondimaginary) = S ge_signed_half_last_fixed_multiplysecondimaginarydecode))) /\ ((ge_second_ip_last_fixed_multiply) + ge_balance_negative_last_fixed_multiplysecondimaginary = (ge_second_in_last_fixed_multiply) + ge_balance_positive_last_fixed_multiplysecondimaginary)))))) /\ (exists ge_representation_real_code_last_fixed_multiplyoutput ge_representation_imaginary_code_last_fixed_multiplyoutput. (((P) = ((ge_representation_real_code_last_fixed_multiplyoutput) + (ge_representation_imaginary_code_last_fixed_multiplyoutput)) * S ((ge_representation_real_code_last_fixed_multiplyoutput) + (ge_representation_imaginary_code_last_fixed_multiplyoutput)) + ((ge_representation_imaginary_code_last_fixed_multiplyoutput) + (ge_representation_imaginary_code_last_fixed_multiplyoutput))) /\ ((exists ge_balance_positive_last_fixed_multiplyoutputreal ge_balance_negative_last_fixed_multiplyoutputreal. (((((ge_representation_real_code_last_fixed_multiplyoutput) = 2 * (ge_balance_positive_last_fixed_multiplyoutputreal) /\ (ge_balance_negative_last_fixed_multiplyoutputreal) = 0) \/ exists ge_signed_half_last_fixed_multiplyoutputrealdecode. (((ge_representation_real_code_last_fixed_multiplyoutput) = 2 * ge_signed_half_last_fixed_multiplyoutputrealdecode + 1 /\ (ge_balance_positive_last_fixed_multiplyoutputreal) = 0) /\ (ge_balance_negative_last_fixed_multiplyoutputreal) = S ge_signed_half_last_fixed_multiplyoutputrealdecode))) /\ ((((((((ge_first_rp_last_fixed_multiply) * (ge_second_rp_last_fixed_multiply))) + (((ge_first_rn_last_fixed_multiply) * (ge_second_rn_last_fixed_multiply))))) + (((((ge_first_ip_last_fixed_multiply) * (ge_second_in_last_fixed_multiply))) + (((ge_first_in_last_fixed_multiply) * (ge_second_ip_last_fixed_multiply))))))) + ge_balance_negative_last_fixed_multiplyoutputreal = (((((((ge_first_rp_last_fixed_multiply) * (ge_second_rn_last_fixed_multiply))) + (((ge_first_rn_last_fixed_multiply) * (ge_second_rp_last_fixed_multiply))))) + (((((ge_first_ip_last_fixed_multiply) * (ge_second_ip_last_fixed_multiply))) + (((ge_first_in_last_fixed_multiply) * (ge_second_in_last_fixed_multiply))))))) + ge_balance_positive_last_fixed_multiplyoutputreal))) /\ (exists ge_balance_positive_last_fixed_multiplyoutputimaginary ge_balance_negative_last_fixed_multiplyoutputimaginary. (((((ge_representation_imaginary_code_last_fixed_multiplyoutput) = 2 * (ge_balance_positive_last_fixed_multiplyoutputimaginary) /\ (ge_balance_negative_last_fixed_multiplyoutputimaginary) = 0) \/ exists ge_signed_half_last_fixed_multiplyoutputimaginarydecode. (((ge_representation_imaginary_code_last_fixed_multiplyoutput) = 2 * ge_signed_half_last_fixed_multiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_multiplyoutputimaginary) = 0) /\ (ge_balance_negative_last_fixed_multiplyoutputimaginary) = S ge_signed_half_last_fixed_multiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_last_fixed_multiply) * (ge_second_ip_last_fixed_multiply))) + (((ge_first_rn_last_fixed_multiply) * (ge_second_in_last_fixed_multiply))))) + (((((ge_first_ip_last_fixed_multiply) * (ge_second_rp_last_fixed_multiply))) + (((ge_first_in_last_fixed_multiply) * (ge_second_rn_last_fixed_multiply))))))) + ge_balance_negative_last_fixed_multiplyoutputimaginary = (((((((ge_first_rp_last_fixed_multiply) * (ge_second_in_last_fixed_multiply))) + (((ge_first_rn_last_fixed_multiply) * (ge_second_ip_last_fixed_multiply))))) + (((((ge_first_ip_last_fixed_multiply) * (ge_second_rn_last_fixed_multiply))) + (((ge_first_in_last_fixed_multiply) * (ge_second_rp_last_fixed_multiply))))))) + ge_balance_positive_last_fixed_multiplyoutputimaginary))))))))))Complete tactic proof in conservative notation
All 32 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
32 script commands · 9 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)
01Fix variables and assumptionsL1–7
02Establish hsL8–14
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product successor decompose.
- L8
have hs : ∃ a. ∃ R. BetaAt(b,c,l,a) ∧ (GProduct(b,c,l,R) ∧ GMul(R,a,P))Definitions: BetaAt(b,c,l,a)GProduct(b,c,l,R)GMul(R,a,P)Original native command in the exact edition - L9
specialize gaussian_product_successor_decompose (b) - L10
specialize gaussian_product_successor_decompose (c) - L11
specialize gaussian_product_successor_decompose (l) - L12
specialize gaussian_product_successor_decompose (P) - L13
apply gaussian_product_successor_decompose - L14
exact hP
03Separate the logical casesL15–18
04Establish heqL19–27
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
05Construct an explicit witnessL28–28
Supply the displayed value, then prove that it has the required property.
- L28
exists (x1)
06Separate the logical casesL29–29
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L29
split
07Use earlier factsL30–30
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L30
exact hs_witness_witness_right_left
08Calculate and transport equalitiesL31–31
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L31
rewrite heq at hs_witness_witness_right_right
09Use earlier factsL32–32
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L32
exact hs_witness_witness_right_right
Original defined command ledger · 32 lines
- 0001
intro b - 0002
intro c - 0003
intro l - 0004
intro P - 0005
intro p - 0006
intro hP - 0007
intro hp - 0008
have hs : ∃ a. ∃ R. BetaAt(b,c,l,a) ∧ (GProduct(b,c,l,R) ∧ GMul(R,a,P)) - 0009
specialize gaussian_product_successor_decompose (b) - 0010
specialize gaussian_product_successor_decompose (c) - 0011
specialize gaussian_product_successor_decompose (l) - 0012
specialize gaussian_product_successor_decompose (P) - 0013
apply gaussian_product_successor_decompose - 0014
exact hP - 0015
cases hs - 0016
cases hs_witness - 0017
cases hs_witness_witness - 0018
cases hs_witness_witness_right - 0019
have heq : x=p - 0020
specialize beta_at_unique (b) - 0021
specialize beta_at_unique (c) - 0022
specialize beta_at_unique (l) - 0023
specialize beta_at_unique (x) - 0024
specialize beta_at_unique (p) - 0025
apply beta_at_unique - 0026
exact hs_witness_witness_left - 0027
exact hp - 0028
exists (x1) - 0029
split - 0030
exact hs_witness_witness_right_left - 0031
rewrite heq at hs_witness_witness_right_right - 0032
exact hs_witness_witness_right_right