BA0039

cf_convergent_matrix_empty_constructor

An actual encoded identity state constructs the zero-length quotient-prefix product with no transition obligations.

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. ∀ h. ∀ e. ConvergentMatrixAt(h,e,0,s,1,0,0,1) → ConvergentMatrixTrace(s,h,e,0,1,0,0,1)

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

Definition DAG

ConvergentMatrixAt(h,e,j,s,u,U,v,V) · 1ConvergentMatrixTrace(s,h,e,k,u,U,v,V) · 1

Actual proof prerequisites

cf_convergent_no_index_below_zero
Original expanded first-order statement 
forall s h e. (exists cfc_state_empty_constructor_state. ((exists cfc_left_empty_constructor_statecode cfc_right_empty_constructor_statecode cfc_matrix_empty_constructor_statecode. ((cfc_left_empty_constructor_statecode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_empty_constructor_statecode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_empty_constructor_statecode = ((cfc_left_empty_constructor_statecode) + (cfc_right_empty_constructor_statecode)) * S ((cfc_left_empty_constructor_statecode) + (cfc_right_empty_constructor_statecode)) + ((cfc_right_empty_constructor_statecode) + (cfc_right_empty_constructor_statecode))) /\ ((cfc_state_empty_constructor_state) = ((s) + (cfc_matrix_empty_constructor_statecode)) * S ((s) + (cfc_matrix_empty_constructor_statecode)) + ((cfc_matrix_empty_constructor_statecode) + (cfc_matrix_empty_constructor_statecode))))))) /\ (((exists ff_h_empty_constructor_stateentry. ff_h_empty_constructor_stateentry + S (cfc_state_empty_constructor_state) = S ((S (0)) * e)) /\ exists ff_q_empty_constructor_stateentry. h = ff_q_empty_constructor_stateentry * S ((S (0)) * e) + (cfc_state_empty_constructor_state))))) -> (exists cfc_tail_empty_constructor_trace. ((exists cfc_state_empty_constructor_traceinitial. ((exists cfc_left_empty_constructor_traceinitialcode cfc_right_empty_constructor_traceinitialcode cfc_matrix_empty_constructor_traceinitialcode. ((cfc_left_empty_constructor_traceinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_empty_constructor_traceinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_empty_constructor_traceinitialcode = ((cfc_left_empty_constructor_traceinitialcode) + (cfc_right_empty_constructor_traceinitialcode)) * S ((cfc_left_empty_constructor_traceinitialcode) + (cfc_right_empty_constructor_traceinitialcode)) + ((cfc_right_empty_constructor_traceinitialcode) + (cfc_right_empty_constructor_traceinitialcode))) /\ ((cfc_state_empty_constructor_traceinitial) = ((cfc_tail_empty_constructor_trace) + (cfc_matrix_empty_constructor_traceinitialcode)) * S ((cfc_tail_empty_constructor_trace) + (cfc_matrix_empty_constructor_traceinitialcode)) + ((cfc_matrix_empty_constructor_traceinitialcode) + (cfc_matrix_empty_constructor_traceinitialcode))))))) /\ (((exists ff_h_empty_constructor_traceinitialentry. ff_h_empty_constructor_traceinitialentry + S (cfc_state_empty_constructor_traceinitial) = S ((S (0)) * e)) /\ exists ff_q_empty_constructor_traceinitialentry. h = ff_q_empty_constructor_traceinitialentry * S ((S (0)) * e) + (cfc_state_empty_constructor_traceinitial))))) /\ ((exists cfc_state_empty_constructor_traceterminal. ((exists cfc_left_empty_constructor_traceterminalcode cfc_right_empty_constructor_traceterminalcode cfc_matrix_empty_constructor_traceterminalcode. ((cfc_left_empty_constructor_traceterminalcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_empty_constructor_traceterminalcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_empty_constructor_traceterminalcode = ((cfc_left_empty_constructor_traceterminalcode) + (cfc_right_empty_constructor_traceterminalcode)) * S ((cfc_left_empty_constructor_traceterminalcode) + (cfc_right_empty_constructor_traceterminalcode)) + ((cfc_right_empty_constructor_traceterminalcode) + (cfc_right_empty_constructor_traceterminalcode))) /\ ((cfc_state_empty_constructor_traceterminal) = ((s) + (cfc_matrix_empty_constructor_traceterminalcode)) * S ((s) + (cfc_matrix_empty_constructor_traceterminalcode)) + ((cfc_matrix_empty_constructor_traceterminalcode) + (cfc_matrix_empty_constructor_traceterminalcode))))))) /\ (((exists ff_h_empty_constructor_traceterminalentry. ff_h_empty_constructor_traceterminalentry + S (cfc_state_empty_constructor_traceterminal) = S ((S (0)) * e)) /\ exists ff_q_empty_constructor_traceterminalentry. h = ff_q_empty_constructor_traceterminalentry * S ((S (0)) * e) + (cfc_state_empty_constructor_traceterminal))))) /\ (forall cfc_index_empty_constructor_trace. (exists cfba_gap_empty_constructor_tracebound. cfba_gap_empty_constructor_tracebound + S (cfc_index_empty_constructor_trace) = (0)) -> exists cfc_old_empty_constructor_trace cfc_a_empty_constructor_trace cfc_b_empty_constructor_trace cfc_c_empty_constructor_trace cfc_d_empty_constructor_trace cfc_new_empty_constructor_trace cfc_quotient_empty_constructor_trace. ((exists cfc_state_empty_constructor_traceprevious. ((exists cfc_left_empty_constructor_tracepreviouscode cfc_right_empty_constructor_tracepreviouscode cfc_matrix_empty_constructor_tracepreviouscode. ((cfc_left_empty_constructor_tracepreviouscode = ((cfc_a_empty_constructor_trace) + (cfc_b_empty_constructor_trace)) * S ((cfc_a_empty_constructor_trace) + (cfc_b_empty_constructor_trace)) + ((cfc_b_empty_constructor_trace) + (cfc_b_empty_constructor_trace))) /\ ((cfc_right_empty_constructor_tracepreviouscode = ((cfc_c_empty_constructor_trace) + (cfc_d_empty_constructor_trace)) * S ((cfc_c_empty_constructor_trace) + (cfc_d_empty_constructor_trace)) + ((cfc_d_empty_constructor_trace) + (cfc_d_empty_constructor_trace))) /\ ((cfc_matrix_empty_constructor_tracepreviouscode = ((cfc_left_empty_constructor_tracepreviouscode) + (cfc_right_empty_constructor_tracepreviouscode)) * S ((cfc_left_empty_constructor_tracepreviouscode) + (cfc_right_empty_constructor_tracepreviouscode)) + ((cfc_right_empty_constructor_tracepreviouscode) + (cfc_right_empty_constructor_tracepreviouscode))) /\ ((cfc_state_empty_constructor_traceprevious) = ((cfc_old_empty_constructor_trace) + (cfc_matrix_empty_constructor_tracepreviouscode)) * S ((cfc_old_empty_constructor_trace) + (cfc_matrix_empty_constructor_tracepreviouscode)) + ((cfc_matrix_empty_constructor_tracepreviouscode) + (cfc_matrix_empty_constructor_tracepreviouscode))))))) /\ (((exists ff_h_empty_constructor_tracepreviousentry. ff_h_empty_constructor_tracepreviousentry + S (cfc_state_empty_constructor_traceprevious) = S ((S (cfc_index_empty_constructor_trace)) * e)) /\ exists ff_q_empty_constructor_tracepreviousentry. h = ff_q_empty_constructor_tracepreviousentry * S ((S (cfc_index_empty_constructor_trace)) * e) + (cfc_state_empty_constructor_traceprevious))))) /\ ((exists cfc_state_empty_constructor_tracefollowing. ((exists cfc_left_empty_constructor_tracefollowingcode cfc_right_empty_constructor_tracefollowingcode cfc_matrix_empty_constructor_tracefollowingcode. ((cfc_left_empty_constructor_tracefollowingcode = (((cfc_quotient_empty_constructor_trace * cfc_a_empty_constructor_trace + cfc_c_empty_constructor_trace)) + ((cfc_quotient_empty_constructor_trace * cfc_b_empty_constructor_trace + cfc_d_empty_constructor_trace))) * S (((cfc_quotient_empty_constructor_trace * cfc_a_empty_constructor_trace + cfc_c_empty_constructor_trace)) + ((cfc_quotient_empty_constructor_trace * cfc_b_empty_constructor_trace + cfc_d_empty_constructor_trace))) + (((cfc_quotient_empty_constructor_trace * cfc_b_empty_constructor_trace + cfc_d_empty_constructor_trace)) + ((cfc_quotient_empty_constructor_trace * cfc_b_empty_constructor_trace + cfc_d_empty_constructor_trace)))) /\ ((cfc_right_empty_constructor_tracefollowingcode = ((cfc_a_empty_constructor_trace) + (cfc_b_empty_constructor_trace)) * S ((cfc_a_empty_constructor_trace) + (cfc_b_empty_constructor_trace)) + ((cfc_b_empty_constructor_trace) + (cfc_b_empty_constructor_trace))) /\ ((cfc_matrix_empty_constructor_tracefollowingcode = ((cfc_left_empty_constructor_tracefollowingcode) + (cfc_right_empty_constructor_tracefollowingcode)) * S ((cfc_left_empty_constructor_tracefollowingcode) + (cfc_right_empty_constructor_tracefollowingcode)) + ((cfc_right_empty_constructor_tracefollowingcode) + (cfc_right_empty_constructor_tracefollowingcode))) /\ ((cfc_state_empty_constructor_tracefollowing) = ((cfc_new_empty_constructor_trace) + (cfc_matrix_empty_constructor_tracefollowingcode)) * S ((cfc_new_empty_constructor_trace) + (cfc_matrix_empty_constructor_tracefollowingcode)) + ((cfc_matrix_empty_constructor_tracefollowingcode) + (cfc_matrix_empty_constructor_tracefollowingcode))))))) /\ (((exists ff_h_empty_constructor_tracefollowingentry. ff_h_empty_constructor_tracefollowingentry + S (cfc_state_empty_constructor_tracefollowing) = S ((S (S cfc_index_empty_constructor_trace)) * e)) /\ exists ff_q_empty_constructor_tracefollowingentry. h = ff_q_empty_constructor_tracefollowingentry * S ((S (S cfc_index_empty_constructor_trace)) * e) + (cfc_state_empty_constructor_tracefollowing))))) /\ (cfc_new_empty_constructor_trace = S ((cfc_quotient_empty_constructor_trace + cfc_old_empty_constructor_trace) * S (cfc_quotient_empty_constructor_trace + cfc_old_empty_constructor_trace) + (cfc_old_empty_constructor_trace + cfc_old_empty_constructor_trace)))))))))

