DL0043

matrix_rank_selected_prefix_extend

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

Append one actual selected parent entry while preserving every earlier selected entry in the same new beta code.

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 b c w rb rc cb cc q ub uc l a. (forall mdr_i_prefix_previous. (exists mdr_gap_prefix_previousbound. mdr_gap_prefix_previousbound + S (mdr_i_prefix_previous) = (l)) -> exists mdr_a_prefix_previous. (((exists mdr_r_prefix_previouspoint mdr_s_prefix_previouspoint mdr_u_prefix_previouspoint mdr_v_prefix_previouspoint. ((mdr_i_prefix_previous = (q) * mdr_r_prefix_previouspoint + mdr_s_prefix_previouspoint) /\ ((exists mdr_gap_prefix_previouspointcolumn. mdr_gap_prefix_previouspointcolumn + S (mdr_s_prefix_previouspoint) = (q)) /\ ((((exists ff_h_mdr_prefix_previouspointrow_index. ff_h_mdr_prefix_previouspointrow_index + S (mdr_u_prefix_previouspoint) = S ((S (mdr_r_prefix_previouspoint)) * rc)) /\ exists ff_q_mdr_prefix_previouspointrow_index. rb = ff_q_mdr_prefix_previouspointrow_index * S ((S (mdr_r_prefix_previouspoint)) * rc) + (mdr_u_prefix_previouspoint))) /\ ((((exists ff_h_mdr_prefix_previouspointcolumn_index. ff_h_mdr_prefix_previouspointcolumn_index + S (mdr_v_prefix_previouspoint) = S ((S (mdr_s_prefix_previouspoint)) * cc)) /\ exists ff_q_mdr_prefix_previouspointcolumn_index. cb = ff_q_mdr_prefix_previouspointcolumn_index * S ((S (mdr_s_prefix_previouspoint)) * cc) + (mdr_v_prefix_previouspoint))) /\ (((exists ff_h_mdr_prefix_previouspointsource. ff_h_mdr_prefix_previouspointsource + S (mdr_a_prefix_previous) = S ((S ((mdr_u_prefix_previouspoint) * (w) + (mdr_v_prefix_previouspoint))) * c)) /\ exists ff_q_mdr_prefix_previouspointsource. b = ff_q_mdr_prefix_previouspointsource * S ((S ((mdr_u_prefix_previouspoint) * (w) + (mdr_v_prefix_previouspoint))) * c) + (mdr_a_prefix_previous)))))))) /\ (((exists ff_h_mdr_prefix_previousoutput. ff_h_mdr_prefix_previousoutput + S (mdr_a_prefix_previous) = S ((S (mdr_i_prefix_previous)) * uc)) /\ exists ff_q_mdr_prefix_previousoutput. ub = ff_q_mdr_prefix_previousoutput * S ((S (mdr_i_prefix_previous)) * uc) + (mdr_a_prefix_previous)))))) -> (exists mdr_r_prefix_last mdr_s_prefix_last mdr_u_prefix_last mdr_v_prefix_last. ((l = (q) * mdr_r_prefix_last + mdr_s_prefix_last) /\ ((exists mdr_gap_prefix_lastcolumn. mdr_gap_prefix_lastcolumn + S (mdr_s_prefix_last) = (q)) /\ ((((exists ff_h_mdr_prefix_lastrow_index. ff_h_mdr_prefix_lastrow_index + S (mdr_u_prefix_last) = S ((S (mdr_r_prefix_last)) * rc)) /\ exists ff_q_mdr_prefix_lastrow_index. rb = ff_q_mdr_prefix_lastrow_index * S ((S (mdr_r_prefix_last)) * rc) + (mdr_u_prefix_last))) /\ ((((exists ff_h_mdr_prefix_lastcolumn_index. ff_h_mdr_prefix_lastcolumn_index + S (mdr_v_prefix_last) = S ((S (mdr_s_prefix_last)) * cc)) /\ exists ff_q_mdr_prefix_lastcolumn_index. cb = ff_q_mdr_prefix_lastcolumn_index * S ((S (mdr_s_prefix_last)) * cc) + (mdr_v_prefix_last))) /\ (((exists ff_h_mdr_prefix_lastsource. ff_h_mdr_prefix_lastsource + S (a) = S ((S ((mdr_u_prefix_last) * (w) + (mdr_v_prefix_last))) * c)) /\ exists ff_q_mdr_prefix_lastsource. b = ff_q_mdr_prefix_lastsource * S ((S ((mdr_u_prefix_last) * (w) + (mdr_v_prefix_last))) * c) + (a)))))))) -> exists vb vc. (forall mdr_i_prefix_successor. (exists mdr_gap_prefix_successorbound. mdr_gap_prefix_successorbound + S (mdr_i_prefix_successor) = (S l)) -> exists mdr_a_prefix_successor. (((exists mdr_r_prefix_successorpoint mdr_s_prefix_successorpoint mdr_u_prefix_successorpoint mdr_v_prefix_successorpoint. ((mdr_i_prefix_successor = (q) * mdr_r_prefix_successorpoint + mdr_s_prefix_successorpoint) /\ ((exists mdr_gap_prefix_successorpointcolumn. mdr_gap_prefix_successorpointcolumn + S (mdr_s_prefix_successorpoint) = (q)) /\ ((((exists ff_h_mdr_prefix_successorpointrow_index. ff_h_mdr_prefix_successorpointrow_index + S (mdr_u_prefix_successorpoint) = S ((S (mdr_r_prefix_successorpoint)) * rc)) /\ exists ff_q_mdr_prefix_successorpointrow_index. rb = ff_q_mdr_prefix_successorpointrow_index * S ((S (mdr_r_prefix_successorpoint)) * rc) + (mdr_u_prefix_successorpoint))) /\ ((((exists ff_h_mdr_prefix_successorpointcolumn_index. ff_h_mdr_prefix_successorpointcolumn_index + S (mdr_v_prefix_successorpoint) = S ((S (mdr_s_prefix_successorpoint)) * cc)) /\ exists ff_q_mdr_prefix_successorpointcolumn_index. cb = ff_q_mdr_prefix_successorpointcolumn_index * S ((S (mdr_s_prefix_successorpoint)) * cc) + (mdr_v_prefix_successorpoint))) /\ (((exists ff_h_mdr_prefix_successorpointsource. ff_h_mdr_prefix_successorpointsource + S (mdr_a_prefix_successor) = S ((S ((mdr_u_prefix_successorpoint) * (w) + (mdr_v_prefix_successorpoint))) * c)) /\ exists ff_q_mdr_prefix_successorpointsource. b = ff_q_mdr_prefix_successorpointsource * S ((S ((mdr_u_prefix_successorpoint) * (w) + (mdr_v_prefix_successorpoint))) * c) + (mdr_a_prefix_successor)))))))) /\ (((exists ff_h_mdr_prefix_successoroutput. ff_h_mdr_prefix_successoroutput + S (mdr_a_prefix_successor) = S ((S (mdr_i_prefix_successor)) * vc)) /\ exists ff_q_mdr_prefix_successoroutput. vb = ff_q_mdr_prefix_successoroutput * S ((S (mdr_i_prefix_successor)) * vc) + (mdr_a_prefix_successor))))))

