BA0042 — continued_fraction_convergent_index_is_valid

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 L i u v. (exists cf_gcd_convergent_index_history. ((((exists ff_h_cf_convergent_index_history_initial_state. ff_h_cf_convergent_index_history_initial_state + S (((cf_gcd_convergent_index_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_convergent_index_history) + (((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_convergent_index_history_initial_state. h = ff_q_cf_convergent_index_history_initial_state * S ((S (0)) * e) + (((cf_gcd_convergent_index_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_convergent_index_history) + (((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_convergent_index_history_terminal_state. ff_h_cf_convergent_index_history_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 (L)) * e)) /\ exists ff_q_cf_convergent_index_history_terminal_state. h = ff_q_cf_convergent_index_history_terminal_state * S ((S (L)) * 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_convergent_index_history. (exists ff_lt_cf_convergent_index_history_index. ff_lt_cf_convergent_index_history_index + S cf_index_convergent_index_history = L) -> exists cf_old_a_convergent_index_history cf_old_b_convergent_index_history cf_tail_convergent_index_history cf_new_a_convergent_index_history cf_new_b_convergent_index_history cf_head_convergent_index_history cf_quotient_convergent_index_history. ((((exists ff_h_cf_convergent_index_history_previous_state. ff_h_cf_convergent_index_history_previous_state + S (((cf_old_a_convergent_index_history) + (((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) * S ((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) + ((cf_tail_convergent_index_history) + (cf_tail_convergent_index_history)))) * S ((cf_old_a_convergent_index_history) + (((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) * S ((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) + ((cf_tail_convergent_index_history) + (cf_tail_convergent_index_history)))) + ((((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) * S ((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) + ((cf_tail_convergent_index_history) + (cf_tail_convergent_index_history))) + (((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) * S ((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) + ((cf_tail_convergent_index_history) + (cf_tail_convergent_index_history))))) = S ((S (cf_index_convergent_index_history)) * e)) /\ exists ff_q_cf_convergent_index_history_previous_state. h = ff_q_cf_convergent_index_history_previous_state * S ((S (cf_index_convergent_index_history)) * e) + (((cf_old_a_convergent_index_history) + (((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) * S ((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) + ((cf_tail_convergent_index_history) + (cf_tail_convergent_index_history)))) * S ((cf_old_a_convergent_index_history) + (((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) * S ((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) + ((cf_tail_convergent_index_history) + (cf_tail_convergent_index_history)))) + ((((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) * S ((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) + ((cf_tail_convergent_index_history) + (cf_tail_convergent_index_history))) + (((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) * S ((cf_old_b_convergent_index_history) + (cf_tail_convergent_index_history)) + ((cf_tail_convergent_index_history) + (cf_tail_convergent_index_history))))))) /\ ((((exists ff_h_cf_convergent_index_history_following_state. ff_h_cf_convergent_index_history_following_state + S (((cf_new_a_convergent_index_history) + (((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) * S ((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) + ((cf_head_convergent_index_history) + (cf_head_convergent_index_history)))) * S ((cf_new_a_convergent_index_history) + (((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) * S ((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) + ((cf_head_convergent_index_history) + (cf_head_convergent_index_history)))) + ((((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) * S ((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) + ((cf_head_convergent_index_history) + (cf_head_convergent_index_history))) + (((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) * S ((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) + ((cf_head_convergent_index_history) + (cf_head_convergent_index_history))))) = S ((S (S cf_index_convergent_index_history)) * e)) /\ exists ff_q_cf_convergent_index_history_following_state. h = ff_q_cf_convergent_index_history_following_state * S ((S (S cf_index_convergent_index_history)) * e) + (((cf_new_a_convergent_index_history) + (((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) * S ((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) + ((cf_head_convergent_index_history) + (cf_head_convergent_index_history)))) * S ((cf_new_a_convergent_index_history) + (((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) * S ((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) + ((cf_head_convergent_index_history) + (cf_head_convergent_index_history)))) + ((((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) * S ((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) + ((cf_head_convergent_index_history) + (cf_head_convergent_index_history))) + (((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) * S ((cf_new_b_convergent_index_history) + (cf_head_convergent_index_history)) + ((cf_head_convergent_index_history) + (cf_head_convergent_index_history))))))) /\ (cf_new_b_convergent_index_history = cf_old_a_convergent_index_history /\ (cf_new_a_convergent_index_history = cf_new_b_convergent_index_history * cf_quotient_convergent_index_history + cf_old_b_convergent_index_history /\ ((exists ff_lt_cf_convergent_index_history_remainder. ff_lt_cf_convergent_index_history_remainder + S cf_old_b_convergent_index_history = cf_new_b_convergent_index_history) /\ (cf_head_convergent_index_history = S ((cf_quotient_convergent_index_history + cf_tail_convergent_index_history) * S (cf_quotient_convergent_index_history + cf_tail_convergent_index_history) + (cf_tail_convergent_index_history + cf_tail_convergent_index_history))))))))))) -> (exists cfc_previous_numerator_existing_convergent cfc_previous_denominator_existing_convergent cfc_code_existing_convergent cfc_scale_existing_convergent. ((~(v = 0)) /\ (exists cfc_tail_existing_convergentcomputation. ((exists cfc_state_existing_convergentcomputationinitial. ((exists cfc_left_existing_convergentcomputationinitialcode cfc_right_existing_convergentcomputationinitialcode cfc_matrix_existing_convergentcomputationinitialcode. ((cfc_left_existing_convergentcomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_existing_convergentcomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_existing_convergentcomputationinitialcode = ((cfc_left_existing_convergentcomputationinitialcode) + (cfc_right_existing_convergentcomputationinitialcode)) * S ((cfc_left_existing_convergentcomputationinitialcode) + (cfc_right_existing_convergentcomputationinitialcode)) + ((cfc_right_existing_convergentcomputationinitialcode) + (cfc_right_existing_convergentcomputationinitialcode))) /\ ((cfc_state_existing_convergentcomputationinitial) = ((cfc_tail_existing_convergentcomputation) + (cfc_matrix_existing_convergentcomputationinitialcode)) * S ((cfc_tail_existing_convergentcomputation) + (cfc_matrix_existing_convergentcomputationinitialcode)) + ((cfc_matrix_existing_convergentcomputationinitialcode) + (cfc_matrix_existing_convergentcomputationinitialcode))))))) /\ (((exists ff_h_existing_convergentcomputationinitialentry. ff_h_existing_convergentcomputationinitialentry + S (cfc_state_existing_convergentcomputationinitial) = S ((S (0)) * cfc_scale_existing_convergent)) /\ exists ff_q_existing_convergentcomputationinitialentry. cfc_code_existing_convergent = ff_q_existing_convergentcomputationinitialentry * S ((S (0)) * cfc_scale_existing_convergent) + (cfc_state_existing_convergentcomputationinitial))))) /\ ((exists cfc_state_existing_convergentcomputationterminal. ((exists cfc_left_existing_convergentcomputationterminalcode cfc_right_existing_convergentcomputationterminalcode cfc_matrix_existing_convergentcomputationterminalcode. ((cfc_left_existing_convergentcomputationterminalcode = ((u) + (cfc_previous_numerator_existing_convergent)) * S ((u) + (cfc_previous_numerator_existing_convergent)) + ((cfc_previous_numerator_existing_convergent) + (cfc_previous_numerator_existing_convergent))) /\ ((cfc_right_existing_convergentcomputationterminalcode = ((v) + (cfc_previous_denominator_existing_convergent)) * S ((v) + (cfc_previous_denominator_existing_convergent)) + ((cfc_previous_denominator_existing_convergent) + (cfc_previous_denominator_existing_convergent))) /\ ((cfc_matrix_existing_convergentcomputationterminalcode = ((cfc_left_existing_convergentcomputationterminalcode) + (cfc_right_existing_convergentcomputationterminalcode)) * S ((cfc_left_existing_convergentcomputationterminalcode) + (cfc_right_existing_convergentcomputationterminalcode)) + ((cfc_right_existing_convergentcomputationterminalcode) + (cfc_right_existing_convergentcomputationterminalcode))) /\ ((cfc_state_existing_convergentcomputationterminal) = ((s) + (cfc_matrix_existing_convergentcomputationterminalcode)) * S ((s) + (cfc_matrix_existing_convergentcomputationterminalcode)) + ((cfc_matrix_existing_convergentcomputationterminalcode) + (cfc_matrix_existing_convergentcomputationterminalcode))))))) /\ (((exists ff_h_existing_convergentcomputationterminalentry. ff_h_existing_convergentcomputationterminalentry + S (cfc_state_existing_convergentcomputationterminal) = S ((S (S (i))) * cfc_scale_existing_convergent)) /\ exists ff_q_existing_convergentcomputationterminalentry. cfc_code_existing_convergent = ff_q_existing_convergentcomputationterminalentry * S ((S (S (i))) * cfc_scale_existing_convergent) + (cfc_state_existing_convergentcomputationterminal))))) /\ (forall cfc_index_existing_convergentcomputation. (exists cfba_gap_existing_convergentcomputationbound. cfba_gap_existing_convergentcomputationbound + S (cfc_index_existing_convergentcomputation) = (S (i))) -> exists cfc_old_existing_convergentcomputation cfc_a_existing_convergentcomputation cfc_b_existing_convergentcomputation cfc_c_existing_convergentcomputation cfc_d_existing_convergentcomputation cfc_new_existing_convergentcomputation cfc_quotient_existing_convergentcomputation. ((exists cfc_state_existing_convergentcomputationprevious. ((exists cfc_left_existing_convergentcomputationpreviouscode cfc_right_existing_convergentcomputationpreviouscode cfc_matrix_existing_convergentcomputationpreviouscode. ((cfc_left_existing_convergentcomputationpreviouscode = ((cfc_a_existing_convergentcomputation) + (cfc_b_existing_convergentcomputation)) * S ((cfc_a_existing_convergentcomputation) + (cfc_b_existing_convergentcomputation)) + ((cfc_b_existing_convergentcomputation) + (cfc_b_existing_convergentcomputation))) /\ ((cfc_right_existing_convergentcomputationpreviouscode = ((cfc_c_existing_convergentcomputation) + (cfc_d_existing_convergentcomputation)) * S ((cfc_c_existing_convergentcomputation) + (cfc_d_existing_convergentcomputation)) + ((cfc_d_existing_convergentcomputation) + (cfc_d_existing_convergentcomputation))) /\ ((cfc_matrix_existing_convergentcomputationpreviouscode = ((cfc_left_existing_convergentcomputationpreviouscode) + (cfc_right_existing_convergentcomputationpreviouscode)) * S ((cfc_left_existing_convergentcomputationpreviouscode) + (cfc_right_existing_convergentcomputationpreviouscode)) + ((cfc_right_existing_convergentcomputationpreviouscode) + (cfc_right_existing_convergentcomputationpreviouscode))) /\ ((cfc_state_existing_convergentcomputationprevious) = ((cfc_old_existing_convergentcomputation) + (cfc_matrix_existing_convergentcomputationpreviouscode)) * S ((cfc_old_existing_convergentcomputation) + (cfc_matrix_existing_convergentcomputationpreviouscode)) + ((cfc_matrix_existing_convergentcomputationpreviouscode) + (cfc_matrix_existing_convergentcomputationpreviouscode))))))) /\ (((exists ff_h_existing_convergentcomputationpreviousentry. ff_h_existing_convergentcomputationpreviousentry + S (cfc_state_existing_convergentcomputationprevious) = S ((S (cfc_index_existing_convergentcomputation)) * cfc_scale_existing_convergent)) /\ exists ff_q_existing_convergentcomputationpreviousentry. cfc_code_existing_convergent = ff_q_existing_convergentcomputationpreviousentry * S ((S (cfc_index_existing_convergentcomputation)) * cfc_scale_existing_convergent) + (cfc_state_existing_convergentcomputationprevious))))) /\ ((exists cfc_state_existing_convergentcomputationfollowing. ((exists cfc_left_existing_convergentcomputationfollowingcode cfc_right_existing_convergentcomputationfollowingcode cfc_matrix_existing_convergentcomputationfollowingcode. ((cfc_left_existing_convergentcomputationfollowingcode = (((cfc_quotient_existing_convergentcomputation * cfc_a_existing_convergentcomputation + cfc_c_existing_convergentcomputation)) + ((cfc_quotient_existing_convergentcomputation * cfc_b_existing_convergentcomputation + cfc_d_existing_convergentcomputation))) * S (((cfc_quotient_existing_convergentcomputation * cfc_a_existing_convergentcomputation + cfc_c_existing_convergentcomputation)) + ((cfc_quotient_existing_convergentcomputation * cfc_b_existing_convergentcomputation + cfc_d_existing_convergentcomputation))) + (((cfc_quotient_existing_convergentcomputation * cfc_b_existing_convergentcomputation + cfc_d_existing_convergentcomputation)) + ((cfc_quotient_existing_convergentcomputation * cfc_b_existing_convergentcomputation + cfc_d_existing_convergentcomputation)))) /\ ((cfc_right_existing_convergentcomputationfollowingcode = ((cfc_a_existing_convergentcomputation) + (cfc_b_existing_convergentcomputation)) * S ((cfc_a_existing_convergentcomputation) + (cfc_b_existing_convergentcomputation)) + ((cfc_b_existing_convergentcomputation) + (cfc_b_existing_convergentcomputation))) /\ ((cfc_matrix_existing_convergentcomputationfollowingcode = ((cfc_left_existing_convergentcomputationfollowingcode) + (cfc_right_existing_convergentcomputationfollowingcode)) * S ((cfc_left_existing_convergentcomputationfollowingcode) + (cfc_right_existing_convergentcomputationfollowingcode)) + ((cfc_right_existing_convergentcomputationfollowingcode) + (cfc_right_existing_convergentcomputationfollowingcode))) /\ ((cfc_state_existing_convergentcomputationfollowing) = ((cfc_new_existing_convergentcomputation) + (cfc_matrix_existing_convergentcomputationfollowingcode)) * S ((cfc_new_existing_convergentcomputation) + (cfc_matrix_existing_convergentcomputationfollowingcode)) + ((cfc_matrix_existing_convergentcomputationfollowingcode) + (cfc_matrix_existing_convergentcomputationfollowingcode))))))) /\ (((exists ff_h_existing_convergentcomputationfollowingentry. ff_h_existing_convergentcomputationfollowingentry + S (cfc_state_existing_convergentcomputationfollowing) = S ((S (S cfc_index_existing_convergentcomputation)) * cfc_scale_existing_convergent)) /\ exists ff_q_existing_convergentcomputationfollowingentry. cfc_code_existing_convergent = ff_q_existing_convergentcomputationfollowingentry * S ((S (S cfc_index_existing_convergentcomputation)) * cfc_scale_existing_convergent) + (cfc_state_existing_convergentcomputationfollowing))))) /\ (cfc_new_existing_convergentcomputation = S ((cfc_quotient_existing_convergentcomputation + cfc_old_existing_convergentcomputation) * S (cfc_quotient_existing_convergentcomputation + cfc_old_existing_convergentcomputation) + (cfc_old_existing_convergentcomputation + cfc_old_existing_convergentcomputation))))))))))) -> (exists cfba_gap_convergent_index_valid. cfba_gap_convergent_index_valid + S (i) = (L))

Constructive proof overview

Generated structural guide

The actual prefix computation proves the advertised index belongs to the complete G071 list; it is not merely a tagged pair of positive integers.

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

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

Proof neighborhood

Direct dependencies

BA0040 cf_convergent_actual_prefix_index_bound

Direct dependents

none

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

32 script commands · 5 reading checkpoints · 0 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 actual prefix index bound

01Fix variables and assumptionsL1–10

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