Complete tactic proof in conservative notation

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

15 script commands · 9 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.

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 no index below zero
01Fix variables and assumptionsL1–4

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

  1. L1
    intro s
  2. L2
    intro h
  3. L3
    intro e
  4. L4
    intro ha
02Construct an explicit witnessL5–5

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

  1. L5
    exists s
03Separate the logical casesL6–6

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

  1. L6
    split
04Use earlier factsL7–7

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

  1. L7
    exact ha
05Separate the logical casesL8–8

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

  1. L8
    split
06Use earlier factsL9–9

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

  1. L9
    exact ha
07Fix variables and assumptionsL10–11

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

  1. L10
    intro j
  2. L11
    intro hj
08Separate the logical casesL12–12

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

  1. L12
    exfalso
09Use earlier factsL13–15

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

  1. L13
    specialize cf_convergent_no_index_below_zero (j)
  2. L14
    apply cf_convergent_no_index_below_zero
  3. L15
    exact hj

Library-wide reading audit

Original defined command ledger · 15 lines
  1. 0001intro s
  2. 0002intro h
  3. 0003intro e
  4. 0004intro ha
  5. 0005exists s
  6. 0006split
  7. 0007exact ha
  8. 0008split
  9. 0009exact ha
  10. 0010intro j
  11. 0011intro hj
  12. 0012exfalso
  13. 0013specialize cf_convergent_no_index_below_zero (j)
  14. 0014apply cf_convergent_no_index_below_zero
  15. 0015exact hj