Constructive proof overview

Generated structural guide

Append one actual selected parent entry while preserving every earlier selected entry in the same new beta code.

The unchanged tactic script uses 2 declared prerequisites and contains 54 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_prefix_extend Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized

Direct dependents

DL0044 matrix_rank_selected_prefix_exists_nonzero

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

54 script commands · 19 reading checkpoints · 3 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.

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

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro w
  4. L4
    intro rb
  5. L5
    intro rc
  6. L6
    intro cb
  7. L7
    intro cc
  8. L8
    intro q
  9. L9
    intro ub
  10. L10
    intro uc
02Fix variables and assumptionsL11–14

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

  1. L11
    intro l
  2. L12
    intro a
  3. L13
    intro hprevious
  4. L14
    intro hpoint
03Establish hcodeL15–20

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

  1. L15
    have hcode : ∃ vb. ∃ vc. BetaAt(vb,vc,l,a) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(ub,uc,x,y) → BetaAt(vb,vc,x,y))Definitions: LtBetaAt
  2. L16
    specialize beta_prefix_extend (l)
  3. L17
    specialize beta_prefix_extend (ub)
  4. L18
    specialize beta_prefix_extend (uc)
  5. L19
    specialize beta_prefix_extend (a)
  6. L20
    apply beta_prefix_extend
