EC0007

euclidean_trace_bound_weaken

An already witnessed complete beta-coded history remains within the successor of its original linear step budget.

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. (∃ x. ∃ y. ∃ z. ∃ n. ContinuedFractionTrace(a,b,x,y,z,n) ∧ n ≤ B) → ∃ x. ∃ y. ∃ z. ∃ n. ContinuedFractionTrace(a,b,x,y,z,n) ∧ n ≤ S B

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

Definition DAG

ContinuedFractionTrace(a,b,s,u,v,ell) · 2

Actual proof prerequisites

le_succ · checked external prerequisite
Original expanded first-order statement 
forall a b B. (exists s h e l. ((exists cf_gcd_ec_induction_bounded. ((((exists ff_h_cf_ec_induction_bounded_initial_state. ff_h_cf_ec_induction_bounded_initial_state + S (((cf_gcd_ec_induction_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_induction_bounded) + (((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_induction_bounded_initial_state. h = ff_q_cf_ec_induction_bounded_initial_state * S ((S (0)) * e) + (((cf_gcd_ec_induction_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_induction_bounded) + (((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_induction_bounded_terminal_state. ff_h_cf_ec_induction_bounded_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_ec_induction_bounded_terminal_state. h = ff_q_cf_ec_induction_bounded_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_ec_induction_bounded. (exists ff_lt_cf_ec_induction_bounded_index. ff_lt_cf_ec_induction_bounded_index + S cf_index_ec_induction_bounded = l) -> exists cf_old_a_ec_induction_bounded cf_old_b_ec_induction_bounded cf_tail_ec_induction_bounded cf_new_a_ec_induction_bounded cf_new_b_ec_induction_bounded cf_head_ec_induction_bounded cf_quotient_ec_induction_bounded. ((((exists ff_h_cf_ec_induction_bounded_previous_state. ff_h_cf_ec_induction_bounded_previous_state + S (((cf_old_a_ec_induction_bounded) + (((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded)))) * S ((cf_old_a_ec_induction_bounded) + (((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded)))) + ((((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded))) + (((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded))))) = S ((S (cf_index_ec_induction_bounded)) * e)) /\ exists ff_q_cf_ec_induction_bounded_previous_state. h = ff_q_cf_ec_induction_bounded_previous_state * S ((S (cf_index_ec_induction_bounded)) * e) + (((cf_old_a_ec_induction_bounded) + (((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded)))) * S ((cf_old_a_ec_induction_bounded) + (((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded)))) + ((((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded))) + (((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded))))))) /\ ((((exists ff_h_cf_ec_induction_bounded_following_state. ff_h_cf_ec_induction_bounded_following_state + S (((cf_new_a_ec_induction_bounded) + (((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded)))) * S ((cf_new_a_ec_induction_bounded) + (((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded)))) + ((((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded))) + (((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded))))) = S ((S (S cf_index_ec_induction_bounded)) * e)) /\ exists ff_q_cf_ec_induction_bounded_following_state. h = ff_q_cf_ec_induction_bounded_following_state * S ((S (S cf_index_ec_induction_bounded)) * e) + (((cf_new_a_ec_induction_bounded) + (((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded)))) * S ((cf_new_a_ec_induction_bounded) + (((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded)))) + ((((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded))) + (((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded))))))) /\ (cf_new_b_ec_induction_bounded = cf_old_a_ec_induction_bounded /\ (cf_new_a_ec_induction_bounded = cf_new_b_ec_induction_bounded * cf_quotient_ec_induction_bounded + cf_old_b_ec_induction_bounded /\ ((exists ff_lt_cf_ec_induction_bounded_remainder. ff_lt_cf_ec_induction_bounded_remainder + S cf_old_b_ec_induction_bounded = cf_new_b_ec_induction_bounded) /\ (cf_head_ec_induction_bounded = S ((cf_quotient_ec_induction_bounded + cf_tail_ec_induction_bounded) * S (cf_quotient_ec_induction_bounded + cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded + cf_tail_ec_induction_bounded))))))))))) /\ (exists ec_bound_gap_induction. ec_bound_gap_induction + l = B))) -> (exists s h e l. ((exists cf_gcd_ec_weakened_bounded. ((((exists ff_h_cf_ec_weakened_bounded_initial_state. ff_h_cf_ec_weakened_bounded_initial_state + S (((cf_gcd_ec_weakened_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_weakened_bounded) + (((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_weakened_bounded_initial_state. h = ff_q_cf_ec_weakened_bounded_initial_state * S ((S (0)) * e) + (((cf_gcd_ec_weakened_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_weakened_bounded) + (((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_weakened_bounded_terminal_state. ff_h_cf_ec_weakened_bounded_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_ec_weakened_bounded_terminal_state. h = ff_q_cf_ec_weakened_bounded_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_ec_weakened_bounded. (exists ff_lt_cf_ec_weakened_bounded_index. ff_lt_cf_ec_weakened_bounded_index + S cf_index_ec_weakened_bounded = l) -> exists cf_old_a_ec_weakened_bounded cf_old_b_ec_weakened_bounded cf_tail_ec_weakened_bounded cf_new_a_ec_weakened_bounded cf_new_b_ec_weakened_bounded cf_head_ec_weakened_bounded cf_quotient_ec_weakened_bounded. ((((exists ff_h_cf_ec_weakened_bounded_previous_state. ff_h_cf_ec_weakened_bounded_previous_state + S (((cf_old_a_ec_weakened_bounded) + (((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) * S ((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) + ((cf_tail_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)))) * S ((cf_old_a_ec_weakened_bounded) + (((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) * S ((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) + ((cf_tail_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)))) + ((((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) * S ((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) + ((cf_tail_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded))) + (((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) * S ((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) + ((cf_tail_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded))))) = S ((S (cf_index_ec_weakened_bounded)) * e)) /\ exists ff_q_cf_ec_weakened_bounded_previous_state. h = ff_q_cf_ec_weakened_bounded_previous_state * S ((S (cf_index_ec_weakened_bounded)) * e) + (((cf_old_a_ec_weakened_bounded) + (((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) * S ((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) + ((cf_tail_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)))) * S ((cf_old_a_ec_weakened_bounded) + (((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) * S ((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) + ((cf_tail_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)))) + ((((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) * S ((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) + ((cf_tail_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded))) + (((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) * S ((cf_old_b_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded)) + ((cf_tail_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded))))))) /\ ((((exists ff_h_cf_ec_weakened_bounded_following_state. ff_h_cf_ec_weakened_bounded_following_state + S (((cf_new_a_ec_weakened_bounded) + (((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) * S ((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) + ((cf_head_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)))) * S ((cf_new_a_ec_weakened_bounded) + (((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) * S ((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) + ((cf_head_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)))) + ((((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) * S ((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) + ((cf_head_ec_weakened_bounded) + (cf_head_ec_weakened_bounded))) + (((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) * S ((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) + ((cf_head_ec_weakened_bounded) + (cf_head_ec_weakened_bounded))))) = S ((S (S cf_index_ec_weakened_bounded)) * e)) /\ exists ff_q_cf_ec_weakened_bounded_following_state. h = ff_q_cf_ec_weakened_bounded_following_state * S ((S (S cf_index_ec_weakened_bounded)) * e) + (((cf_new_a_ec_weakened_bounded) + (((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) * S ((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) + ((cf_head_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)))) * S ((cf_new_a_ec_weakened_bounded) + (((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) * S ((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) + ((cf_head_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)))) + ((((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) * S ((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) + ((cf_head_ec_weakened_bounded) + (cf_head_ec_weakened_bounded))) + (((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) * S ((cf_new_b_ec_weakened_bounded) + (cf_head_ec_weakened_bounded)) + ((cf_head_ec_weakened_bounded) + (cf_head_ec_weakened_bounded))))))) /\ (cf_new_b_ec_weakened_bounded = cf_old_a_ec_weakened_bounded /\ (cf_new_a_ec_weakened_bounded = cf_new_b_ec_weakened_bounded * cf_quotient_ec_weakened_bounded + cf_old_b_ec_weakened_bounded /\ ((exists ff_lt_cf_ec_weakened_bounded_remainder. ff_lt_cf_ec_weakened_bounded_remainder + S cf_old_b_ec_weakened_bounded = cf_new_b_ec_weakened_bounded) /\ (cf_head_ec_weakened_bounded = S ((cf_quotient_ec_weakened_bounded + cf_tail_ec_weakened_bounded) * S (cf_quotient_ec_weakened_bounded + cf_tail_ec_weakened_bounded) + (cf_tail_ec_weakened_bounded + cf_tail_ec_weakened_bounded))))))))))) /\ (exists ec_bound_gap_weakened. ec_bound_gap_weakened + l = S B)))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

19 script commands · 5 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–4

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro B
  4. L4
    intro htrace
02Separate the logical casesL5–9

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

  1. L5
    cases htrace
  2. L6
    cases htrace_witness
  3. L7
    cases htrace_witness_witness
  4. L8
    cases htrace_witness_witness_witness
  5. L9
    cases htrace_witness_witness_witness_witness
03Construct an explicit witnessL10–13

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

  1. L10
    exists x
  2. L11
    exists x1
  3. L12
    exists x2
  4. L13
    exists x3
04Separate the logical casesL14–14

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

  1. L14
    split
05Use earlier factsL15–19

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

  1. L15
    exact htrace_witness_witness_witness_witness_left
  2. L16
    specialize le_succ x3
  3. L17
    specialize le_succ B
  4. L18
    apply le_succ
  5. L19
    exact htrace_witness_witness_witness_witness_right

Library-wide reading audit

Original defined command ledger · 19 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro B
  4. 0004intro htrace
  5. 0005cases htrace
  6. 0006cases htrace_witness
  7. 0007cases htrace_witness_witness
  8. 0008cases htrace_witness_witness_witness
  9. 0009cases htrace_witness_witness_witness_witness
  10. 0010exists x
  11. 0011exists x1
  12. 0012exists x2
  13. 0013exists x3
  14. 0014split
  15. 0015exact htrace_witness_witness_witness_witness_left
  16. 0016specialize le_succ x3
  17. 0017specialize le_succ B
  18. 0018apply le_succ
  19. 0019exact htrace_witness_witness_witness_witness_right