BA003A

cf_convergent_matrix_empty_exists

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

The zero-step matrix prefix has a genuine finite beta certificate for every unconsumed tagged list.

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. exists h e. (exists cfc_tail_empty_exists_trace. ((exists cfc_state_empty_exists_traceinitial. ((exists cfc_left_empty_exists_traceinitialcode cfc_right_empty_exists_traceinitialcode cfc_matrix_empty_exists_traceinitialcode. ((cfc_left_empty_exists_traceinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_empty_exists_traceinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_empty_exists_traceinitialcode = ((cfc_left_empty_exists_traceinitialcode) + (cfc_right_empty_exists_traceinitialcode)) * S ((cfc_left_empty_exists_traceinitialcode) + (cfc_right_empty_exists_traceinitialcode)) + ((cfc_right_empty_exists_traceinitialcode) + (cfc_right_empty_exists_traceinitialcode))) /\ ((cfc_state_empty_exists_traceinitial) = ((cfc_tail_empty_exists_trace) + (cfc_matrix_empty_exists_traceinitialcode)) * S ((cfc_tail_empty_exists_trace) + (cfc_matrix_empty_exists_traceinitialcode)) + ((cfc_matrix_empty_exists_traceinitialcode) + (cfc_matrix_empty_exists_traceinitialcode))))))) /\ (((exists ff_h_empty_exists_traceinitialentry. ff_h_empty_exists_traceinitialentry + S (cfc_state_empty_exists_traceinitial) = S ((S (0)) * e)) /\ exists ff_q_empty_exists_traceinitialentry. h = ff_q_empty_exists_traceinitialentry * S ((S (0)) * e) + (cfc_state_empty_exists_traceinitial))))) /\ ((exists cfc_state_empty_exists_traceterminal. ((exists cfc_left_empty_exists_traceterminalcode cfc_right_empty_exists_traceterminalcode cfc_matrix_empty_exists_traceterminalcode. ((cfc_left_empty_exists_traceterminalcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_empty_exists_traceterminalcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_empty_exists_traceterminalcode = ((cfc_left_empty_exists_traceterminalcode) + (cfc_right_empty_exists_traceterminalcode)) * S ((cfc_left_empty_exists_traceterminalcode) + (cfc_right_empty_exists_traceterminalcode)) + ((cfc_right_empty_exists_traceterminalcode) + (cfc_right_empty_exists_traceterminalcode))) /\ ((cfc_state_empty_exists_traceterminal) = ((s) + (cfc_matrix_empty_exists_traceterminalcode)) * S ((s) + (cfc_matrix_empty_exists_traceterminalcode)) + ((cfc_matrix_empty_exists_traceterminalcode) + (cfc_matrix_empty_exists_traceterminalcode))))))) /\ (((exists ff_h_empty_exists_traceterminalentry. ff_h_empty_exists_traceterminalentry + S (cfc_state_empty_exists_traceterminal) = S ((S (0)) * e)) /\ exists ff_q_empty_exists_traceterminalentry. h = ff_q_empty_exists_traceterminalentry * S ((S (0)) * e) + (cfc_state_empty_exists_traceterminal))))) /\ (forall cfc_index_empty_exists_trace. (exists cfba_gap_empty_exists_tracebound. cfba_gap_empty_exists_tracebound + S (cfc_index_empty_exists_trace) = (0)) -> exists cfc_old_empty_exists_trace cfc_a_empty_exists_trace cfc_b_empty_exists_trace cfc_c_empty_exists_trace cfc_d_empty_exists_trace cfc_new_empty_exists_trace cfc_quotient_empty_exists_trace. ((exists cfc_state_empty_exists_traceprevious. ((exists cfc_left_empty_exists_tracepreviouscode cfc_right_empty_exists_tracepreviouscode cfc_matrix_empty_exists_tracepreviouscode. ((cfc_left_empty_exists_tracepreviouscode = ((cfc_a_empty_exists_trace) + (cfc_b_empty_exists_trace)) * S ((cfc_a_empty_exists_trace) + (cfc_b_empty_exists_trace)) + ((cfc_b_empty_exists_trace) + (cfc_b_empty_exists_trace))) /\ ((cfc_right_empty_exists_tracepreviouscode = ((cfc_c_empty_exists_trace) + (cfc_d_empty_exists_trace)) * S ((cfc_c_empty_exists_trace) + (cfc_d_empty_exists_trace)) + ((cfc_d_empty_exists_trace) + (cfc_d_empty_exists_trace))) /\ ((cfc_matrix_empty_exists_tracepreviouscode = ((cfc_left_empty_exists_tracepreviouscode) + (cfc_right_empty_exists_tracepreviouscode)) * S ((cfc_left_empty_exists_tracepreviouscode) + (cfc_right_empty_exists_tracepreviouscode)) + ((cfc_right_empty_exists_tracepreviouscode) + (cfc_right_empty_exists_tracepreviouscode))) /\ ((cfc_state_empty_exists_traceprevious) = ((cfc_old_empty_exists_trace) + (cfc_matrix_empty_exists_tracepreviouscode)) * S ((cfc_old_empty_exists_trace) + (cfc_matrix_empty_exists_tracepreviouscode)) + ((cfc_matrix_empty_exists_tracepreviouscode) + (cfc_matrix_empty_exists_tracepreviouscode))))))) /\ (((exists ff_h_empty_exists_tracepreviousentry. ff_h_empty_exists_tracepreviousentry + S (cfc_state_empty_exists_traceprevious) = S ((S (cfc_index_empty_exists_trace)) * e)) /\ exists ff_q_empty_exists_tracepreviousentry. h = ff_q_empty_exists_tracepreviousentry * S ((S (cfc_index_empty_exists_trace)) * e) + (cfc_state_empty_exists_traceprevious))))) /\ ((exists cfc_state_empty_exists_tracefollowing. ((exists cfc_left_empty_exists_tracefollowingcode cfc_right_empty_exists_tracefollowingcode cfc_matrix_empty_exists_tracefollowingcode. ((cfc_left_empty_exists_tracefollowingcode = (((cfc_quotient_empty_exists_trace * cfc_a_empty_exists_trace + cfc_c_empty_exists_trace)) + ((cfc_quotient_empty_exists_trace * cfc_b_empty_exists_trace + cfc_d_empty_exists_trace))) * S (((cfc_quotient_empty_exists_trace * cfc_a_empty_exists_trace + cfc_c_empty_exists_trace)) + ((cfc_quotient_empty_exists_trace * cfc_b_empty_exists_trace + cfc_d_empty_exists_trace))) + (((cfc_quotient_empty_exists_trace * cfc_b_empty_exists_trace + cfc_d_empty_exists_trace)) + ((cfc_quotient_empty_exists_trace * cfc_b_empty_exists_trace + cfc_d_empty_exists_trace)))) /\ ((cfc_right_empty_exists_tracefollowingcode = ((cfc_a_empty_exists_trace) + (cfc_b_empty_exists_trace)) * S ((cfc_a_empty_exists_trace) + (cfc_b_empty_exists_trace)) + ((cfc_b_empty_exists_trace) + (cfc_b_empty_exists_trace))) /\ ((cfc_matrix_empty_exists_tracefollowingcode = ((cfc_left_empty_exists_tracefollowingcode) + (cfc_right_empty_exists_tracefollowingcode)) * S ((cfc_left_empty_exists_tracefollowingcode) + (cfc_right_empty_exists_tracefollowingcode)) + ((cfc_right_empty_exists_tracefollowingcode) + (cfc_right_empty_exists_tracefollowingcode))) /\ ((cfc_state_empty_exists_tracefollowing) = ((cfc_new_empty_exists_trace) + (cfc_matrix_empty_exists_tracefollowingcode)) * S ((cfc_new_empty_exists_trace) + (cfc_matrix_empty_exists_tracefollowingcode)) + ((cfc_matrix_empty_exists_tracefollowingcode) + (cfc_matrix_empty_exists_tracefollowingcode))))))) /\ (((exists ff_h_empty_exists_tracefollowingentry. ff_h_empty_exists_tracefollowingentry + S (cfc_state_empty_exists_tracefollowing) = S ((S (S cfc_index_empty_exists_trace)) * e)) /\ exists ff_q_empty_exists_tracefollowingentry. h = ff_q_empty_exists_tracefollowingentry * S ((S (S cfc_index_empty_exists_trace)) * e) + (cfc_state_empty_exists_tracefollowing))))) /\ (cfc_new_empty_exists_trace = S ((cfc_quotient_empty_exists_trace + cfc_old_empty_exists_trace) * S (cfc_quotient_empty_exists_trace + cfc_old_empty_exists_trace) + (cfc_old_empty_exists_trace + cfc_old_empty_exists_trace)))))))))

