GF008A

gaussian_product_successor_intro

Append a genuine Gaussian multiplication step using a constructed beta extension of the product trace, preserving all previous steps.

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

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

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

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ l. ∀ P. ∀ a. ∀ Q. GProduct(b,c,l,P) → BetaAt(b,c,l,a) → GMul(P,a,Q) → GProduct(b,c,S l,Q)

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

Definition DAG

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

Actual proof prerequisites

beta_prefix_extend · checked external prerequisitesucc_le_succ · checked external prerequisitezero_le · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisitegaussian_product_beta_index_transportle_refl · checked external prerequisitelt_of_lt_of_le · checked external prerequisitele_succ_self · checked external prerequisite
Original expanded first-order statement 
forall b c l P a Q. (exists gr_product_trace_append_product_before gr_product_scale_append_product_before. ((((exists ff_h_gprod_append_product_beforestart. ff_h_gprod_append_product_beforestart + S (6) = S ((S (0)) * gr_product_scale_append_product_before)) /\ exists ff_q_gprod_append_product_beforestart. gr_product_trace_append_product_before = ff_q_gprod_append_product_beforestart * S ((S (0)) * gr_product_scale_append_product_before) + (6))) /\ ((((exists ff_h_gprod_append_product_beforeend. ff_h_gprod_append_product_beforeend + S (P) = S ((S (l)) * gr_product_scale_append_product_before)) /\ exists ff_q_gprod_append_product_beforeend. gr_product_trace_append_product_before = ff_q_gprod_append_product_beforeend * S ((S (l)) * gr_product_scale_append_product_before) + (P))) /\ (forall gr_product_index_append_product_beforesteps. (exists ge_gap_append_product_beforestepsindex_bound. ge_gap_append_product_beforestepsindex_bound + S (gr_product_index_append_product_beforesteps) = (l)) -> exists gr_product_factor_append_product_beforesteps gr_product_before_append_product_beforesteps gr_product_after_append_product_beforesteps. ((((exists ff_h_gprod_append_product_beforestepsfactor. ff_h_gprod_append_product_beforestepsfactor + S (gr_product_factor_append_product_beforesteps) = S ((S (gr_product_index_append_product_beforesteps)) * c)) /\ exists ff_q_gprod_append_product_beforestepsfactor. b = ff_q_gprod_append_product_beforestepsfactor * S ((S (gr_product_index_append_product_beforesteps)) * c) + (gr_product_factor_append_product_beforesteps))) /\ ((((exists ff_h_gprod_append_product_beforestepsbefore. ff_h_gprod_append_product_beforestepsbefore + S (gr_product_before_append_product_beforesteps) = S ((S (gr_product_index_append_product_beforesteps)) * gr_product_scale_append_product_before)) /\ exists ff_q_gprod_append_product_beforestepsbefore. gr_product_trace_append_product_before = ff_q_gprod_append_product_beforestepsbefore * S ((S (gr_product_index_append_product_beforesteps)) * gr_product_scale_append_product_before) + (gr_product_before_append_product_beforesteps))) /\ ((((exists ff_h_gprod_append_product_beforestepsafter. ff_h_gprod_append_product_beforestepsafter + S (gr_product_after_append_product_beforesteps) = S ((S (S (gr_product_index_append_product_beforesteps))) * gr_product_scale_append_product_before)) /\ exists ff_q_gprod_append_product_beforestepsafter. gr_product_trace_append_product_before = ff_q_gprod_append_product_beforestepsafter * S ((S (S (gr_product_index_append_product_beforesteps))) * gr_product_scale_append_product_before) + (gr_product_after_append_product_beforesteps))) /\ (exists ge_first_rp_append_product_beforestepsmultiply ge_first_rn_append_product_beforestepsmultiply ge_first_ip_append_product_beforestepsmultiply ge_first_in_append_product_beforestepsmultiply ge_second_rp_append_product_beforestepsmultiply ge_second_rn_append_product_beforestepsmultiply ge_second_ip_append_product_beforestepsmultiply ge_second_in_append_product_beforestepsmultiply. ((exists ge_representation_real_code_append_product_beforestepsmultiplyfirst ge_representation_imaginary_code_append_product_beforestepsmultiplyfirst. (((gr_product_before_append_product_beforesteps) = ((ge_representation_real_code_append_product_beforestepsmultiplyfirst) + (ge_representation_imaginary_code_append_product_beforestepsmultiplyfirst)) * S ((ge_representation_real_code_append_product_beforestepsmultiplyfirst) + (ge_representation_imaginary_code_append_product_beforestepsmultiplyfirst)) + ((ge_representation_imaginary_code_append_product_beforestepsmultiplyfirst) + (ge_representation_imaginary_code_append_product_beforestepsmultiplyfirst))) /\ ((exists ge_balance_positive_append_product_beforestepsmultiplyfirstreal ge_balance_negative_append_product_beforestepsmultiplyfirstreal. (((((ge_representation_real_code_append_product_beforestepsmultiplyfirst) = 2 * (ge_balance_positive_append_product_beforestepsmultiplyfirstreal) /\ (ge_balance_negative_append_product_beforestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_append_product_beforestepsmultiplyfirstrealdecode. (((ge_representation_real_code_append_product_beforestepsmultiplyfirst) = 2 * ge_signed_half_append_product_beforestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_append_product_beforestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_append_product_beforestepsmultiplyfirstreal) = S ge_signed_half_append_product_beforestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_append_product_beforestepsmultiply) + ge_balance_negative_append_product_beforestepsmultiplyfirstreal = (ge_first_rn_append_product_beforestepsmultiply) + ge_balance_positive_append_product_beforestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_append_product_beforestepsmultiplyfirstimaginary ge_balance_negative_append_product_beforestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_append_product_beforestepsmultiplyfirst) = 2 * (ge_balance_positive_append_product_beforestepsmultiplyfirstimaginary) /\ (ge_balance_negative_append_product_beforestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_append_product_beforestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_append_product_beforestepsmultiplyfirst) = 2 * ge_signed_half_append_product_beforestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_append_product_beforestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_append_product_beforestepsmultiplyfirstimaginary) = S ge_signed_half_append_product_beforestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_append_product_beforestepsmultiply) + ge_balance_negative_append_product_beforestepsmultiplyfirstimaginary = (ge_first_in_append_product_beforestepsmultiply) + ge_balance_positive_append_product_beforestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_product_beforestepsmultiplysecond ge_representation_imaginary_code_append_product_beforestepsmultiplysecond. (((gr_product_factor_append_product_beforesteps) = ((ge_representation_real_code_append_product_beforestepsmultiplysecond) + (ge_representation_imaginary_code_append_product_beforestepsmultiplysecond)) * S ((ge_representation_real_code_append_product_beforestepsmultiplysecond) + (ge_representation_imaginary_code_append_product_beforestepsmultiplysecond)) + ((ge_representation_imaginary_code_append_product_beforestepsmultiplysecond) + (ge_representation_imaginary_code_append_product_beforestepsmultiplysecond))) /\ ((exists ge_balance_positive_append_product_beforestepsmultiplysecondreal ge_balance_negative_append_product_beforestepsmultiplysecondreal. (((((ge_representation_real_code_append_product_beforestepsmultiplysecond) = 2 * (ge_balance_positive_append_product_beforestepsmultiplysecondreal) /\ (ge_balance_negative_append_product_beforestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_append_product_beforestepsmultiplysecondrealdecode. (((ge_representation_real_code_append_product_beforestepsmultiplysecond) = 2 * ge_signed_half_append_product_beforestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_append_product_beforestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_append_product_beforestepsmultiplysecondreal) = S ge_signed_half_append_product_beforestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_append_product_beforestepsmultiply) + ge_balance_negative_append_product_beforestepsmultiplysecondreal = (ge_second_rn_append_product_beforestepsmultiply) + ge_balance_positive_append_product_beforestepsmultiplysecondreal))) /\ (exists ge_balance_positive_append_product_beforestepsmultiplysecondimaginary ge_balance_negative_append_product_beforestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_append_product_beforestepsmultiplysecond) = 2 * (ge_balance_positive_append_product_beforestepsmultiplysecondimaginary) /\ (ge_balance_negative_append_product_beforestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_append_product_beforestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_append_product_beforestepsmultiplysecond) = 2 * ge_signed_half_append_product_beforestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_append_product_beforestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_append_product_beforestepsmultiplysecondimaginary) = S ge_signed_half_append_product_beforestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_append_product_beforestepsmultiply) + ge_balance_negative_append_product_beforestepsmultiplysecondimaginary = (ge_second_in_append_product_beforestepsmultiply) + ge_balance_positive_append_product_beforestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_append_product_beforestepsmultiplyoutput ge_representation_imaginary_code_append_product_beforestepsmultiplyoutput. (((gr_product_after_append_product_beforesteps) = ((ge_representation_real_code_append_product_beforestepsmultiplyoutput) + (ge_representation_imaginary_code_append_product_beforestepsmultiplyoutput)) * S ((ge_representation_real_code_append_product_beforestepsmultiplyoutput) + (ge_representation_imaginary_code_append_product_beforestepsmultiplyoutput)) + ((ge_representation_imaginary_code_append_product_beforestepsmultiplyoutput) + (ge_representation_imaginary_code_append_product_beforestepsmultiplyoutput))) /\ ((exists ge_balance_positive_append_product_beforestepsmultiplyoutputreal ge_balance_negative_append_product_beforestepsmultiplyoutputreal. (((((ge_representation_real_code_append_product_beforestepsmultiplyoutput) = 2 * (ge_balance_positive_append_product_beforestepsmultiplyoutputreal) /\ (ge_balance_negative_append_product_beforestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_append_product_beforestepsmultiplyoutputrealdecode. (((ge_representation_real_code_append_product_beforestepsmultiplyoutput) = 2 * ge_signed_half_append_product_beforestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_append_product_beforestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_append_product_beforestepsmultiplyoutputreal) = S ge_signed_half_append_product_beforestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_append_product_beforestepsmultiply) * (ge_second_rp_append_product_beforestepsmultiply))) + (((ge_first_rn_append_product_beforestepsmultiply) * (ge_second_rn_append_product_beforestepsmultiply))))) + (((((ge_first_ip_append_product_beforestepsmultiply) * (ge_second_in_append_product_beforestepsmultiply))) + (((ge_first_in_append_product_beforestepsmultiply) * (ge_second_ip_append_product_beforestepsmultiply))))))) + ge_balance_negative_append_product_beforestepsmultiplyoutputreal = (((((((ge_first_rp_append_product_beforestepsmultiply) * (ge_second_rn_append_product_beforestepsmultiply))) + (((ge_first_rn_append_product_beforestepsmultiply) * (ge_second_rp_append_product_beforestepsmultiply))))) + (((((ge_first_ip_append_product_beforestepsmultiply) * (ge_second_ip_append_product_beforestepsmultiply))) + (((ge_first_in_append_product_beforestepsmultiply) * (ge_second_in_append_product_beforestepsmultiply))))))) + ge_balance_positive_append_product_beforestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_append_product_beforestepsmultiplyoutputimaginary ge_balance_negative_append_product_beforestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_append_product_beforestepsmultiplyoutput) = 2 * (ge_balance_positive_append_product_beforestepsmultiplyoutputimaginary) /\ (ge_balance_negative_append_product_beforestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_append_product_beforestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_append_product_beforestepsmultiplyoutput) = 2 * ge_signed_half_append_product_beforestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_append_product_beforestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_append_product_beforestepsmultiplyoutputimaginary) = S ge_signed_half_append_product_beforestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_product_beforestepsmultiply) * (ge_second_ip_append_product_beforestepsmultiply))) + (((ge_first_rn_append_product_beforestepsmultiply) * (ge_second_in_append_product_beforestepsmultiply))))) + (((((ge_first_ip_append_product_beforestepsmultiply) * (ge_second_rp_append_product_beforestepsmultiply))) + (((ge_first_in_append_product_beforestepsmultiply) * (ge_second_rn_append_product_beforestepsmultiply))))))) + ge_balance_negative_append_product_beforestepsmultiplyoutputimaginary = (((((((ge_first_rp_append_product_beforestepsmultiply) * (ge_second_in_append_product_beforestepsmultiply))) + (((ge_first_rn_append_product_beforestepsmultiply) * (ge_second_ip_append_product_beforestepsmultiply))))) + (((((ge_first_ip_append_product_beforestepsmultiply) * (ge_second_rn_append_product_beforestepsmultiply))) + (((ge_first_in_append_product_beforestepsmultiply) * (ge_second_rp_append_product_beforestepsmultiply))))))) + ge_balance_positive_append_product_beforestepsmultiplyoutputimaginary)))))))))))))))) -> (((exists ff_h_gprod_append_factor. ff_h_gprod_append_factor + S (a) = S ((S (l)) * c)) /\ exists ff_q_gprod_append_factor. b = ff_q_gprod_append_factor * S ((S (l)) * c) + (a))) -> (exists ge_first_rp_append_multiply ge_first_rn_append_multiply ge_first_ip_append_multiply ge_first_in_append_multiply ge_second_rp_append_multiply ge_second_rn_append_multiply ge_second_ip_append_multiply ge_second_in_append_multiply. ((exists ge_representation_real_code_append_multiplyfirst ge_representation_imaginary_code_append_multiplyfirst. (((P) = ((ge_representation_real_code_append_multiplyfirst) + (ge_representation_imaginary_code_append_multiplyfirst)) * S ((ge_representation_real_code_append_multiplyfirst) + (ge_representation_imaginary_code_append_multiplyfirst)) + ((ge_representation_imaginary_code_append_multiplyfirst) + (ge_representation_imaginary_code_append_multiplyfirst))) /\ ((exists ge_balance_positive_append_multiplyfirstreal ge_balance_negative_append_multiplyfirstreal. (((((ge_representation_real_code_append_multiplyfirst) = 2 * (ge_balance_positive_append_multiplyfirstreal) /\ (ge_balance_negative_append_multiplyfirstreal) = 0) \/ exists ge_signed_half_append_multiplyfirstrealdecode. (((ge_representation_real_code_append_multiplyfirst) = 2 * ge_signed_half_append_multiplyfirstrealdecode + 1 /\ (ge_balance_positive_append_multiplyfirstreal) = 0) /\ (ge_balance_negative_append_multiplyfirstreal) = S ge_signed_half_append_multiplyfirstrealdecode))) /\ ((ge_first_rp_append_multiply) + ge_balance_negative_append_multiplyfirstreal = (ge_first_rn_append_multiply) + ge_balance_positive_append_multiplyfirstreal))) /\ (exists ge_balance_positive_append_multiplyfirstimaginary ge_balance_negative_append_multiplyfirstimaginary. (((((ge_representation_imaginary_code_append_multiplyfirst) = 2 * (ge_balance_positive_append_multiplyfirstimaginary) /\ (ge_balance_negative_append_multiplyfirstimaginary) = 0) \/ exists ge_signed_half_append_multiplyfirstimaginarydecode. (((ge_representation_imaginary_code_append_multiplyfirst) = 2 * ge_signed_half_append_multiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_append_multiplyfirstimaginary) = 0) /\ (ge_balance_negative_append_multiplyfirstimaginary) = S ge_signed_half_append_multiplyfirstimaginarydecode))) /\ ((ge_first_ip_append_multiply) + ge_balance_negative_append_multiplyfirstimaginary = (ge_first_in_append_multiply) + ge_balance_positive_append_multiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_multiplysecond ge_representation_imaginary_code_append_multiplysecond. (((a) = ((ge_representation_real_code_append_multiplysecond) + (ge_representation_imaginary_code_append_multiplysecond)) * S ((ge_representation_real_code_append_multiplysecond) + (ge_representation_imaginary_code_append_multiplysecond)) + ((ge_representation_imaginary_code_append_multiplysecond) + (ge_representation_imaginary_code_append_multiplysecond))) /\ ((exists ge_balance_positive_append_multiplysecondreal ge_balance_negative_append_multiplysecondreal. (((((ge_representation_real_code_append_multiplysecond) = 2 * (ge_balance_positive_append_multiplysecondreal) /\ (ge_balance_negative_append_multiplysecondreal) = 0) \/ exists ge_signed_half_append_multiplysecondrealdecode. (((ge_representation_real_code_append_multiplysecond) = 2 * ge_signed_half_append_multiplysecondrealdecode + 1 /\ (ge_balance_positive_append_multiplysecondreal) = 0) /\ (ge_balance_negative_append_multiplysecondreal) = S ge_signed_half_append_multiplysecondrealdecode))) /\ ((ge_second_rp_append_multiply) + ge_balance_negative_append_multiplysecondreal = (ge_second_rn_append_multiply) + ge_balance_positive_append_multiplysecondreal))) /\ (exists ge_balance_positive_append_multiplysecondimaginary ge_balance_negative_append_multiplysecondimaginary. (((((ge_representation_imaginary_code_append_multiplysecond) = 2 * (ge_balance_positive_append_multiplysecondimaginary) /\ (ge_balance_negative_append_multiplysecondimaginary) = 0) \/ exists ge_signed_half_append_multiplysecondimaginarydecode. (((ge_representation_imaginary_code_append_multiplysecond) = 2 * ge_signed_half_append_multiplysecondimaginarydecode + 1 /\ (ge_balance_positive_append_multiplysecondimaginary) = 0) /\ (ge_balance_negative_append_multiplysecondimaginary) = S ge_signed_half_append_multiplysecondimaginarydecode))) /\ ((ge_second_ip_append_multiply) + ge_balance_negative_append_multiplysecondimaginary = (ge_second_in_append_multiply) + ge_balance_positive_append_multiplysecondimaginary)))))) /\ (exists ge_representation_real_code_append_multiplyoutput ge_representation_imaginary_code_append_multiplyoutput. (((Q) = ((ge_representation_real_code_append_multiplyoutput) + (ge_representation_imaginary_code_append_multiplyoutput)) * S ((ge_representation_real_code_append_multiplyoutput) + (ge_representation_imaginary_code_append_multiplyoutput)) + ((ge_representation_imaginary_code_append_multiplyoutput) + (ge_representation_imaginary_code_append_multiplyoutput))) /\ ((exists ge_balance_positive_append_multiplyoutputreal ge_balance_negative_append_multiplyoutputreal. (((((ge_representation_real_code_append_multiplyoutput) = 2 * (ge_balance_positive_append_multiplyoutputreal) /\ (ge_balance_negative_append_multiplyoutputreal) = 0) \/ exists ge_signed_half_append_multiplyoutputrealdecode. (((ge_representation_real_code_append_multiplyoutput) = 2 * ge_signed_half_append_multiplyoutputrealdecode + 1 /\ (ge_balance_positive_append_multiplyoutputreal) = 0) /\ (ge_balance_negative_append_multiplyoutputreal) = S ge_signed_half_append_multiplyoutputrealdecode))) /\ ((((((((ge_first_rp_append_multiply) * (ge_second_rp_append_multiply))) + (((ge_first_rn_append_multiply) * (ge_second_rn_append_multiply))))) + (((((ge_first_ip_append_multiply) * (ge_second_in_append_multiply))) + (((ge_first_in_append_multiply) * (ge_second_ip_append_multiply))))))) + ge_balance_negative_append_multiplyoutputreal = (((((((ge_first_rp_append_multiply) * (ge_second_rn_append_multiply))) + (((ge_first_rn_append_multiply) * (ge_second_rp_append_multiply))))) + (((((ge_first_ip_append_multiply) * (ge_second_ip_append_multiply))) + (((ge_first_in_append_multiply) * (ge_second_in_append_multiply))))))) + ge_balance_positive_append_multiplyoutputreal))) /\ (exists ge_balance_positive_append_multiplyoutputimaginary ge_balance_negative_append_multiplyoutputimaginary. (((((ge_representation_imaginary_code_append_multiplyoutput) = 2 * (ge_balance_positive_append_multiplyoutputimaginary) /\ (ge_balance_negative_append_multiplyoutputimaginary) = 0) \/ exists ge_signed_half_append_multiplyoutputimaginarydecode. (((ge_representation_imaginary_code_append_multiplyoutput) = 2 * ge_signed_half_append_multiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_append_multiplyoutputimaginary) = 0) /\ (ge_balance_negative_append_multiplyoutputimaginary) = S ge_signed_half_append_multiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_multiply) * (ge_second_ip_append_multiply))) + (((ge_first_rn_append_multiply) * (ge_second_in_append_multiply))))) + (((((ge_first_ip_append_multiply) * (ge_second_rp_append_multiply))) + (((ge_first_in_append_multiply) * (ge_second_rn_append_multiply))))))) + ge_balance_negative_append_multiplyoutputimaginary = (((((((ge_first_rp_append_multiply) * (ge_second_in_append_multiply))) + (((ge_first_rn_append_multiply) * (ge_second_ip_append_multiply))))) + (((((ge_first_ip_append_multiply) * (ge_second_rn_append_multiply))) + (((ge_first_in_append_multiply) * (ge_second_rp_append_multiply))))))) + ge_balance_positive_append_multiplyoutputimaginary))))))))) -> (exists gr_product_trace_append_product_after gr_product_scale_append_product_after. ((((exists ff_h_gprod_append_product_afterstart. ff_h_gprod_append_product_afterstart + S (6) = S ((S (0)) * gr_product_scale_append_product_after)) /\ exists ff_q_gprod_append_product_afterstart. gr_product_trace_append_product_after = ff_q_gprod_append_product_afterstart * S ((S (0)) * gr_product_scale_append_product_after) + (6))) /\ ((((exists ff_h_gprod_append_product_afterend. ff_h_gprod_append_product_afterend + S (Q) = S ((S (S l)) * gr_product_scale_append_product_after)) /\ exists ff_q_gprod_append_product_afterend. gr_product_trace_append_product_after = ff_q_gprod_append_product_afterend * S ((S (S l)) * gr_product_scale_append_product_after) + (Q))) /\ (forall gr_product_index_append_product_aftersteps. (exists ge_gap_append_product_afterstepsindex_bound. ge_gap_append_product_afterstepsindex_bound + S (gr_product_index_append_product_aftersteps) = (S l)) -> exists gr_product_factor_append_product_aftersteps gr_product_before_append_product_aftersteps gr_product_after_append_product_aftersteps. ((((exists ff_h_gprod_append_product_afterstepsfactor. ff_h_gprod_append_product_afterstepsfactor + S (gr_product_factor_append_product_aftersteps) = S ((S (gr_product_index_append_product_aftersteps)) * c)) /\ exists ff_q_gprod_append_product_afterstepsfactor. b = ff_q_gprod_append_product_afterstepsfactor * S ((S (gr_product_index_append_product_aftersteps)) * c) + (gr_product_factor_append_product_aftersteps))) /\ ((((exists ff_h_gprod_append_product_afterstepsbefore. ff_h_gprod_append_product_afterstepsbefore + S (gr_product_before_append_product_aftersteps) = S ((S (gr_product_index_append_product_aftersteps)) * gr_product_scale_append_product_after)) /\ exists ff_q_gprod_append_product_afterstepsbefore. gr_product_trace_append_product_after = ff_q_gprod_append_product_afterstepsbefore * S ((S (gr_product_index_append_product_aftersteps)) * gr_product_scale_append_product_after) + (gr_product_before_append_product_aftersteps))) /\ ((((exists ff_h_gprod_append_product_afterstepsafter. ff_h_gprod_append_product_afterstepsafter + S (gr_product_after_append_product_aftersteps) = S ((S (S (gr_product_index_append_product_aftersteps))) * gr_product_scale_append_product_after)) /\ exists ff_q_gprod_append_product_afterstepsafter. gr_product_trace_append_product_after = ff_q_gprod_append_product_afterstepsafter * S ((S (S (gr_product_index_append_product_aftersteps))) * gr_product_scale_append_product_after) + (gr_product_after_append_product_aftersteps))) /\ (exists ge_first_rp_append_product_afterstepsmultiply ge_first_rn_append_product_afterstepsmultiply ge_first_ip_append_product_afterstepsmultiply ge_first_in_append_product_afterstepsmultiply ge_second_rp_append_product_afterstepsmultiply ge_second_rn_append_product_afterstepsmultiply ge_second_ip_append_product_afterstepsmultiply ge_second_in_append_product_afterstepsmultiply. ((exists ge_representation_real_code_append_product_afterstepsmultiplyfirst ge_representation_imaginary_code_append_product_afterstepsmultiplyfirst. (((gr_product_before_append_product_aftersteps) = ((ge_representation_real_code_append_product_afterstepsmultiplyfirst) + (ge_representation_imaginary_code_append_product_afterstepsmultiplyfirst)) * S ((ge_representation_real_code_append_product_afterstepsmultiplyfirst) + (ge_representation_imaginary_code_append_product_afterstepsmultiplyfirst)) + ((ge_representation_imaginary_code_append_product_afterstepsmultiplyfirst) + (ge_representation_imaginary_code_append_product_afterstepsmultiplyfirst))) /\ ((exists ge_balance_positive_append_product_afterstepsmultiplyfirstreal ge_balance_negative_append_product_afterstepsmultiplyfirstreal. (((((ge_representation_real_code_append_product_afterstepsmultiplyfirst) = 2 * (ge_balance_positive_append_product_afterstepsmultiplyfirstreal) /\ (ge_balance_negative_append_product_afterstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_append_product_afterstepsmultiplyfirstrealdecode. (((ge_representation_real_code_append_product_afterstepsmultiplyfirst) = 2 * ge_signed_half_append_product_afterstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_append_product_afterstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_append_product_afterstepsmultiplyfirstreal) = S ge_signed_half_append_product_afterstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_append_product_afterstepsmultiply) + ge_balance_negative_append_product_afterstepsmultiplyfirstreal = (ge_first_rn_append_product_afterstepsmultiply) + ge_balance_positive_append_product_afterstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_append_product_afterstepsmultiplyfirstimaginary ge_balance_negative_append_product_afterstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_append_product_afterstepsmultiplyfirst) = 2 * (ge_balance_positive_append_product_afterstepsmultiplyfirstimaginary) /\ (ge_balance_negative_append_product_afterstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_append_product_afterstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_append_product_afterstepsmultiplyfirst) = 2 * ge_signed_half_append_product_afterstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_append_product_afterstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_append_product_afterstepsmultiplyfirstimaginary) = S ge_signed_half_append_product_afterstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_append_product_afterstepsmultiply) + ge_balance_negative_append_product_afterstepsmultiplyfirstimaginary = (ge_first_in_append_product_afterstepsmultiply) + ge_balance_positive_append_product_afterstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_product_afterstepsmultiplysecond ge_representation_imaginary_code_append_product_afterstepsmultiplysecond. (((gr_product_factor_append_product_aftersteps) = ((ge_representation_real_code_append_product_afterstepsmultiplysecond) + (ge_representation_imaginary_code_append_product_afterstepsmultiplysecond)) * S ((ge_representation_real_code_append_product_afterstepsmultiplysecond) + (ge_representation_imaginary_code_append_product_afterstepsmultiplysecond)) + ((ge_representation_imaginary_code_append_product_afterstepsmultiplysecond) + (ge_representation_imaginary_code_append_product_afterstepsmultiplysecond))) /\ ((exists ge_balance_positive_append_product_afterstepsmultiplysecondreal ge_balance_negative_append_product_afterstepsmultiplysecondreal. (((((ge_representation_real_code_append_product_afterstepsmultiplysecond) = 2 * (ge_balance_positive_append_product_afterstepsmultiplysecondreal) /\ (ge_balance_negative_append_product_afterstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_append_product_afterstepsmultiplysecondrealdecode. (((ge_representation_real_code_append_product_afterstepsmultiplysecond) = 2 * ge_signed_half_append_product_afterstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_append_product_afterstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_append_product_afterstepsmultiplysecondreal) = S ge_signed_half_append_product_afterstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_append_product_afterstepsmultiply) + ge_balance_negative_append_product_afterstepsmultiplysecondreal = (ge_second_rn_append_product_afterstepsmultiply) + ge_balance_positive_append_product_afterstepsmultiplysecondreal))) /\ (exists ge_balance_positive_append_product_afterstepsmultiplysecondimaginary ge_balance_negative_append_product_afterstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_append_product_afterstepsmultiplysecond) = 2 * (ge_balance_positive_append_product_afterstepsmultiplysecondimaginary) /\ (ge_balance_negative_append_product_afterstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_append_product_afterstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_append_product_afterstepsmultiplysecond) = 2 * ge_signed_half_append_product_afterstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_append_product_afterstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_append_product_afterstepsmultiplysecondimaginary) = S ge_signed_half_append_product_afterstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_append_product_afterstepsmultiply) + ge_balance_negative_append_product_afterstepsmultiplysecondimaginary = (ge_second_in_append_product_afterstepsmultiply) + ge_balance_positive_append_product_afterstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_append_product_afterstepsmultiplyoutput ge_representation_imaginary_code_append_product_afterstepsmultiplyoutput. (((gr_product_after_append_product_aftersteps) = ((ge_representation_real_code_append_product_afterstepsmultiplyoutput) + (ge_representation_imaginary_code_append_product_afterstepsmultiplyoutput)) * S ((ge_representation_real_code_append_product_afterstepsmultiplyoutput) + (ge_representation_imaginary_code_append_product_afterstepsmultiplyoutput)) + ((ge_representation_imaginary_code_append_product_afterstepsmultiplyoutput) + (ge_representation_imaginary_code_append_product_afterstepsmultiplyoutput))) /\ ((exists ge_balance_positive_append_product_afterstepsmultiplyoutputreal ge_balance_negative_append_product_afterstepsmultiplyoutputreal. (((((ge_representation_real_code_append_product_afterstepsmultiplyoutput) = 2 * (ge_balance_positive_append_product_afterstepsmultiplyoutputreal) /\ (ge_balance_negative_append_product_afterstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_append_product_afterstepsmultiplyoutputrealdecode. (((ge_representation_real_code_append_product_afterstepsmultiplyoutput) = 2 * ge_signed_half_append_product_afterstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_append_product_afterstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_append_product_afterstepsmultiplyoutputreal) = S ge_signed_half_append_product_afterstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_append_product_afterstepsmultiply) * (ge_second_rp_append_product_afterstepsmultiply))) + (((ge_first_rn_append_product_afterstepsmultiply) * (ge_second_rn_append_product_afterstepsmultiply))))) + (((((ge_first_ip_append_product_afterstepsmultiply) * (ge_second_in_append_product_afterstepsmultiply))) + (((ge_first_in_append_product_afterstepsmultiply) * (ge_second_ip_append_product_afterstepsmultiply))))))) + ge_balance_negative_append_product_afterstepsmultiplyoutputreal = (((((((ge_first_rp_append_product_afterstepsmultiply) * (ge_second_rn_append_product_afterstepsmultiply))) + (((ge_first_rn_append_product_afterstepsmultiply) * (ge_second_rp_append_product_afterstepsmultiply))))) + (((((ge_first_ip_append_product_afterstepsmultiply) * (ge_second_ip_append_product_afterstepsmultiply))) + (((ge_first_in_append_product_afterstepsmultiply) * (ge_second_in_append_product_afterstepsmultiply))))))) + ge_balance_positive_append_product_afterstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_append_product_afterstepsmultiplyoutputimaginary ge_balance_negative_append_product_afterstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_append_product_afterstepsmultiplyoutput) = 2 * (ge_balance_positive_append_product_afterstepsmultiplyoutputimaginary) /\ (ge_balance_negative_append_product_afterstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_append_product_afterstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_append_product_afterstepsmultiplyoutput) = 2 * ge_signed_half_append_product_afterstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_append_product_afterstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_append_product_afterstepsmultiplyoutputimaginary) = S ge_signed_half_append_product_afterstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_product_afterstepsmultiply) * (ge_second_ip_append_product_afterstepsmultiply))) + (((ge_first_rn_append_product_afterstepsmultiply) * (ge_second_in_append_product_afterstepsmultiply))))) + (((((ge_first_ip_append_product_afterstepsmultiply) * (ge_second_rp_append_product_afterstepsmultiply))) + (((ge_first_in_append_product_afterstepsmultiply) * (ge_second_rn_append_product_afterstepsmultiply))))))) + ge_balance_negative_append_product_afterstepsmultiplyoutputimaginary = (((((((ge_first_rp_append_product_afterstepsmultiply) * (ge_second_in_append_product_afterstepsmultiply))) + (((ge_first_rn_append_product_afterstepsmultiply) * (ge_second_ip_append_product_afterstepsmultiply))))) + (((((ge_first_ip_append_product_afterstepsmultiply) * (ge_second_rn_append_product_afterstepsmultiply))) + (((ge_first_in_append_product_afterstepsmultiply) * (ge_second_rp_append_product_afterstepsmultiply))))))) + ge_balance_positive_append_product_afterstepsmultiplyoutputimaginary))))))))))))))))

