GT000E

euclidean_trace_initial_state_is_gcd

The actual value encoded in the zeroth terminal Euclidean beta-state is a relational gcd of the original terminal input pair.

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. ∀ s. ∀ h. ∀ e. ∀ l. ∀ g. ContinuedFractionTrace(a,b,s,h,e,l) → EuclideanStateAt(h,e,0,g,0,0) → IsGCD(g,a,b)

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

Definition DAG

ContinuedFractionTrace(a,b,s,u,v,ell) · 1EuclideanStateAt(h,s,i,a,b,q) · 1IsGCD(g,a,b) · 1

Actual proof prerequisites

euclidean_trace_prefix_gcd_invarianteuclidean_beta_state_functionalle_refl · checked external prerequisite
Original expanded first-order statement 
forall a b s h e l g. (exists cf_gcd_egt_trace. ((((exists ff_h_cf_egt_trace_initial_state. ff_h_cf_egt_trace_initial_state + S (((cf_gcd_egt_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_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)) * e)) /\ exists ff_q_cf_egt_trace_initial_state. h = ff_q_cf_egt_trace_initial_state * S ((S (0)) * e) + (((cf_gcd_egt_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_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_trace_terminal_state. ff_h_cf_egt_trace_terminal_state + S (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))) = S ((S (l)) * e)) /\ exists ff_q_cf_egt_trace_terminal_state. h = ff_q_cf_egt_trace_terminal_state * S ((S (l)) * e) + (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))))) /\ forall cf_index_egt_trace. (exists ff_lt_cf_egt_trace_index. ff_lt_cf_egt_trace_index + S cf_index_egt_trace = l) -> exists cf_old_a_egt_trace cf_old_b_egt_trace cf_tail_egt_trace cf_new_a_egt_trace cf_new_b_egt_trace cf_head_egt_trace cf_quotient_egt_trace. ((((exists ff_h_cf_egt_trace_previous_state. ff_h_cf_egt_trace_previous_state + S (((cf_old_a_egt_trace) + (((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace)))) * S ((cf_old_a_egt_trace) + (((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace)))) + ((((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace))) + (((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace))))) = S ((S (cf_index_egt_trace)) * e)) /\ exists ff_q_cf_egt_trace_previous_state. h = ff_q_cf_egt_trace_previous_state * S ((S (cf_index_egt_trace)) * e) + (((cf_old_a_egt_trace) + (((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace)))) * S ((cf_old_a_egt_trace) + (((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace)))) + ((((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace))) + (((cf_old_b_egt_trace) + (cf_tail_egt_trace)) * S ((cf_old_b_egt_trace) + (cf_tail_egt_trace)) + ((cf_tail_egt_trace) + (cf_tail_egt_trace))))))) /\ ((((exists ff_h_cf_egt_trace_following_state. ff_h_cf_egt_trace_following_state + S (((cf_new_a_egt_trace) + (((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace)))) * S ((cf_new_a_egt_trace) + (((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace)))) + ((((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace))) + (((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace))))) = S ((S (S cf_index_egt_trace)) * e)) /\ exists ff_q_cf_egt_trace_following_state. h = ff_q_cf_egt_trace_following_state * S ((S (S cf_index_egt_trace)) * e) + (((cf_new_a_egt_trace) + (((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace)))) * S ((cf_new_a_egt_trace) + (((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace)))) + ((((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace))) + (((cf_new_b_egt_trace) + (cf_head_egt_trace)) * S ((cf_new_b_egt_trace) + (cf_head_egt_trace)) + ((cf_head_egt_trace) + (cf_head_egt_trace))))))) /\ (cf_new_b_egt_trace = cf_old_a_egt_trace /\ (cf_new_a_egt_trace = cf_new_b_egt_trace * cf_quotient_egt_trace + cf_old_b_egt_trace /\ ((exists ff_lt_cf_egt_trace_remainder. ff_lt_cf_egt_trace_remainder + S cf_old_b_egt_trace = cf_new_b_egt_trace) /\ (cf_head_egt_trace = S ((cf_quotient_egt_trace + cf_tail_egt_trace) * S (cf_quotient_egt_trace + cf_tail_egt_trace) + (cf_tail_egt_trace + cf_tail_egt_trace))))))))))) -> (((exists ff_h_cf_egt_start_state. ff_h_cf_egt_start_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)) * e)) /\ exists ff_q_cf_egt_start_state. h = ff_q_cf_egt_start_state * S ((S (0)) * e) + (((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 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 52 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

52 script commands · 9 reading checkpoints · 3 local claims

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

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

Named ingredients (2)
euclidean trace prefix gcd invarianteuclidean beta state functional

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–9

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro s
  4. L4
    intro h
  5. L5
    intro e
  6. L6
    intro l
  7. L7
    intro g
  8. L8
    intro htrace
  9. L9
    intro hstart
02Establish hinvariantL10–17

Establish this local claim before using it. It is not an additional assumption.

  1. L10
    have hinvariant : ∃ egt_left_terminal. ∃ egt_right_terminal. ∃ egt_list_terminal. EuclideanStateAt(h,e,l,egt_left_terminal,egt_right_terminal,egt_list_terminal) ∧ IsGCD(g,egt_left_terminal,egt_right_terminal)Definitions: EuclideanStateAtIsGCDOriginal native command in the exact edition
  2. L11
    specialize euclidean_trace_prefix_gcd_invariant a
  3. L12
    specialize euclidean_trace_prefix_gcd_invariant b
  4. L13
    specialize euclidean_trace_prefix_gcd_invariant s
  5. L14
    specialize euclidean_trace_prefix_gcd_invariant h
  6. L15
    specialize euclidean_trace_prefix_gcd_invariant e
  7. L16
    specialize euclidean_trace_prefix_gcd_invariant l
  8. L17
    specialize euclidean_trace_prefix_gcd_invariant g
03Establish hallL18–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean trace prefix gcd invariant.

  1. L18
    have hall : ∀ i. Le(i,l) → ∃ x. ∃ y. ∃ z. EuclideanStateAt(h,e,i,x,y,z) ∧ IsGCD(g,x,y)Definitions: EuclideanStateAtLeIsGCDOriginal native command in the exact edition
  2. L19
    apply euclidean_trace_prefix_gcd_invariant
  3. L20
    exact htrace
  4. L21
    exact hstart
  5. L22
    specialize hall l
  6. L23
    apply hall
  7. L24
    specialize le_refl l
  8. L25
    exact le_refl
04Separate the logical casesL26–32

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

  1. L26
    cases hinvariant
  2. L27
    cases hinvariant_witness
  3. L28
    cases hinvariant_witness_witness
  4. L29
    cases hinvariant_witness_witness_witness
  5. L30
    cases htrace
  6. L31
    cases htrace_witness
  7. L32
    cases htrace_witness_right
05Establish halignL33–42

Establish this local claim before using it. It is not an additional assumption.

  1. L33
    have halign : x = a /\ (x1 = b /\ x2 = s)
  2. L34
    specialize euclidean_beta_state_functional h
  3. L35
    specialize euclidean_beta_state_functional e
  4. L36
    specialize euclidean_beta_state_functional l
  5. L37
    specialize euclidean_beta_state_functional x
  6. L38
    specialize euclidean_beta_state_functional x1
  7. L39
    specialize euclidean_beta_state_functional x2
  8. L40
    specialize euclidean_beta_state_functional a
  9. L41
    specialize euclidean_beta_state_functional b
  10. L42
    specialize euclidean_beta_state_functional s
06Use earlier factsL43–45

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

  1. L43
    apply euclidean_beta_state_functional
  2. L44
    exact hinvariant_witness_witness_witness_left
  3. L45
    exact htrace_witness_right_left
07Separate the logical casesL46–47

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

  1. L46
    cases halign
  2. L47
    cases halign_right
08Calculate and transport equalitiesL48–51

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

  1. L48
    rewrite halign_left at hinvariant_witness_witness_witness_right
  2. L49
    rewrite halign_left at hinvariant_witness_witness_witness_right
  3. L50
    rewrite halign_right_left at hinvariant_witness_witness_witness_right
  4. L51
    rewrite halign_right_left at hinvariant_witness_witness_witness_right
09Use earlier factsL52–52

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

  1. L52
    exact hinvariant_witness_witness_witness_right

Library-wide reading audit

Original defined command ledger · 52 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro s
  4. 0004intro h
  5. 0005intro e
  6. 0006intro l
  7. 0007intro g
  8. 0008intro htrace
  9. 0009intro hstart
  10. 0010have hinvariant : exists egt_left_terminal egt_right_terminal egt_list_terminal. ((((exists ff_h_cf_egt_terminal_state_state. ff_h_cf_egt_terminal_state_state + S (((egt_left_terminal) + (((egt_right_terminal) + (egt_list_terminal)) * S ((egt_right_terminal) + (egt_list_terminal)) + ((egt_list_terminal) + (egt_list_terminal)))) * S ((egt_left_terminal) + (((egt_right_terminal) + (egt_list_terminal)) * S ((egt_right_terminal) + (egt_list_terminal)) + ((egt_list_terminal) + (egt_list_terminal)))) + ((((egt_right_terminal) + (egt_list_terminal)) * S ((egt_right_terminal) + (egt_list_terminal)) + ((egt_list_terminal) + (egt_list_terminal))) + (((egt_right_terminal) + (egt_list_terminal)) * S ((egt_right_terminal) + (egt_list_terminal)) + ((egt_list_terminal) + (egt_list_terminal))))) = S ((S (l)) * e)) /\ exists ff_q_cf_egt_terminal_state_state. h = ff_q_cf_egt_terminal_state_state * S ((S (l)) * e) + (((egt_left_terminal) + (((egt_right_terminal) + (egt_list_terminal)) * S ((egt_right_terminal) + (egt_list_terminal)) + ((egt_list_terminal) + (egt_list_terminal)))) * S ((egt_left_terminal) + (((egt_right_terminal) + (egt_list_terminal)) * S ((egt_right_terminal) + (egt_list_terminal)) + ((egt_list_terminal) + (egt_list_terminal)))) + ((((egt_right_terminal) + (egt_list_terminal)) * S ((egt_right_terminal) + (egt_list_terminal)) + ((egt_list_terminal) + (egt_list_terminal))) + (((egt_right_terminal) + (egt_list_terminal)) * S ((egt_right_terminal) + (egt_list_terminal)) + ((egt_list_terminal) + (egt_list_terminal))))))) /\ ((((exists ec_gcd_left_egt_terminal_gcd. egt_left_terminal = g * ec_gcd_left_egt_terminal_gcd) /\ (exists ec_gcd_right_egt_terminal_gcd. egt_right_terminal = g * ec_gcd_right_egt_terminal_gcd)) /\ forall ec_gcd_common_egt_terminal_gcd. (exists ec_gcd_common_left_egt_terminal_gcd. egt_left_terminal = ec_gcd_common_egt_terminal_gcd * ec_gcd_common_left_egt_terminal_gcd) -> (exists ec_gcd_common_right_egt_terminal_gcd. egt_right_terminal = ec_gcd_common_egt_terminal_gcd * ec_gcd_common_right_egt_terminal_gcd) -> exists ec_gcd_greatest_egt_terminal_gcd. g = ec_gcd_common_egt_terminal_gcd * ec_gcd_greatest_egt_terminal_gcd)))
  11. 0011specialize euclidean_trace_prefix_gcd_invariant a
  12. 0012specialize euclidean_trace_prefix_gcd_invariant b
  13. 0013specialize euclidean_trace_prefix_gcd_invariant s
  14. 0014specialize euclidean_trace_prefix_gcd_invariant h
  15. 0015specialize euclidean_trace_prefix_gcd_invariant e
  16. 0016specialize euclidean_trace_prefix_gcd_invariant l
  17. 0017specialize euclidean_trace_prefix_gcd_invariant g
  18. 0018have hall : forall i. (exists gap. gap + i = l) -> (exists egt_left_terminal_all egt_right_terminal_all egt_list_terminal_all. ((((exists ff_h_cf_egt_terminal_all_state_state. ff_h_cf_egt_terminal_all_state_state + S (((egt_left_terminal_all) + (((egt_right_terminal_all) + (egt_list_terminal_all)) * S ((egt_right_terminal_all) + (egt_list_terminal_all)) + ((egt_list_terminal_all) + (egt_list_terminal_all)))) * S ((egt_left_terminal_all) + (((egt_right_terminal_all) + (egt_list_terminal_all)) * S ((egt_right_terminal_all) + (egt_list_terminal_all)) + ((egt_list_terminal_all) + (egt_list_terminal_all)))) + ((((egt_right_terminal_all) + (egt_list_terminal_all)) * S ((egt_right_terminal_all) + (egt_list_terminal_all)) + ((egt_list_terminal_all) + (egt_list_terminal_all))) + (((egt_right_terminal_all) + (egt_list_terminal_all)) * S ((egt_right_terminal_all) + (egt_list_terminal_all)) + ((egt_list_terminal_all) + (egt_list_terminal_all))))) = S ((S (i)) * e)) /\ exists ff_q_cf_egt_terminal_all_state_state. h = ff_q_cf_egt_terminal_all_state_state * S ((S (i)) * e) + (((egt_left_terminal_all) + (((egt_right_terminal_all) + (egt_list_terminal_all)) * S ((egt_right_terminal_all) + (egt_list_terminal_all)) + ((egt_list_terminal_all) + (egt_list_terminal_all)))) * S ((egt_left_terminal_all) + (((egt_right_terminal_all) + (egt_list_terminal_all)) * S ((egt_right_terminal_all) + (egt_list_terminal_all)) + ((egt_list_terminal_all) + (egt_list_terminal_all)))) + ((((egt_right_terminal_all) + (egt_list_terminal_all)) * S ((egt_right_terminal_all) + (egt_list_terminal_all)) + ((egt_list_terminal_all) + (egt_list_terminal_all))) + (((egt_right_terminal_all) + (egt_list_terminal_all)) * S ((egt_right_terminal_all) + (egt_list_terminal_all)) + ((egt_list_terminal_all) + (egt_list_terminal_all))))))) /\ ((((exists ec_gcd_left_egt_terminal_all_gcd. egt_left_terminal_all = g * ec_gcd_left_egt_terminal_all_gcd) /\ (exists ec_gcd_right_egt_terminal_all_gcd. egt_right_terminal_all = g * ec_gcd_right_egt_terminal_all_gcd)) /\ forall ec_gcd_common_egt_terminal_all_gcd. (exists ec_gcd_common_left_egt_terminal_all_gcd. egt_left_terminal_all = ec_gcd_common_egt_terminal_all_gcd * ec_gcd_common_left_egt_terminal_all_gcd) -> (exists ec_gcd_common_right_egt_terminal_all_gcd. egt_right_terminal_all = ec_gcd_common_egt_terminal_all_gcd * ec_gcd_common_right_egt_terminal_all_gcd) -> exists ec_gcd_greatest_egt_terminal_all_gcd. g = ec_gcd_common_egt_terminal_all_gcd * ec_gcd_greatest_egt_terminal_all_gcd))))
  19. 0019apply euclidean_trace_prefix_gcd_invariant
  20. 0020exact htrace
  21. 0021exact hstart
  22. 0022specialize hall l
  23. 0023apply hall
  24. 0024specialize le_refl l
  25. 0025exact le_refl
  26. 0026cases hinvariant
  27. 0027cases hinvariant_witness
  28. 0028cases hinvariant_witness_witness
  29. 0029cases hinvariant_witness_witness_witness
  30. 0030cases htrace
  31. 0031cases htrace_witness
  32. 0032cases htrace_witness_right
  33. 0033have halign : x = a /\ (x1 = b /\ x2 = s)
  34. 0034specialize euclidean_beta_state_functional h
  35. 0035specialize euclidean_beta_state_functional e
  36. 0036specialize euclidean_beta_state_functional l
  37. 0037specialize euclidean_beta_state_functional x
  38. 0038specialize euclidean_beta_state_functional x1
  39. 0039specialize euclidean_beta_state_functional x2
  40. 0040specialize euclidean_beta_state_functional a
  41. 0041specialize euclidean_beta_state_functional b
  42. 0042specialize euclidean_beta_state_functional s
  43. 0043apply euclidean_beta_state_functional
  44. 0044exact hinvariant_witness_witness_witness_left
  45. 0045exact htrace_witness_right_left
  46. 0046cases halign
  47. 0047cases halign_right
  48. 0048rewrite halign_left at hinvariant_witness_witness_witness_right
  49. 0049rewrite halign_left at hinvariant_witness_witness_witness_right
  50. 0050rewrite halign_right_left at hinvariant_witness_witness_witness_right
  51. 0051rewrite halign_right_left at hinvariant_witness_witness_witness_right
  52. 0052exact hinvariant_witness_witness_witness_right