EC000E

euclidean_nonzero_execution_exists

For every nonzero initial divisor, an actual certified Euclidean execution exists and makes at least one division.

Alpha v34 checked-use · first admitted v21 · 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 when this family was first admitted in Alpha v21. It is now CLOSED in Alpha v23: the actual anchored Euclidean history, terminal gcd, and exact bound steps≤2*BitLen(b)+1 are proved.

Exact theorem in conservative defined notation

∀ a. ∀ b. ¬b = 0 → ∃ x. ∃ y. EuclideanExecution(a,b,x,S y)

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

Definition DAG

EuclideanExecution(a,b,g,k) · 1

Actual proof prerequisites

continued_fraction_nonzero_divisor_exists · checked external prerequisitegcd_exists_relational · checked external prerequisite
Original expanded first-order statement 
forall a b. ~(b = 0) -> exists g k. (exists ec_list_positive ec_history_positive ec_scale_positive. ((exists cf_gcd_ec_positive_trace. ((((exists ff_h_cf_ec_positive_trace_initial_state. ff_h_cf_ec_positive_trace_initial_state + S (((cf_gcd_ec_positive_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_positive_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)) * ec_scale_positive)) /\ exists ff_q_cf_ec_positive_trace_initial_state. ec_history_positive = ff_q_cf_ec_positive_trace_initial_state * S ((S (0)) * ec_scale_positive) + (((cf_gcd_ec_positive_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_positive_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_ec_positive_trace_terminal_state. ff_h_cf_ec_positive_trace_terminal_state + S (((a) + (((b) + (ec_list_positive)) * S ((b) + (ec_list_positive)) + ((ec_list_positive) + (ec_list_positive)))) * S ((a) + (((b) + (ec_list_positive)) * S ((b) + (ec_list_positive)) + ((ec_list_positive) + (ec_list_positive)))) + ((((b) + (ec_list_positive)) * S ((b) + (ec_list_positive)) + ((ec_list_positive) + (ec_list_positive))) + (((b) + (ec_list_positive)) * S ((b) + (ec_list_positive)) + ((ec_list_positive) + (ec_list_positive))))) = S ((S (S k)) * ec_scale_positive)) /\ exists ff_q_cf_ec_positive_trace_terminal_state. ec_history_positive = ff_q_cf_ec_positive_trace_terminal_state * S ((S (S k)) * ec_scale_positive) + (((a) + (((b) + (ec_list_positive)) * S ((b) + (ec_list_positive)) + ((ec_list_positive) + (ec_list_positive)))) * S ((a) + (((b) + (ec_list_positive)) * S ((b) + (ec_list_positive)) + ((ec_list_positive) + (ec_list_positive)))) + ((((b) + (ec_list_positive)) * S ((b) + (ec_list_positive)) + ((ec_list_positive) + (ec_list_positive))) + (((b) + (ec_list_positive)) * S ((b) + (ec_list_positive)) + ((ec_list_positive) + (ec_list_positive))))))) /\ forall cf_index_ec_positive_trace. (exists ff_lt_cf_ec_positive_trace_index. ff_lt_cf_ec_positive_trace_index + S cf_index_ec_positive_trace = S k) -> exists cf_old_a_ec_positive_trace cf_old_b_ec_positive_trace cf_tail_ec_positive_trace cf_new_a_ec_positive_trace cf_new_b_ec_positive_trace cf_head_ec_positive_trace cf_quotient_ec_positive_trace. ((((exists ff_h_cf_ec_positive_trace_previous_state. ff_h_cf_ec_positive_trace_previous_state + S (((cf_old_a_ec_positive_trace) + (((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) * S ((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) + ((cf_tail_ec_positive_trace) + (cf_tail_ec_positive_trace)))) * S ((cf_old_a_ec_positive_trace) + (((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) * S ((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) + ((cf_tail_ec_positive_trace) + (cf_tail_ec_positive_trace)))) + ((((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) * S ((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) + ((cf_tail_ec_positive_trace) + (cf_tail_ec_positive_trace))) + (((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) * S ((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) + ((cf_tail_ec_positive_trace) + (cf_tail_ec_positive_trace))))) = S ((S (cf_index_ec_positive_trace)) * ec_scale_positive)) /\ exists ff_q_cf_ec_positive_trace_previous_state. ec_history_positive = ff_q_cf_ec_positive_trace_previous_state * S ((S (cf_index_ec_positive_trace)) * ec_scale_positive) + (((cf_old_a_ec_positive_trace) + (((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) * S ((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) + ((cf_tail_ec_positive_trace) + (cf_tail_ec_positive_trace)))) * S ((cf_old_a_ec_positive_trace) + (((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) * S ((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) + ((cf_tail_ec_positive_trace) + (cf_tail_ec_positive_trace)))) + ((((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) * S ((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) + ((cf_tail_ec_positive_trace) + (cf_tail_ec_positive_trace))) + (((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) * S ((cf_old_b_ec_positive_trace) + (cf_tail_ec_positive_trace)) + ((cf_tail_ec_positive_trace) + (cf_tail_ec_positive_trace))))))) /\ ((((exists ff_h_cf_ec_positive_trace_following_state. ff_h_cf_ec_positive_trace_following_state + S (((cf_new_a_ec_positive_trace) + (((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) * S ((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) + ((cf_head_ec_positive_trace) + (cf_head_ec_positive_trace)))) * S ((cf_new_a_ec_positive_trace) + (((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) * S ((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) + ((cf_head_ec_positive_trace) + (cf_head_ec_positive_trace)))) + ((((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) * S ((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) + ((cf_head_ec_positive_trace) + (cf_head_ec_positive_trace))) + (((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) * S ((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) + ((cf_head_ec_positive_trace) + (cf_head_ec_positive_trace))))) = S ((S (S cf_index_ec_positive_trace)) * ec_scale_positive)) /\ exists ff_q_cf_ec_positive_trace_following_state. ec_history_positive = ff_q_cf_ec_positive_trace_following_state * S ((S (S cf_index_ec_positive_trace)) * ec_scale_positive) + (((cf_new_a_ec_positive_trace) + (((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) * S ((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) + ((cf_head_ec_positive_trace) + (cf_head_ec_positive_trace)))) * S ((cf_new_a_ec_positive_trace) + (((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) * S ((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) + ((cf_head_ec_positive_trace) + (cf_head_ec_positive_trace)))) + ((((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) * S ((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) + ((cf_head_ec_positive_trace) + (cf_head_ec_positive_trace))) + (((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) * S ((cf_new_b_ec_positive_trace) + (cf_head_ec_positive_trace)) + ((cf_head_ec_positive_trace) + (cf_head_ec_positive_trace))))))) /\ (cf_new_b_ec_positive_trace = cf_old_a_ec_positive_trace /\ (cf_new_a_ec_positive_trace = cf_new_b_ec_positive_trace * cf_quotient_ec_positive_trace + cf_old_b_ec_positive_trace /\ ((exists ff_lt_cf_ec_positive_trace_remainder. ff_lt_cf_ec_positive_trace_remainder + S cf_old_b_ec_positive_trace = cf_new_b_ec_positive_trace) /\ (cf_head_ec_positive_trace = S ((cf_quotient_ec_positive_trace + cf_tail_ec_positive_trace) * S (cf_quotient_ec_positive_trace + cf_tail_ec_positive_trace) + (cf_tail_ec_positive_trace + cf_tail_ec_positive_trace))))))))))) /\ ((((exists ec_gcd_left_positive_result. a = g * ec_gcd_left_positive_result) /\ (exists ec_gcd_right_positive_result. b = g * ec_gcd_right_positive_result)) /\ forall ec_gcd_common_positive_result. (exists ec_gcd_common_left_positive_result. a = ec_gcd_common_positive_result * ec_gcd_common_left_positive_result) -> (exists ec_gcd_common_right_positive_result. b = ec_gcd_common_positive_result * ec_gcd_common_right_positive_result) -> exists ec_gcd_greatest_positive_result. g = ec_gcd_common_positive_result * ec_gcd_greatest_positive_result))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

24 script commands · 9 reading checkpoints · 1 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.

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

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro hb
02Use earlier factsL4–5

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

  1. L4
    specialize gcd_exists_relational a
  2. L5
    specialize gcd_exists_relational b
03Separate the logical casesL6–6

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

  1. L6
    cases gcd_exists_relational
04Use earlier factsL7–8

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

  1. L7
    specialize continued_fraction_nonzero_divisor_exists a
  2. L8
    specialize continued_fraction_nonzero_divisor_exists b
05Establish htraceL9–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply continued fraction nonzero divisor exists.

  1. L9
    have htrace : ∃ s. ∃ h. ∃ e. ∃ k. ¬s = 0 ∧ ContinuedFractionTrace(a,b,s,h,e,S k)Definitions: ContinuedFractionTraceOriginal native command in the exact edition
  2. L10
    apply continued_fraction_nonzero_divisor_exists
  3. L11
    exact hb
06Separate the logical casesL12–16

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

  1. L12
    cases htrace
  2. L13
    cases htrace_witness
  3. L14
    cases htrace_witness_witness
  4. L15
    cases htrace_witness_witness_witness
  5. L16
    cases htrace_witness_witness_witness_witness
07Construct an explicit witnessL17–21

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

  1. L17
    exists x
  2. L18
    exists x4
  3. L19
    exists x1
  4. L20
    exists x2
  5. L21
    exists x3
08Separate the logical casesL22–22

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

  1. L22
    split
09Use earlier factsL23–24

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

  1. L23
    exact htrace_witness_witness_witness_witness_right
  2. L24
    exact gcd_exists_relational_witness

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro hb
  4. 0004specialize gcd_exists_relational a
  5. 0005specialize gcd_exists_relational b
  6. 0006cases gcd_exists_relational
  7. 0007specialize continued_fraction_nonzero_divisor_exists a
  8. 0008specialize continued_fraction_nonzero_divisor_exists b
  9. 0009have htrace : exists s h e k. (~(s = 0) /\ (exists cf_gcd_ec_nonzero_have. ((((exists ff_h_cf_ec_nonzero_have_initial_state. ff_h_cf_ec_nonzero_have_initial_state + S (((cf_gcd_ec_nonzero_have) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_nonzero_have) + (((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_ec_nonzero_have_initial_state. h = ff_q_cf_ec_nonzero_have_initial_state * S ((S (0)) * e) + (((cf_gcd_ec_nonzero_have) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_nonzero_have) + (((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_ec_nonzero_have_terminal_state. ff_h_cf_ec_nonzero_have_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 (S k)) * e)) /\ exists ff_q_cf_ec_nonzero_have_terminal_state. h = ff_q_cf_ec_nonzero_have_terminal_state * S ((S (S k)) * 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_ec_nonzero_have. (exists ff_lt_cf_ec_nonzero_have_index. ff_lt_cf_ec_nonzero_have_index + S cf_index_ec_nonzero_have = S k) -> exists cf_old_a_ec_nonzero_have cf_old_b_ec_nonzero_have cf_tail_ec_nonzero_have cf_new_a_ec_nonzero_have cf_new_b_ec_nonzero_have cf_head_ec_nonzero_have cf_quotient_ec_nonzero_have. ((((exists ff_h_cf_ec_nonzero_have_previous_state. ff_h_cf_ec_nonzero_have_previous_state + S (((cf_old_a_ec_nonzero_have) + (((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) * S ((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) + ((cf_tail_ec_nonzero_have) + (cf_tail_ec_nonzero_have)))) * S ((cf_old_a_ec_nonzero_have) + (((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) * S ((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) + ((cf_tail_ec_nonzero_have) + (cf_tail_ec_nonzero_have)))) + ((((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) * S ((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) + ((cf_tail_ec_nonzero_have) + (cf_tail_ec_nonzero_have))) + (((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) * S ((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) + ((cf_tail_ec_nonzero_have) + (cf_tail_ec_nonzero_have))))) = S ((S (cf_index_ec_nonzero_have)) * e)) /\ exists ff_q_cf_ec_nonzero_have_previous_state. h = ff_q_cf_ec_nonzero_have_previous_state * S ((S (cf_index_ec_nonzero_have)) * e) + (((cf_old_a_ec_nonzero_have) + (((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) * S ((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) + ((cf_tail_ec_nonzero_have) + (cf_tail_ec_nonzero_have)))) * S ((cf_old_a_ec_nonzero_have) + (((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) * S ((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) + ((cf_tail_ec_nonzero_have) + (cf_tail_ec_nonzero_have)))) + ((((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) * S ((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) + ((cf_tail_ec_nonzero_have) + (cf_tail_ec_nonzero_have))) + (((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) * S ((cf_old_b_ec_nonzero_have) + (cf_tail_ec_nonzero_have)) + ((cf_tail_ec_nonzero_have) + (cf_tail_ec_nonzero_have))))))) /\ ((((exists ff_h_cf_ec_nonzero_have_following_state. ff_h_cf_ec_nonzero_have_following_state + S (((cf_new_a_ec_nonzero_have) + (((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) * S ((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) + ((cf_head_ec_nonzero_have) + (cf_head_ec_nonzero_have)))) * S ((cf_new_a_ec_nonzero_have) + (((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) * S ((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) + ((cf_head_ec_nonzero_have) + (cf_head_ec_nonzero_have)))) + ((((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) * S ((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) + ((cf_head_ec_nonzero_have) + (cf_head_ec_nonzero_have))) + (((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) * S ((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) + ((cf_head_ec_nonzero_have) + (cf_head_ec_nonzero_have))))) = S ((S (S cf_index_ec_nonzero_have)) * e)) /\ exists ff_q_cf_ec_nonzero_have_following_state. h = ff_q_cf_ec_nonzero_have_following_state * S ((S (S cf_index_ec_nonzero_have)) * e) + (((cf_new_a_ec_nonzero_have) + (((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) * S ((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) + ((cf_head_ec_nonzero_have) + (cf_head_ec_nonzero_have)))) * S ((cf_new_a_ec_nonzero_have) + (((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) * S ((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) + ((cf_head_ec_nonzero_have) + (cf_head_ec_nonzero_have)))) + ((((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) * S ((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) + ((cf_head_ec_nonzero_have) + (cf_head_ec_nonzero_have))) + (((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) * S ((cf_new_b_ec_nonzero_have) + (cf_head_ec_nonzero_have)) + ((cf_head_ec_nonzero_have) + (cf_head_ec_nonzero_have))))))) /\ (cf_new_b_ec_nonzero_have = cf_old_a_ec_nonzero_have /\ (cf_new_a_ec_nonzero_have = cf_new_b_ec_nonzero_have * cf_quotient_ec_nonzero_have + cf_old_b_ec_nonzero_have /\ ((exists ff_lt_cf_ec_nonzero_have_remainder. ff_lt_cf_ec_nonzero_have_remainder + S cf_old_b_ec_nonzero_have = cf_new_b_ec_nonzero_have) /\ (cf_head_ec_nonzero_have = S ((cf_quotient_ec_nonzero_have + cf_tail_ec_nonzero_have) * S (cf_quotient_ec_nonzero_have + cf_tail_ec_nonzero_have) + (cf_tail_ec_nonzero_have + cf_tail_ec_nonzero_have))))))))))))
  10. 0010apply continued_fraction_nonzero_divisor_exists
  11. 0011exact hb
  12. 0012cases htrace
  13. 0013cases htrace_witness
  14. 0014cases htrace_witness_witness
  15. 0015cases htrace_witness_witness_witness
  16. 0016cases htrace_witness_witness_witness_witness
  17. 0017exists x
  18. 0018exists x4
  19. 0019exists x1
  20. 0020exists x2
  21. 0021exists x3
  22. 0022split
  23. 0023exact htrace_witness_witness_witness_witness_right
  24. 0024exact gcd_exists_relational_witness