DL000D

matrix_recursive_children_empty

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

The empty minor-value prefix makes no unproved determinant claim.

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 l pb pc nb nc q eb ec fb fc. (forall mdr_j_empty_children. (exists mdr_gap_empty_childrenj. mdr_gap_empty_childrenj + S (mdr_j_empty_children) = (0)) -> exists mdr_i_empty_children mdr_up_empty_children mdr_us_empty_children mdr_un_empty_children mdr_ut_empty_children mdr_p_empty_children mdr_n_empty_children. ((exists mdr_gap_empty_childreni. mdr_gap_empty_childreni + S (mdr_i_empty_children) = (l)) /\ ((exists mdr_z_empty_childrenr. ((exists mdr_a_empty_childrenrc mdr_b_empty_childrenrc mdr_c_empty_childrenrc mdr_e_empty_childrenrc mdr_f_empty_childrenrc. ((mdr_a_empty_childrenrc = ((q) + (mdr_up_empty_children)) * S ((q) + (mdr_up_empty_children)) + ((mdr_up_empty_children) + (mdr_up_empty_children))) /\ ((mdr_b_empty_childrenrc = ((mdr_us_empty_children) + (mdr_un_empty_children)) * S ((mdr_us_empty_children) + (mdr_un_empty_children)) + ((mdr_un_empty_children) + (mdr_un_empty_children))) /\ ((mdr_c_empty_childrenrc = ((mdr_a_empty_childrenrc) + (mdr_b_empty_childrenrc)) * S ((mdr_a_empty_childrenrc) + (mdr_b_empty_childrenrc)) + ((mdr_b_empty_childrenrc) + (mdr_b_empty_childrenrc))) /\ ((mdr_e_empty_childrenrc = ((mdr_p_empty_children) + (mdr_n_empty_children)) * S ((mdr_p_empty_children) + (mdr_n_empty_children)) + ((mdr_n_empty_children) + (mdr_n_empty_children))) /\ ((mdr_f_empty_childrenrc = ((mdr_ut_empty_children) + (mdr_e_empty_childrenrc)) * S ((mdr_ut_empty_children) + (mdr_e_empty_childrenrc)) + ((mdr_e_empty_childrenrc) + (mdr_e_empty_childrenrc))) /\ ((mdr_z_empty_childrenr) = ((mdr_c_empty_childrenrc) + (mdr_f_empty_childrenrc)) * S ((mdr_c_empty_childrenrc) + (mdr_f_empty_childrenrc)) + ((mdr_f_empty_childrenrc) + (mdr_f_empty_childrenrc))))))))) /\ (((exists ff_h_mdr_empty_childrenrb. ff_h_mdr_empty_childrenrb + S (mdr_z_empty_childrenr) = S ((S (mdr_i_empty_children)) * c)) /\ exists ff_q_mdr_empty_childrenrb. b = ff_q_mdr_empty_childrenrb * S ((S (mdr_i_empty_children)) * c) + (mdr_z_empty_childrenr))))) /\ ((((forall ff_index_mdm_prefix_mdr_empty_childrenm_positive. (exists ff_gap_mdm_lt_mdr_empty_childrenm_positive_index_bound. ff_gap_mdm_lt_mdr_empty_childrenm_positive_index_bound + S (ff_index_mdm_prefix_mdr_empty_childrenm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_empty_childrenm_positive ff_column_mdm_prefix_mdr_empty_childrenm_positive ff_value_mdm_prefix_mdr_empty_childrenm_positive. (ff_index_mdm_prefix_mdr_empty_childrenm_positive = (q) * ff_row_mdm_prefix_mdr_empty_childrenm_positive + ff_column_mdm_prefix_mdr_empty_childrenm_positive /\ ((exists ff_gap_mdm_lt_mdr_empty_childrenm_positive_column_bound. ff_gap_mdm_lt_mdr_empty_childrenm_positive_column_bound + S (ff_column_mdm_prefix_mdr_empty_childrenm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_empty_childrenm_positive_cell ff_column_mdm_cell_mdr_empty_childrenm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_empty_childrenm_positive_cell_row_before. ff_gap_mdm_lt_mdr_empty_childrenm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_empty_childrenm_positive) = (0)) /\ ff_row_mdm_cell_mdr_empty_childrenm_positive_cell = ff_row_mdm_prefix_mdr_empty_childrenm_positive) \/ ((exists ff_gap_mdm_le_mdr_empty_childrenm_positive_cell_row_after. ff_gap_mdm_le_mdr_empty_childrenm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_empty_childrenm_positive)) /\ ff_row_mdm_cell_mdr_empty_childrenm_positive_cell = S ff_row_mdm_prefix_mdr_empty_childrenm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_empty_childrenm_positive_cell_column_before. ff_gap_mdm_lt_mdr_empty_childrenm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_empty_childrenm_positive) = (mdr_j_empty_children)) /\ ff_column_mdm_cell_mdr_empty_childrenm_positive_cell = ff_column_mdm_prefix_mdr_empty_childrenm_positive) \/ ((exists ff_gap_mdm_le_mdr_empty_childrenm_positive_cell_column_after. ff_gap_mdm_le_mdr_empty_childrenm_positive_cell_column_after + (mdr_j_empty_children) = (ff_column_mdm_prefix_mdr_empty_childrenm_positive)) /\ ff_column_mdm_cell_mdr_empty_childrenm_positive_cell = S ff_column_mdm_prefix_mdr_empty_childrenm_positive))) /\ (((exists ff_h_mdm_mdr_empty_childrenm_positive_cell_source. ff_h_mdm_mdr_empty_childrenm_positive_cell_source + S (ff_value_mdm_prefix_mdr_empty_childrenm_positive) = S ((S ((ff_row_mdm_cell_mdr_empty_childrenm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_empty_childrenm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_empty_childrenm_positive_cell_source. pb = ff_q_mdm_mdr_empty_childrenm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_empty_childrenm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_empty_childrenm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_empty_childrenm_positive)))))) /\ (((exists ff_h_mdm_mdr_empty_childrenm_positive_target. ff_h_mdm_mdr_empty_childrenm_positive_target + S (ff_value_mdm_prefix_mdr_empty_childrenm_positive) = S ((S (ff_index_mdm_prefix_mdr_empty_childrenm_positive)) * mdr_us_empty_children)) /\ exists ff_q_mdm_mdr_empty_childrenm_positive_target. mdr_up_empty_children = ff_q_mdm_mdr_empty_childrenm_positive_target * S ((S (ff_index_mdm_prefix_mdr_empty_childrenm_positive)) * mdr_us_empty_children) + (ff_value_mdm_prefix_mdr_empty_childrenm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_empty_childrenm_negative. (exists ff_gap_mdm_lt_mdr_empty_childrenm_negative_index_bound. ff_gap_mdm_lt_mdr_empty_childrenm_negative_index_bound + S (ff_index_mdm_prefix_mdr_empty_childrenm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_empty_childrenm_negative ff_column_mdm_prefix_mdr_empty_childrenm_negative ff_value_mdm_prefix_mdr_empty_childrenm_negative. (ff_index_mdm_prefix_mdr_empty_childrenm_negative = (q) * ff_row_mdm_prefix_mdr_empty_childrenm_negative + ff_column_mdm_prefix_mdr_empty_childrenm_negative /\ ((exists ff_gap_mdm_lt_mdr_empty_childrenm_negative_column_bound. ff_gap_mdm_lt_mdr_empty_childrenm_negative_column_bound + S (ff_column_mdm_prefix_mdr_empty_childrenm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_empty_childrenm_negative_cell ff_column_mdm_cell_mdr_empty_childrenm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_empty_childrenm_negative_cell_row_before. ff_gap_mdm_lt_mdr_empty_childrenm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_empty_childrenm_negative) = (0)) /\ ff_row_mdm_cell_mdr_empty_childrenm_negative_cell = ff_row_mdm_prefix_mdr_empty_childrenm_negative) \/ ((exists ff_gap_mdm_le_mdr_empty_childrenm_negative_cell_row_after. ff_gap_mdm_le_mdr_empty_childrenm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_empty_childrenm_negative)) /\ ff_row_mdm_cell_mdr_empty_childrenm_negative_cell = S ff_row_mdm_prefix_mdr_empty_childrenm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_empty_childrenm_negative_cell_column_before. ff_gap_mdm_lt_mdr_empty_childrenm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_empty_childrenm_negative) = (mdr_j_empty_children)) /\ ff_column_mdm_cell_mdr_empty_childrenm_negative_cell = ff_column_mdm_prefix_mdr_empty_childrenm_negative) \/ ((exists ff_gap_mdm_le_mdr_empty_childrenm_negative_cell_column_after. ff_gap_mdm_le_mdr_empty_childrenm_negative_cell_column_after + (mdr_j_empty_children) = (ff_column_mdm_prefix_mdr_empty_childrenm_negative)) /\ ff_column_mdm_cell_mdr_empty_childrenm_negative_cell = S ff_column_mdm_prefix_mdr_empty_childrenm_negative))) /\ (((exists ff_h_mdm_mdr_empty_childrenm_negative_cell_source. ff_h_mdm_mdr_empty_childrenm_negative_cell_source + S (ff_value_mdm_prefix_mdr_empty_childrenm_negative) = S ((S ((ff_row_mdm_cell_mdr_empty_childrenm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_empty_childrenm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_empty_childrenm_negative_cell_source. nb = ff_q_mdm_mdr_empty_childrenm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_empty_childrenm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_empty_childrenm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_empty_childrenm_negative)))))) /\ (((exists ff_h_mdm_mdr_empty_childrenm_negative_target. ff_h_mdm_mdr_empty_childrenm_negative_target + S (ff_value_mdm_prefix_mdr_empty_childrenm_negative) = S ((S (ff_index_mdm_prefix_mdr_empty_childrenm_negative)) * mdr_ut_empty_children)) /\ exists ff_q_mdm_mdr_empty_childrenm_negative_target. mdr_un_empty_children = ff_q_mdm_mdr_empty_childrenm_negative_target * S ((S (ff_index_mdm_prefix_mdr_empty_childrenm_negative)) * mdr_ut_empty_children) + (ff_value_mdm_prefix_mdr_empty_childrenm_negative))))))))) /\ ((((exists ff_h_mdr_empty_childrenp. ff_h_mdr_empty_childrenp + S (mdr_p_empty_children) = S ((S (mdr_j_empty_children)) * ec)) /\ exists ff_q_mdr_empty_childrenp. eb = ff_q_mdr_empty_childrenp * S ((S (mdr_j_empty_children)) * ec) + (mdr_p_empty_children))) /\ (((exists ff_h_mdr_empty_childrenn. ff_h_mdr_empty_childrenn + S (mdr_n_empty_children) = S ((S (mdr_j_empty_children)) * fc)) /\ exists ff_q_mdr_empty_childrenn. fb = ff_q_mdr_empty_childrenn * S ((S (mdr_j_empty_children)) * fc) + (mdr_n_empty_children))))))))

