EC000F

euclidean_gcd_execution_linear_bound

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every pair has a complete actual beta-coded Euclidean execution, a genuinely certified gcd output, and the exact constructive linear bound steps <= initial divisor; the stronger BitLen bound remains open.

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.

Exact expanded first-order arithmetic statement

forall a b. exists g l. ((exists ec_list_linear ec_history_linear ec_scale_linear. ((exists cf_gcd_ec_linear_trace. ((((exists ff_h_cf_ec_linear_trace_initial_state. ff_h_cf_ec_linear_trace_initial_state + S (((cf_gcd_ec_linear_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_linear_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_linear)) /\ exists ff_q_cf_ec_linear_trace_initial_state. ec_history_linear = ff_q_cf_ec_linear_trace_initial_state * S ((S (0)) * ec_scale_linear) + (((cf_gcd_ec_linear_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_linear_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_linear_trace_terminal_state. ff_h_cf_ec_linear_trace_terminal_state + S (((a) + (((b) + (ec_list_linear)) * S ((b) + (ec_list_linear)) + ((ec_list_linear) + (ec_list_linear)))) * S ((a) + (((b) + (ec_list_linear)) * S ((b) + (ec_list_linear)) + ((ec_list_linear) + (ec_list_linear)))) + ((((b) + (ec_list_linear)) * S ((b) + (ec_list_linear)) + ((ec_list_linear) + (ec_list_linear))) + (((b) + (ec_list_linear)) * S ((b) + (ec_list_linear)) + ((ec_list_linear) + (ec_list_linear))))) = S ((S (l)) * ec_scale_linear)) /\ exists ff_q_cf_ec_linear_trace_terminal_state. ec_history_linear = ff_q_cf_ec_linear_trace_terminal_state * S ((S (l)) * ec_scale_linear) + (((a) + (((b) + (ec_list_linear)) * S ((b) + (ec_list_linear)) + ((ec_list_linear) + (ec_list_linear)))) * S ((a) + (((b) + (ec_list_linear)) * S ((b) + (ec_list_linear)) + ((ec_list_linear) + (ec_list_linear)))) + ((((b) + (ec_list_linear)) * S ((b) + (ec_list_linear)) + ((ec_list_linear) + (ec_list_linear))) + (((b) + (ec_list_linear)) * S ((b) + (ec_list_linear)) + ((ec_list_linear) + (ec_list_linear))))))) /\ forall cf_index_ec_linear_trace. (exists ff_lt_cf_ec_linear_trace_index. ff_lt_cf_ec_linear_trace_index + S cf_index_ec_linear_trace = l) -> exists cf_old_a_ec_linear_trace cf_old_b_ec_linear_trace cf_tail_ec_linear_trace cf_new_a_ec_linear_trace cf_new_b_ec_linear_trace cf_head_ec_linear_trace cf_quotient_ec_linear_trace. ((((exists ff_h_cf_ec_linear_trace_previous_state. ff_h_cf_ec_linear_trace_previous_state + S (((cf_old_a_ec_linear_trace) + (((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) * S ((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) + ((cf_tail_ec_linear_trace) + (cf_tail_ec_linear_trace)))) * S ((cf_old_a_ec_linear_trace) + (((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) * S ((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) + ((cf_tail_ec_linear_trace) + (cf_tail_ec_linear_trace)))) + ((((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) * S ((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) + ((cf_tail_ec_linear_trace) + (cf_tail_ec_linear_trace))) + (((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) * S ((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) + ((cf_tail_ec_linear_trace) + (cf_tail_ec_linear_trace))))) = S ((S (cf_index_ec_linear_trace)) * ec_scale_linear)) /\ exists ff_q_cf_ec_linear_trace_previous_state. ec_history_linear = ff_q_cf_ec_linear_trace_previous_state * S ((S (cf_index_ec_linear_trace)) * ec_scale_linear) + (((cf_old_a_ec_linear_trace) + (((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) * S ((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) + ((cf_tail_ec_linear_trace) + (cf_tail_ec_linear_trace)))) * S ((cf_old_a_ec_linear_trace) + (((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) * S ((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) + ((cf_tail_ec_linear_trace) + (cf_tail_ec_linear_trace)))) + ((((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) * S ((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) + ((cf_tail_ec_linear_trace) + (cf_tail_ec_linear_trace))) + (((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) * S ((cf_old_b_ec_linear_trace) + (cf_tail_ec_linear_trace)) + ((cf_tail_ec_linear_trace) + (cf_tail_ec_linear_trace))))))) /\ ((((exists ff_h_cf_ec_linear_trace_following_state. ff_h_cf_ec_linear_trace_following_state + S (((cf_new_a_ec_linear_trace) + (((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) * S ((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) + ((cf_head_ec_linear_trace) + (cf_head_ec_linear_trace)))) * S ((cf_new_a_ec_linear_trace) + (((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) * S ((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) + ((cf_head_ec_linear_trace) + (cf_head_ec_linear_trace)))) + ((((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) * S ((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) + ((cf_head_ec_linear_trace) + (cf_head_ec_linear_trace))) + (((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) * S ((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) + ((cf_head_ec_linear_trace) + (cf_head_ec_linear_trace))))) = S ((S (S cf_index_ec_linear_trace)) * ec_scale_linear)) /\ exists ff_q_cf_ec_linear_trace_following_state. ec_history_linear = ff_q_cf_ec_linear_trace_following_state * S ((S (S cf_index_ec_linear_trace)) * ec_scale_linear) + (((cf_new_a_ec_linear_trace) + (((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) * S ((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) + ((cf_head_ec_linear_trace) + (cf_head_ec_linear_trace)))) * S ((cf_new_a_ec_linear_trace) + (((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) * S ((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) + ((cf_head_ec_linear_trace) + (cf_head_ec_linear_trace)))) + ((((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) * S ((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) + ((cf_head_ec_linear_trace) + (cf_head_ec_linear_trace))) + (((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) * S ((cf_new_b_ec_linear_trace) + (cf_head_ec_linear_trace)) + ((cf_head_ec_linear_trace) + (cf_head_ec_linear_trace))))))) /\ (cf_new_b_ec_linear_trace = cf_old_a_ec_linear_trace /\ (cf_new_a_ec_linear_trace = cf_new_b_ec_linear_trace * cf_quotient_ec_linear_trace + cf_old_b_ec_linear_trace /\ ((exists ff_lt_cf_ec_linear_trace_remainder. ff_lt_cf_ec_linear_trace_remainder + S cf_old_b_ec_linear_trace = cf_new_b_ec_linear_trace) /\ (cf_head_ec_linear_trace = S ((cf_quotient_ec_linear_trace + cf_tail_ec_linear_trace) * S (cf_quotient_ec_linear_trace + cf_tail_ec_linear_trace) + (cf_tail_ec_linear_trace + cf_tail_ec_linear_trace))))))))))) /\ ((((exists ec_gcd_left_linear_result. a = g * ec_gcd_left_linear_result) /\ (exists ec_gcd_right_linear_result. b = g * ec_gcd_right_linear_result)) /\ forall ec_gcd_common_linear_result. (exists ec_gcd_common_left_linear_result. a = ec_gcd_common_linear_result * ec_gcd_common_left_linear_result) -> (exists ec_gcd_common_right_linear_result. b = ec_gcd_common_linear_result * ec_gcd_common_right_linear_result) -> exists ec_gcd_greatest_linear_result. g = ec_gcd_common_linear_result * ec_gcd_greatest_linear_result)))) /\ exists gap. gap + l = b)

Constructive proof overview

Generated structural guide

Every pair has a complete actual beta-coded Euclidean execution, a genuinely certified gcd output, and the exact constructive linear bound steps <= initial divisor; the stronger BitLen bound remains open.

The unchanged tactic script uses 2 declared prerequisites and contains 22 exact native proof lines.

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

Proof neighborhood

Direct dependencies

EC0009 euclidean_trace_exists_linear gcd_exists_relational Stable theorem; checked-use authorized

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

22 script commands · 10 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.

Named ingredients (1)
euclidean trace exists linear
01Fix variables and assumptionsL1–2

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

  1. L1
    intro a
  2. L2
    intro b
02Use earlier factsL3–4

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

  1. L3
    specialize gcd_exists_relational a
  2. L4
    specialize gcd_exists_relational b
03Separate the logical casesL5–5

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

  1. L5
    cases gcd_exists_relational
04Use earlier factsL6–7

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

  1. L6
    specialize euclidean_trace_exists_linear a
  2. L7
    specialize euclidean_trace_exists_linear b
05Separate the logical casesL8–12

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

  1. L8
    cases euclidean_trace_exists_linear
  2. L9
    cases euclidean_trace_exists_linear_witness
  3. L10
    cases euclidean_trace_exists_linear_witness_witness
  4. L11
    cases euclidean_trace_exists_linear_witness_witness_witness
  5. L12
    cases euclidean_trace_exists_linear_witness_witness_witness_witness
06Construct an explicit witnessL13–14

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

  1. L13
    exists x
  2. L14
    exists x4
07Separate the logical casesL15–15

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

  1. L15
    split
08Construct an explicit witnessL16–18

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

  1. L16
    exists x1
  2. L17
    exists x2
  3. L18
    exists x3
09Separate the logical casesL19–19

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

  1. L19
    split
10Use earlier factsL20–22

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

  1. L20
    exact euclidean_trace_exists_linear_witness_witness_witness_witness_left
  2. L21
    exact gcd_exists_relational_witness
  3. L22
    exact euclidean_trace_exists_linear_witness_witness_witness_witness_right

Library-wide reading audit

Original exact command ledger · 22 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003specialize gcd_exists_relational a
  4. 0004specialize gcd_exists_relational b
  5. 0005cases gcd_exists_relational
  6. 0006specialize euclidean_trace_exists_linear a
  7. 0007specialize euclidean_trace_exists_linear b
  8. 0008cases euclidean_trace_exists_linear
  9. 0009cases euclidean_trace_exists_linear_witness
  10. 0010cases euclidean_trace_exists_linear_witness_witness
  11. 0011cases euclidean_trace_exists_linear_witness_witness_witness
  12. 0012cases euclidean_trace_exists_linear_witness_witness_witness_witness
  13. 0013exists x
  14. 0014exists x4
  15. 0015split
  16. 0016exists x1
  17. 0017exists x2
  18. 0018exists x3
  19. 0019split
  20. 0020exact euclidean_trace_exists_linear_witness_witness_witness_witness_left
  21. 0021exact gcd_exists_relational_witness
  22. 0022exact euclidean_trace_exists_linear_witness_witness_witness_witness_right