Constructive proof overview

Generated structural guide

The zero-step matrix prefix has a genuine finite beta certificate for every unconsumed tagged list.

The unchanged tactic script uses 3 declared prerequisites and contains 28 exact native proof lines.

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

Proof neighborhood

Direct dependencies

BA002F cf_convergent_state_code_exists beta_prefix_extend Stable theorem; checked-use authorized BA0039 cf_convergent_matrix_empty_constructor

Direct dependents

BA003F cf_convergent_every_valid_matrix_prefix_exists BA0043 cf_convergent_initial_matrix_exists BA004F cf_convergent_second_column_is_previous_prefix

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

28 script commands · 10 reading checkpoints · 2 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 (2)
cf convergent state code existscf convergent matrix empty constructor

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–1

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

  1. L1
    intro s
02Establish hzL2–8

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent state code exists.

  1. L2
    have hz : ∃ z. ConvergentMatrixCode(s,1,0,0,1,z)Definitions: ConvergentMatrixCode
  2. L3
    specialize cf_convergent_state_code_exists (s)
  3. L4
    specialize cf_convergent_state_code_exists (1)
  4. L5
    specialize cf_convergent_state_code_exists (0)
  5. L6
    specialize cf_convergent_state_code_exists (0)
  6. L7
    specialize cf_convergent_state_code_exists (1)
  7. L8
    apply cf_convergent_state_code_exists
