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 i u p v. u = p -> (exists cfc_previous_numerator_numerator_source cfc_previous_denominator_numerator_source cfc_code_numerator_source cfc_scale_numerator_source. ((~(v = 0)) /\ (exists cfc_tail_numerator_sourcecomputation. ((exists cfc_state_numerator_sourcecomputationinitial. ((exists cfc_left_numerator_sourcecomputationinitialcode cfc_right_numerator_sourcecomputationinitialcode cfc_matrix_numerator_sourcecomputationinitialcode. ((cfc_left_numerator_sourcecomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_numerator_sourcecomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_numerator_sourcecomputationinitialcode = ((cfc_left_numerator_sourcecomputationinitialcode) + (cfc_right_numerator_sourcecomputationinitialcode)) * S ((cfc_left_numerator_sourcecomputationinitialcode) + (cfc_right_numerator_sourcecomputationinitialcode)) + ((cfc_right_numerator_sourcecomputationinitialcode) + (cfc_right_numerator_sourcecomputationinitialcode))) /\ ((cfc_state_numerator_sourcecomputationinitial) = ((cfc_tail_numerator_sourcecomputation) + (cfc_matrix_numerator_sourcecomputationinitialcode)) * S ((cfc_tail_numerator_sourcecomputation) + (cfc_matrix_numerator_sourcecomputationinitialcode)) + ((cfc_matrix_numerator_sourcecomputationinitialcode) + (cfc_matrix_numerator_sourcecomputationinitialcode))))))) /\ (((exists ff_h_numerator_sourcecomputationinitialentry. ff_h_numerator_sourcecomputationinitialentry + S (cfc_state_numerator_sourcecomputationinitial) = S ((S (0)) * cfc_scale_numerator_source)) /\ exists ff_q_numerator_sourcecomputationinitialentry. cfc_code_numerator_source = ff_q_numerator_sourcecomputationinitialentry * S ((S (0)) * cfc_scale_numerator_source) + (cfc_state_numerator_sourcecomputationinitial))))) /\ ((exists cfc_state_numerator_sourcecomputationterminal. ((exists cfc_left_numerator_sourcecomputationterminalcode cfc_right_numerator_sourcecomputationterminalcode cfc_matrix_numerator_sourcecomputationterminalcode. ((cfc_left_numerator_sourcecomputationterminalcode = ((u) + (cfc_previous_numerator_numerator_source)) * S ((u) + (cfc_previous_numerator_numerator_source)) + ((cfc_previous_numerator_numerator_source) + (cfc_previous_numerator_numerator_source))) /\ ((cfc_right_numerator_sourcecomputationterminalcode = ((v) + (cfc_previous_denominator_numerator_source)) * S ((v) + (cfc_previous_denominator_numerator_source)) + ((cfc_previous_denominator_numerator_source) + (cfc_previous_denominator_numerator_source))) /\ ((cfc_matrix_numerator_sourcecomputationterminalcode = ((cfc_left_numerator_sourcecomputationterminalcode) + (cfc_right_numerator_sourcecomputationterminalcode)) * S ((cfc_left_numerator_sourcecomputationterminalcode) + (cfc_right_numerator_sourcecomputationterminalcode)) + ((cfc_right_numerator_sourcecomputationterminalcode) + (cfc_right_numerator_sourcecomputationterminalcode))) /\ ((cfc_state_numerator_sourcecomputationterminal) = ((s) + (cfc_matrix_numerator_sourcecomputationterminalcode)) * S ((s) + (cfc_matrix_numerator_sourcecomputationterminalcode)) + ((cfc_matrix_numerator_sourcecomputationterminalcode) + (cfc_matrix_numerator_sourcecomputationterminalcode))))))) /\ (((exists ff_h_numerator_sourcecomputationterminalentry. ff_h_numerator_sourcecomputationterminalentry + S (cfc_state_numerator_sourcecomputationterminal) = S ((S (S (i))) * cfc_scale_numerator_source)) /\ exists ff_q_numerator_sourcecomputationterminalentry. cfc_code_numerator_source = ff_q_numerator_sourcecomputationterminalentry * S ((S (S (i))) * cfc_scale_numerator_source) + (cfc_state_numerator_sourcecomputationterminal))))) /\ (forall cfc_index_numerator_sourcecomputation. (exists cfba_gap_numerator_sourcecomputationbound. cfba_gap_numerator_sourcecomputationbound + S (cfc_index_numerator_sourcecomputation) = (S (i))) -> exists cfc_old_numerator_sourcecomputation cfc_a_numerator_sourcecomputation cfc_b_numerator_sourcecomputation cfc_c_numerator_sourcecomputation cfc_d_numerator_sourcecomputation cfc_new_numerator_sourcecomputation cfc_quotient_numerator_sourcecomputation. ((exists cfc_state_numerator_sourcecomputationprevious. ((exists cfc_left_numerator_sourcecomputationpreviouscode cfc_right_numerator_sourcecomputationpreviouscode cfc_matrix_numerator_sourcecomputationpreviouscode. ((cfc_left_numerator_sourcecomputationpreviouscode = ((cfc_a_numerator_sourcecomputation) + (cfc_b_numerator_sourcecomputation)) * S ((cfc_a_numerator_sourcecomputation) + (cfc_b_numerator_sourcecomputation)) + ((cfc_b_numerator_sourcecomputation) + (cfc_b_numerator_sourcecomputation))) /\ ((cfc_right_numerator_sourcecomputationpreviouscode = ((cfc_c_numerator_sourcecomputation) + (cfc_d_numerator_sourcecomputation)) * S ((cfc_c_numerator_sourcecomputation) + (cfc_d_numerator_sourcecomputation)) + ((cfc_d_numerator_sourcecomputation) + (cfc_d_numerator_sourcecomputation))) /\ ((cfc_matrix_numerator_sourcecomputationpreviouscode = ((cfc_left_numerator_sourcecomputationpreviouscode) + (cfc_right_numerator_sourcecomputationpreviouscode)) * S ((cfc_left_numerator_sourcecomputationpreviouscode) + (cfc_right_numerator_sourcecomputationpreviouscode)) + ((cfc_right_numerator_sourcecomputationpreviouscode) + (cfc_right_numerator_sourcecomputationpreviouscode))) /\ ((cfc_state_numerator_sourcecomputationprevious) = ((cfc_old_numerator_sourcecomputation) + (cfc_matrix_numerator_sourcecomputationpreviouscode)) * S ((cfc_old_numerator_sourcecomputation) + (cfc_matrix_numerator_sourcecomputationpreviouscode)) + ((cfc_matrix_numerator_sourcecomputationpreviouscode) + (cfc_matrix_numerator_sourcecomputationpreviouscode))))))) /\ (((exists ff_h_numerator_sourcecomputationpreviousentry. ff_h_numerator_sourcecomputationpreviousentry + S (cfc_state_numerator_sourcecomputationprevious) = S ((S (cfc_index_numerator_sourcecomputation)) * cfc_scale_numerator_source)) /\ exists ff_q_numerator_sourcecomputationpreviousentry. cfc_code_numerator_source = ff_q_numerator_sourcecomputationpreviousentry * S ((S (cfc_index_numerator_sourcecomputation)) * cfc_scale_numerator_source) + (cfc_state_numerator_sourcecomputationprevious))))) /\ ((exists cfc_state_numerator_sourcecomputationfollowing. ((exists cfc_left_numerator_sourcecomputationfollowingcode cfc_right_numerator_sourcecomputationfollowingcode cfc_matrix_numerator_sourcecomputationfollowingcode. ((cfc_left_numerator_sourcecomputationfollowingcode = (((cfc_quotient_numerator_sourcecomputation * cfc_a_numerator_sourcecomputation + cfc_c_numerator_sourcecomputation)) + ((cfc_quotient_numerator_sourcecomputation * cfc_b_numerator_sourcecomputation + cfc_d_numerator_sourcecomputation))) * S (((cfc_quotient_numerator_sourcecomputation * cfc_a_numerator_sourcecomputation + cfc_c_numerator_sourcecomputation)) + ((cfc_quotient_numerator_sourcecomputation * cfc_b_numerator_sourcecomputation + cfc_d_numerator_sourcecomputation))) + (((cfc_quotient_numerator_sourcecomputation * cfc_b_numerator_sourcecomputation + cfc_d_numerator_sourcecomputation)) + ((cfc_quotient_numerator_sourcecomputation * cfc_b_numerator_sourcecomputation + cfc_d_numerator_sourcecomputation)))) /\ ((cfc_right_numerator_sourcecomputationfollowingcode = ((cfc_a_numerator_sourcecomputation) + (cfc_b_numerator_sourcecomputation)) * S ((cfc_a_numerator_sourcecomputation) + (cfc_b_numerator_sourcecomputation)) + ((cfc_b_numerator_sourcecomputation) + (cfc_b_numerator_sourcecomputation))) /\ ((cfc_matrix_numerator_sourcecomputationfollowingcode = ((cfc_left_numerator_sourcecomputationfollowingcode) + (cfc_right_numerator_sourcecomputationfollowingcode)) * S ((cfc_left_numerator_sourcecomputationfollowingcode) + (cfc_right_numerator_sourcecomputationfollowingcode)) + ((cfc_right_numerator_sourcecomputationfollowingcode) + (cfc_right_numerator_sourcecomputationfollowingcode))) /\ ((cfc_state_numerator_sourcecomputationfollowing) = ((cfc_new_numerator_sourcecomputation) + (cfc_matrix_numerator_sourcecomputationfollowingcode)) * S ((cfc_new_numerator_sourcecomputation) + (cfc_matrix_numerator_sourcecomputationfollowingcode)) + ((cfc_matrix_numerator_sourcecomputationfollowingcode) + (cfc_matrix_numerator_sourcecomputationfollowingcode))))))) /\ (((exists ff_h_numerator_sourcecomputationfollowingentry. ff_h_numerator_sourcecomputationfollowingentry + S (cfc_state_numerator_sourcecomputationfollowing) = S ((S (S cfc_index_numerator_sourcecomputation)) * cfc_scale_numerator_source)) /\ exists ff_q_numerator_sourcecomputationfollowingentry. cfc_code_numerator_source = ff_q_numerator_sourcecomputationfollowingentry * S ((S (S cfc_index_numerator_sourcecomputation)) * cfc_scale_numerator_source) + (cfc_state_numerator_sourcecomputationfollowing))))) /\ (cfc_new_numerator_sourcecomputation = S ((cfc_quotient_numerator_sourcecomputation + cfc_old_numerator_sourcecomputation) * S (cfc_quotient_numerator_sourcecomputation + cfc_old_numerator_sourcecomputation) + (cfc_old_numerator_sourcecomputation + cfc_old_numerator_sourcecomputation))))))))))) -> (exists cfc_previous_numerator_numerator_target cfc_previous_denominator_numerator_target cfc_code_numerator_target cfc_scale_numerator_target. ((~(v = 0)) /\ (exists cfc_tail_numerator_targetcomputation. ((exists cfc_state_numerator_targetcomputationinitial. ((exists cfc_left_numerator_targetcomputationinitialcode cfc_right_numerator_targetcomputationinitialcode cfc_matrix_numerator_targetcomputationinitialcode. ((cfc_left_numerator_targetcomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_numerator_targetcomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_numerator_targetcomputationinitialcode = ((cfc_left_numerator_targetcomputationinitialcode) + (cfc_right_numerator_targetcomputationinitialcode)) * S ((cfc_left_numerator_targetcomputationinitialcode) + (cfc_right_numerator_targetcomputationinitialcode)) + ((cfc_right_numerator_targetcomputationinitialcode) + (cfc_right_numerator_targetcomputationinitialcode))) /\ ((cfc_state_numerator_targetcomputationinitial) = ((cfc_tail_numerator_targetcomputation) + (cfc_matrix_numerator_targetcomputationinitialcode)) * S ((cfc_tail_numerator_targetcomputation) + (cfc_matrix_numerator_targetcomputationinitialcode)) + ((cfc_matrix_numerator_targetcomputationinitialcode) + (cfc_matrix_numerator_targetcomputationinitialcode))))))) /\ (((exists ff_h_numerator_targetcomputationinitialentry. ff_h_numerator_targetcomputationinitialentry + S (cfc_state_numerator_targetcomputationinitial) = S ((S (0)) * cfc_scale_numerator_target)) /\ exists ff_q_numerator_targetcomputationinitialentry. cfc_code_numerator_target = ff_q_numerator_targetcomputationinitialentry * S ((S (0)) * cfc_scale_numerator_target) + (cfc_state_numerator_targetcomputationinitial))))) /\ ((exists cfc_state_numerator_targetcomputationterminal. ((exists cfc_left_numerator_targetcomputationterminalcode cfc_right_numerator_targetcomputationterminalcode cfc_matrix_numerator_targetcomputationterminalcode. ((cfc_left_numerator_targetcomputationterminalcode = ((p) + (cfc_previous_numerator_numerator_target)) * S ((p) + (cfc_previous_numerator_numerator_target)) + ((cfc_previous_numerator_numerator_target) + (cfc_previous_numerator_numerator_target))) /\ ((cfc_right_numerator_targetcomputationterminalcode = ((v) + (cfc_previous_denominator_numerator_target)) * S ((v) + (cfc_previous_denominator_numerator_target)) + ((cfc_previous_denominator_numerator_target) + (cfc_previous_denominator_numerator_target))) /\ ((cfc_matrix_numerator_targetcomputationterminalcode = ((cfc_left_numerator_targetcomputationterminalcode) + (cfc_right_numerator_targetcomputationterminalcode)) * S ((cfc_left_numerator_targetcomputationterminalcode) + (cfc_right_numerator_targetcomputationterminalcode)) + ((cfc_right_numerator_targetcomputationterminalcode) + (cfc_right_numerator_targetcomputationterminalcode))) /\ ((cfc_state_numerator_targetcomputationterminal) = ((s) + (cfc_matrix_numerator_targetcomputationterminalcode)) * S ((s) + (cfc_matrix_numerator_targetcomputationterminalcode)) + ((cfc_matrix_numerator_targetcomputationterminalcode) + (cfc_matrix_numerator_targetcomputationterminalcode))))))) /\ (((exists ff_h_numerator_targetcomputationterminalentry. ff_h_numerator_targetcomputationterminalentry + S (cfc_state_numerator_targetcomputationterminal) = S ((S (S (i))) * cfc_scale_numerator_target)) /\ exists ff_q_numerator_targetcomputationterminalentry. cfc_code_numerator_target = ff_q_numerator_targetcomputationterminalentry * S ((S (S (i))) * cfc_scale_numerator_target) + (cfc_state_numerator_targetcomputationterminal))))) /\ (forall cfc_index_numerator_targetcomputation. (exists cfba_gap_numerator_targetcomputationbound. cfba_gap_numerator_targetcomputationbound + S (cfc_index_numerator_targetcomputation) = (S (i))) -> exists cfc_old_numerator_targetcomputation cfc_a_numerator_targetcomputation cfc_b_numerator_targetcomputation cfc_c_numerator_targetcomputation cfc_d_numerator_targetcomputation cfc_new_numerator_targetcomputation cfc_quotient_numerator_targetcomputation. ((exists cfc_state_numerator_targetcomputationprevious. ((exists cfc_left_numerator_targetcomputationpreviouscode cfc_right_numerator_targetcomputationpreviouscode cfc_matrix_numerator_targetcomputationpreviouscode. ((cfc_left_numerator_targetcomputationpreviouscode = ((cfc_a_numerator_targetcomputation) + (cfc_b_numerator_targetcomputation)) * S ((cfc_a_numerator_targetcomputation) + (cfc_b_numerator_targetcomputation)) + ((cfc_b_numerator_targetcomputation) + (cfc_b_numerator_targetcomputation))) /\ ((cfc_right_numerator_targetcomputationpreviouscode = ((cfc_c_numerator_targetcomputation) + (cfc_d_numerator_targetcomputation)) * S ((cfc_c_numerator_targetcomputation) + (cfc_d_numerator_targetcomputation)) + ((cfc_d_numerator_targetcomputation) + (cfc_d_numerator_targetcomputation))) /\ ((cfc_matrix_numerator_targetcomputationpreviouscode = ((cfc_left_numerator_targetcomputationpreviouscode) + (cfc_right_numerator_targetcomputationpreviouscode)) * S ((cfc_left_numerator_targetcomputationpreviouscode) + (cfc_right_numerator_targetcomputationpreviouscode)) + ((cfc_right_numerator_targetcomputationpreviouscode) + (cfc_right_numerator_targetcomputationpreviouscode))) /\ ((cfc_state_numerator_targetcomputationprevious) = ((cfc_old_numerator_targetcomputation) + (cfc_matrix_numerator_targetcomputationpreviouscode)) * S ((cfc_old_numerator_targetcomputation) + (cfc_matrix_numerator_targetcomputationpreviouscode)) + ((cfc_matrix_numerator_targetcomputationpreviouscode) + (cfc_matrix_numerator_targetcomputationpreviouscode))))))) /\ (((exists ff_h_numerator_targetcomputationpreviousentry. ff_h_numerator_targetcomputationpreviousentry + S (cfc_state_numerator_targetcomputationprevious) = S ((S (cfc_index_numerator_targetcomputation)) * cfc_scale_numerator_target)) /\ exists ff_q_numerator_targetcomputationpreviousentry. cfc_code_numerator_target = ff_q_numerator_targetcomputationpreviousentry * S ((S (cfc_index_numerator_targetcomputation)) * cfc_scale_numerator_target) + (cfc_state_numerator_targetcomputationprevious))))) /\ ((exists cfc_state_numerator_targetcomputationfollowing. ((exists cfc_left_numerator_targetcomputationfollowingcode cfc_right_numerator_targetcomputationfollowingcode cfc_matrix_numerator_targetcomputationfollowingcode. ((cfc_left_numerator_targetcomputationfollowingcode = (((cfc_quotient_numerator_targetcomputation * cfc_a_numerator_targetcomputation + cfc_c_numerator_targetcomputation)) + ((cfc_quotient_numerator_targetcomputation * cfc_b_numerator_targetcomputation + cfc_d_numerator_targetcomputation))) * S (((cfc_quotient_numerator_targetcomputation * cfc_a_numerator_targetcomputation + cfc_c_numerator_targetcomputation)) + ((cfc_quotient_numerator_targetcomputation * cfc_b_numerator_targetcomputation + cfc_d_numerator_targetcomputation))) + (((cfc_quotient_numerator_targetcomputation * cfc_b_numerator_targetcomputation + cfc_d_numerator_targetcomputation)) + ((cfc_quotient_numerator_targetcomputation * cfc_b_numerator_targetcomputation + cfc_d_numerator_targetcomputation)))) /\ ((cfc_right_numerator_targetcomputationfollowingcode = ((cfc_a_numerator_targetcomputation) + (cfc_b_numerator_targetcomputation)) * S ((cfc_a_numerator_targetcomputation) + (cfc_b_numerator_targetcomputation)) + ((cfc_b_numerator_targetcomputation) + (cfc_b_numerator_targetcomputation))) /\ ((cfc_matrix_numerator_targetcomputationfollowingcode = ((cfc_left_numerator_targetcomputationfollowingcode) + (cfc_right_numerator_targetcomputationfollowingcode)) * S ((cfc_left_numerator_targetcomputationfollowingcode) + (cfc_right_numerator_targetcomputationfollowingcode)) + ((cfc_right_numerator_targetcomputationfollowingcode) + (cfc_right_numerator_targetcomputationfollowingcode))) /\ ((cfc_state_numerator_targetcomputationfollowing) = ((cfc_new_numerator_targetcomputation) + (cfc_matrix_numerator_targetcomputationfollowingcode)) * S ((cfc_new_numerator_targetcomputation) + (cfc_matrix_numerator_targetcomputationfollowingcode)) + ((cfc_matrix_numerator_targetcomputationfollowingcode) + (cfc_matrix_numerator_targetcomputationfollowingcode))))))) /\ (((exists ff_h_numerator_targetcomputationfollowingentry. ff_h_numerator_targetcomputationfollowingentry + S (cfc_state_numerator_targetcomputationfollowing) = S ((S (S cfc_index_numerator_targetcomputation)) * cfc_scale_numerator_target)) /\ exists ff_q_numerator_targetcomputationfollowingentry. cfc_code_numerator_target = ff_q_numerator_targetcomputationfollowingentry * S ((S (S cfc_index_numerator_targetcomputation)) * cfc_scale_numerator_target) + (cfc_state_numerator_targetcomputationfollowing))))) /\ (cfc_new_numerator_targetcomputation = S ((cfc_quotient_numerator_targetcomputation + cfc_old_numerator_targetcomputation) * S (cfc_quotient_numerator_targetcomputation + cfc_old_numerator_targetcomputation) + (cfc_old_numerator_targetcomputation + cfc_old_numerator_targetcomputation)))))))))))Constructive proof overview
Generated structural guide
Actual numerator equality transports a convergent while preserving its index, positive denominator, and complete computation certificate.
The unchanged tactic script uses 0 declared prerequisites and contains 10 exact native proof lines.
Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
none
Direct dependents
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
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.
01Fix variables and assumptionsL1–7
02Calculate and transport equalitiesL8–9
03Use earlier factsL10–10
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L10
exact hc