04Separate the logical casesL21–23

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

  1. L21
    cases hcode
  2. L22
    cases hcode_witness
  3. L23
    cases hcode_witness_witness
05Construct an explicit witnessL24–25

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

  1. L24
    exists x
  2. L25
    exists x1
06Fix variables and assumptionsL26–27

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

  1. L26
    intro i
  2. L27
    intro hi
07Establish hindexL28–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L28
    have hindex : i = l \/ (exists mdr_gap_old_index. mdr_gap_old_index + S (i) = (l))
  2. L29
    specialize finite_lt_succ_eq_or_lt (l)
  3. L30
    specialize finite_lt_succ_eq_or_lt (i)
  4. L31
    apply finite_lt_succ_eq_or_lt
  5. L32
    exact hi
08Separate the logical casesL33–33

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

  1. L33
    cases hindex
09Construct an explicit witnessL34–34

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

  1. L34
    exists a
10Separate the logical casesL35–35

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

  1. L35
    split
11Calculate and transport equalitiesL36–36

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L36
    rewrite hindex_left
12Use earlier factsL37–37

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

  1. L37
    exact hpoint
13Calculate and transport equalitiesL38–39

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L38
    rewrite hindex_left
  2. L39
    rewrite hindex_left
14Use earlier factsL40–40

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

  1. L40
    exact hcode_witness_witness_left
15Establish holdL41–44

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

  1. L41
    have hold : ∃ z. (∃ x. ∃ y. ∃ n. ∃ m. i = q · x + y ∧ (Lt(y,q) ∧ (BetaAt(rb,rc,x,n) ∧ (BetaAt(cb,cc,y,m) ∧ BetaAt(b,c,n · w + m,z))))) ∧ BetaAt(ub,uc,i,z)Definitions: LtBetaAt
  2. L42
    specialize hprevious (i)
  3. L43
    apply hprevious
  4. L44
    exact hindex_right
16Separate the logical casesL45–46

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

  1. L45
    cases hold
  2. L46
    cases hold_witness
17Construct an explicit witnessL47–47

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

  1. L47
    exists x2
18Separate the logical casesL48–48

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

  1. L48
    split
19Use earlier factsL49–54

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

  1. L49
    exact hold_witness_left
  2. L50
    specialize hcode_witness_witness_right (i)
  3. L51
    specialize hcode_witness_witness_right (x2)
  4. L52
    apply hcode_witness_witness_right
  5. L53
    exact hindex_right
  6. L54
    exact hold_witness_right

Library-wide reading audit