Constructive proof overview

Generated structural guide

The empty minor-value prefix makes no unproved determinant claim.

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

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

Proof neighborhood

Direct dependencies

add_eq_zero_right Stable theorem; checked-use authorized succ_ne_zero Stable theorem; checked-use authorized

Direct dependents

DL0010 matrix_recursive_cofactor_prefix_from_recursion

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

24 script commands · 4 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.

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 l
  4. L4
    intro pb
  5. L5
    intro pc
  6. L6
    intro nb
  7. L7
    intro nc
  8. L8
    intro q
  9. L9
    intro eb
  10. L10
    intro ec
02Fix variables and assumptionsL11–14

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

  1. L11
    intro fb
  2. L12
    intro fc
  3. L13
    intro j
  4. L14
    intro hj
03Separate the logical casesL15–16

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

  1. L15
    exfalso
  2. L16
    cases hj
04Establish hzeroL17–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L17
    have hzero : S j = 0
  2. L18
    specialize add_eq_zero_right (x)
  3. L19
    specialize add_eq_zero_right (S j)
  4. L20
    apply add_eq_zero_right
  5. L21
    exact hj_witness
  6. L22
    specialize succ_ne_zero (j)
  7. L23
    apply succ_ne_zero
  8. L24
    exact hzero

Library-wide reading audit

Original exact command ledger · 24 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro pb
  5. 0005intro pc
  6. 0006intro nb
  7. 0007intro nc
  8. 0008intro q
  9. 0009intro eb
  10. 0010intro ec
  11. 0011intro fb
  12. 0012intro fc
  13. 0013intro j
  14. 0014intro hj
  15. 0015exfalso
  16. 0016cases hj
  17. 0017have hzero : S j = 0
  18. 0018specialize add_eq_zero_right (x)
  19. 0019specialize add_eq_zero_right (S j)
  20. 0020apply add_eq_zero_right
  21. 0021exact hj_witness
  22. 0022specialize succ_ne_zero (j)
  23. 0023apply succ_ne_zero
  24. 0024exact hzero