GF008D

gaussian_product_functional

Two actual Gaussian multiplication traces on the same finite beta prefix have literally equal canonical endpoint codes.

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

∀ l. ∀ b. ∀ c. ∀ P. ∀ Q. GProduct(b,c,l,P) → GProduct(b,c,l,Q) → P = Q

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

Definition DAG

GMul(a,b,c) · 2GProduct(b,c,l,P) · 4BetaAt(b,c,i,x) · 2

Actual proof prerequisites

gaussian_product_empty_valuegaussian_product_successor_decomposebeta_at_unique · checked external prerequisitegaussian_multiply_functional · checked external prerequisite
Original expanded first-order statement 
forall l b c P Q. (exists gr_product_trace_functional_first gr_product_scale_functional_first. ((((exists ff_h_gprod_functional_firststart. ff_h_gprod_functional_firststart + S (6) = S ((S (0)) * gr_product_scale_functional_first)) /\ exists ff_q_gprod_functional_firststart. gr_product_trace_functional_first = ff_q_gprod_functional_firststart * S ((S (0)) * gr_product_scale_functional_first) + (6))) /\ ((((exists ff_h_gprod_functional_firstend. ff_h_gprod_functional_firstend + S (P) = S ((S (l)) * gr_product_scale_functional_first)) /\ exists ff_q_gprod_functional_firstend. gr_product_trace_functional_first = ff_q_gprod_functional_firstend * S ((S (l)) * gr_product_scale_functional_first) + (P))) /\ (forall gr_product_index_functional_firststeps. (exists ge_gap_functional_firststepsindex_bound. ge_gap_functional_firststepsindex_bound + S (gr_product_index_functional_firststeps) = (l)) -> exists gr_product_factor_functional_firststeps gr_product_before_functional_firststeps gr_product_after_functional_firststeps. ((((exists ff_h_gprod_functional_firststepsfactor. ff_h_gprod_functional_firststepsfactor + S (gr_product_factor_functional_firststeps) = S ((S (gr_product_index_functional_firststeps)) * c)) /\ exists ff_q_gprod_functional_firststepsfactor. b = ff_q_gprod_functional_firststepsfactor * S ((S (gr_product_index_functional_firststeps)) * c) + (gr_product_factor_functional_firststeps))) /\ ((((exists ff_h_gprod_functional_firststepsbefore. ff_h_gprod_functional_firststepsbefore + S (gr_product_before_functional_firststeps) = S ((S (gr_product_index_functional_firststeps)) * gr_product_scale_functional_first)) /\ exists ff_q_gprod_functional_firststepsbefore. gr_product_trace_functional_first = ff_q_gprod_functional_firststepsbefore * S ((S (gr_product_index_functional_firststeps)) * gr_product_scale_functional_first) + (gr_product_before_functional_firststeps))) /\ ((((exists ff_h_gprod_functional_firststepsafter. ff_h_gprod_functional_firststepsafter + S (gr_product_after_functional_firststeps) = S ((S (S (gr_product_index_functional_firststeps))) * gr_product_scale_functional_first)) /\ exists ff_q_gprod_functional_firststepsafter. gr_product_trace_functional_first = ff_q_gprod_functional_firststepsafter * S ((S (S (gr_product_index_functional_firststeps))) * gr_product_scale_functional_first) + (gr_product_after_functional_firststeps))) /\ (exists ge_first_rp_functional_firststepsmultiply ge_first_rn_functional_firststepsmultiply ge_first_ip_functional_firststepsmultiply ge_first_in_functional_firststepsmultiply ge_second_rp_functional_firststepsmultiply ge_second_rn_functional_firststepsmultiply ge_second_ip_functional_firststepsmultiply ge_second_in_functional_firststepsmultiply. ((exists ge_representation_real_code_functional_firststepsmultiplyfirst ge_representation_imaginary_code_functional_firststepsmultiplyfirst. (((gr_product_before_functional_firststeps) = ((ge_representation_real_code_functional_firststepsmultiplyfirst) + (ge_representation_imaginary_code_functional_firststepsmultiplyfirst)) * S ((ge_representation_real_code_functional_firststepsmultiplyfirst) + (ge_representation_imaginary_code_functional_firststepsmultiplyfirst)) + ((ge_representation_imaginary_code_functional_firststepsmultiplyfirst) + (ge_representation_imaginary_code_functional_firststepsmultiplyfirst))) /\ ((exists ge_balance_positive_functional_firststepsmultiplyfirstreal ge_balance_negative_functional_firststepsmultiplyfirstreal. (((((ge_representation_real_code_functional_firststepsmultiplyfirst) = 2 * (ge_balance_positive_functional_firststepsmultiplyfirstreal) /\ (ge_balance_negative_functional_firststepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_functional_firststepsmultiplyfirstrealdecode. (((ge_representation_real_code_functional_firststepsmultiplyfirst) = 2 * ge_signed_half_functional_firststepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_functional_firststepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_functional_firststepsmultiplyfirstreal) = S ge_signed_half_functional_firststepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_functional_firststepsmultiply) + ge_balance_negative_functional_firststepsmultiplyfirstreal = (ge_first_rn_functional_firststepsmultiply) + ge_balance_positive_functional_firststepsmultiplyfirstreal))) /\ (exists ge_balance_positive_functional_firststepsmultiplyfirstimaginary ge_balance_negative_functional_firststepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_functional_firststepsmultiplyfirst) = 2 * (ge_balance_positive_functional_firststepsmultiplyfirstimaginary) /\ (ge_balance_negative_functional_firststepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_functional_firststepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_functional_firststepsmultiplyfirst) = 2 * ge_signed_half_functional_firststepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_functional_firststepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_functional_firststepsmultiplyfirstimaginary) = S ge_signed_half_functional_firststepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_functional_firststepsmultiply) + ge_balance_negative_functional_firststepsmultiplyfirstimaginary = (ge_first_in_functional_firststepsmultiply) + ge_balance_positive_functional_firststepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_functional_firststepsmultiplysecond ge_representation_imaginary_code_functional_firststepsmultiplysecond. (((gr_product_factor_functional_firststeps) = ((ge_representation_real_code_functional_firststepsmultiplysecond) + (ge_representation_imaginary_code_functional_firststepsmultiplysecond)) * S ((ge_representation_real_code_functional_firststepsmultiplysecond) + (ge_representation_imaginary_code_functional_firststepsmultiplysecond)) + ((ge_representation_imaginary_code_functional_firststepsmultiplysecond) + (ge_representation_imaginary_code_functional_firststepsmultiplysecond))) /\ ((exists ge_balance_positive_functional_firststepsmultiplysecondreal ge_balance_negative_functional_firststepsmultiplysecondreal. (((((ge_representation_real_code_functional_firststepsmultiplysecond) = 2 * (ge_balance_positive_functional_firststepsmultiplysecondreal) /\ (ge_balance_negative_functional_firststepsmultiplysecondreal) = 0) \/ exists ge_signed_half_functional_firststepsmultiplysecondrealdecode. (((ge_representation_real_code_functional_firststepsmultiplysecond) = 2 * ge_signed_half_functional_firststepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_functional_firststepsmultiplysecondreal) = 0) /\ (ge_balance_negative_functional_firststepsmultiplysecondreal) = S ge_signed_half_functional_firststepsmultiplysecondrealdecode))) /\ ((ge_second_rp_functional_firststepsmultiply) + ge_balance_negative_functional_firststepsmultiplysecondreal = (ge_second_rn_functional_firststepsmultiply) + ge_balance_positive_functional_firststepsmultiplysecondreal))) /\ (exists ge_balance_positive_functional_firststepsmultiplysecondimaginary ge_balance_negative_functional_firststepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_functional_firststepsmultiplysecond) = 2 * (ge_balance_positive_functional_firststepsmultiplysecondimaginary) /\ (ge_balance_negative_functional_firststepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_functional_firststepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_functional_firststepsmultiplysecond) = 2 * ge_signed_half_functional_firststepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_functional_firststepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_functional_firststepsmultiplysecondimaginary) = S ge_signed_half_functional_firststepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_functional_firststepsmultiply) + ge_balance_negative_functional_firststepsmultiplysecondimaginary = (ge_second_in_functional_firststepsmultiply) + ge_balance_positive_functional_firststepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_functional_firststepsmultiplyoutput ge_representation_imaginary_code_functional_firststepsmultiplyoutput. (((gr_product_after_functional_firststeps) = ((ge_representation_real_code_functional_firststepsmultiplyoutput) + (ge_representation_imaginary_code_functional_firststepsmultiplyoutput)) * S ((ge_representation_real_code_functional_firststepsmultiplyoutput) + (ge_representation_imaginary_code_functional_firststepsmultiplyoutput)) + ((ge_representation_imaginary_code_functional_firststepsmultiplyoutput) + (ge_representation_imaginary_code_functional_firststepsmultiplyoutput))) /\ ((exists ge_balance_positive_functional_firststepsmultiplyoutputreal ge_balance_negative_functional_firststepsmultiplyoutputreal. (((((ge_representation_real_code_functional_firststepsmultiplyoutput) = 2 * (ge_balance_positive_functional_firststepsmultiplyoutputreal) /\ (ge_balance_negative_functional_firststepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_functional_firststepsmultiplyoutputrealdecode. (((ge_representation_real_code_functional_firststepsmultiplyoutput) = 2 * ge_signed_half_functional_firststepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_functional_firststepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_functional_firststepsmultiplyoutputreal) = S ge_signed_half_functional_firststepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_functional_firststepsmultiply) * (ge_second_rp_functional_firststepsmultiply))) + (((ge_first_rn_functional_firststepsmultiply) * (ge_second_rn_functional_firststepsmultiply))))) + (((((ge_first_ip_functional_firststepsmultiply) * (ge_second_in_functional_firststepsmultiply))) + (((ge_first_in_functional_firststepsmultiply) * (ge_second_ip_functional_firststepsmultiply))))))) + ge_balance_negative_functional_firststepsmultiplyoutputreal = (((((((ge_first_rp_functional_firststepsmultiply) * (ge_second_rn_functional_firststepsmultiply))) + (((ge_first_rn_functional_firststepsmultiply) * (ge_second_rp_functional_firststepsmultiply))))) + (((((ge_first_ip_functional_firststepsmultiply) * (ge_second_ip_functional_firststepsmultiply))) + (((ge_first_in_functional_firststepsmultiply) * (ge_second_in_functional_firststepsmultiply))))))) + ge_balance_positive_functional_firststepsmultiplyoutputreal))) /\ (exists ge_balance_positive_functional_firststepsmultiplyoutputimaginary ge_balance_negative_functional_firststepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_functional_firststepsmultiplyoutput) = 2 * (ge_balance_positive_functional_firststepsmultiplyoutputimaginary) /\ (ge_balance_negative_functional_firststepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_functional_firststepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_functional_firststepsmultiplyoutput) = 2 * ge_signed_half_functional_firststepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_functional_firststepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_functional_firststepsmultiplyoutputimaginary) = S ge_signed_half_functional_firststepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_functional_firststepsmultiply) * (ge_second_ip_functional_firststepsmultiply))) + (((ge_first_rn_functional_firststepsmultiply) * (ge_second_in_functional_firststepsmultiply))))) + (((((ge_first_ip_functional_firststepsmultiply) * (ge_second_rp_functional_firststepsmultiply))) + (((ge_first_in_functional_firststepsmultiply) * (ge_second_rn_functional_firststepsmultiply))))))) + ge_balance_negative_functional_firststepsmultiplyoutputimaginary = (((((((ge_first_rp_functional_firststepsmultiply) * (ge_second_in_functional_firststepsmultiply))) + (((ge_first_rn_functional_firststepsmultiply) * (ge_second_ip_functional_firststepsmultiply))))) + (((((ge_first_ip_functional_firststepsmultiply) * (ge_second_rn_functional_firststepsmultiply))) + (((ge_first_in_functional_firststepsmultiply) * (ge_second_rp_functional_firststepsmultiply))))))) + ge_balance_positive_functional_firststepsmultiplyoutputimaginary)))))))))))))))) -> (exists gr_product_trace_functional_second gr_product_scale_functional_second. ((((exists ff_h_gprod_functional_secondstart. ff_h_gprod_functional_secondstart + S (6) = S ((S (0)) * gr_product_scale_functional_second)) /\ exists ff_q_gprod_functional_secondstart. gr_product_trace_functional_second = ff_q_gprod_functional_secondstart * S ((S (0)) * gr_product_scale_functional_second) + (6))) /\ ((((exists ff_h_gprod_functional_secondend. ff_h_gprod_functional_secondend + S (Q) = S ((S (l)) * gr_product_scale_functional_second)) /\ exists ff_q_gprod_functional_secondend. gr_product_trace_functional_second = ff_q_gprod_functional_secondend * S ((S (l)) * gr_product_scale_functional_second) + (Q))) /\ (forall gr_product_index_functional_secondsteps. (exists ge_gap_functional_secondstepsindex_bound. ge_gap_functional_secondstepsindex_bound + S (gr_product_index_functional_secondsteps) = (l)) -> exists gr_product_factor_functional_secondsteps gr_product_before_functional_secondsteps gr_product_after_functional_secondsteps. ((((exists ff_h_gprod_functional_secondstepsfactor. ff_h_gprod_functional_secondstepsfactor + S (gr_product_factor_functional_secondsteps) = S ((S (gr_product_index_functional_secondsteps)) * c)) /\ exists ff_q_gprod_functional_secondstepsfactor. b = ff_q_gprod_functional_secondstepsfactor * S ((S (gr_product_index_functional_secondsteps)) * c) + (gr_product_factor_functional_secondsteps))) /\ ((((exists ff_h_gprod_functional_secondstepsbefore. ff_h_gprod_functional_secondstepsbefore + S (gr_product_before_functional_secondsteps) = S ((S (gr_product_index_functional_secondsteps)) * gr_product_scale_functional_second)) /\ exists ff_q_gprod_functional_secondstepsbefore. gr_product_trace_functional_second = ff_q_gprod_functional_secondstepsbefore * S ((S (gr_product_index_functional_secondsteps)) * gr_product_scale_functional_second) + (gr_product_before_functional_secondsteps))) /\ ((((exists ff_h_gprod_functional_secondstepsafter. ff_h_gprod_functional_secondstepsafter + S (gr_product_after_functional_secondsteps) = S ((S (S (gr_product_index_functional_secondsteps))) * gr_product_scale_functional_second)) /\ exists ff_q_gprod_functional_secondstepsafter. gr_product_trace_functional_second = ff_q_gprod_functional_secondstepsafter * S ((S (S (gr_product_index_functional_secondsteps))) * gr_product_scale_functional_second) + (gr_product_after_functional_secondsteps))) /\ (exists ge_first_rp_functional_secondstepsmultiply ge_first_rn_functional_secondstepsmultiply ge_first_ip_functional_secondstepsmultiply ge_first_in_functional_secondstepsmultiply ge_second_rp_functional_secondstepsmultiply ge_second_rn_functional_secondstepsmultiply ge_second_ip_functional_secondstepsmultiply ge_second_in_functional_secondstepsmultiply. ((exists ge_representation_real_code_functional_secondstepsmultiplyfirst ge_representation_imaginary_code_functional_secondstepsmultiplyfirst. (((gr_product_before_functional_secondsteps) = ((ge_representation_real_code_functional_secondstepsmultiplyfirst) + (ge_representation_imaginary_code_functional_secondstepsmultiplyfirst)) * S ((ge_representation_real_code_functional_secondstepsmultiplyfirst) + (ge_representation_imaginary_code_functional_secondstepsmultiplyfirst)) + ((ge_representation_imaginary_code_functional_secondstepsmultiplyfirst) + (ge_representation_imaginary_code_functional_secondstepsmultiplyfirst))) /\ ((exists ge_balance_positive_functional_secondstepsmultiplyfirstreal ge_balance_negative_functional_secondstepsmultiplyfirstreal. (((((ge_representation_real_code_functional_secondstepsmultiplyfirst) = 2 * (ge_balance_positive_functional_secondstepsmultiplyfirstreal) /\ (ge_balance_negative_functional_secondstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_functional_secondstepsmultiplyfirstrealdecode. (((ge_representation_real_code_functional_secondstepsmultiplyfirst) = 2 * ge_signed_half_functional_secondstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_functional_secondstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_functional_secondstepsmultiplyfirstreal) = S ge_signed_half_functional_secondstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_functional_secondstepsmultiply) + ge_balance_negative_functional_secondstepsmultiplyfirstreal = (ge_first_rn_functional_secondstepsmultiply) + ge_balance_positive_functional_secondstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_functional_secondstepsmultiplyfirstimaginary ge_balance_negative_functional_secondstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_functional_secondstepsmultiplyfirst) = 2 * (ge_balance_positive_functional_secondstepsmultiplyfirstimaginary) /\ (ge_balance_negative_functional_secondstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_functional_secondstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_functional_secondstepsmultiplyfirst) = 2 * ge_signed_half_functional_secondstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_functional_secondstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_functional_secondstepsmultiplyfirstimaginary) = S ge_signed_half_functional_secondstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_functional_secondstepsmultiply) + ge_balance_negative_functional_secondstepsmultiplyfirstimaginary = (ge_first_in_functional_secondstepsmultiply) + ge_balance_positive_functional_secondstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_functional_secondstepsmultiplysecond ge_representation_imaginary_code_functional_secondstepsmultiplysecond. (((gr_product_factor_functional_secondsteps) = ((ge_representation_real_code_functional_secondstepsmultiplysecond) + (ge_representation_imaginary_code_functional_secondstepsmultiplysecond)) * S ((ge_representation_real_code_functional_secondstepsmultiplysecond) + (ge_representation_imaginary_code_functional_secondstepsmultiplysecond)) + ((ge_representation_imaginary_code_functional_secondstepsmultiplysecond) + (ge_representation_imaginary_code_functional_secondstepsmultiplysecond))) /\ ((exists ge_balance_positive_functional_secondstepsmultiplysecondreal ge_balance_negative_functional_secondstepsmultiplysecondreal. (((((ge_representation_real_code_functional_secondstepsmultiplysecond) = 2 * (ge_balance_positive_functional_secondstepsmultiplysecondreal) /\ (ge_balance_negative_functional_secondstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_functional_secondstepsmultiplysecondrealdecode. (((ge_representation_real_code_functional_secondstepsmultiplysecond) = 2 * ge_signed_half_functional_secondstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_functional_secondstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_functional_secondstepsmultiplysecondreal) = S ge_signed_half_functional_secondstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_functional_secondstepsmultiply) + ge_balance_negative_functional_secondstepsmultiplysecondreal = (ge_second_rn_functional_secondstepsmultiply) + ge_balance_positive_functional_secondstepsmultiplysecondreal))) /\ (exists ge_balance_positive_functional_secondstepsmultiplysecondimaginary ge_balance_negative_functional_secondstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_functional_secondstepsmultiplysecond) = 2 * (ge_balance_positive_functional_secondstepsmultiplysecondimaginary) /\ (ge_balance_negative_functional_secondstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_functional_secondstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_functional_secondstepsmultiplysecond) = 2 * ge_signed_half_functional_secondstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_functional_secondstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_functional_secondstepsmultiplysecondimaginary) = S ge_signed_half_functional_secondstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_functional_secondstepsmultiply) + ge_balance_negative_functional_secondstepsmultiplysecondimaginary = (ge_second_in_functional_secondstepsmultiply) + ge_balance_positive_functional_secondstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_functional_secondstepsmultiplyoutput ge_representation_imaginary_code_functional_secondstepsmultiplyoutput. (((gr_product_after_functional_secondsteps) = ((ge_representation_real_code_functional_secondstepsmultiplyoutput) + (ge_representation_imaginary_code_functional_secondstepsmultiplyoutput)) * S ((ge_representation_real_code_functional_secondstepsmultiplyoutput) + (ge_representation_imaginary_code_functional_secondstepsmultiplyoutput)) + ((ge_representation_imaginary_code_functional_secondstepsmultiplyoutput) + (ge_representation_imaginary_code_functional_secondstepsmultiplyoutput))) /\ ((exists ge_balance_positive_functional_secondstepsmultiplyoutputreal ge_balance_negative_functional_secondstepsmultiplyoutputreal. (((((ge_representation_real_code_functional_secondstepsmultiplyoutput) = 2 * (ge_balance_positive_functional_secondstepsmultiplyoutputreal) /\ (ge_balance_negative_functional_secondstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_functional_secondstepsmultiplyoutputrealdecode. (((ge_representation_real_code_functional_secondstepsmultiplyoutput) = 2 * ge_signed_half_functional_secondstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_functional_secondstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_functional_secondstepsmultiplyoutputreal) = S ge_signed_half_functional_secondstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_functional_secondstepsmultiply) * (ge_second_rp_functional_secondstepsmultiply))) + (((ge_first_rn_functional_secondstepsmultiply) * (ge_second_rn_functional_secondstepsmultiply))))) + (((((ge_first_ip_functional_secondstepsmultiply) * (ge_second_in_functional_secondstepsmultiply))) + (((ge_first_in_functional_secondstepsmultiply) * (ge_second_ip_functional_secondstepsmultiply))))))) + ge_balance_negative_functional_secondstepsmultiplyoutputreal = (((((((ge_first_rp_functional_secondstepsmultiply) * (ge_second_rn_functional_secondstepsmultiply))) + (((ge_first_rn_functional_secondstepsmultiply) * (ge_second_rp_functional_secondstepsmultiply))))) + (((((ge_first_ip_functional_secondstepsmultiply) * (ge_second_ip_functional_secondstepsmultiply))) + (((ge_first_in_functional_secondstepsmultiply) * (ge_second_in_functional_secondstepsmultiply))))))) + ge_balance_positive_functional_secondstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_functional_secondstepsmultiplyoutputimaginary ge_balance_negative_functional_secondstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_functional_secondstepsmultiplyoutput) = 2 * (ge_balance_positive_functional_secondstepsmultiplyoutputimaginary) /\ (ge_balance_negative_functional_secondstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_functional_secondstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_functional_secondstepsmultiplyoutput) = 2 * ge_signed_half_functional_secondstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_functional_secondstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_functional_secondstepsmultiplyoutputimaginary) = S ge_signed_half_functional_secondstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_functional_secondstepsmultiply) * (ge_second_ip_functional_secondstepsmultiply))) + (((ge_first_rn_functional_secondstepsmultiply) * (ge_second_in_functional_secondstepsmultiply))))) + (((((ge_first_ip_functional_secondstepsmultiply) * (ge_second_rp_functional_secondstepsmultiply))) + (((ge_first_in_functional_secondstepsmultiply) * (ge_second_rn_functional_secondstepsmultiply))))))) + ge_balance_negative_functional_secondstepsmultiplyoutputimaginary = (((((((ge_first_rp_functional_secondstepsmultiply) * (ge_second_in_functional_secondstepsmultiply))) + (((ge_first_rn_functional_secondstepsmultiply) * (ge_second_ip_functional_secondstepsmultiply))))) + (((((ge_first_ip_functional_secondstepsmultiply) * (ge_second_rn_functional_secondstepsmultiply))) + (((ge_first_in_functional_secondstepsmultiply) * (ge_second_rp_functional_secondstepsmultiply))))))) + ge_balance_positive_functional_secondstepsmultiplyoutputimaginary)))))))))))))))) -> P=Q

