GF00A2

gaussian_product_swap_last_invariant

An actual interior/last beta swap preserves the literal canonical value of a genuine Gaussian multiplication trace, without nonzero, irreducibility or unit hypotheses.

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

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

Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ d. ∀ e. ∀ l. ∀ i. ∀ p. ∀ q. ∀ P. ∀ Q. Lt(i,l) → BetaAt(b,c,i,p) ∧ (BetaAt(b,c,l,q) ∧ (BetaAt(d,e,i,q) ∧ (BetaAt(d,e,l,p) ∧ (∀ x. ∀ y. Lt(x,S l) → ¬x = i → ¬x = l → BetaAt(b,c,x,y) → BetaAt(d,e,x,y))))) → GProduct(b,c,S l,P) → GProduct(d,e,S 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) · 4Lt(a,b) · 2BetaAt(b,c,i,x) · 8

Actual proof prerequisites

gaussian_product_successor_decomposebeta_at_unique · checked external prerequisitegaussian_multiply_functional · checked external prerequisitegaussian_product_replace_balancele_succ · checked external prerequisitelt_irrefl_expanded · checked external prerequisite
Original expanded first-order statement 
forall b c d e l i p q P Q. (exists ge_gap_swap_interior. ge_gap_swap_interior + S (i) = (l)) -> (((((exists ff_h_pfp_swap_actual_entriesoldi. ff_h_pfp_swap_actual_entriesoldi + S (p) = S ((S (i)) * c)) /\ exists ff_q_pfp_swap_actual_entriesoldi. b = ff_q_pfp_swap_actual_entriesoldi * S ((S (i)) * c) + (p))) /\ (((((exists ff_h_pfp_swap_actual_entriesoldlast. ff_h_pfp_swap_actual_entriesoldlast + S (q) = S ((S (l)) * c)) /\ exists ff_q_pfp_swap_actual_entriesoldlast. b = ff_q_pfp_swap_actual_entriesoldlast * S ((S (l)) * c) + (q))) /\ (((((exists ff_h_pfp_swap_actual_entriesnewi. ff_h_pfp_swap_actual_entriesnewi + S (q) = S ((S (i)) * e)) /\ exists ff_q_pfp_swap_actual_entriesnewi. d = ff_q_pfp_swap_actual_entriesnewi * S ((S (i)) * e) + (q))) /\ (((((exists ff_h_pfp_swap_actual_entriesnewlast. ff_h_pfp_swap_actual_entriesnewlast + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_swap_actual_entriesnewlast. d = ff_q_pfp_swap_actual_entriesnewlast * S ((S (l)) * e) + (p))) /\ (forall pfp_j_swap_actual_entries pfp_a_swap_actual_entries. (exists pfp_gap_swap_actual_entriesbound. pfp_gap_swap_actual_entriesbound + S (pfp_j_swap_actual_entries) = (S (l))) -> ~(pfp_j_swap_actual_entries = i) -> ~(pfp_j_swap_actual_entries = l) -> (((exists ff_h_pfp_swap_actual_entriesold. ff_h_pfp_swap_actual_entriesold + S (pfp_a_swap_actual_entries) = S ((S (pfp_j_swap_actual_entries)) * c)) /\ exists ff_q_pfp_swap_actual_entriesold. b = ff_q_pfp_swap_actual_entriesold * S ((S (pfp_j_swap_actual_entries)) * c) + (pfp_a_swap_actual_entries))) -> (((exists ff_h_pfp_swap_actual_entriesnew. ff_h_pfp_swap_actual_entriesnew + S (pfp_a_swap_actual_entries) = S ((S (pfp_j_swap_actual_entries)) * e)) /\ exists ff_q_pfp_swap_actual_entriesnew. d = ff_q_pfp_swap_actual_entriesnew * S ((S (pfp_j_swap_actual_entries)) * e) + (pfp_a_swap_actual_entries)))))))))))) -> (exists gr_product_trace_swap_first_product gr_product_scale_swap_first_product. ((((exists ff_h_gprod_swap_first_productstart. ff_h_gprod_swap_first_productstart + S (6) = S ((S (0)) * gr_product_scale_swap_first_product)) /\ exists ff_q_gprod_swap_first_productstart. gr_product_trace_swap_first_product = ff_q_gprod_swap_first_productstart * S ((S (0)) * gr_product_scale_swap_first_product) + (6))) /\ ((((exists ff_h_gprod_swap_first_productend. ff_h_gprod_swap_first_productend + S (P) = S ((S (S l)) * gr_product_scale_swap_first_product)) /\ exists ff_q_gprod_swap_first_productend. gr_product_trace_swap_first_product = ff_q_gprod_swap_first_productend * S ((S (S l)) * gr_product_scale_swap_first_product) + (P))) /\ (forall gr_product_index_swap_first_productsteps. (exists ge_gap_swap_first_productstepsindex_bound. ge_gap_swap_first_productstepsindex_bound + S (gr_product_index_swap_first_productsteps) = (S l)) -> exists gr_product_factor_swap_first_productsteps gr_product_before_swap_first_productsteps gr_product_after_swap_first_productsteps. ((((exists ff_h_gprod_swap_first_productstepsfactor. ff_h_gprod_swap_first_productstepsfactor + S (gr_product_factor_swap_first_productsteps) = S ((S (gr_product_index_swap_first_productsteps)) * c)) /\ exists ff_q_gprod_swap_first_productstepsfactor. b = ff_q_gprod_swap_first_productstepsfactor * S ((S (gr_product_index_swap_first_productsteps)) * c) + (gr_product_factor_swap_first_productsteps))) /\ ((((exists ff_h_gprod_swap_first_productstepsbefore. ff_h_gprod_swap_first_productstepsbefore + S (gr_product_before_swap_first_productsteps) = S ((S (gr_product_index_swap_first_productsteps)) * gr_product_scale_swap_first_product)) /\ exists ff_q_gprod_swap_first_productstepsbefore. gr_product_trace_swap_first_product = ff_q_gprod_swap_first_productstepsbefore * S ((S (gr_product_index_swap_first_productsteps)) * gr_product_scale_swap_first_product) + (gr_product_before_swap_first_productsteps))) /\ ((((exists ff_h_gprod_swap_first_productstepsafter. ff_h_gprod_swap_first_productstepsafter + S (gr_product_after_swap_first_productsteps) = S ((S (S (gr_product_index_swap_first_productsteps))) * gr_product_scale_swap_first_product)) /\ exists ff_q_gprod_swap_first_productstepsafter. gr_product_trace_swap_first_product = ff_q_gprod_swap_first_productstepsafter * S ((S (S (gr_product_index_swap_first_productsteps))) * gr_product_scale_swap_first_product) + (gr_product_after_swap_first_productsteps))) /\ (exists ge_first_rp_swap_first_productstepsmultiply ge_first_rn_swap_first_productstepsmultiply ge_first_ip_swap_first_productstepsmultiply ge_first_in_swap_first_productstepsmultiply ge_second_rp_swap_first_productstepsmultiply ge_second_rn_swap_first_productstepsmultiply ge_second_ip_swap_first_productstepsmultiply ge_second_in_swap_first_productstepsmultiply. ((exists ge_representation_real_code_swap_first_productstepsmultiplyfirst ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst. (((gr_product_before_swap_first_productsteps) = ((ge_representation_real_code_swap_first_productstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst)) * S ((ge_representation_real_code_swap_first_productstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_swap_first_productstepsmultiplyfirstreal ge_balance_negative_swap_first_productstepsmultiplyfirstreal. (((((ge_representation_real_code_swap_first_productstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_first_productstepsmultiplyfirstreal) /\ (ge_balance_negative_swap_first_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_swap_first_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_swap_first_productstepsmultiplyfirst) = 2 * ge_signed_half_swap_first_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_swap_first_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_swap_first_productstepsmultiplyfirstreal) = S ge_signed_half_swap_first_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_swap_first_productstepsmultiply) + ge_balance_negative_swap_first_productstepsmultiplyfirstreal = (ge_first_rn_swap_first_productstepsmultiply) + ge_balance_positive_swap_first_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_swap_first_productstepsmultiplyfirstimaginary ge_balance_negative_swap_first_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_first_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_swap_first_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_swap_first_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_swap_first_productstepsmultiplyfirst) = 2 * ge_signed_half_swap_first_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_first_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_swap_first_productstepsmultiplyfirstimaginary) = S ge_signed_half_swap_first_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_swap_first_productstepsmultiply) + ge_balance_negative_swap_first_productstepsmultiplyfirstimaginary = (ge_first_in_swap_first_productstepsmultiply) + ge_balance_positive_swap_first_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_first_productstepsmultiplysecond ge_representation_imaginary_code_swap_first_productstepsmultiplysecond. (((gr_product_factor_swap_first_productsteps) = ((ge_representation_real_code_swap_first_productstepsmultiplysecond) + (ge_representation_imaginary_code_swap_first_productstepsmultiplysecond)) * S ((ge_representation_real_code_swap_first_productstepsmultiplysecond) + (ge_representation_imaginary_code_swap_first_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_swap_first_productstepsmultiplysecond) + (ge_representation_imaginary_code_swap_first_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_swap_first_productstepsmultiplysecondreal ge_balance_negative_swap_first_productstepsmultiplysecondreal. (((((ge_representation_real_code_swap_first_productstepsmultiplysecond) = 2 * (ge_balance_positive_swap_first_productstepsmultiplysecondreal) /\ (ge_balance_negative_swap_first_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_swap_first_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_swap_first_productstepsmultiplysecond) = 2 * ge_signed_half_swap_first_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_swap_first_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_swap_first_productstepsmultiplysecondreal) = S ge_signed_half_swap_first_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_swap_first_productstepsmultiply) + ge_balance_negative_swap_first_productstepsmultiplysecondreal = (ge_second_rn_swap_first_productstepsmultiply) + ge_balance_positive_swap_first_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_swap_first_productstepsmultiplysecondimaginary ge_balance_negative_swap_first_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_swap_first_productstepsmultiplysecond) = 2 * (ge_balance_positive_swap_first_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_swap_first_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_swap_first_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_swap_first_productstepsmultiplysecond) = 2 * ge_signed_half_swap_first_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_first_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_swap_first_productstepsmultiplysecondimaginary) = S ge_signed_half_swap_first_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_swap_first_productstepsmultiply) + ge_balance_negative_swap_first_productstepsmultiplysecondimaginary = (ge_second_in_swap_first_productstepsmultiply) + ge_balance_positive_swap_first_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_first_productstepsmultiplyoutput ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput. (((gr_product_after_swap_first_productsteps) = ((ge_representation_real_code_swap_first_productstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput)) * S ((ge_representation_real_code_swap_first_productstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_swap_first_productstepsmultiplyoutputreal ge_balance_negative_swap_first_productstepsmultiplyoutputreal. (((((ge_representation_real_code_swap_first_productstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_first_productstepsmultiplyoutputreal) /\ (ge_balance_negative_swap_first_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_swap_first_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_swap_first_productstepsmultiplyoutput) = 2 * ge_signed_half_swap_first_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_swap_first_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_swap_first_productstepsmultiplyoutputreal) = S ge_signed_half_swap_first_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_swap_first_productstepsmultiply) * (ge_second_rp_swap_first_productstepsmultiply))) + (((ge_first_rn_swap_first_productstepsmultiply) * (ge_second_rn_swap_first_productstepsmultiply))))) + (((((ge_first_ip_swap_first_productstepsmultiply) * (ge_second_in_swap_first_productstepsmultiply))) + (((ge_first_in_swap_first_productstepsmultiply) * (ge_second_ip_swap_first_productstepsmultiply))))))) + ge_balance_negative_swap_first_productstepsmultiplyoutputreal = (((((((ge_first_rp_swap_first_productstepsmultiply) * (ge_second_rn_swap_first_productstepsmultiply))) + (((ge_first_rn_swap_first_productstepsmultiply) * (ge_second_rp_swap_first_productstepsmultiply))))) + (((((ge_first_ip_swap_first_productstepsmultiply) * (ge_second_ip_swap_first_productstepsmultiply))) + (((ge_first_in_swap_first_productstepsmultiply) * (ge_second_in_swap_first_productstepsmultiply))))))) + ge_balance_positive_swap_first_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_swap_first_productstepsmultiplyoutputimaginary ge_balance_negative_swap_first_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_first_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_swap_first_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_swap_first_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_swap_first_productstepsmultiplyoutput) = 2 * ge_signed_half_swap_first_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_first_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_swap_first_productstepsmultiplyoutputimaginary) = S ge_signed_half_swap_first_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_first_productstepsmultiply) * (ge_second_ip_swap_first_productstepsmultiply))) + (((ge_first_rn_swap_first_productstepsmultiply) * (ge_second_in_swap_first_productstepsmultiply))))) + (((((ge_first_ip_swap_first_productstepsmultiply) * (ge_second_rp_swap_first_productstepsmultiply))) + (((ge_first_in_swap_first_productstepsmultiply) * (ge_second_rn_swap_first_productstepsmultiply))))))) + ge_balance_negative_swap_first_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_swap_first_productstepsmultiply) * (ge_second_in_swap_first_productstepsmultiply))) + (((ge_first_rn_swap_first_productstepsmultiply) * (ge_second_ip_swap_first_productstepsmultiply))))) + (((((ge_first_ip_swap_first_productstepsmultiply) * (ge_second_rn_swap_first_productstepsmultiply))) + (((ge_first_in_swap_first_productstepsmultiply) * (ge_second_rp_swap_first_productstepsmultiply))))))) + ge_balance_positive_swap_first_productstepsmultiplyoutputimaginary)))))))))))))))) -> (exists gr_product_trace_swap_second_product gr_product_scale_swap_second_product. ((((exists ff_h_gprod_swap_second_productstart. ff_h_gprod_swap_second_productstart + S (6) = S ((S (0)) * gr_product_scale_swap_second_product)) /\ exists ff_q_gprod_swap_second_productstart. gr_product_trace_swap_second_product = ff_q_gprod_swap_second_productstart * S ((S (0)) * gr_product_scale_swap_second_product) + (6))) /\ ((((exists ff_h_gprod_swap_second_productend. ff_h_gprod_swap_second_productend + S (Q) = S ((S (S l)) * gr_product_scale_swap_second_product)) /\ exists ff_q_gprod_swap_second_productend. gr_product_trace_swap_second_product = ff_q_gprod_swap_second_productend * S ((S (S l)) * gr_product_scale_swap_second_product) + (Q))) /\ (forall gr_product_index_swap_second_productsteps. (exists ge_gap_swap_second_productstepsindex_bound. ge_gap_swap_second_productstepsindex_bound + S (gr_product_index_swap_second_productsteps) = (S l)) -> exists gr_product_factor_swap_second_productsteps gr_product_before_swap_second_productsteps gr_product_after_swap_second_productsteps. ((((exists ff_h_gprod_swap_second_productstepsfactor. ff_h_gprod_swap_second_productstepsfactor + S (gr_product_factor_swap_second_productsteps) = S ((S (gr_product_index_swap_second_productsteps)) * e)) /\ exists ff_q_gprod_swap_second_productstepsfactor. d = ff_q_gprod_swap_second_productstepsfactor * S ((S (gr_product_index_swap_second_productsteps)) * e) + (gr_product_factor_swap_second_productsteps))) /\ ((((exists ff_h_gprod_swap_second_productstepsbefore. ff_h_gprod_swap_second_productstepsbefore + S (gr_product_before_swap_second_productsteps) = S ((S (gr_product_index_swap_second_productsteps)) * gr_product_scale_swap_second_product)) /\ exists ff_q_gprod_swap_second_productstepsbefore. gr_product_trace_swap_second_product = ff_q_gprod_swap_second_productstepsbefore * S ((S (gr_product_index_swap_second_productsteps)) * gr_product_scale_swap_second_product) + (gr_product_before_swap_second_productsteps))) /\ ((((exists ff_h_gprod_swap_second_productstepsafter. ff_h_gprod_swap_second_productstepsafter + S (gr_product_after_swap_second_productsteps) = S ((S (S (gr_product_index_swap_second_productsteps))) * gr_product_scale_swap_second_product)) /\ exists ff_q_gprod_swap_second_productstepsafter. gr_product_trace_swap_second_product = ff_q_gprod_swap_second_productstepsafter * S ((S (S (gr_product_index_swap_second_productsteps))) * gr_product_scale_swap_second_product) + (gr_product_after_swap_second_productsteps))) /\ (exists ge_first_rp_swap_second_productstepsmultiply ge_first_rn_swap_second_productstepsmultiply ge_first_ip_swap_second_productstepsmultiply ge_first_in_swap_second_productstepsmultiply ge_second_rp_swap_second_productstepsmultiply ge_second_rn_swap_second_productstepsmultiply ge_second_ip_swap_second_productstepsmultiply ge_second_in_swap_second_productstepsmultiply. ((exists ge_representation_real_code_swap_second_productstepsmultiplyfirst ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst. (((gr_product_before_swap_second_productsteps) = ((ge_representation_real_code_swap_second_productstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst)) * S ((ge_representation_real_code_swap_second_productstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_swap_second_productstepsmultiplyfirstreal ge_balance_negative_swap_second_productstepsmultiplyfirstreal. (((((ge_representation_real_code_swap_second_productstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_second_productstepsmultiplyfirstreal) /\ (ge_balance_negative_swap_second_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_swap_second_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_swap_second_productstepsmultiplyfirst) = 2 * ge_signed_half_swap_second_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_swap_second_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_swap_second_productstepsmultiplyfirstreal) = S ge_signed_half_swap_second_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_swap_second_productstepsmultiply) + ge_balance_negative_swap_second_productstepsmultiplyfirstreal = (ge_first_rn_swap_second_productstepsmultiply) + ge_balance_positive_swap_second_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_swap_second_productstepsmultiplyfirstimaginary ge_balance_negative_swap_second_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_second_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_swap_second_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_swap_second_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_swap_second_productstepsmultiplyfirst) = 2 * ge_signed_half_swap_second_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_second_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_swap_second_productstepsmultiplyfirstimaginary) = S ge_signed_half_swap_second_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_swap_second_productstepsmultiply) + ge_balance_negative_swap_second_productstepsmultiplyfirstimaginary = (ge_first_in_swap_second_productstepsmultiply) + ge_balance_positive_swap_second_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_second_productstepsmultiplysecond ge_representation_imaginary_code_swap_second_productstepsmultiplysecond. (((gr_product_factor_swap_second_productsteps) = ((ge_representation_real_code_swap_second_productstepsmultiplysecond) + (ge_representation_imaginary_code_swap_second_productstepsmultiplysecond)) * S ((ge_representation_real_code_swap_second_productstepsmultiplysecond) + (ge_representation_imaginary_code_swap_second_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_swap_second_productstepsmultiplysecond) + (ge_representation_imaginary_code_swap_second_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_swap_second_productstepsmultiplysecondreal ge_balance_negative_swap_second_productstepsmultiplysecondreal. (((((ge_representation_real_code_swap_second_productstepsmultiplysecond) = 2 * (ge_balance_positive_swap_second_productstepsmultiplysecondreal) /\ (ge_balance_negative_swap_second_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_swap_second_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_swap_second_productstepsmultiplysecond) = 2 * ge_signed_half_swap_second_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_swap_second_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_swap_second_productstepsmultiplysecondreal) = S ge_signed_half_swap_second_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_swap_second_productstepsmultiply) + ge_balance_negative_swap_second_productstepsmultiplysecondreal = (ge_second_rn_swap_second_productstepsmultiply) + ge_balance_positive_swap_second_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_swap_second_productstepsmultiplysecondimaginary ge_balance_negative_swap_second_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_swap_second_productstepsmultiplysecond) = 2 * (ge_balance_positive_swap_second_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_swap_second_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_swap_second_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_swap_second_productstepsmultiplysecond) = 2 * ge_signed_half_swap_second_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_second_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_swap_second_productstepsmultiplysecondimaginary) = S ge_signed_half_swap_second_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_swap_second_productstepsmultiply) + ge_balance_negative_swap_second_productstepsmultiplysecondimaginary = (ge_second_in_swap_second_productstepsmultiply) + ge_balance_positive_swap_second_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_second_productstepsmultiplyoutput ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput. (((gr_product_after_swap_second_productsteps) = ((ge_representation_real_code_swap_second_productstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput)) * S ((ge_representation_real_code_swap_second_productstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_swap_second_productstepsmultiplyoutputreal ge_balance_negative_swap_second_productstepsmultiplyoutputreal. (((((ge_representation_real_code_swap_second_productstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_second_productstepsmultiplyoutputreal) /\ (ge_balance_negative_swap_second_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_swap_second_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_swap_second_productstepsmultiplyoutput) = 2 * ge_signed_half_swap_second_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_swap_second_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_swap_second_productstepsmultiplyoutputreal) = S ge_signed_half_swap_second_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_swap_second_productstepsmultiply) * (ge_second_rp_swap_second_productstepsmultiply))) + (((ge_first_rn_swap_second_productstepsmultiply) * (ge_second_rn_swap_second_productstepsmultiply))))) + (((((ge_first_ip_swap_second_productstepsmultiply) * (ge_second_in_swap_second_productstepsmultiply))) + (((ge_first_in_swap_second_productstepsmultiply) * (ge_second_ip_swap_second_productstepsmultiply))))))) + ge_balance_negative_swap_second_productstepsmultiplyoutputreal = (((((((ge_first_rp_swap_second_productstepsmultiply) * (ge_second_rn_swap_second_productstepsmultiply))) + (((ge_first_rn_swap_second_productstepsmultiply) * (ge_second_rp_swap_second_productstepsmultiply))))) + (((((ge_first_ip_swap_second_productstepsmultiply) * (ge_second_ip_swap_second_productstepsmultiply))) + (((ge_first_in_swap_second_productstepsmultiply) * (ge_second_in_swap_second_productstepsmultiply))))))) + ge_balance_positive_swap_second_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_swap_second_productstepsmultiplyoutputimaginary ge_balance_negative_swap_second_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_second_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_swap_second_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_swap_second_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_swap_second_productstepsmultiplyoutput) = 2 * ge_signed_half_swap_second_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_second_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_swap_second_productstepsmultiplyoutputimaginary) = S ge_signed_half_swap_second_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_second_productstepsmultiply) * (ge_second_ip_swap_second_productstepsmultiply))) + (((ge_first_rn_swap_second_productstepsmultiply) * (ge_second_in_swap_second_productstepsmultiply))))) + (((((ge_first_ip_swap_second_productstepsmultiply) * (ge_second_rp_swap_second_productstepsmultiply))) + (((ge_first_in_swap_second_productstepsmultiply) * (ge_second_rn_swap_second_productstepsmultiply))))))) + ge_balance_negative_swap_second_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_swap_second_productstepsmultiply) * (ge_second_in_swap_second_productstepsmultiply))) + (((ge_first_rn_swap_second_productstepsmultiply) * (ge_second_ip_swap_second_productstepsmultiply))))) + (((((ge_first_ip_swap_second_productstepsmultiply) * (ge_second_rn_swap_second_productstepsmultiply))) + (((ge_first_in_swap_second_productstepsmultiply) * (ge_second_rp_swap_second_productstepsmultiply))))))) + ge_balance_positive_swap_second_productstepsmultiplyoutputimaginary)))))))))))))))) -> P=Q