Original exact command ledger · 54 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro w
  4. 0004intro rb
  5. 0005intro rc
  6. 0006intro cb
  7. 0007intro cc
  8. 0008intro q
  9. 0009intro ub
  10. 0010intro uc
  11. 0011intro l
  12. 0012intro a
  13. 0013intro hprevious
  14. 0014intro hpoint
  15. 0015have hcode : exists vb vc. ((((exists ff_h_mdr_new_entry. ff_h_mdr_new_entry + S (a) = S ((S (l)) * vc)) /\ exists ff_q_mdr_new_entry. vb = ff_q_mdr_new_entry * S ((S (l)) * vc) + (a))) /\ (forall mdr_i_old_entries mdr_a_old_entries. (exists mdr_gap_old_entriesb. mdr_gap_old_entriesb + S (mdr_i_old_entries) = (l)) -> (((exists ff_h_mdr_old_entrieso. ff_h_mdr_old_entrieso + S (mdr_a_old_entries) = S ((S (mdr_i_old_entries)) * uc)) /\ exists ff_q_mdr_old_entrieso. ub = ff_q_mdr_old_entrieso * S ((S (mdr_i_old_entries)) * uc) + (mdr_a_old_entries))) -> (((exists ff_h_mdr_old_entriesn. ff_h_mdr_old_entriesn + S (mdr_a_old_entries) = S ((S (mdr_i_old_entries)) * vc)) /\ exists ff_q_mdr_old_entriesn. vb = ff_q_mdr_old_entriesn * S ((S (mdr_i_old_entries)) * vc) + (mdr_a_old_entries)))))
  16. 0016specialize beta_prefix_extend (l)
  17. 0017specialize beta_prefix_extend (ub)
  18. 0018specialize beta_prefix_extend (uc)
  19. 0019specialize beta_prefix_extend (a)
  20. 0020apply beta_prefix_extend
  21. 0021cases hcode
  22. 0022cases hcode_witness
  23. 0023cases hcode_witness_witness
  24. 0024exists x
  25. 0025exists x1
  26. 0026intro i
  27. 0027intro hi
  28. 0028have hindex : i = l \/ (exists mdr_gap_old_index. mdr_gap_old_index + S (i) = (l))
  29. 0029specialize finite_lt_succ_eq_or_lt (l)
  30. 0030specialize finite_lt_succ_eq_or_lt (i)
  31. 0031apply finite_lt_succ_eq_or_lt
  32. 0032exact hi
  33. 0033cases hindex
  34. 0034exists a
  35. 0035split
  36. 0036rewrite hindex_left
  37. 0037exact hpoint
  38. 0038rewrite hindex_left
  39. 0039rewrite hindex_left
  40. 0040exact hcode_witness_witness_left
  41. 0041have hold : exists z. ((exists mdr_r_old_point mdr_s_old_point mdr_u_old_point mdr_v_old_point. ((i = (q) * mdr_r_old_point + mdr_s_old_point) /\ ((exists mdr_gap_old_pointcolumn. mdr_gap_old_pointcolumn + S (mdr_s_old_point) = (q)) /\ ((((exists ff_h_mdr_old_pointrow_index. ff_h_mdr_old_pointrow_index + S (mdr_u_old_point) = S ((S (mdr_r_old_point)) * rc)) /\ exists ff_q_mdr_old_pointrow_index. rb = ff_q_mdr_old_pointrow_index * S ((S (mdr_r_old_point)) * rc) + (mdr_u_old_point))) /\ ((((exists ff_h_mdr_old_pointcolumn_index. ff_h_mdr_old_pointcolumn_index + S (mdr_v_old_point) = S ((S (mdr_s_old_point)) * cc)) /\ exists ff_q_mdr_old_pointcolumn_index. cb = ff_q_mdr_old_pointcolumn_index * S ((S (mdr_s_old_point)) * cc) + (mdr_v_old_point))) /\ (((exists ff_h_mdr_old_pointsource. ff_h_mdr_old_pointsource + S (z) = S ((S ((mdr_u_old_point) * (w) + (mdr_v_old_point))) * c)) /\ exists ff_q_mdr_old_pointsource. b = ff_q_mdr_old_pointsource * S ((S ((mdr_u_old_point) * (w) + (mdr_v_old_point))) * c) + (z)))))))) /\ (((exists ff_h_mdr_old_output. ff_h_mdr_old_output + S (z) = S ((S (i)) * uc)) /\ exists ff_q_mdr_old_output. ub = ff_q_mdr_old_output * S ((S (i)) * uc) + (z))))
  42. 0042specialize hprevious (i)
  43. 0043apply hprevious
  44. 0044exact hindex_right
  45. 0045cases hold
  46. 0046cases hold_witness
  47. 0047exists x2
  48. 0048split
  49. 0049exact hold_witness_left
  50. 0050specialize hcode_witness_witness_right (i)
  51. 0051specialize hcode_witness_witness_right (x2)
  52. 0052apply hcode_witness_witness_right
  53. 0053exact hindex_right
  54. 0054exact hold_witness_right