Complete tactic proof in conservative notation

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

123 script commands · 36 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 (1)
gaussian product beta index transport
01Fix variables and assumptionsL1–9

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro P
  5. L5
    intro a
  6. L6
    intro Q
  7. L7
    intro hp
  8. L8
    intro ha
  9. L9
    intro hm
02Separate the logical casesL10–13

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

  1. L10
    cases hp
  2. L11
    cases hp_witness
  3. L12
    cases hp_witness_witness
  4. L13
    cases hp_witness_witness_right
03Establish hextL14–19

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

  1. L14
    have hext : ∃ h. ∃ e. BetaAt(h,e,S l,Q) ∧ (∀ y. ∀ z. Lt(y,S l) → BetaAt(x,x1,y,z) → BetaAt(h,e,y,z))Definitions: BetaAt(h,e,S l,Q)Lt(y,S l)BetaAt(x,x1,y,z)BetaAt(h,e,y,z)Original native command in the exact edition
  2. L15
    specialize beta_prefix_extend (S l)
  3. L16
    specialize beta_prefix_extend (x)
  4. L17
    specialize beta_prefix_extend (x1)
  5. L18
    specialize beta_prefix_extend (Q)
  6. L19
    apply beta_prefix_extend
04Separate the logical casesL20–22

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

  1. L20
    cases hext
  2. L21
    cases hext_witness
  3. L22
    cases hext_witness_witness