Complete tactic proof in conservative notation

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

103 script commands · 18 reading checkpoints · 4 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 successor decomposegaussian product replace balance
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro l
  6. L6
    intro i
  7. L7
    intro p
  8. L8
    intro q
  9. L9
    intro P
  10. L10
    intro Q
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hi
  2. L12
    intro hswap
  3. L13
    intro hP
  4. L14
    intro hQ
03Separate the logical casesL15–18

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

  1. L15
    cases hswap
  2. L16
    cases hswap_right
  3. L17
    cases hswap_right_right
  4. L18
    cases hswap_right_right_right
04Establish holdL19–25

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

  1. L19
    have hold : ∃ 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. L20
    specialize gaussian_product_successor_decompose (b)
  3. L21
    specialize gaussian_product_successor_decompose (c)
  4. L22
    specialize gaussian_product_successor_decompose (l)
  5. L23
    specialize gaussian_product_successor_decompose (P)
  6. L24
    apply gaussian_product_successor_decompose
  7. L25
    exact hP
05Establish hnewL26–32

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

  1. L26
    have hnew : ∃ a. ∃ R. BetaAt(d,e,l,a) ∧ (GProduct(d,e,l,R) ∧ GMul(R,a,Q))Definitions: BetaAt(d,e,l,a)GProduct(d,e,l,R)GMul(R,a,Q)Original native command in the exact edition
  2. L27
    specialize gaussian_product_successor_decompose (d)
  3. L28
    specialize gaussian_product_successor_decompose (e)
  4. L29
    specialize gaussian_product_successor_decompose (l)
  5. L30
    specialize gaussian_product_successor_decompose (Q)
  6. L31
    apply gaussian_product_successor_decompose
  7. L32
    exact hQ