Complete tactic proof in conservative notation

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

75 script commands · 11 reading checkpoints · 5 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 (2)
gaussian product empty valuegaussian product successor decompose
01Induction on lL1–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction l
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro P
  5. L5
    intro Q
  6. L6
    intro hP
  7. L7
    intro hQ
  8. L8
    trans 6
  9. L9
    specialize gaussian_product_empty_value (b)
  10. L10
    specialize gaussian_product_empty_value (c)
02Use earlier factsL11–13

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

  1. L11
    specialize gaussian_product_empty_value (P)
  2. L12
    apply gaussian_product_empty_value
  3. L13
    exact hP
03Establish heqL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product empty value.

  1. L14
    have heq : Q=6
  2. L15
    specialize gaussian_product_empty_value (b)
  3. L16
    specialize gaussian_product_empty_value (c)
  4. L17
    specialize gaussian_product_empty_value (Q)
  5. L18
    apply gaussian_product_empty_value
  6. L19
    exact hQ
  7. L20
    symm
  8. L21
    exact heq
  9. L22
    intro b
  10. L23
    intro c
04Fix variables and assumptionsL24–27

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

  1. L24
    intro P
  2. L25
    intro Q
  3. L26
    intro hP
  4. L27
    intro hQ
05Establish hsL28–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product successor decompose.

  1. L28
    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
  2. L29
    specialize gaussian_product_successor_decompose (b)
  3. L30
    specialize gaussian_product_successor_decompose (c)
  4. L31
    specialize gaussian_product_successor_decompose (l)
  5. L32
    specialize gaussian_product_successor_decompose (P)
  6. L33
    apply gaussian_product_successor_decompose
  7. L34
    exact hP
