BA0044

continued_fraction_first_cell_is_initial_convergent

The genuine zeroth convergent is q/1 for the actual first quotient q; no positivity condition is imposed on its numerator.

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

∀ s. ∀ q. ∀ t. ListCell(s,q,t) → Convergent(s,0,q,1)

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

Definition DAG

ListCell(s,q,t) · 1ConvergentMatrixTrace(s,h,e,k,u,U,v,V) · 1Convergent(s,i,u,v) · 1

Actual proof prerequisites

cf_convergent_initial_matrix_existssucc_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall s q t. (s = S ((q + t) * S (q + t) + (t + t))) -> (exists cfc_previous_numerator_initial_convergent cfc_previous_denominator_initial_convergent cfc_code_initial_convergent cfc_scale_initial_convergent. ((~(1 = 0)) /\ (exists cfc_tail_initial_convergentcomputation. ((exists cfc_state_initial_convergentcomputationinitial. ((exists cfc_left_initial_convergentcomputationinitialcode cfc_right_initial_convergentcomputationinitialcode cfc_matrix_initial_convergentcomputationinitialcode. ((cfc_left_initial_convergentcomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_initial_convergentcomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_initial_convergentcomputationinitialcode = ((cfc_left_initial_convergentcomputationinitialcode) + (cfc_right_initial_convergentcomputationinitialcode)) * S ((cfc_left_initial_convergentcomputationinitialcode) + (cfc_right_initial_convergentcomputationinitialcode)) + ((cfc_right_initial_convergentcomputationinitialcode) + (cfc_right_initial_convergentcomputationinitialcode))) /\ ((cfc_state_initial_convergentcomputationinitial) = ((cfc_tail_initial_convergentcomputation) + (cfc_matrix_initial_convergentcomputationinitialcode)) * S ((cfc_tail_initial_convergentcomputation) + (cfc_matrix_initial_convergentcomputationinitialcode)) + ((cfc_matrix_initial_convergentcomputationinitialcode) + (cfc_matrix_initial_convergentcomputationinitialcode))))))) /\ (((exists ff_h_initial_convergentcomputationinitialentry. ff_h_initial_convergentcomputationinitialentry + S (cfc_state_initial_convergentcomputationinitial) = S ((S (0)) * cfc_scale_initial_convergent)) /\ exists ff_q_initial_convergentcomputationinitialentry. cfc_code_initial_convergent = ff_q_initial_convergentcomputationinitialentry * S ((S (0)) * cfc_scale_initial_convergent) + (cfc_state_initial_convergentcomputationinitial))))) /\ ((exists cfc_state_initial_convergentcomputationterminal. ((exists cfc_left_initial_convergentcomputationterminalcode cfc_right_initial_convergentcomputationterminalcode cfc_matrix_initial_convergentcomputationterminalcode. ((cfc_left_initial_convergentcomputationterminalcode = ((q) + (cfc_previous_numerator_initial_convergent)) * S ((q) + (cfc_previous_numerator_initial_convergent)) + ((cfc_previous_numerator_initial_convergent) + (cfc_previous_numerator_initial_convergent))) /\ ((cfc_right_initial_convergentcomputationterminalcode = ((1) + (cfc_previous_denominator_initial_convergent)) * S ((1) + (cfc_previous_denominator_initial_convergent)) + ((cfc_previous_denominator_initial_convergent) + (cfc_previous_denominator_initial_convergent))) /\ ((cfc_matrix_initial_convergentcomputationterminalcode = ((cfc_left_initial_convergentcomputationterminalcode) + (cfc_right_initial_convergentcomputationterminalcode)) * S ((cfc_left_initial_convergentcomputationterminalcode) + (cfc_right_initial_convergentcomputationterminalcode)) + ((cfc_right_initial_convergentcomputationterminalcode) + (cfc_right_initial_convergentcomputationterminalcode))) /\ ((cfc_state_initial_convergentcomputationterminal) = ((s) + (cfc_matrix_initial_convergentcomputationterminalcode)) * S ((s) + (cfc_matrix_initial_convergentcomputationterminalcode)) + ((cfc_matrix_initial_convergentcomputationterminalcode) + (cfc_matrix_initial_convergentcomputationterminalcode))))))) /\ (((exists ff_h_initial_convergentcomputationterminalentry. ff_h_initial_convergentcomputationterminalentry + S (cfc_state_initial_convergentcomputationterminal) = S ((S (S (0))) * cfc_scale_initial_convergent)) /\ exists ff_q_initial_convergentcomputationterminalentry. cfc_code_initial_convergent = ff_q_initial_convergentcomputationterminalentry * S ((S (S (0))) * cfc_scale_initial_convergent) + (cfc_state_initial_convergentcomputationterminal))))) /\ (forall cfc_index_initial_convergentcomputation. (exists cfba_gap_initial_convergentcomputationbound. cfba_gap_initial_convergentcomputationbound + S (cfc_index_initial_convergentcomputation) = (S (0))) -> exists cfc_old_initial_convergentcomputation cfc_a_initial_convergentcomputation cfc_b_initial_convergentcomputation cfc_c_initial_convergentcomputation cfc_d_initial_convergentcomputation cfc_new_initial_convergentcomputation cfc_quotient_initial_convergentcomputation. ((exists cfc_state_initial_convergentcomputationprevious. ((exists cfc_left_initial_convergentcomputationpreviouscode cfc_right_initial_convergentcomputationpreviouscode cfc_matrix_initial_convergentcomputationpreviouscode. ((cfc_left_initial_convergentcomputationpreviouscode = ((cfc_a_initial_convergentcomputation) + (cfc_b_initial_convergentcomputation)) * S ((cfc_a_initial_convergentcomputation) + (cfc_b_initial_convergentcomputation)) + ((cfc_b_initial_convergentcomputation) + (cfc_b_initial_convergentcomputation))) /\ ((cfc_right_initial_convergentcomputationpreviouscode = ((cfc_c_initial_convergentcomputation) + (cfc_d_initial_convergentcomputation)) * S ((cfc_c_initial_convergentcomputation) + (cfc_d_initial_convergentcomputation)) + ((cfc_d_initial_convergentcomputation) + (cfc_d_initial_convergentcomputation))) /\ ((cfc_matrix_initial_convergentcomputationpreviouscode = ((cfc_left_initial_convergentcomputationpreviouscode) + (cfc_right_initial_convergentcomputationpreviouscode)) * S ((cfc_left_initial_convergentcomputationpreviouscode) + (cfc_right_initial_convergentcomputationpreviouscode)) + ((cfc_right_initial_convergentcomputationpreviouscode) + (cfc_right_initial_convergentcomputationpreviouscode))) /\ ((cfc_state_initial_convergentcomputationprevious) = ((cfc_old_initial_convergentcomputation) + (cfc_matrix_initial_convergentcomputationpreviouscode)) * S ((cfc_old_initial_convergentcomputation) + (cfc_matrix_initial_convergentcomputationpreviouscode)) + ((cfc_matrix_initial_convergentcomputationpreviouscode) + (cfc_matrix_initial_convergentcomputationpreviouscode))))))) /\ (((exists ff_h_initial_convergentcomputationpreviousentry. ff_h_initial_convergentcomputationpreviousentry + S (cfc_state_initial_convergentcomputationprevious) = S ((S (cfc_index_initial_convergentcomputation)) * cfc_scale_initial_convergent)) /\ exists ff_q_initial_convergentcomputationpreviousentry. cfc_code_initial_convergent = ff_q_initial_convergentcomputationpreviousentry * S ((S (cfc_index_initial_convergentcomputation)) * cfc_scale_initial_convergent) + (cfc_state_initial_convergentcomputationprevious))))) /\ ((exists cfc_state_initial_convergentcomputationfollowing. ((exists cfc_left_initial_convergentcomputationfollowingcode cfc_right_initial_convergentcomputationfollowingcode cfc_matrix_initial_convergentcomputationfollowingcode. ((cfc_left_initial_convergentcomputationfollowingcode = (((cfc_quotient_initial_convergentcomputation * cfc_a_initial_convergentcomputation + cfc_c_initial_convergentcomputation)) + ((cfc_quotient_initial_convergentcomputation * cfc_b_initial_convergentcomputation + cfc_d_initial_convergentcomputation))) * S (((cfc_quotient_initial_convergentcomputation * cfc_a_initial_convergentcomputation + cfc_c_initial_convergentcomputation)) + ((cfc_quotient_initial_convergentcomputation * cfc_b_initial_convergentcomputation + cfc_d_initial_convergentcomputation))) + (((cfc_quotient_initial_convergentcomputation * cfc_b_initial_convergentcomputation + cfc_d_initial_convergentcomputation)) + ((cfc_quotient_initial_convergentcomputation * cfc_b_initial_convergentcomputation + cfc_d_initial_convergentcomputation)))) /\ ((cfc_right_initial_convergentcomputationfollowingcode = ((cfc_a_initial_convergentcomputation) + (cfc_b_initial_convergentcomputation)) * S ((cfc_a_initial_convergentcomputation) + (cfc_b_initial_convergentcomputation)) + ((cfc_b_initial_convergentcomputation) + (cfc_b_initial_convergentcomputation))) /\ ((cfc_matrix_initial_convergentcomputationfollowingcode = ((cfc_left_initial_convergentcomputationfollowingcode) + (cfc_right_initial_convergentcomputationfollowingcode)) * S ((cfc_left_initial_convergentcomputationfollowingcode) + (cfc_right_initial_convergentcomputationfollowingcode)) + ((cfc_right_initial_convergentcomputationfollowingcode) + (cfc_right_initial_convergentcomputationfollowingcode))) /\ ((cfc_state_initial_convergentcomputationfollowing) = ((cfc_new_initial_convergentcomputation) + (cfc_matrix_initial_convergentcomputationfollowingcode)) * S ((cfc_new_initial_convergentcomputation) + (cfc_matrix_initial_convergentcomputationfollowingcode)) + ((cfc_matrix_initial_convergentcomputationfollowingcode) + (cfc_matrix_initial_convergentcomputationfollowingcode))))))) /\ (((exists ff_h_initial_convergentcomputationfollowingentry. ff_h_initial_convergentcomputationfollowingentry + S (cfc_state_initial_convergentcomputationfollowing) = S ((S (S cfc_index_initial_convergentcomputation)) * cfc_scale_initial_convergent)) /\ exists ff_q_initial_convergentcomputationfollowingentry. cfc_code_initial_convergent = ff_q_initial_convergentcomputationfollowingentry * S ((S (S cfc_index_initial_convergentcomputation)) * cfc_scale_initial_convergent) + (cfc_state_initial_convergentcomputationfollowing))))) /\ (cfc_new_initial_convergentcomputation = S ((cfc_quotient_initial_convergentcomputation + cfc_old_initial_convergentcomputation) * S (cfc_quotient_initial_convergentcomputation + cfc_old_initial_convergentcomputation) + (cfc_old_initial_convergentcomputation + cfc_old_initial_convergentcomputation)))))))))))

