DL001D

matrix_recursive_minor_prefix_transport

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

An actual finite cofactor-minor code remains the same minor after extensionally equal recoding of its parent matrix.

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 B C q j u v. (forall mdr_i_minor_parent mdr_a_minor_parent. (exists mdr_gap_minor_parentb. mdr_gap_minor_parentb + S (mdr_i_minor_parent) = ((S q) * (S q))) -> (((exists ff_h_mdr_minor_parento. ff_h_mdr_minor_parento + S (mdr_a_minor_parent) = S ((S (mdr_i_minor_parent)) * c)) /\ exists ff_q_mdr_minor_parento. b = ff_q_mdr_minor_parento * S ((S (mdr_i_minor_parent)) * c) + (mdr_a_minor_parent))) -> (((exists ff_h_mdr_minor_parentn. ff_h_mdr_minor_parentn + S (mdr_a_minor_parent) = S ((S (mdr_i_minor_parent)) * C)) /\ exists ff_q_mdr_minor_parentn. B = ff_q_mdr_minor_parentn * S ((S (mdr_i_minor_parent)) * C) + (mdr_a_minor_parent)))) -> (forall ff_index_mdm_prefix_mdre_minor_source. (exists ff_gap_mdm_lt_mdre_minor_source_index_bound. ff_gap_mdm_lt_mdre_minor_source_index_bound + S (ff_index_mdm_prefix_mdre_minor_source) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdre_minor_source ff_column_mdm_prefix_mdre_minor_source ff_value_mdm_prefix_mdre_minor_source. (ff_index_mdm_prefix_mdre_minor_source = (q) * ff_row_mdm_prefix_mdre_minor_source + ff_column_mdm_prefix_mdre_minor_source /\ ((exists ff_gap_mdm_lt_mdre_minor_source_column_bound. ff_gap_mdm_lt_mdre_minor_source_column_bound + S (ff_column_mdm_prefix_mdre_minor_source) = (q)) /\ ((exists ff_row_mdm_cell_mdre_minor_source_cell ff_column_mdm_cell_mdre_minor_source_cell. (((((exists ff_gap_mdm_lt_mdre_minor_source_cell_row_before. ff_gap_mdm_lt_mdre_minor_source_cell_row_before + S (ff_row_mdm_prefix_mdre_minor_source) = (0)) /\ ff_row_mdm_cell_mdre_minor_source_cell = ff_row_mdm_prefix_mdre_minor_source) \/ ((exists ff_gap_mdm_le_mdre_minor_source_cell_row_after. ff_gap_mdm_le_mdre_minor_source_cell_row_after + (0) = (ff_row_mdm_prefix_mdre_minor_source)) /\ ff_row_mdm_cell_mdre_minor_source_cell = S ff_row_mdm_prefix_mdre_minor_source))) /\ (((((exists ff_gap_mdm_lt_mdre_minor_source_cell_column_before. ff_gap_mdm_lt_mdre_minor_source_cell_column_before + S (ff_column_mdm_prefix_mdre_minor_source) = (j)) /\ ff_column_mdm_cell_mdre_minor_source_cell = ff_column_mdm_prefix_mdre_minor_source) \/ ((exists ff_gap_mdm_le_mdre_minor_source_cell_column_after. ff_gap_mdm_le_mdre_minor_source_cell_column_after + (j) = (ff_column_mdm_prefix_mdre_minor_source)) /\ ff_column_mdm_cell_mdre_minor_source_cell = S ff_column_mdm_prefix_mdre_minor_source))) /\ (((exists ff_h_mdm_mdre_minor_source_cell_source. ff_h_mdm_mdre_minor_source_cell_source + S (ff_value_mdm_prefix_mdre_minor_source) = S ((S ((ff_row_mdm_cell_mdre_minor_source_cell) * (S (q)) + (ff_column_mdm_cell_mdre_minor_source_cell))) * c)) /\ exists ff_q_mdm_mdre_minor_source_cell_source. b = ff_q_mdm_mdre_minor_source_cell_source * S ((S ((ff_row_mdm_cell_mdre_minor_source_cell) * (S (q)) + (ff_column_mdm_cell_mdre_minor_source_cell))) * c) + (ff_value_mdm_prefix_mdre_minor_source)))))) /\ (((exists ff_h_mdm_mdre_minor_source_target. ff_h_mdm_mdre_minor_source_target + S (ff_value_mdm_prefix_mdre_minor_source) = S ((S (ff_index_mdm_prefix_mdre_minor_source)) * v)) /\ exists ff_q_mdm_mdre_minor_source_target. u = ff_q_mdm_mdre_minor_source_target * S ((S (ff_index_mdm_prefix_mdre_minor_source)) * v) + (ff_value_mdm_prefix_mdre_minor_source))))))) -> (forall ff_index_mdm_prefix_mdre_minor_result. (exists ff_gap_mdm_lt_mdre_minor_result_index_bound. ff_gap_mdm_lt_mdre_minor_result_index_bound + S (ff_index_mdm_prefix_mdre_minor_result) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdre_minor_result ff_column_mdm_prefix_mdre_minor_result ff_value_mdm_prefix_mdre_minor_result. (ff_index_mdm_prefix_mdre_minor_result = (q) * ff_row_mdm_prefix_mdre_minor_result + ff_column_mdm_prefix_mdre_minor_result /\ ((exists ff_gap_mdm_lt_mdre_minor_result_column_bound. ff_gap_mdm_lt_mdre_minor_result_column_bound + S (ff_column_mdm_prefix_mdre_minor_result) = (q)) /\ ((exists ff_row_mdm_cell_mdre_minor_result_cell ff_column_mdm_cell_mdre_minor_result_cell. (((((exists ff_gap_mdm_lt_mdre_minor_result_cell_row_before. ff_gap_mdm_lt_mdre_minor_result_cell_row_before + S (ff_row_mdm_prefix_mdre_minor_result) = (0)) /\ ff_row_mdm_cell_mdre_minor_result_cell = ff_row_mdm_prefix_mdre_minor_result) \/ ((exists ff_gap_mdm_le_mdre_minor_result_cell_row_after. ff_gap_mdm_le_mdre_minor_result_cell_row_after + (0) = (ff_row_mdm_prefix_mdre_minor_result)) /\ ff_row_mdm_cell_mdre_minor_result_cell = S ff_row_mdm_prefix_mdre_minor_result))) /\ (((((exists ff_gap_mdm_lt_mdre_minor_result_cell_column_before. ff_gap_mdm_lt_mdre_minor_result_cell_column_before + S (ff_column_mdm_prefix_mdre_minor_result) = (j)) /\ ff_column_mdm_cell_mdre_minor_result_cell = ff_column_mdm_prefix_mdre_minor_result) \/ ((exists ff_gap_mdm_le_mdre_minor_result_cell_column_after. ff_gap_mdm_le_mdre_minor_result_cell_column_after + (j) = (ff_column_mdm_prefix_mdre_minor_result)) /\ ff_column_mdm_cell_mdre_minor_result_cell = S ff_column_mdm_prefix_mdre_minor_result))) /\ (((exists ff_h_mdm_mdre_minor_result_cell_source. ff_h_mdm_mdre_minor_result_cell_source + S (ff_value_mdm_prefix_mdre_minor_result) = S ((S ((ff_row_mdm_cell_mdre_minor_result_cell) * (S (q)) + (ff_column_mdm_cell_mdre_minor_result_cell))) * C)) /\ exists ff_q_mdm_mdre_minor_result_cell_source. B = ff_q_mdm_mdre_minor_result_cell_source * S ((S ((ff_row_mdm_cell_mdre_minor_result_cell) * (S (q)) + (ff_column_mdm_cell_mdre_minor_result_cell))) * C) + (ff_value_mdm_prefix_mdre_minor_result)))))) /\ (((exists ff_h_mdm_mdre_minor_result_target. ff_h_mdm_mdre_minor_result_target + S (ff_value_mdm_prefix_mdre_minor_result) = S ((S (ff_index_mdm_prefix_mdre_minor_result)) * v)) /\ exists ff_q_mdm_mdre_minor_result_target. u = ff_q_mdm_mdre_minor_result_target * S ((S (ff_index_mdm_prefix_mdre_minor_result)) * v) + (ff_value_mdm_prefix_mdre_minor_result)))))))

Constructive proof overview

Generated structural guide

An actual finite cofactor-minor code remains the same minor after extensionally equal recoding of its parent matrix.

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

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

Proof neighborhood

Direct dependencies

DL001B matrix_recursive_quotient_row_bound DL001C matrix_recursive_minor_cell_transport

Direct dependents

DL001F matrix_recursive_signed_minor_extensional

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

51 script commands · 13 reading checkpoints · 1 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)
matrix recursive quotient row boundmatrix recursive minor cell transport

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 B
  4. L4
    intro C
  5. L5
    intro q
  6. L6
    intro j
  7. L7
    intro u
  8. L8
    intro v
  9. L9
    intro hprefix
  10. L10
    intro hminor
02Fix variables and assumptionsL11–12

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

  1. L11
    intro k
  2. L12
    intro hk
03Establish hentryL13–16

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

  1. L13
    have hentry : ∃ r. ∃ s. ∃ a. k = q · r + s ∧ (Lt(s,q) ∧ (MatrixMinorCell(b,c,S q,0,j,r,s,a) ∧ BetaAt(u,v,k,a)))Definitions: MatrixMinorCellLtBetaAt
  2. L14
    specialize hminor (k)
  3. L15
    apply hminor
  4. L16
    exact hk
04Separate the logical casesL17–22

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

  1. L17
    cases hentry
  2. L18
    cases hentry_witness
  3. L19
    cases hentry_witness_witness
  4. L20
    cases hentry_witness_witness_witness
  5. L21
    cases hentry_witness_witness_witness_right
  6. L22
    cases hentry_witness_witness_witness_right_right
05Construct an explicit witnessL23–25

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

  1. L23
    exists x
  2. L24
    exists x1
  3. L25
    exists x2
06Separate the logical casesL26–26

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

  1. L26
    split
07Use earlier factsL27–27

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

  1. L27
    exact hentry_witness_witness_witness_left
08Separate the logical casesL28–28

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

  1. L28
    split
09Use earlier factsL29–29

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

  1. L29
    exact hentry_witness_witness_witness_right_left
10Separate the logical casesL30–30

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

  1. L30
    split
11Use earlier factsL31–40

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

  1. L31
    specialize matrix_recursive_minor_cell_transport (b)
  2. L32
    specialize matrix_recursive_minor_cell_transport (c)
  3. L33
    specialize matrix_recursive_minor_cell_transport (B)
  4. L34
    specialize matrix_recursive_minor_cell_transport (C)
  5. L35
    specialize matrix_recursive_minor_cell_transport (q)
  6. L36
    specialize matrix_recursive_minor_cell_transport (j)
  7. L37
    specialize matrix_recursive_minor_cell_transport (x)
  8. L38
    specialize matrix_recursive_minor_cell_transport (x1)
  9. L39
    specialize matrix_recursive_minor_cell_transport (x2)
  10. L40
    apply matrix_recursive_minor_cell_transport
12Use earlier factsL41–50

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

  1. L41
    exact hprefix
  2. L42
    specialize matrix_recursive_quotient_row_bound (q)
  3. L43
    specialize matrix_recursive_quotient_row_bound (k)
  4. L44
    specialize matrix_recursive_quotient_row_bound (x)
  5. L45
    specialize matrix_recursive_quotient_row_bound (x1)
  6. L46
    apply matrix_recursive_quotient_row_bound
  7. L47
    exact hentry_witness_witness_witness_left
  8. L48
    exact hk
  9. L49
    exact hentry_witness_witness_witness_right_left
  10. L50
    exact hentry_witness_witness_witness_right_right_left
13Use earlier factsL51–51

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

  1. L51
    exact hentry_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 51 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro B
  4. 0004intro C
  5. 0005intro q
  6. 0006intro j
  7. 0007intro u
  8. 0008intro v
  9. 0009intro hprefix
  10. 0010intro hminor
  11. 0011intro k
  12. 0012intro hk
  13. 0013have hentry : exists r s a. ((k = q * r + s) /\ ((exists mdr_gap_entry_s. mdr_gap_entry_s + S (s) = (q)) /\ ((exists ff_row_mdm_cell_mdre_entry_cell ff_column_mdm_cell_mdre_entry_cell. (((((exists ff_gap_mdm_lt_mdre_entry_cell_row_before. ff_gap_mdm_lt_mdre_entry_cell_row_before + S (r) = (0)) /\ ff_row_mdm_cell_mdre_entry_cell = r) \/ ((exists ff_gap_mdm_le_mdre_entry_cell_row_after. ff_gap_mdm_le_mdre_entry_cell_row_after + (0) = (r)) /\ ff_row_mdm_cell_mdre_entry_cell = S r))) /\ (((((exists ff_gap_mdm_lt_mdre_entry_cell_column_before. ff_gap_mdm_lt_mdre_entry_cell_column_before + S (s) = (j)) /\ ff_column_mdm_cell_mdre_entry_cell = s) \/ ((exists ff_gap_mdm_le_mdre_entry_cell_column_after. ff_gap_mdm_le_mdre_entry_cell_column_after + (j) = (s)) /\ ff_column_mdm_cell_mdre_entry_cell = S s))) /\ (((exists ff_h_mdm_mdre_entry_cell_source. ff_h_mdm_mdre_entry_cell_source + S (a) = S ((S ((ff_row_mdm_cell_mdre_entry_cell) * (S (q)) + (ff_column_mdm_cell_mdre_entry_cell))) * c)) /\ exists ff_q_mdm_mdre_entry_cell_source. b = ff_q_mdm_mdre_entry_cell_source * S ((S ((ff_row_mdm_cell_mdre_entry_cell) * (S (q)) + (ff_column_mdm_cell_mdre_entry_cell))) * c) + (a)))))) /\ (((exists ff_h_mdr_entry_value. ff_h_mdr_entry_value + S (a) = S ((S (k)) * v)) /\ exists ff_q_mdr_entry_value. u = ff_q_mdr_entry_value * S ((S (k)) * v) + (a))))))
  14. 0014specialize hminor (k)
  15. 0015apply hminor
  16. 0016exact hk
  17. 0017cases hentry
  18. 0018cases hentry_witness
  19. 0019cases hentry_witness_witness
  20. 0020cases hentry_witness_witness_witness
  21. 0021cases hentry_witness_witness_witness_right
  22. 0022cases hentry_witness_witness_witness_right_right
  23. 0023exists x
  24. 0024exists x1
  25. 0025exists x2
  26. 0026split
  27. 0027exact hentry_witness_witness_witness_left
  28. 0028split
  29. 0029exact hentry_witness_witness_witness_right_left
  30. 0030split
  31. 0031specialize matrix_recursive_minor_cell_transport (b)
  32. 0032specialize matrix_recursive_minor_cell_transport (c)
  33. 0033specialize matrix_recursive_minor_cell_transport (B)
  34. 0034specialize matrix_recursive_minor_cell_transport (C)
  35. 0035specialize matrix_recursive_minor_cell_transport (q)
  36. 0036specialize matrix_recursive_minor_cell_transport (j)
  37. 0037specialize matrix_recursive_minor_cell_transport (x)
  38. 0038specialize matrix_recursive_minor_cell_transport (x1)
  39. 0039specialize matrix_recursive_minor_cell_transport (x2)
  40. 0040apply matrix_recursive_minor_cell_transport
  41. 0041exact hprefix
  42. 0042specialize matrix_recursive_quotient_row_bound (q)
  43. 0043specialize matrix_recursive_quotient_row_bound (k)
  44. 0044specialize matrix_recursive_quotient_row_bound (x)
  45. 0045specialize matrix_recursive_quotient_row_bound (x1)
  46. 0046apply matrix_recursive_quotient_row_bound
  47. 0047exact hentry_witness_witness_witness_left
  48. 0048exact hk
  49. 0049exact hentry_witness_witness_witness_right_left
  50. 0050exact hentry_witness_witness_witness_right_right_left
  51. 0051exact hentry_witness_witness_witness_right_right_right