06Separate the logical casesL33–40

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

  1. L33
    cases hold
  2. L34
    cases hold_witness
  3. L35
    cases hold_witness_witness
  4. L36
    cases hold_witness_witness_right
  5. L37
    cases hnew
  6. L38
    cases hnew_witness
  7. L39
    cases hnew_witness_witness
  8. L40
    cases hnew_witness_witness_right
07Establish hlastoldL41–49

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

  1. L41
    have hlastold : x=q
  2. L42
    specialize beta_at_unique (b)
  3. L43
    specialize beta_at_unique (c)
  4. L44
    specialize beta_at_unique (l)
  5. L45
    specialize beta_at_unique (x)
  6. L46
    specialize beta_at_unique (q)
  7. L47
    apply beta_at_unique
  8. L48
    exact hold_witness_witness_left
  9. L49
    exact hswap_right_left
08Establish hlastnewL50–59

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

  1. L50
    have hlastnew : x2=p
  2. L51
    specialize beta_at_unique (d)
  3. L52
    specialize beta_at_unique (e)
  4. L53
    specialize beta_at_unique (l)
  5. L54
    specialize beta_at_unique (x2)
  6. L55
    specialize beta_at_unique (p)
  7. L56
    apply beta_at_unique
  8. L57
    exact hnew_witness_witness_left
  9. L58
    exact hswap_right_right_right_left
  10. L59
    rewrite hlastold at hold_witness_witness_right_right
