BA0044

continued_fraction_first_cell_is_initial_convergent

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 22 exact native proof lines.

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

Proof neighborhood

Direct dependencies

BA0043 cf_convergent_initial_matrix_exists succ_ne_zero Stable theorem; checked-use authorized

Direct dependents

BA0046 continued_fraction_initial_zero_over_one BA004E continued_fraction_initial_convergent_is_first_quotient

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

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.

Named ingredients (1)
cf convergent initial matrix 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 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
  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 exact command ledger · 22 lines
  1. 0001intro s
  2. 0002intro q
  3. 0003intro t
  4. 0004intro hc
  5. 0005have hm : exists h e. exists cfc_tail_initial_actual. ((exists cfc_state_initial_actualinitial. ((exists cfc_left_initial_actualinitialcode cfc_right_initial_actualinitialcode cfc_matrix_initial_actualinitialcode. ((cfc_left_initial_actualinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_initial_actualinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_initial_actualinitialcode = ((cfc_left_initial_actualinitialcode) + (cfc_right_initial_actualinitialcode)) * S ((cfc_left_initial_actualinitialcode) + (cfc_right_initial_actualinitialcode)) + ((cfc_right_initial_actualinitialcode) + (cfc_right_initial_actualinitialcode))) /\ ((cfc_state_initial_actualinitial) = ((cfc_tail_initial_actual) + (cfc_matrix_initial_actualinitialcode)) * S ((cfc_tail_initial_actual) + (cfc_matrix_initial_actualinitialcode)) + ((cfc_matrix_initial_actualinitialcode) + (cfc_matrix_initial_actualinitialcode))))))) /\ (((exists ff_h_initial_actualinitialentry. ff_h_initial_actualinitialentry + S (cfc_state_initial_actualinitial) = S ((S (0)) * e)) /\ exists ff_q_initial_actualinitialentry. h = ff_q_initial_actualinitialentry * S ((S (0)) * e) + (cfc_state_initial_actualinitial))))) /\ ((exists cfc_state_initial_actualterminal. ((exists cfc_left_initial_actualterminalcode cfc_right_initial_actualterminalcode cfc_matrix_initial_actualterminalcode. ((cfc_left_initial_actualterminalcode = ((q) + (1)) * S ((q) + (1)) + ((1) + (1))) /\ ((cfc_right_initial_actualterminalcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_matrix_initial_actualterminalcode = ((cfc_left_initial_actualterminalcode) + (cfc_right_initial_actualterminalcode)) * S ((cfc_left_initial_actualterminalcode) + (cfc_right_initial_actualterminalcode)) + ((cfc_right_initial_actualterminalcode) + (cfc_right_initial_actualterminalcode))) /\ ((cfc_state_initial_actualterminal) = ((s) + (cfc_matrix_initial_actualterminalcode)) * S ((s) + (cfc_matrix_initial_actualterminalcode)) + ((cfc_matrix_initial_actualterminalcode) + (cfc_matrix_initial_actualterminalcode))))))) /\ (((exists ff_h_initial_actualterminalentry. ff_h_initial_actualterminalentry + S (cfc_state_initial_actualterminal) = S ((S (1)) * e)) /\ exists ff_q_initial_actualterminalentry. h = ff_q_initial_actualterminalentry * S ((S (1)) * e) + (cfc_state_initial_actualterminal))))) /\ (forall cfc_index_initial_actual. (exists cfba_gap_initial_actualbound. cfba_gap_initial_actualbound + S (cfc_index_initial_actual) = (1)) -> exists cfc_old_initial_actual cfc_a_initial_actual cfc_b_initial_actual cfc_c_initial_actual cfc_d_initial_actual cfc_new_initial_actual cfc_quotient_initial_actual. ((exists cfc_state_initial_actualprevious. ((exists cfc_left_initial_actualpreviouscode cfc_right_initial_actualpreviouscode cfc_matrix_initial_actualpreviouscode. ((cfc_left_initial_actualpreviouscode = ((cfc_a_initial_actual) + (cfc_b_initial_actual)) * S ((cfc_a_initial_actual) + (cfc_b_initial_actual)) + ((cfc_b_initial_actual) + (cfc_b_initial_actual))) /\ ((cfc_right_initial_actualpreviouscode = ((cfc_c_initial_actual) + (cfc_d_initial_actual)) * S ((cfc_c_initial_actual) + (cfc_d_initial_actual)) + ((cfc_d_initial_actual) + (cfc_d_initial_actual))) /\ ((cfc_matrix_initial_actualpreviouscode = ((cfc_left_initial_actualpreviouscode) + (cfc_right_initial_actualpreviouscode)) * S ((cfc_left_initial_actualpreviouscode) + (cfc_right_initial_actualpreviouscode)) + ((cfc_right_initial_actualpreviouscode) + (cfc_right_initial_actualpreviouscode))) /\ ((cfc_state_initial_actualprevious) = ((cfc_old_initial_actual) + (cfc_matrix_initial_actualpreviouscode)) * S ((cfc_old_initial_actual) + (cfc_matrix_initial_actualpreviouscode)) + ((cfc_matrix_initial_actualpreviouscode) + (cfc_matrix_initial_actualpreviouscode))))))) /\ (((exists ff_h_initial_actualpreviousentry. ff_h_initial_actualpreviousentry + S (cfc_state_initial_actualprevious) = S ((S (cfc_index_initial_actual)) * e)) /\ exists ff_q_initial_actualpreviousentry. h = ff_q_initial_actualpreviousentry * S ((S (cfc_index_initial_actual)) * e) + (cfc_state_initial_actualprevious))))) /\ ((exists cfc_state_initial_actualfollowing. ((exists cfc_left_initial_actualfollowingcode cfc_right_initial_actualfollowingcode cfc_matrix_initial_actualfollowingcode. ((cfc_left_initial_actualfollowingcode = (((cfc_quotient_initial_actual * cfc_a_initial_actual + cfc_c_initial_actual)) + ((cfc_quotient_initial_actual * cfc_b_initial_actual + cfc_d_initial_actual))) * S (((cfc_quotient_initial_actual * cfc_a_initial_actual + cfc_c_initial_actual)) + ((cfc_quotient_initial_actual * cfc_b_initial_actual + cfc_d_initial_actual))) + (((cfc_quotient_initial_actual * cfc_b_initial_actual + cfc_d_initial_actual)) + ((cfc_quotient_initial_actual * cfc_b_initial_actual + cfc_d_initial_actual)))) /\ ((cfc_right_initial_actualfollowingcode = ((cfc_a_initial_actual) + (cfc_b_initial_actual)) * S ((cfc_a_initial_actual) + (cfc_b_initial_actual)) + ((cfc_b_initial_actual) + (cfc_b_initial_actual))) /\ ((cfc_matrix_initial_actualfollowingcode = ((cfc_left_initial_actualfollowingcode) + (cfc_right_initial_actualfollowingcode)) * S ((cfc_left_initial_actualfollowingcode) + (cfc_right_initial_actualfollowingcode)) + ((cfc_right_initial_actualfollowingcode) + (cfc_right_initial_actualfollowingcode))) /\ ((cfc_state_initial_actualfollowing) = ((cfc_new_initial_actual) + (cfc_matrix_initial_actualfollowingcode)) * S ((cfc_new_initial_actual) + (cfc_matrix_initial_actualfollowingcode)) + ((cfc_matrix_initial_actualfollowingcode) + (cfc_matrix_initial_actualfollowingcode))))))) /\ (((exists ff_h_initial_actualfollowingentry. ff_h_initial_actualfollowingentry + S (cfc_state_initial_actualfollowing) = S ((S (S cfc_index_initial_actual)) * e)) /\ exists ff_q_initial_actualfollowingentry. h = ff_q_initial_actualfollowingentry * S ((S (S cfc_index_initial_actual)) * e) + (cfc_state_initial_actualfollowing))))) /\ (cfc_new_initial_actual = S ((cfc_quotient_initial_actual + cfc_old_initial_actual) * S (cfc_quotient_initial_actual + cfc_old_initial_actual) + (cfc_old_initial_actual + cfc_old_initial_actual))))))))
  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