05Establish hlastL23–29

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

  1. L23
    have hlast : BetaAt(x2,x3,l,P)Definitions: BetaAt(x2,x3,l,P)Original native command in the exact edition
  2. L24
    specialize hext_witness_witness_right (l)
  3. L25
    specialize hext_witness_witness_right (P)
  4. L26
    apply hext_witness_witness_right
  5. L27
    specialize le_refl (S l)
  6. L28
    apply le_refl
  7. L29
    exact hp_witness_witness_right_left
06Construct an explicit witnessL30–31

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

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

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

  1. L32
    split
08Use earlier factsL33–41

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

  1. L33
    specialize hext_witness_witness_right (0)
  2. L34
    specialize hext_witness_witness_right (6)
  3. L35
    apply hext_witness_witness_right
  4. L36
    specialize succ_le_succ (0)
  5. L37
    specialize succ_le_succ (l)
  6. L38
    apply succ_le_succ
  7. L39
    specialize zero_le (l)
  8. L40
    apply zero_le
  9. L41
    exact hp_witness_witness_left
09Separate the logical casesL42–42

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

  1. L42
    split
10Use earlier factsL43–43

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

  1. L43
    exact hext_witness_witness_left
11Fix variables and assumptionsL44–45

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

  1. L44
    intro i
  2. L45
    intro hi