09Calculate and transport equalitiesL60–60

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L60
    rewrite hlastnew at hnew_witness_witness_right_right
10Use earlier factsL61–70

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

  1. L61
    specialize gaussian_multiply_functional (x1)
  2. L62
    specialize gaussian_multiply_functional (q)
  3. L63
    specialize gaussian_multiply_functional (P)
  4. L64
    specialize gaussian_multiply_functional (Q)
  5. L65
    apply gaussian_multiply_functional
  6. L66
    exact hold_witness_witness_right_right
  7. L67
    specialize gaussian_product_replace_balance (l)
  8. L68
    specialize gaussian_product_replace_balance (b)
  9. L69
    specialize gaussian_product_replace_balance (c)
  10. L70
    specialize gaussian_product_replace_balance (d)
11Use earlier factsL71–80

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

  1. L71
    specialize gaussian_product_replace_balance (e)
  2. L72
    specialize gaussian_product_replace_balance (i)
  3. L73
    specialize gaussian_product_replace_balance (p)
  4. L74
    specialize gaussian_product_replace_balance (q)
  5. L75
    specialize gaussian_product_replace_balance (x1)
  6. L76
    specialize gaussian_product_replace_balance (x3)
  7. L77
    specialize gaussian_product_replace_balance (Q)
  8. L78
    apply gaussian_product_replace_balance
  9. L79
    exact hi
  10. L80
    exact hswap_left
