CF0009

continued_fraction_positive_exists

G071: every pair of strictly positive naturals admits its complete witnessed finite simple continued-fraction quotient list.

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)

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

Definition DAG

ContinuedFraction(a,b,s) · 1

Actual proof prerequisites

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

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

14 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)
continued fraction positive nonempty 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
02Use earlier factsL5–6

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

  1. L5
    specialize continued_fraction_positive_nonempty_exists a
  2. L6
    specialize continued_fraction_positive_nonempty_exists b
03Establish hpositiveL7–10

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

  1. L7
    have hpositive : ∃ s. ContinuedFraction(a,b,s) ∧ ¬s = 0Definitions: ContinuedFractionOriginal native command in the exact edition
  2. L8
    apply continued_fraction_positive_nonempty_exists
  3. L9
    exact ha
  4. L10
    exact hb
04Separate the logical casesL11–12

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

  1. L11
    cases hpositive
  2. L12
    cases hpositive_witness
05Construct an explicit witnessL13–13

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

  1. L13
    exists x
06Use earlier factsL14–14

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

  1. L14
    exact hpositive_witness_left

Library-wide reading audit

Original defined command ledger · 14 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro ha
  4. 0004intro hb
  5. 0005specialize continued_fraction_positive_nonempty_exists a
  6. 0006specialize continued_fraction_positive_nonempty_exists b
  7. 0007have hpositive : 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))
  8. 0008apply continued_fraction_positive_nonempty_exists
  9. 0009exact ha
  10. 0010exact hb
  11. 0011cases hpositive
  12. 0012cases hpositive_witness
  13. 0013exists x
  14. 0014exact hpositive_witness_left