CF0008

continued_fraction_positive_nonempty_exists

Every positive rational input has a complete simple continued fraction whose exact cell-coded quotient list is nonempty.

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

Exact theorem in conservative defined notation

∀ a. ∀ b. ¬a = 0 → ¬b = 0 → ∃ x. ContinuedFraction(a,b,x) ∧ ¬x = 0

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

Definition DAG

ContinuedFraction(a,b,s) · 1

Actual proof prerequisites

nonzero_is_succ · checked external prerequisitecontinued_fraction_nonzero_divisor_exists
Original expanded first-order statement 
forall a b. ~(a = 0) -> ~(b = 0) -> exists s. ((exists cf_a_pred_positive_result cf_b_pred_positive_result cf_code_positive_result cf_scale_positive_result cf_length_pred_positive_result. (a = S cf_a_pred_positive_result /\ (b = S cf_b_pred_positive_result /\ (exists cf_gcd_positive_result_trace. ((((exists ff_h_cf_positive_result_trace_initial_state. ff_h_cf_positive_result_trace_initial_state + S (((cf_gcd_positive_result_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_positive_result_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)) * cf_scale_positive_result)) /\ exists ff_q_cf_positive_result_trace_initial_state. cf_code_positive_result = ff_q_cf_positive_result_trace_initial_state * S ((S (0)) * cf_scale_positive_result) + (((cf_gcd_positive_result_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_positive_result_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_positive_result_trace_terminal_state. ff_h_cf_positive_result_trace_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 cf_length_pred_positive_result)) * cf_scale_positive_result)) /\ exists ff_q_cf_positive_result_trace_terminal_state. cf_code_positive_result = ff_q_cf_positive_result_trace_terminal_state * S ((S (S cf_length_pred_positive_result)) * cf_scale_positive_result) + (((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_positive_result_trace. (exists ff_lt_cf_positive_result_trace_index. ff_lt_cf_positive_result_trace_index + S cf_index_positive_result_trace = S cf_length_pred_positive_result) -> exists cf_old_a_positive_result_trace cf_old_b_positive_result_trace cf_tail_positive_result_trace cf_new_a_positive_result_trace cf_new_b_positive_result_trace cf_head_positive_result_trace cf_quotient_positive_result_trace. ((((exists ff_h_cf_positive_result_trace_previous_state. ff_h_cf_positive_result_trace_previous_state + S (((cf_old_a_positive_result_trace) + (((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) * S ((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) + ((cf_tail_positive_result_trace) + (cf_tail_positive_result_trace)))) * S ((cf_old_a_positive_result_trace) + (((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) * S ((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) + ((cf_tail_positive_result_trace) + (cf_tail_positive_result_trace)))) + ((((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) * S ((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) + ((cf_tail_positive_result_trace) + (cf_tail_positive_result_trace))) + (((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) * S ((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) + ((cf_tail_positive_result_trace) + (cf_tail_positive_result_trace))))) = S ((S (cf_index_positive_result_trace)) * cf_scale_positive_result)) /\ exists ff_q_cf_positive_result_trace_previous_state. cf_code_positive_result = ff_q_cf_positive_result_trace_previous_state * S ((S (cf_index_positive_result_trace)) * cf_scale_positive_result) + (((cf_old_a_positive_result_trace) + (((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) * S ((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) + ((cf_tail_positive_result_trace) + (cf_tail_positive_result_trace)))) * S ((cf_old_a_positive_result_trace) + (((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) * S ((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) + ((cf_tail_positive_result_trace) + (cf_tail_positive_result_trace)))) + ((((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) * S ((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) + ((cf_tail_positive_result_trace) + (cf_tail_positive_result_trace))) + (((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) * S ((cf_old_b_positive_result_trace) + (cf_tail_positive_result_trace)) + ((cf_tail_positive_result_trace) + (cf_tail_positive_result_trace))))))) /\ ((((exists ff_h_cf_positive_result_trace_following_state. ff_h_cf_positive_result_trace_following_state + S (((cf_new_a_positive_result_trace) + (((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) * S ((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) + ((cf_head_positive_result_trace) + (cf_head_positive_result_trace)))) * S ((cf_new_a_positive_result_trace) + (((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) * S ((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) + ((cf_head_positive_result_trace) + (cf_head_positive_result_trace)))) + ((((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) * S ((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) + ((cf_head_positive_result_trace) + (cf_head_positive_result_trace))) + (((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) * S ((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) + ((cf_head_positive_result_trace) + (cf_head_positive_result_trace))))) = S ((S (S cf_index_positive_result_trace)) * cf_scale_positive_result)) /\ exists ff_q_cf_positive_result_trace_following_state. cf_code_positive_result = ff_q_cf_positive_result_trace_following_state * S ((S (S cf_index_positive_result_trace)) * cf_scale_positive_result) + (((cf_new_a_positive_result_trace) + (((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) * S ((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) + ((cf_head_positive_result_trace) + (cf_head_positive_result_trace)))) * S ((cf_new_a_positive_result_trace) + (((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) * S ((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) + ((cf_head_positive_result_trace) + (cf_head_positive_result_trace)))) + ((((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) * S ((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) + ((cf_head_positive_result_trace) + (cf_head_positive_result_trace))) + (((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) * S ((cf_new_b_positive_result_trace) + (cf_head_positive_result_trace)) + ((cf_head_positive_result_trace) + (cf_head_positive_result_trace))))))) /\ (cf_new_b_positive_result_trace = cf_old_a_positive_result_trace /\ (cf_new_a_positive_result_trace = cf_new_b_positive_result_trace * cf_quotient_positive_result_trace + cf_old_b_positive_result_trace /\ ((exists ff_lt_cf_positive_result_trace_remainder. ff_lt_cf_positive_result_trace_remainder + S cf_old_b_positive_result_trace = cf_new_b_positive_result_trace) /\ (cf_head_positive_result_trace = S ((cf_quotient_positive_result_trace + cf_tail_positive_result_trace) * S (cf_quotient_positive_result_trace + cf_tail_positive_result_trace) + (cf_tail_positive_result_trace + cf_tail_positive_result_trace)))))))))))))) /\ ~(s = 0))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

39 script commands · 17 reading checkpoints · 4 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)
continued fraction nonzero divisor exists

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

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro ha
  4. L4
    intro hb
02Establish hsucc_bL5–7

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

  1. L5
    have hsucc_b : forall n. ~(n = 0) -> exists p. n = S p
  2. L6
    exact nonzero_is_succ
  3. L7
    specialize nonzero_is_succ a
03Establish ha_positiveL8–10

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

  1. L8
    have ha_positive : exists p. a = S p
  2. L9
    apply nonzero_is_succ
  3. L10
    exact ha
04Separate the logical casesL11–11

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

  1. L11
    cases ha_positive
05Use earlier factsL12–12

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

  1. L12
    specialize hsucc_b b
06Establish hb_positiveL13–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hsucc b.

  1. L13
    have hb_positive : exists p. b = S p
  2. L14
    apply hsucc_b
  3. L15
    exact hb
07Separate the logical casesL16–16

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

  1. L16
    cases hb_positive
08Use earlier factsL17–18

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

  1. L17
    specialize continued_fraction_nonzero_divisor_exists a
  2. L18
    specialize continued_fraction_nonzero_divisor_exists b
09Establish htraceL19–21

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

  1. L19
    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. L20
    apply continued_fraction_nonzero_divisor_exists
  3. L21
    exact hb
10Separate the logical casesL22–26

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

  1. L22
    cases htrace
  2. L23
    cases htrace_witness
  3. L24
    cases htrace_witness_witness
  4. L25
    cases htrace_witness_witness_witness
  5. L26
    cases htrace_witness_witness_witness_witness
11Construct an explicit witnessL27–27

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

  1. L27
    exists x2
12Separate the logical casesL28–28

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

  1. L28
    split
13Construct an explicit witnessL29–33

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

  1. L29
    exists x
  2. L30
    exists x1
  3. L31
    exists x3
  4. L32
    exists x4
  5. L33
    exists x5
14Separate the logical casesL34–34

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

  1. L34
    split
15Use earlier factsL35–35

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

  1. L35
    exact ha_positive_witness
16Separate the logical casesL36–36

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

  1. L36
    split
17Use earlier factsL37–39

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

  1. L37
    exact hb_positive_witness
  2. L38
    exact htrace_witness_witness_witness_witness_right
  3. L39
    exact htrace_witness_witness_witness_witness_left

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro ha
  4. 0004intro hb
  5. 0005have hsucc_b : forall n. ~(n = 0) -> exists p. n = S p
  6. 0006exact nonzero_is_succ
  7. 0007specialize nonzero_is_succ a
  8. 0008have ha_positive : exists p. a = S p
  9. 0009apply nonzero_is_succ
  10. 0010exact ha
  11. 0011cases ha_positive
  12. 0012specialize hsucc_b b
  13. 0013have hb_positive : exists p. b = S p
  14. 0014apply hsucc_b
  15. 0015exact hb
  16. 0016cases hb_positive
  17. 0017specialize continued_fraction_nonzero_divisor_exists a
  18. 0018specialize continued_fraction_nonzero_divisor_exists b
  19. 0019have htrace : exists s h e k. (~(s = 0) /\ (exists cf_gcd_nonzero_result. ((((exists ff_h_cf_nonzero_result_initial_state. ff_h_cf_nonzero_result_initial_state + S (((cf_gcd_nonzero_result) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_nonzero_result) + (((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_nonzero_result_initial_state. h = ff_q_cf_nonzero_result_initial_state * S ((S (0)) * e) + (((cf_gcd_nonzero_result) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_nonzero_result) + (((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_nonzero_result_terminal_state. ff_h_cf_nonzero_result_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_nonzero_result_terminal_state. h = ff_q_cf_nonzero_result_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_nonzero_result. (exists ff_lt_cf_nonzero_result_index. ff_lt_cf_nonzero_result_index + S cf_index_nonzero_result = S k) -> exists cf_old_a_nonzero_result cf_old_b_nonzero_result cf_tail_nonzero_result cf_new_a_nonzero_result cf_new_b_nonzero_result cf_head_nonzero_result cf_quotient_nonzero_result. ((((exists ff_h_cf_nonzero_result_previous_state. ff_h_cf_nonzero_result_previous_state + S (((cf_old_a_nonzero_result) + (((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result)))) * S ((cf_old_a_nonzero_result) + (((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result)))) + ((((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result))) + (((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result))))) = S ((S (cf_index_nonzero_result)) * e)) /\ exists ff_q_cf_nonzero_result_previous_state. h = ff_q_cf_nonzero_result_previous_state * S ((S (cf_index_nonzero_result)) * e) + (((cf_old_a_nonzero_result) + (((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result)))) * S ((cf_old_a_nonzero_result) + (((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result)))) + ((((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result))) + (((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result))))))) /\ ((((exists ff_h_cf_nonzero_result_following_state. ff_h_cf_nonzero_result_following_state + S (((cf_new_a_nonzero_result) + (((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result)))) * S ((cf_new_a_nonzero_result) + (((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result)))) + ((((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result))) + (((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result))))) = S ((S (S cf_index_nonzero_result)) * e)) /\ exists ff_q_cf_nonzero_result_following_state. h = ff_q_cf_nonzero_result_following_state * S ((S (S cf_index_nonzero_result)) * e) + (((cf_new_a_nonzero_result) + (((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result)))) * S ((cf_new_a_nonzero_result) + (((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result)))) + ((((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result))) + (((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result))))))) /\ (cf_new_b_nonzero_result = cf_old_a_nonzero_result /\ (cf_new_a_nonzero_result = cf_new_b_nonzero_result * cf_quotient_nonzero_result + cf_old_b_nonzero_result /\ ((exists ff_lt_cf_nonzero_result_remainder. ff_lt_cf_nonzero_result_remainder + S cf_old_b_nonzero_result = cf_new_b_nonzero_result) /\ (cf_head_nonzero_result = S ((cf_quotient_nonzero_result + cf_tail_nonzero_result) * S (cf_quotient_nonzero_result + cf_tail_nonzero_result) + (cf_tail_nonzero_result + cf_tail_nonzero_result))))))))))))
  20. 0020apply continued_fraction_nonzero_divisor_exists
  21. 0021exact hb
  22. 0022cases htrace
  23. 0023cases htrace_witness
  24. 0024cases htrace_witness_witness
  25. 0025cases htrace_witness_witness_witness
  26. 0026cases htrace_witness_witness_witness_witness
  27. 0027exists x2
  28. 0028split
  29. 0029exists x
  30. 0030exists x1
  31. 0031exists x3
  32. 0032exists x4
  33. 0033exists x5
  34. 0034split
  35. 0035exact ha_positive_witness
  36. 0036split
  37. 0037exact hb_positive_witness
  38. 0038exact htrace_witness_witness_witness_witness_right
  39. 0039exact htrace_witness_witness_witness_witness_left