GT0013

euclidean_anchored_execution_gcd_correct

Every anchored Euclidean execution independently satisfies the full original relational greatest-common-divisor specification.

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

G101 was OPEN at this family's Alpha-v22 first admission: its complete anchored trace and actual terminal gcd were proved but its logarithmic bound was not. G101 is now CLOSED in Alpha v23, including the exact first-order bound steps≤2*BitLen(b)+1.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ g. ∀ l. EuclideanAnchoredExecution(a,b,g,l) → IsGCD(g,a,b)

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

Definition DAG

EuclideanAnchoredExecution(a,b,g,k) · 1IsGCD(g,a,b) · 1

Actual proof prerequisites

none
Original expanded first-order statement 
forall a b g l. (exists egt_list_egt_anchored egt_history_egt_anchored egt_scale_egt_anchored. ((exists cf_gcd_egt_egt_anchored_trace. ((((exists ff_h_cf_egt_egt_anchored_trace_initial_state. ff_h_cf_egt_egt_anchored_trace_initial_state + S (((cf_gcd_egt_egt_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_egt_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_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_trace_initial_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_trace_initial_state * S ((S (0)) * egt_scale_egt_anchored) + (((cf_gcd_egt_egt_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_egt_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_egt_anchored_trace_terminal_state. ff_h_cf_egt_egt_anchored_trace_terminal_state + S (((a) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored)))) * S ((a) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored)))) + ((((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored))) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored))))) = S ((S (l)) * egt_scale_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_trace_terminal_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_trace_terminal_state * S ((S (l)) * egt_scale_egt_anchored) + (((a) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored)))) * S ((a) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored)))) + ((((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored))) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored))))))) /\ forall cf_index_egt_egt_anchored_trace. (exists ff_lt_cf_egt_egt_anchored_trace_index. ff_lt_cf_egt_egt_anchored_trace_index + S cf_index_egt_egt_anchored_trace = l) -> exists cf_old_a_egt_egt_anchored_trace cf_old_b_egt_egt_anchored_trace cf_tail_egt_egt_anchored_trace cf_new_a_egt_egt_anchored_trace cf_new_b_egt_egt_anchored_trace cf_head_egt_egt_anchored_trace cf_quotient_egt_egt_anchored_trace. ((((exists ff_h_cf_egt_egt_anchored_trace_previous_state. ff_h_cf_egt_egt_anchored_trace_previous_state + S (((cf_old_a_egt_egt_anchored_trace) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)))) * S ((cf_old_a_egt_egt_anchored_trace) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)))) + ((((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace))) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace))))) = S ((S (cf_index_egt_egt_anchored_trace)) * egt_scale_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_trace_previous_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_trace_previous_state * S ((S (cf_index_egt_egt_anchored_trace)) * egt_scale_egt_anchored) + (((cf_old_a_egt_egt_anchored_trace) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)))) * S ((cf_old_a_egt_egt_anchored_trace) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)))) + ((((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace))) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace))))))) /\ ((((exists ff_h_cf_egt_egt_anchored_trace_following_state. ff_h_cf_egt_egt_anchored_trace_following_state + S (((cf_new_a_egt_egt_anchored_trace) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)))) * S ((cf_new_a_egt_egt_anchored_trace) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)))) + ((((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace))) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace))))) = S ((S (S cf_index_egt_egt_anchored_trace)) * egt_scale_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_trace_following_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_trace_following_state * S ((S (S cf_index_egt_egt_anchored_trace)) * egt_scale_egt_anchored) + (((cf_new_a_egt_egt_anchored_trace) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)))) * S ((cf_new_a_egt_egt_anchored_trace) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)))) + ((((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace))) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace))))))) /\ (cf_new_b_egt_egt_anchored_trace = cf_old_a_egt_egt_anchored_trace /\ (cf_new_a_egt_egt_anchored_trace = cf_new_b_egt_egt_anchored_trace * cf_quotient_egt_egt_anchored_trace + cf_old_b_egt_egt_anchored_trace /\ ((exists ff_lt_cf_egt_egt_anchored_trace_remainder. ff_lt_cf_egt_egt_anchored_trace_remainder + S cf_old_b_egt_egt_anchored_trace = cf_new_b_egt_egt_anchored_trace) /\ (cf_head_egt_egt_anchored_trace = S ((cf_quotient_egt_egt_anchored_trace + cf_tail_egt_egt_anchored_trace) * S (cf_quotient_egt_egt_anchored_trace + cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace + cf_tail_egt_egt_anchored_trace))))))))))) /\ ((((exists ff_h_cf_egt_egt_anchored_initial_state. ff_h_cf_egt_egt_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_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_initial_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_initial_state * S ((S (0)) * egt_scale_egt_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_egt_anchored_result. a = g * ec_gcd_left_egt_egt_anchored_result) /\ (exists ec_gcd_right_egt_egt_anchored_result. b = g * ec_gcd_right_egt_egt_anchored_result)) /\ forall ec_gcd_common_egt_egt_anchored_result. (exists ec_gcd_common_left_egt_egt_anchored_result. a = ec_gcd_common_egt_egt_anchored_result * ec_gcd_common_left_egt_egt_anchored_result) -> (exists ec_gcd_common_right_egt_egt_anchored_result. b = ec_gcd_common_egt_egt_anchored_result * ec_gcd_common_right_egt_egt_anchored_result) -> exists ec_gcd_greatest_egt_egt_anchored_result. g = ec_gcd_common_egt_egt_anchored_result * ec_gcd_greatest_egt_egt_anchored_result))))) -> ((((exists hag_left_factor_egt_terminal. a = g * hag_left_factor_egt_terminal) /\ (exists hag_right_factor_egt_terminal. b = g * hag_right_factor_egt_terminal)) /\ forall hag_divisor_egt_terminal. (exists hag_common_left_egt_terminal. a = hag_divisor_egt_terminal * hag_common_left_egt_terminal) -> (exists hag_common_right_egt_terminal. b = hag_divisor_egt_terminal * hag_common_right_egt_terminal) -> exists hag_greatest_factor_egt_terminal. g = hag_divisor_egt_terminal * hag_greatest_factor_egt_terminal))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

11 script commands · 3 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro g
  4. L4
    intro l
  5. L5
    intro hanchored
02Separate the logical casesL6–10

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

  1. L6
    cases hanchored
  2. L7
    cases hanchored_witness
  3. L8
    cases hanchored_witness_witness
  4. L9
    cases hanchored_witness_witness_witness
  5. L10
    cases hanchored_witness_witness_witness_right
03Use earlier factsL11–11

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

  1. L11
    exact hanchored_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 11 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro g
  4. 0004intro l
  5. 0005intro hanchored
  6. 0006cases hanchored
  7. 0007cases hanchored_witness
  8. 0008cases hanchored_witness_witness
  9. 0009cases hanchored_witness_witness_witness
  10. 0010cases hanchored_witness_witness_witness_right
  11. 0011exact hanchored_witness_witness_witness_right_right