12Establish hcL46–50

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L46
    have hc : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L47
    specialize finite_lt_succ_eq_or_lt (l)
  3. L48
    specialize finite_lt_succ_eq_or_lt (i)
  4. L49
    apply finite_lt_succ_eq_or_lt
  5. L50
    exact hi
13Separate the logical casesL51–51

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

  1. L51
    cases hc
14Construct an explicit witnessL52–54

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

  1. L52
    exists (a)
  2. L53
    exists (P)
  3. L54
    exists (Q)
15Separate the logical casesL55–55

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

  1. L55
    split
16Use earlier factsL56–61

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

  1. L56
    specialize gaussian_product_beta_index_transport (b)
  2. L57
    specialize gaussian_product_beta_index_transport (c)
  3. L58
    specialize gaussian_product_beta_index_transport (l)
  4. L59
    specialize gaussian_product_beta_index_transport (i)
  5. L60
    specialize gaussian_product_beta_index_transport (a)
  6. L61
    apply gaussian_product_beta_index_transport
17Calculate and transport equalitiesL62–62

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

  1. L62
    symm
18Use earlier factsL63–64

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

  1. L63
    exact hc_left
  2. L64
    exact ha
19Separate the logical casesL65–65

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

  1. L65
    split
20Use earlier factsL66–71

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

  1. L66
    specialize gaussian_product_beta_index_transport (x2)
  2. L67
    specialize gaussian_product_beta_index_transport (x3)
  3. L68
    specialize gaussian_product_beta_index_transport (l)
  4. L69
    specialize gaussian_product_beta_index_transport (i)
  5. L70
    specialize gaussian_product_beta_index_transport (P)
  6. L71
    apply gaussian_product_beta_index_transport
