BA0039

cf_convergent_matrix_empty_constructor

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

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

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

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

BA002B cf_convergent_no_index_below_zero

Direct dependents

BA003A cf_convergent_matrix_empty_exists

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

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.

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