BA0029

cf_convergent_old_history_zero_elimination

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 1 declared prerequisite and contains 24 exact native proof lines.

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

Proof neighborhood

Direct dependencies

BA0028 cf_convergent_old_history_state_unique

Direct dependents

BA002D cf_convergent_old_history_nonempty_head BA0047 cf_convergent_full_matrix_is_exact

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

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.

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 exact 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