21Calculate and transport equalitiesL72–72

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

  1. L72
    symm
22Use earlier factsL73–74

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

  1. L73
    exact hc_left
  2. L74
    exact hlast
23Separate the logical casesL75–75

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

  1. L75
    split
24Use earlier factsL76–81

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

  1. L76
    specialize gaussian_product_beta_index_transport (x2)
  2. L77
    specialize gaussian_product_beta_index_transport (x3)
  3. L78
    specialize gaussian_product_beta_index_transport (S l)
  4. L79
    specialize gaussian_product_beta_index_transport (S i)
  5. L80
    specialize gaussian_product_beta_index_transport (Q)
  6. L81
    apply gaussian_product_beta_index_transport
25Calculate and transport equalitiesL82–83

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

  1. L82
    congr
  2. L83
    symm
26Use earlier factsL84–86

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

  1. L84
    exact hc_left
  2. L85
    exact hext_witness_witness_left
  3. L86
    exact hm
27Establish hsL87–90

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

  1. L87
    have hs : GProductStep(b,c,x,x1,i)Definitions: GProductStep(b,c,x,x1,i)Original native command in the exact edition
  2. L88
    specialize hp_witness_witness_right_right (i)
  3. L89
    apply hp_witness_witness_right_right
  4. L90
    exact hc_right
