BA0029

cf_convergent_old_history_zero_elimination

An empty actual Euclidean history has divisor zero and the empty quotient list, not a spurious convergent.

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

The initial 0/1 convergent is included: u is natural, not necessarily positive. Comparison denominators are strictly smaller and positive. Signed competitors are represented by an arbitrary difference rp−rn. Approximation inequalities are proved from the trace, never stored as assumptions in Convergent.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ s. ∀ h. ∀ e. ContinuedFractionTrace(a,b,s,h,e,0) → b = 0 ∧ s = 0

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

Definition DAG

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

Actual proof prerequisites

cf_convergent_old_history_state_unique
Original expanded first-order statement 
forall a b s h e. (exists cf_gcd_old_zero. ((((exists ff_h_cf_old_zero_initial_state. ff_h_cf_old_zero_initial_state + S (((cf_gcd_old_zero) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_old_zero) + (((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_old_zero_initial_state. h = ff_q_cf_old_zero_initial_state * S ((S (0)) * e) + (((cf_gcd_old_zero) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_old_zero) + (((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_old_zero_terminal_state. ff_h_cf_old_zero_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 (0)) * e)) /\ exists ff_q_cf_old_zero_terminal_state. h = ff_q_cf_old_zero_terminal_state * S ((S (0)) * 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_old_zero. (exists ff_lt_cf_old_zero_index. ff_lt_cf_old_zero_index + S cf_index_old_zero = 0) -> exists cf_old_a_old_zero cf_old_b_old_zero cf_tail_old_zero cf_new_a_old_zero cf_new_b_old_zero cf_head_old_zero cf_quotient_old_zero. ((((exists ff_h_cf_old_zero_previous_state. ff_h_cf_old_zero_previous_state + S (((cf_old_a_old_zero) + (((cf_old_b_old_zero) + (cf_tail_old_zero)) * S ((cf_old_b_old_zero) + (cf_tail_old_zero)) + ((cf_tail_old_zero) + (cf_tail_old_zero)))) * S ((cf_old_a_old_zero) + (((cf_old_b_old_zero) + (cf_tail_old_zero)) * S ((cf_old_b_old_zero) + (cf_tail_old_zero)) + ((cf_tail_old_zero) + (cf_tail_old_zero)))) + ((((cf_old_b_old_zero) + (cf_tail_old_zero)) * S ((cf_old_b_old_zero) + (cf_tail_old_zero)) + ((cf_tail_old_zero) + (cf_tail_old_zero))) + (((cf_old_b_old_zero) + (cf_tail_old_zero)) * S ((cf_old_b_old_zero) + (cf_tail_old_zero)) + ((cf_tail_old_zero) + (cf_tail_old_zero))))) = S ((S (cf_index_old_zero)) * e)) /\ exists ff_q_cf_old_zero_previous_state. h = ff_q_cf_old_zero_previous_state * S ((S (cf_index_old_zero)) * e) + (((cf_old_a_old_zero) + (((cf_old_b_old_zero) + (cf_tail_old_zero)) * S ((cf_old_b_old_zero) + (cf_tail_old_zero)) + ((cf_tail_old_zero) + (cf_tail_old_zero)))) * S ((cf_old_a_old_zero) + (((cf_old_b_old_zero) + (cf_tail_old_zero)) * S ((cf_old_b_old_zero) + (cf_tail_old_zero)) + ((cf_tail_old_zero) + (cf_tail_old_zero)))) + ((((cf_old_b_old_zero) + (cf_tail_old_zero)) * S ((cf_old_b_old_zero) + (cf_tail_old_zero)) + ((cf_tail_old_zero) + (cf_tail_old_zero))) + (((cf_old_b_old_zero) + (cf_tail_old_zero)) * S ((cf_old_b_old_zero) + (cf_tail_old_zero)) + ((cf_tail_old_zero) + (cf_tail_old_zero))))))) /\ ((((exists ff_h_cf_old_zero_following_state. ff_h_cf_old_zero_following_state + S (((cf_new_a_old_zero) + (((cf_new_b_old_zero) + (cf_head_old_zero)) * S ((cf_new_b_old_zero) + (cf_head_old_zero)) + ((cf_head_old_zero) + (cf_head_old_zero)))) * S ((cf_new_a_old_zero) + (((cf_new_b_old_zero) + (cf_head_old_zero)) * S ((cf_new_b_old_zero) + (cf_head_old_zero)) + ((cf_head_old_zero) + (cf_head_old_zero)))) + ((((cf_new_b_old_zero) + (cf_head_old_zero)) * S ((cf_new_b_old_zero) + (cf_head_old_zero)) + ((cf_head_old_zero) + (cf_head_old_zero))) + (((cf_new_b_old_zero) + (cf_head_old_zero)) * S ((cf_new_b_old_zero) + (cf_head_old_zero)) + ((cf_head_old_zero) + (cf_head_old_zero))))) = S ((S (S cf_index_old_zero)) * e)) /\ exists ff_q_cf_old_zero_following_state. h = ff_q_cf_old_zero_following_state * S ((S (S cf_index_old_zero)) * e) + (((cf_new_a_old_zero) + (((cf_new_b_old_zero) + (cf_head_old_zero)) * S ((cf_new_b_old_zero) + (cf_head_old_zero)) + ((cf_head_old_zero) + (cf_head_old_zero)))) * S ((cf_new_a_old_zero) + (((cf_new_b_old_zero) + (cf_head_old_zero)) * S ((cf_new_b_old_zero) + (cf_head_old_zero)) + ((cf_head_old_zero) + (cf_head_old_zero)))) + ((((cf_new_b_old_zero) + (cf_head_old_zero)) * S ((cf_new_b_old_zero) + (cf_head_old_zero)) + ((cf_head_old_zero) + (cf_head_old_zero))) + (((cf_new_b_old_zero) + (cf_head_old_zero)) * S ((cf_new_b_old_zero) + (cf_head_old_zero)) + ((cf_head_old_zero) + (cf_head_old_zero))))))) /\ (cf_new_b_old_zero = cf_old_a_old_zero /\ (cf_new_a_old_zero = cf_new_b_old_zero * cf_quotient_old_zero + cf_old_b_old_zero /\ ((exists ff_lt_cf_old_zero_remainder. ff_lt_cf_old_zero_remainder + S cf_old_b_old_zero = cf_new_b_old_zero) /\ (cf_head_old_zero = S ((cf_quotient_old_zero + cf_tail_old_zero) * S (cf_quotient_old_zero + cf_tail_old_zero) + (cf_tail_old_zero + cf_tail_old_zero))))))))))) -> b = 0 /\ s = 0

Complete tactic proof in conservative notation

All 24 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

24 script commands · 6 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.

Named ingredients (1)
cf convergent old history state unique
01Fix variables and assumptionsL1–6

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 ht
02Separate the logical casesL7–9

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

  1. L7
    cases ht
  2. L8
    cases ht_witness
  3. L9
    cases ht_witness_right
03Establish heqL10–19

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

  1. L10
    have heq : ((a = x) /\ ((b = 0) /\ (s = 0)))
  2. L11
    specialize cf_convergent_old_history_state_unique (h)
  3. L12
    specialize cf_convergent_old_history_state_unique (e)
  4. L13
    specialize cf_convergent_old_history_state_unique (0)
  5. L14
    specialize cf_convergent_old_history_state_unique (a)
  6. L15
    specialize cf_convergent_old_history_state_unique (b)
  7. L16
    specialize cf_convergent_old_history_state_unique (s)
  8. L17
    specialize cf_convergent_old_history_state_unique (x)
  9. L18
    specialize cf_convergent_old_history_state_unique (0)
  10. L19
    specialize cf_convergent_old_history_state_unique (0)
04Use earlier factsL20–22

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

  1. L20
    apply cf_convergent_old_history_state_unique
  2. L21
    exact ht_witness_right_left
  3. L22
    exact ht_witness_left
05Separate the logical casesL23–23

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

  1. L23
    cases heq
06Use earlier factsL24–24

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

  1. L24
    exact heq_right

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro s
  4. 0004intro h
  5. 0005intro e
  6. 0006intro ht
  7. 0007cases ht
  8. 0008cases ht_witness
  9. 0009cases ht_witness_right
  10. 0010have heq : ((a = x) /\ ((b = 0) /\ (s = 0)))
  11. 0011specialize cf_convergent_old_history_state_unique (h)
  12. 0012specialize cf_convergent_old_history_state_unique (e)
  13. 0013specialize cf_convergent_old_history_state_unique (0)
  14. 0014specialize cf_convergent_old_history_state_unique (a)
  15. 0015specialize cf_convergent_old_history_state_unique (b)
  16. 0016specialize cf_convergent_old_history_state_unique (s)
  17. 0017specialize cf_convergent_old_history_state_unique (x)
  18. 0018specialize cf_convergent_old_history_state_unique (0)
  19. 0019specialize cf_convergent_old_history_state_unique (0)
  20. 0020apply cf_convergent_old_history_state_unique
  21. 0021exact ht_witness_right_left
  22. 0022exact ht_witness_left
  23. 0023cases heq
  24. 0024exact heq_right