03Separate the logical casesL9–9

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

  1. L9
    cases hz
04Establish hbL10–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta prefix extend.

  1. L10
    have hb : ∃ h. ∃ e. BetaAt(h,e,0,x) ∧ (∀ y. ∀ z. Lt(y,0) → BetaAt(0,0,y,z) → BetaAt(h,e,y,z))Definitions: LtBetaAt
  2. L11
    specialize beta_prefix_extend (0)
  3. L12
    specialize beta_prefix_extend (0)
  4. L13
    specialize beta_prefix_extend (0)
  5. L14
    specialize beta_prefix_extend (x)
  6. L15
    apply beta_prefix_extend
05Separate the logical casesL16–18

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

  1. L16
    cases hb
  2. L17
    cases hb_witness
  3. L18
    cases hb_witness_witness
06Construct an explicit witnessL19–20

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

  1. L19
    exists x1
  2. L20
    exists x2
07Use earlier factsL21–24

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

  1. L21
    specialize cf_convergent_matrix_empty_constructor (s)
  2. L22
    specialize cf_convergent_matrix_empty_constructor (x1)
  3. L23
    specialize cf_convergent_matrix_empty_constructor (x2)
  4. L24
    apply cf_convergent_matrix_empty_constructor
08Construct an explicit witnessL25–25

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

  1. L25
    exists x
09Separate the logical casesL26–26

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

  1. L26
    split
10Use earlier factsL27–28

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

  1. L27
    exact hz_witness
  2. L28
    exact hb_witness_witness_left

Library-wide reading audit

Original exact command ledger · 28 lines
  1. 0001intro s
  2. 0002have hz : exists z. exists cfc_left_empty_exists_code cfc_right_empty_exists_code cfc_matrix_empty_exists_code. ((cfc_left_empty_exists_code = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_empty_exists_code = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_empty_exists_code = ((cfc_left_empty_exists_code) + (cfc_right_empty_exists_code)) * S ((cfc_left_empty_exists_code) + (cfc_right_empty_exists_code)) + ((cfc_right_empty_exists_code) + (cfc_right_empty_exists_code))) /\ ((z) = ((s) + (cfc_matrix_empty_exists_code)) * S ((s) + (cfc_matrix_empty_exists_code)) + ((cfc_matrix_empty_exists_code) + (cfc_matrix_empty_exists_code))))))
  3. 0003specialize cf_convergent_state_code_exists (s)
  4. 0004specialize cf_convergent_state_code_exists (1)
  5. 0005specialize cf_convergent_state_code_exists (0)
  6. 0006specialize cf_convergent_state_code_exists (0)
  7. 0007specialize cf_convergent_state_code_exists (1)
  8. 0008apply cf_convergent_state_code_exists
  9. 0009cases hz
  10. 0010have hb : exists h e. ((((exists ff_h_empty_exists_beta. ff_h_empty_exists_beta + S (x) = S ((S (0)) * e)) /\ exists ff_q_empty_exists_beta. h = ff_q_empty_exists_beta * S ((S (0)) * e) + (x))) /\ (forall cfc_index_empty_exists_preserves cfc_value_empty_exists_preserves. (exists cfba_gap_empty_exists_preservesbound. cfba_gap_empty_exists_preservesbound + S (cfc_index_empty_exists_preserves) = (0)) -> (((exists ff_h_empty_exists_preservessource. ff_h_empty_exists_preservessource + S (cfc_value_empty_exists_preserves) = S ((S (cfc_index_empty_exists_preserves)) * 0)) /\ exists ff_q_empty_exists_preservessource. 0 = ff_q_empty_exists_preservessource * S ((S (cfc_index_empty_exists_preserves)) * 0) + (cfc_value_empty_exists_preserves))) -> (((exists ff_h_empty_exists_preservestarget. ff_h_empty_exists_preservestarget + S (cfc_value_empty_exists_preserves) = S ((S (cfc_index_empty_exists_preserves)) * e)) /\ exists ff_q_empty_exists_preservestarget. h = ff_q_empty_exists_preservestarget * S ((S (cfc_index_empty_exists_preserves)) * e) + (cfc_value_empty_exists_preserves)))))
  11. 0011specialize beta_prefix_extend (0)
  12. 0012specialize beta_prefix_extend (0)
  13. 0013specialize beta_prefix_extend (0)
  14. 0014specialize beta_prefix_extend (x)
  15. 0015apply beta_prefix_extend
  16. 0016cases hb
  17. 0017cases hb_witness
  18. 0018cases hb_witness_witness
  19. 0019exists x1
  20. 0020exists x2
  21. 0021specialize cf_convergent_matrix_empty_constructor (s)
  22. 0022specialize cf_convergent_matrix_empty_constructor (x1)
  23. 0023specialize cf_convergent_matrix_empty_constructor (x2)
  24. 0024apply cf_convergent_matrix_empty_constructor
  25. 0025exists x
  26. 0026split
  27. 0027exact hz_witness
  28. 0028exact hb_witness_witness_left