28Separate the logical casesL91–96

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

  1. L91
    cases hs
  2. L92
    cases hs_witness
  3. L93
    cases hs_witness_witness
  4. L94
    cases hs_witness_witness_witness
  5. L95
    cases hs_witness_witness_witness_right
  6. L96
    cases hs_witness_witness_witness_right_right
29Construct an explicit witnessL97–99

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

  1. L97
    exists (x4)
  2. L98
    exists (x5)
  3. L99
    exists (x6)
30Separate the logical casesL100–100

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

  1. L100
    split
31Use earlier factsL101–101

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

  1. L101
    exact hs_witness_witness_witness_left
32Separate the logical casesL102–102

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

  1. L102
    split
33Use earlier factsL103–112

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

  1. L103
    specialize hext_witness_witness_right (i)
  2. L104
    specialize hext_witness_witness_right (x5)
  3. L105
    apply hext_witness_witness_right
  4. L106
    specialize lt_of_lt_of_le (i)
  5. L107
    specialize lt_of_lt_of_le (l)
  6. L108
    specialize lt_of_lt_of_le (S l)
  7. L109
    apply lt_of_lt_of_le
  8. L110
    exact hc_right
  9. L111
    specialize le_succ_self (l)
  10. L112
    apply le_succ_self
34Use earlier factsL113–113

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

  1. L113
    exact hs_witness_witness_witness_right_left
