BA003A

cf_convergent_matrix_empty_exists

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

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

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

Definition DAG

ConvergentMatrixCode(s,u,U,v,V,z) · 1ConvergentMatrixTrace(s,h,e,k,u,U,v,V) · 1Lt(a,b) · 1BetaAt(b,c,i,x) · 3

Actual proof prerequisites

cf_convergent_state_code_existsbeta_prefix_extend · checked external prerequisitecf_convergent_matrix_empty_constructor
Original expanded first-order 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)))))))))

Complete tactic proof in conservative notation

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

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.

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 (2)
cf convergent state code existscf convergent matrix empty constructor
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(s,1,0,0,1,z)Original native command in the exact edition
  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: BetaAt(h,e,0,x)Lt(y,0)BetaAt(0,0,y,z)BetaAt(h,e,y,z)Original native command in the exact edition
  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 defined command ledger · 28 lines
  1. 0001intro s
  2. 0002have hz : ∃ z. ConvergentMatrixCode(s,1,0,0,1,z)
  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 : ∃ h. ∃ e. BetaAt(h,e,0,x) ∧ (∀ y. ∀ z. Lt(y,0) → BetaAt(0,0,y,z) → BetaAt(h,e,y,z))
  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