06Separate the logical casesL35–38

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

  1. L35
    cases hs
  2. L36
    cases hs_witness
  3. L37
    cases hs_witness_witness
  4. L38
    cases hs_witness_witness_right
07Establish htL39–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product successor decompose.

  1. L39
    have ht : ∃ a. ∃ R. BetaAt(b,c,l,a) ∧ (GProduct(b,c,l,R) ∧ GMul(R,a,Q))Definitions: BetaAt(b,c,l,a)GProduct(b,c,l,R)GMul(R,a,Q)Original native command in the exact edition
  2. L40
    specialize gaussian_product_successor_decompose (b)
  3. L41
    specialize gaussian_product_successor_decompose (c)
  4. L42
    specialize gaussian_product_successor_decompose (l)
  5. L43
    specialize gaussian_product_successor_decompose (Q)
  6. L44
    apply gaussian_product_successor_decompose
  7. L45
    exact hQ
08Separate the logical casesL46–49

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

  1. L46
    cases ht
  2. L47
    cases ht_witness
  3. L48
    cases ht_witness_witness
  4. L49
    cases ht_witness_witness_right
09Establish hfactorL50–58

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

  1. L50
    have hfactor : x=x2
  2. L51
    specialize beta_at_unique (b)
  3. L52
    specialize beta_at_unique (c)
  4. L53
    specialize beta_at_unique (l)
  5. L54
    specialize beta_at_unique (x)
  6. L55
    specialize beta_at_unique (x2)
  7. L56
    apply beta_at_unique
  8. L57
    exact hs_witness_witness_left
  9. L58
    exact ht_witness_witness_left