35Separate the logical casesL114–114

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

  1. L114
    split
36Use earlier factsL115–123

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

  1. L115
    specialize hext_witness_witness_right (S i)
  2. L116
    specialize hext_witness_witness_right (x6)
  3. L117
    apply hext_witness_witness_right
  4. L118
    specialize succ_le_succ (S i)
  5. L119
    specialize succ_le_succ (l)
  6. L120
    apply succ_le_succ
  7. L121
    exact hc_right
  8. L122
    exact hs_witness_witness_witness_right_right_left
  9. L123
    exact hs_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 123 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro P
  5. 0005intro a
  6. 0006intro Q
  7. 0007intro hp
  8. 0008intro ha
  9. 0009intro hm
  10. 0010cases hp
  11. 0011cases hp_witness
  12. 0012cases hp_witness_witness
  13. 0013cases hp_witness_witness_right
  14. 0014have hext : ∃ h. ∃ e. BetaAt(h,e,S l,Q) ∧ (∀ y. ∀ z. Lt(y,S l) → BetaAt(x,x1,y,z) → BetaAt(h,e,y,z))
  15. 0015specialize beta_prefix_extend (S l)
  16. 0016specialize beta_prefix_extend (x)
  17. 0017specialize beta_prefix_extend (x1)
  18. 0018specialize beta_prefix_extend (Q)
  19. 0019apply beta_prefix_extend
  20. 0020cases hext
  21. 0021cases hext_witness
  22. 0022cases hext_witness_witness
  23. 0023have hlast : BetaAt(x2,x3,l,P)
  24. 0024specialize hext_witness_witness_right (l)
  25. 0025specialize hext_witness_witness_right (P)
  26. 0026apply hext_witness_witness_right
  27. 0027specialize le_refl (S l)
  28. 0028apply le_refl
  29. 0029exact hp_witness_witness_right_left
  30. 0030exists (x2)
  31. 0031exists (x3)
  32. 0032split
  33. 0033specialize hext_witness_witness_right (0)
  34. 0034specialize hext_witness_witness_right (6)
  35. 0035apply hext_witness_witness_right
  36. 0036specialize succ_le_succ (0)
  37. 0037specialize succ_le_succ (l)
  38. 0038apply succ_le_succ
  39. 0039specialize zero_le (l)
  40. 0040apply zero_le
  41. 0041exact hp_witness_witness_left
  42. 0042split
  43. 0043exact hext_witness_witness_left
  44. 0044intro i
  45. 0045intro hi
  46. 0046have hc : i = l ∨ Lt(i,l)
  47. 0047specialize finite_lt_succ_eq_or_lt (l)
  48. 0048specialize finite_lt_succ_eq_or_lt (i)
  49. 0049apply finite_lt_succ_eq_or_lt
  50. 0050exact hi
  51. 0051cases hc
  52. 0052exists (a)
  53. 0053exists (P)
  54. 0054exists (Q)
  55. 0055split
  56. 0056specialize gaussian_product_beta_index_transport (b)
  57. 0057specialize gaussian_product_beta_index_transport (c)
  58. 0058specialize gaussian_product_beta_index_transport (l)
  59. 0059specialize gaussian_product_beta_index_transport (i)
  60. 0060specialize gaussian_product_beta_index_transport (a)
  61. 0061apply gaussian_product_beta_index_transport
  62. 0062symm
  63. 0063exact hc_left
  64. 0064exact ha
  65. 0065split
  66. 0066specialize gaussian_product_beta_index_transport (x2)
  67. 0067specialize gaussian_product_beta_index_transport (x3)
  68. 0068specialize gaussian_product_beta_index_transport (l)
  69. 0069specialize gaussian_product_beta_index_transport (i)
  70. 0070specialize gaussian_product_beta_index_transport (P)
  71. 0071apply gaussian_product_beta_index_transport
  72. 0072symm
  73. 0073exact hc_left
  74. 0074exact hlast
  75. 0075split
  76. 0076specialize gaussian_product_beta_index_transport (x2)
  77. 0077specialize gaussian_product_beta_index_transport (x3)
  78. 0078specialize gaussian_product_beta_index_transport (S l)
  79. 0079specialize gaussian_product_beta_index_transport (S i)
  80. 0080specialize gaussian_product_beta_index_transport (Q)
  81. 0081apply gaussian_product_beta_index_transport
  82. 0082congr
  83. 0083symm
  84. 0084exact hc_left
  85. 0085exact hext_witness_witness_left
  86. 0086exact hm
  87. 0087have hs : GProductStep(b,c,x,x1,i)
  88. 0088specialize hp_witness_witness_right_right (i)
  89. 0089apply hp_witness_witness_right_right
  90. 0090exact hc_right
  91. 0091cases hs
  92. 0092cases hs_witness
  93. 0093cases hs_witness_witness
  94. 0094cases hs_witness_witness_witness
  95. 0095cases hs_witness_witness_witness_right
  96. 0096cases hs_witness_witness_witness_right_right
  97. 0097exists (x4)
  98. 0098exists (x5)
  99. 0099exists (x6)
  100. 0100split
  101. 0101exact hs_witness_witness_witness_left
  102. 0102split
  103. 0103specialize hext_witness_witness_right (i)
  104. 0104specialize hext_witness_witness_right (x5)
  105. 0105apply hext_witness_witness_right
  106. 0106specialize lt_of_lt_of_le (i)
  107. 0107specialize lt_of_lt_of_le (l)
  108. 0108specialize lt_of_lt_of_le (S l)
  109. 0109apply lt_of_lt_of_le
  110. 0110exact hc_right
  111. 0111specialize le_succ_self (l)
  112. 0112apply le_succ_self
  113. 0113exact hs_witness_witness_witness_right_left
  114. 0114split
  115. 0115specialize hext_witness_witness_right (S i)
  116. 0116specialize hext_witness_witness_right (x6)
  117. 0117apply hext_witness_witness_right
  118. 0118specialize succ_le_succ (S i)
  119. 0119specialize succ_le_succ (l)
  120. 0120apply succ_le_succ
  121. 0121exact hc_right
  122. 0122exact hs_witness_witness_witness_right_right_left
  123. 0123exact hs_witness_witness_witness_right_right_right