EL0010

euclidean_gcd_execution_logarithmic_bound

Exact G101: every witnessed BitLen(b,l) yields a genuine gcd-anchored Euclidean beta execution with steps <= 2*l+1 in unchanged constructive HA.

Alpha v34 checked-use · first admitted v23 · 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.

The exact G101 milestone is fully proved, including the stronger checked bound k≤2·BitLen(b), a real beta-coded execution, and its actual terminal gcd. The independent T13 determinant/rank/integer-span substrate is now closed in the separate Alpha-v27 integer-linear-algebra branch. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ l. BitLen(b,l) → ∃ x. ∃ y. EuclideanAnchoredExecution(a,b,x,y) ∧ Le(y,2 · l + 1)

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

Definition DAG

BitLen(n,ell) · 1EuclideanAnchoredExecution(a,b,g,k) · 1Le(a,b) · 1

Actual proof prerequisites

euclidean_log_execution_strongle_succ · checked external prerequisitetwo_mul_eq_add_self · checked external prerequisite
Original expanded first-order statement 
forall a b l. ((((b) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_elb_length ff_lower_bl_elb_length ff_upper_bl_elb_length. (((l) = S ff_exponent_bl_elb_length) /\ ((exists ff_positive_bl_elb_length. ff_positive_bl_elb_length + 1 = (b)) /\ ((exists pa_b_bl_elb_length_lower pa_c_bl_elb_length_lower. ((forall pa_i_bl_elb_length_lower_repeat. (exists pa_lt_bl_elb_length_lower_repeat_bound. pa_lt_bl_elb_length_lower_repeat_bound + S pa_i_bl_elb_length_lower_repeat = ff_exponent_bl_elb_length) -> (((exists pa_h_bl_elb_length_lower_repeat_decoded. pa_h_bl_elb_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_elb_length_lower_repeat)) * pa_c_bl_elb_length_lower)) /\ exists pa_q_bl_elb_length_lower_repeat_decoded. pa_b_bl_elb_length_lower = pa_q_bl_elb_length_lower_repeat_decoded * S ((S (pa_i_bl_elb_length_lower_repeat)) * pa_c_bl_elb_length_lower) + (2)))) /\ (exists pa_u_bl_elb_length_lower_product pa_v_bl_elb_length_lower_product. ((((exists pa_h_bl_elb_length_lower_product_start. pa_h_bl_elb_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_start. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_start * S ((S (0)) * pa_v_bl_elb_length_lower_product) + (1))) /\ ((((exists pa_h_bl_elb_length_lower_product_terminal. pa_h_bl_elb_length_lower_product_terminal + S (ff_lower_bl_elb_length) = S ((S (ff_exponent_bl_elb_length)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_terminal. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_terminal * S ((S (ff_exponent_bl_elb_length)) * pa_v_bl_elb_length_lower_product) + (ff_lower_bl_elb_length))) /\ forall pa_i_bl_elb_length_lower_product. (exists pa_lt_bl_elb_length_lower_product_bound. pa_lt_bl_elb_length_lower_product_bound + S pa_i_bl_elb_length_lower_product = ff_exponent_bl_elb_length) -> exists pa_p_bl_elb_length_lower_product pa_r_bl_elb_length_lower_product pa_s_bl_elb_length_lower_product. ((((exists pa_h_bl_elb_length_lower_product_factor. pa_h_bl_elb_length_lower_product_factor + S (pa_p_bl_elb_length_lower_product) = S ((S (pa_i_bl_elb_length_lower_product)) * pa_c_bl_elb_length_lower)) /\ exists pa_q_bl_elb_length_lower_product_factor. pa_b_bl_elb_length_lower = pa_q_bl_elb_length_lower_product_factor * S ((S (pa_i_bl_elb_length_lower_product)) * pa_c_bl_elb_length_lower) + (pa_p_bl_elb_length_lower_product))) /\ ((((exists pa_h_bl_elb_length_lower_product_partial. pa_h_bl_elb_length_lower_product_partial + S (pa_r_bl_elb_length_lower_product) = S ((S (pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_partial. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_partial * S ((S (pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product) + (pa_r_bl_elb_length_lower_product))) /\ ((((exists pa_h_bl_elb_length_lower_product_successor. pa_h_bl_elb_length_lower_product_successor + S (pa_s_bl_elb_length_lower_product) = S ((S (S pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_successor. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_successor * S ((S (S pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product) + (pa_s_bl_elb_length_lower_product))) /\ pa_s_bl_elb_length_lower_product = pa_r_bl_elb_length_lower_product * pa_p_bl_elb_length_lower_product)))))))) /\ ((exists pa_b_bl_elb_length_upper pa_c_bl_elb_length_upper. ((forall pa_i_bl_elb_length_upper_repeat. (exists pa_lt_bl_elb_length_upper_repeat_bound. pa_lt_bl_elb_length_upper_repeat_bound + S pa_i_bl_elb_length_upper_repeat = l) -> (((exists pa_h_bl_elb_length_upper_repeat_decoded. pa_h_bl_elb_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_elb_length_upper_repeat)) * pa_c_bl_elb_length_upper)) /\ exists pa_q_bl_elb_length_upper_repeat_decoded. pa_b_bl_elb_length_upper = pa_q_bl_elb_length_upper_repeat_decoded * S ((S (pa_i_bl_elb_length_upper_repeat)) * pa_c_bl_elb_length_upper) + (2)))) /\ (exists pa_u_bl_elb_length_upper_product pa_v_bl_elb_length_upper_product. ((((exists pa_h_bl_elb_length_upper_product_start. pa_h_bl_elb_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_start. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_start * S ((S (0)) * pa_v_bl_elb_length_upper_product) + (1))) /\ ((((exists pa_h_bl_elb_length_upper_product_terminal. pa_h_bl_elb_length_upper_product_terminal + S (ff_upper_bl_elb_length) = S ((S (l)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_terminal. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_terminal * S ((S (l)) * pa_v_bl_elb_length_upper_product) + (ff_upper_bl_elb_length))) /\ forall pa_i_bl_elb_length_upper_product. (exists pa_lt_bl_elb_length_upper_product_bound. pa_lt_bl_elb_length_upper_product_bound + S pa_i_bl_elb_length_upper_product = l) -> exists pa_p_bl_elb_length_upper_product pa_r_bl_elb_length_upper_product pa_s_bl_elb_length_upper_product. ((((exists pa_h_bl_elb_length_upper_product_factor. pa_h_bl_elb_length_upper_product_factor + S (pa_p_bl_elb_length_upper_product) = S ((S (pa_i_bl_elb_length_upper_product)) * pa_c_bl_elb_length_upper)) /\ exists pa_q_bl_elb_length_upper_product_factor. pa_b_bl_elb_length_upper = pa_q_bl_elb_length_upper_product_factor * S ((S (pa_i_bl_elb_length_upper_product)) * pa_c_bl_elb_length_upper) + (pa_p_bl_elb_length_upper_product))) /\ ((((exists pa_h_bl_elb_length_upper_product_partial. pa_h_bl_elb_length_upper_product_partial + S (pa_r_bl_elb_length_upper_product) = S ((S (pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_partial. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_partial * S ((S (pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product) + (pa_r_bl_elb_length_upper_product))) /\ ((((exists pa_h_bl_elb_length_upper_product_successor. pa_h_bl_elb_length_upper_product_successor + S (pa_s_bl_elb_length_upper_product) = S ((S (S pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_successor. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_successor * S ((S (S pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product) + (pa_s_bl_elb_length_upper_product))) /\ pa_s_bl_elb_length_upper_product = pa_r_bl_elb_length_upper_product * pa_p_bl_elb_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_elb_length. ff_lower_gap_bl_elb_length + (ff_lower_bl_elb_length) = (b)) /\ (exists ff_upper_gap_bl_elb_length. ff_upper_gap_bl_elb_length + S (b) = (ff_upper_bl_elb_length))))))))) -> exists g k. ((exists egt_list_elb_anchored egt_history_elb_anchored egt_scale_elb_anchored. ((exists cf_gcd_egt_elb_anchored_trace. ((((exists ff_h_cf_egt_elb_anchored_trace_initial_state. ff_h_cf_egt_elb_anchored_trace_initial_state + S (((cf_gcd_egt_elb_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_elb_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * egt_scale_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_trace_initial_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_trace_initial_state * S ((S (0)) * egt_scale_elb_anchored) + (((cf_gcd_egt_elb_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_elb_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_egt_elb_anchored_trace_terminal_state. ff_h_cf_egt_elb_anchored_trace_terminal_state + S (((a) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored)))) * S ((a) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored)))) + ((((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored))) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored))))) = S ((S (k)) * egt_scale_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_trace_terminal_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_trace_terminal_state * S ((S (k)) * egt_scale_elb_anchored) + (((a) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored)))) * S ((a) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored)))) + ((((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored))) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored))))))) /\ forall cf_index_egt_elb_anchored_trace. (exists ff_lt_cf_egt_elb_anchored_trace_index. ff_lt_cf_egt_elb_anchored_trace_index + S cf_index_egt_elb_anchored_trace = k) -> exists cf_old_a_egt_elb_anchored_trace cf_old_b_egt_elb_anchored_trace cf_tail_egt_elb_anchored_trace cf_new_a_egt_elb_anchored_trace cf_new_b_egt_elb_anchored_trace cf_head_egt_elb_anchored_trace cf_quotient_egt_elb_anchored_trace. ((((exists ff_h_cf_egt_elb_anchored_trace_previous_state. ff_h_cf_egt_elb_anchored_trace_previous_state + S (((cf_old_a_egt_elb_anchored_trace) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)))) * S ((cf_old_a_egt_elb_anchored_trace) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)))) + ((((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace))) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace))))) = S ((S (cf_index_egt_elb_anchored_trace)) * egt_scale_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_trace_previous_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_trace_previous_state * S ((S (cf_index_egt_elb_anchored_trace)) * egt_scale_elb_anchored) + (((cf_old_a_egt_elb_anchored_trace) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)))) * S ((cf_old_a_egt_elb_anchored_trace) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)))) + ((((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace))) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace))))))) /\ ((((exists ff_h_cf_egt_elb_anchored_trace_following_state. ff_h_cf_egt_elb_anchored_trace_following_state + S (((cf_new_a_egt_elb_anchored_trace) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)))) * S ((cf_new_a_egt_elb_anchored_trace) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)))) + ((((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace))) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace))))) = S ((S (S cf_index_egt_elb_anchored_trace)) * egt_scale_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_trace_following_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_trace_following_state * S ((S (S cf_index_egt_elb_anchored_trace)) * egt_scale_elb_anchored) + (((cf_new_a_egt_elb_anchored_trace) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)))) * S ((cf_new_a_egt_elb_anchored_trace) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)))) + ((((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace))) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace))))))) /\ (cf_new_b_egt_elb_anchored_trace = cf_old_a_egt_elb_anchored_trace /\ (cf_new_a_egt_elb_anchored_trace = cf_new_b_egt_elb_anchored_trace * cf_quotient_egt_elb_anchored_trace + cf_old_b_egt_elb_anchored_trace /\ ((exists ff_lt_cf_egt_elb_anchored_trace_remainder. ff_lt_cf_egt_elb_anchored_trace_remainder + S cf_old_b_egt_elb_anchored_trace = cf_new_b_egt_elb_anchored_trace) /\ (cf_head_egt_elb_anchored_trace = S ((cf_quotient_egt_elb_anchored_trace + cf_tail_egt_elb_anchored_trace) * S (cf_quotient_egt_elb_anchored_trace + cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace + cf_tail_egt_elb_anchored_trace))))))))))) /\ ((((exists ff_h_cf_egt_elb_anchored_initial_state. ff_h_cf_egt_elb_anchored_initial_state + S (((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * egt_scale_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_initial_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_initial_state * S ((S (0)) * egt_scale_elb_anchored) + (((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ec_gcd_left_egt_elb_anchored_result. a = g * ec_gcd_left_egt_elb_anchored_result) /\ (exists ec_gcd_right_egt_elb_anchored_result. b = g * ec_gcd_right_egt_elb_anchored_result)) /\ forall ec_gcd_common_egt_elb_anchored_result. (exists ec_gcd_common_left_egt_elb_anchored_result. a = ec_gcd_common_egt_elb_anchored_result * ec_gcd_common_left_egt_elb_anchored_result) -> (exists ec_gcd_common_right_egt_elb_anchored_result. b = ec_gcd_common_egt_elb_anchored_result * ec_gcd_common_right_egt_elb_anchored_result) -> exists ec_gcd_greatest_egt_elb_anchored_result. g = ec_gcd_common_egt_elb_anchored_result * ec_gcd_greatest_egt_elb_anchored_result))))) /\ exists gap. gap + k = 2 * l + 1)

Complete unchanged native tactic proof

All 29 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

29 script commands · 13 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
euclidean log execution strong

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro l
  4. L4
    intro hlength
02Use earlier factsL5–7

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

  1. L5
    specialize euclidean_log_execution_strong a
  2. L6
    specialize euclidean_log_execution_strong b
  3. L7
    specialize euclidean_log_execution_strong l
03Establish hstrongL8–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean log execution strong.

  1. L8
    have hstrong : ∃ g. ∃ k. EuclideanAnchoredExecution(a,b,g,k) ∧ Le(k,l + l)Definitions: EuclideanAnchoredExecutionLeOriginal native command in the exact edition
  2. L9
    apply euclidean_log_execution_strong
  3. L10
    exact hlength
04Separate the logical casesL11–13

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

  1. L11
    cases hstrong
  2. L12
    cases hstrong_witness
  3. L13
    cases hstrong_witness_witness
05Construct an explicit witnessL14–15

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

  1. L14
    exists x
  2. L15
    exists x1
06Separate the logical casesL16–16

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

  1. L16
    split
07Use earlier factsL17–19

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

  1. L17
    exact hstrong_witness_witness_left
  2. L18
    specialize le_succ x1
  3. L19
    specialize le_succ (l + l)
08Establish hweakenedL20–22

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

  1. L20
    have hweakened : exists gap. gap + x1 = S (l + l)
  2. L21
    apply le_succ
  3. L22
    exact hstrong_witness_witness_right
09Separate the logical casesL23–23

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

  1. L23
    cases hweakened
10Construct an explicit witnessL24–24

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

  1. L24
    exists x2
11Use earlier factsL25–25

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

  1. L25
    specialize two_mul_eq_add_self l
12Calculate and transport equalitiesL26–28

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

  1. L26
    rewrite two_mul_eq_add_self
  2. L27
    rewrite PA4
  3. L28
    rewrite PA3
13Use earlier factsL29–29

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

  1. L29
    exact hweakened_witness

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro l
  4. 0004intro hlength
  5. 0005specialize euclidean_log_execution_strong a
  6. 0006specialize euclidean_log_execution_strong b
  7. 0007specialize euclidean_log_execution_strong l
  8. 0008have hstrong : exists g k. ((exists egt_list_elb_anchored egt_history_elb_anchored egt_scale_elb_anchored. ((exists cf_gcd_egt_elb_anchored_trace. ((((exists ff_h_cf_egt_elb_anchored_trace_initial_state. ff_h_cf_egt_elb_anchored_trace_initial_state + S (((cf_gcd_egt_elb_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_elb_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * egt_scale_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_trace_initial_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_trace_initial_state * S ((S (0)) * egt_scale_elb_anchored) + (((cf_gcd_egt_elb_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_elb_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_egt_elb_anchored_trace_terminal_state. ff_h_cf_egt_elb_anchored_trace_terminal_state + S (((a) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored)))) * S ((a) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored)))) + ((((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored))) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored))))) = S ((S (k)) * egt_scale_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_trace_terminal_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_trace_terminal_state * S ((S (k)) * egt_scale_elb_anchored) + (((a) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored)))) * S ((a) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored)))) + ((((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored))) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored))))))) /\ forall cf_index_egt_elb_anchored_trace. (exists ff_lt_cf_egt_elb_anchored_trace_index. ff_lt_cf_egt_elb_anchored_trace_index + S cf_index_egt_elb_anchored_trace = k) -> exists cf_old_a_egt_elb_anchored_trace cf_old_b_egt_elb_anchored_trace cf_tail_egt_elb_anchored_trace cf_new_a_egt_elb_anchored_trace cf_new_b_egt_elb_anchored_trace cf_head_egt_elb_anchored_trace cf_quotient_egt_elb_anchored_trace. ((((exists ff_h_cf_egt_elb_anchored_trace_previous_state. ff_h_cf_egt_elb_anchored_trace_previous_state + S (((cf_old_a_egt_elb_anchored_trace) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)))) * S ((cf_old_a_egt_elb_anchored_trace) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)))) + ((((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace))) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace))))) = S ((S (cf_index_egt_elb_anchored_trace)) * egt_scale_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_trace_previous_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_trace_previous_state * S ((S (cf_index_egt_elb_anchored_trace)) * egt_scale_elb_anchored) + (((cf_old_a_egt_elb_anchored_trace) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)))) * S ((cf_old_a_egt_elb_anchored_trace) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)))) + ((((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace))) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace))))))) /\ ((((exists ff_h_cf_egt_elb_anchored_trace_following_state. ff_h_cf_egt_elb_anchored_trace_following_state + S (((cf_new_a_egt_elb_anchored_trace) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)))) * S ((cf_new_a_egt_elb_anchored_trace) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)))) + ((((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace))) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace))))) = S ((S (S cf_index_egt_elb_anchored_trace)) * egt_scale_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_trace_following_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_trace_following_state * S ((S (S cf_index_egt_elb_anchored_trace)) * egt_scale_elb_anchored) + (((cf_new_a_egt_elb_anchored_trace) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)))) * S ((cf_new_a_egt_elb_anchored_trace) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)))) + ((((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace))) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace))))))) /\ (cf_new_b_egt_elb_anchored_trace = cf_old_a_egt_elb_anchored_trace /\ (cf_new_a_egt_elb_anchored_trace = cf_new_b_egt_elb_anchored_trace * cf_quotient_egt_elb_anchored_trace + cf_old_b_egt_elb_anchored_trace /\ ((exists ff_lt_cf_egt_elb_anchored_trace_remainder. ff_lt_cf_egt_elb_anchored_trace_remainder + S cf_old_b_egt_elb_anchored_trace = cf_new_b_egt_elb_anchored_trace) /\ (cf_head_egt_elb_anchored_trace = S ((cf_quotient_egt_elb_anchored_trace + cf_tail_egt_elb_anchored_trace) * S (cf_quotient_egt_elb_anchored_trace + cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace + cf_tail_egt_elb_anchored_trace))))))))))) /\ ((((exists ff_h_cf_egt_elb_anchored_initial_state. ff_h_cf_egt_elb_anchored_initial_state + S (((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * egt_scale_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_initial_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_initial_state * S ((S (0)) * egt_scale_elb_anchored) + (((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ec_gcd_left_egt_elb_anchored_result. a = g * ec_gcd_left_egt_elb_anchored_result) /\ (exists ec_gcd_right_egt_elb_anchored_result. b = g * ec_gcd_right_egt_elb_anchored_result)) /\ forall ec_gcd_common_egt_elb_anchored_result. (exists ec_gcd_common_left_egt_elb_anchored_result. a = ec_gcd_common_egt_elb_anchored_result * ec_gcd_common_left_egt_elb_anchored_result) -> (exists ec_gcd_common_right_egt_elb_anchored_result. b = ec_gcd_common_egt_elb_anchored_result * ec_gcd_common_right_egt_elb_anchored_result) -> exists ec_gcd_greatest_egt_elb_anchored_result. g = ec_gcd_common_egt_elb_anchored_result * ec_gcd_greatest_egt_elb_anchored_result))))) /\ exists gap. gap + k = l + l)
  9. 0009apply euclidean_log_execution_strong
  10. 0010exact hlength
  11. 0011cases hstrong
  12. 0012cases hstrong_witness
  13. 0013cases hstrong_witness_witness
  14. 0014exists x
  15. 0015exists x1
  16. 0016split
  17. 0017exact hstrong_witness_witness_left
  18. 0018specialize le_succ x1
  19. 0019specialize le_succ (l + l)
  20. 0020have hweakened : exists gap. gap + x1 = S (l + l)
  21. 0021apply le_succ
  22. 0022exact hstrong_witness_witness_right
  23. 0023cases hweakened
  24. 0024exists x2
  25. 0025specialize two_mul_eq_add_self l
  26. 0026rewrite two_mul_eq_add_self
  27. 0027rewrite PA4
  28. 0028rewrite PA3
  29. 0029exact hweakened_witness