10Establish hprefixL59–68

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

  1. L59
    have hprefix : x1=x3
  2. L60
    specialize IH (b)
  3. L61
    specialize IH (c)
  4. L62
    specialize IH (x1)
  5. L63
    specialize IH (x3)
  6. L64
    apply IH
  7. L65
    exact hs_witness_witness_right_left
  8. L66
    exact ht_witness_witness_right_left
  9. L67
    rewrite hfactor at hs_witness_witness_right_right
  10. L68
    rewrite hprefix at hs_witness_witness_right_right
11Use earlier factsL69–75

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

  1. L69
    specialize gaussian_multiply_functional (x3)
  2. L70
    specialize gaussian_multiply_functional (x2)
  3. L71
    specialize gaussian_multiply_functional (P)
  4. L72
    specialize gaussian_multiply_functional (Q)
  5. L73
    apply gaussian_multiply_functional
  6. L74
    exact hs_witness_witness_right_right
  7. L75
    exact ht_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 75 lines
  1. 0001induction l
  2. 0002intro b
  3. 0003intro c
  4. 0004intro P
  5. 0005intro Q
  6. 0006intro hP
  7. 0007intro hQ
  8. 0008trans 6
  9. 0009specialize gaussian_product_empty_value (b)
  10. 0010specialize gaussian_product_empty_value (c)
  11. 0011specialize gaussian_product_empty_value (P)
  12. 0012apply gaussian_product_empty_value
  13. 0013exact hP
  14. 0014have heq : Q=6
  15. 0015specialize gaussian_product_empty_value (b)
  16. 0016specialize gaussian_product_empty_value (c)
  17. 0017specialize gaussian_product_empty_value (Q)
  18. 0018apply gaussian_product_empty_value
  19. 0019exact hQ
  20. 0020symm
  21. 0021exact heq
  22. 0022intro b
  23. 0023intro c
  24. 0024intro P
  25. 0025intro Q
  26. 0026intro hP
  27. 0027intro hQ
  28. 0028have hs : ∃ a. ∃ R. BetaAt(b,c,l,a) ∧ (GProduct(b,c,l,R) ∧ GMul(R,a,P))
  29. 0029specialize gaussian_product_successor_decompose (b)
  30. 0030specialize gaussian_product_successor_decompose (c)
  31. 0031specialize gaussian_product_successor_decompose (l)
  32. 0032specialize gaussian_product_successor_decompose (P)
  33. 0033apply gaussian_product_successor_decompose
  34. 0034exact hP
  35. 0035cases hs
  36. 0036cases hs_witness
  37. 0037cases hs_witness_witness
  38. 0038cases hs_witness_witness_right
  39. 0039have ht : ∃ a. ∃ R. BetaAt(b,c,l,a) ∧ (GProduct(b,c,l,R) ∧ GMul(R,a,Q))
  40. 0040specialize gaussian_product_successor_decompose (b)
  41. 0041specialize gaussian_product_successor_decompose (c)
  42. 0042specialize gaussian_product_successor_decompose (l)
  43. 0043specialize gaussian_product_successor_decompose (Q)
  44. 0044apply gaussian_product_successor_decompose
  45. 0045exact hQ
  46. 0046cases ht
  47. 0047cases ht_witness
  48. 0048cases ht_witness_witness
  49. 0049cases ht_witness_witness_right
  50. 0050have hfactor : x=x2
  51. 0051specialize beta_at_unique (b)
  52. 0052specialize beta_at_unique (c)
  53. 0053specialize beta_at_unique (l)
  54. 0054specialize beta_at_unique (x)
  55. 0055specialize beta_at_unique (x2)
  56. 0056apply beta_at_unique
  57. 0057exact hs_witness_witness_left
  58. 0058exact ht_witness_witness_left
  59. 0059have hprefix : x1=x3
  60. 0060specialize IH (b)
  61. 0061specialize IH (c)
  62. 0062specialize IH (x1)
  63. 0063specialize IH (x3)
  64. 0064apply IH
  65. 0065exact hs_witness_witness_right_left
  66. 0066exact ht_witness_witness_right_left
  67. 0067rewrite hfactor at hs_witness_witness_right_right
  68. 0068rewrite hprefix at hs_witness_witness_right_right
  69. 0069specialize gaussian_multiply_functional (x3)
  70. 0070specialize gaussian_multiply_functional (x2)
  71. 0071specialize gaussian_multiply_functional (P)
  72. 0072specialize gaussian_multiply_functional (Q)
  73. 0073apply gaussian_multiply_functional
  74. 0074exact hs_witness_witness_right_right
  75. 0075exact ht_witness_witness_right_right