Complete tactic proof in conservative notation

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

22 script commands · 7 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 initial matrix exists
01Fix variables and assumptionsL1–4

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

  1. L1
    intro s
  2. L2
    intro q
  3. L3
    intro t
  4. L4
    intro hc
02Establish hmL5–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent initial matrix exists.

  1. L5
    have hm : ∃ h. ∃ e. ConvergentMatrixTrace(s,h,e,1,q,1,1,0)Definitions: ConvergentMatrixTrace(s,h,e,1,q,1,1,0)Original native command in the exact edition
  2. L6
    specialize cf_convergent_initial_matrix_exists (s)
  3. L7
    specialize cf_convergent_initial_matrix_exists (q)
  4. L8
    specialize cf_convergent_initial_matrix_exists (t)
  5. L9
    apply cf_convergent_initial_matrix_exists
  6. L10
    exact hc
03Separate the logical casesL11–12

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

  1. L11
    cases hm
  2. L12
    cases hm_witness
04Construct an explicit witnessL13–16

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

  1. L13
    exists 1
  2. L14
    exists 0
  3. L15
    exists x
  4. L16
    exists x1
05Separate the logical casesL17–17

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

  1. L17
    split
06Fix variables and assumptionsL18–18

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

  1. L18
    intro hz
07Use earlier factsL19–22

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

  1. L19
    specialize succ_ne_zero (0)
  2. L20
    apply succ_ne_zero
  3. L21
    exact hz
  4. L22
    exact hm_witness_witness

Library-wide reading audit

Original defined command ledger · 22 lines
  1. 0001intro s
  2. 0002intro q
  3. 0003intro t
  4. 0004intro hc
  5. 0005have hm : ∃ h. ∃ e. ConvergentMatrixTrace(s,h,e,1,q,1,1,0)
  6. 0006specialize cf_convergent_initial_matrix_exists (s)
  7. 0007specialize cf_convergent_initial_matrix_exists (q)
  8. 0008specialize cf_convergent_initial_matrix_exists (t)
  9. 0009apply cf_convergent_initial_matrix_exists
  10. 0010exact hc
  11. 0011cases hm
  12. 0012cases hm_witness
  13. 0013exists 1
  14. 0014exists 0
  15. 0015exists x
  16. 0016exists x1
  17. 0017split
  18. 0018intro hz
  19. 0019specialize succ_ne_zero (0)
  20. 0020apply succ_ne_zero
  21. 0021exact hz
  22. 0022exact hm_witness_witness