12Use earlier factsL81–81

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

  1. L81
    exact hswap_right_right_left
13Fix variables and assumptionsL82–86

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

  1. L82
    intro j
  2. L83
    intro a
  3. L84
    intro hj
  4. L85
    intro hne
  5. L86
    intro hentry
14Use earlier factsL87–94

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

  1. L87
    specialize hswap_right_right_right_right (j)
  2. L88
    specialize hswap_right_right_right_right (a)
  3. L89
    apply hswap_right_right_right_right
  4. L90
    specialize le_succ (S j)
  5. L91
    specialize le_succ (l)
  6. L92
    apply le_succ
  7. L93
    exact hj
  8. L94
    exact hne
15Fix variables and assumptionsL95–95

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

  1. L95
    intro heq
16Use earlier factsL96–97

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

  1. L96
    specialize lt_irrefl_expanded (l)
  2. L97
    apply lt_irrefl_expanded
17Calculate and transport equalitiesL98–98

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L98
    rewrite heq at hj
18Use earlier factsL99–103

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

  1. L99
    exact hj
  2. L100
    exact hentry
  3. L101
    exact hold_witness_witness_right_left
  4. L102
    exact hnew_witness_witness_right_left
  5. L103
    exact hnew_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 103 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro l
  6. 0006intro i
  7. 0007intro p
  8. 0008intro q
  9. 0009intro P
  10. 0010intro Q
  11. 0011intro hi
  12. 0012intro hswap
  13. 0013intro hP
  14. 0014intro hQ
  15. 0015cases hswap
  16. 0016cases hswap_right
  17. 0017cases hswap_right_right
  18. 0018cases hswap_right_right_right
  19. 0019have hold : ∃ a. ∃ R. BetaAt(b,c,l,a) ∧ (GProduct(b,c,l,R) ∧ GMul(R,a,P))
  20. 0020specialize gaussian_product_successor_decompose (b)
  21. 0021specialize gaussian_product_successor_decompose (c)
  22. 0022specialize gaussian_product_successor_decompose (l)
  23. 0023specialize gaussian_product_successor_decompose (P)
  24. 0024apply gaussian_product_successor_decompose
  25. 0025exact hP
  26. 0026have hnew : ∃ a. ∃ R. BetaAt(d,e,l,a) ∧ (GProduct(d,e,l,R) ∧ GMul(R,a,Q))
  27. 0027specialize gaussian_product_successor_decompose (d)
  28. 0028specialize gaussian_product_successor_decompose (e)
  29. 0029specialize gaussian_product_successor_decompose (l)
  30. 0030specialize gaussian_product_successor_decompose (Q)
  31. 0031apply gaussian_product_successor_decompose
  32. 0032exact hQ
  33. 0033cases hold
  34. 0034cases hold_witness
  35. 0035cases hold_witness_witness
  36. 0036cases hold_witness_witness_right
  37. 0037cases hnew
  38. 0038cases hnew_witness
  39. 0039cases hnew_witness_witness
  40. 0040cases hnew_witness_witness_right
  41. 0041have hlastold : x=q
  42. 0042specialize beta_at_unique (b)
  43. 0043specialize beta_at_unique (c)
  44. 0044specialize beta_at_unique (l)
  45. 0045specialize beta_at_unique (x)
  46. 0046specialize beta_at_unique (q)
  47. 0047apply beta_at_unique
  48. 0048exact hold_witness_witness_left
  49. 0049exact hswap_right_left
  50. 0050have hlastnew : x2=p
  51. 0051specialize beta_at_unique (d)
  52. 0052specialize beta_at_unique (e)
  53. 0053specialize beta_at_unique (l)
  54. 0054specialize beta_at_unique (x2)
  55. 0055specialize beta_at_unique (p)
  56. 0056apply beta_at_unique
  57. 0057exact hnew_witness_witness_left
  58. 0058exact hswap_right_right_right_left
  59. 0059rewrite hlastold at hold_witness_witness_right_right
  60. 0060rewrite hlastnew at hnew_witness_witness_right_right
  61. 0061specialize gaussian_multiply_functional (x1)
  62. 0062specialize gaussian_multiply_functional (q)
  63. 0063specialize gaussian_multiply_functional (P)
  64. 0064specialize gaussian_multiply_functional (Q)
  65. 0065apply gaussian_multiply_functional
  66. 0066exact hold_witness_witness_right_right
  67. 0067specialize gaussian_product_replace_balance (l)
  68. 0068specialize gaussian_product_replace_balance (b)
  69. 0069specialize gaussian_product_replace_balance (c)
  70. 0070specialize gaussian_product_replace_balance (d)
  71. 0071specialize gaussian_product_replace_balance (e)
  72. 0072specialize gaussian_product_replace_balance (i)
  73. 0073specialize gaussian_product_replace_balance (p)
  74. 0074specialize gaussian_product_replace_balance (q)
  75. 0075specialize gaussian_product_replace_balance (x1)
  76. 0076specialize gaussian_product_replace_balance (x3)
  77. 0077specialize gaussian_product_replace_balance (Q)
  78. 0078apply gaussian_product_replace_balance
  79. 0079exact hi
  80. 0080exact hswap_left
  81. 0081exact hswap_right_right_left
  82. 0082intro j
  83. 0083intro a
  84. 0084intro hj
  85. 0085intro hne
  86. 0086intro hentry
  87. 0087specialize hswap_right_right_right_right (j)
  88. 0088specialize hswap_right_right_right_right (a)
  89. 0089apply hswap_right_right_right_right
  90. 0090specialize le_succ (S j)
  91. 0091specialize le_succ (l)
  92. 0092apply le_succ
  93. 0093exact hj
  94. 0094exact hne
  95. 0095intro heq
  96. 0096specialize lt_irrefl_expanded (l)
  97. 0097apply lt_irrefl_expanded
  98. 0098rewrite heq at hj
  99. 0099exact hj
  100. 0100exact hentry
  101. 0101exact hold_witness_witness_right_left
  102. 0102exact hnew_witness_witness_right_left
  103. 0103exact hnew_witness_witness_right_right