DL0008

matrix_recursive_children_transport

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

Every actual smaller-matrix child remains present when its evaluation DAG is extended.

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 u v l m pb pc nb nc q eb ec fb fc k. (forall mdr_i_source mdr_a_source. (exists mdr_gap_sourceb. mdr_gap_sourceb + S (mdr_i_source) = (l)) -> (((exists ff_h_mdr_sourceo. ff_h_mdr_sourceo + S (mdr_a_source) = S ((S (mdr_i_source)) * c)) /\ exists ff_q_mdr_sourceo. b = ff_q_mdr_sourceo * S ((S (mdr_i_source)) * c) + (mdr_a_source))) -> (((exists ff_h_mdr_sourcen. ff_h_mdr_sourcen + S (mdr_a_source) = S ((S (mdr_i_source)) * v)) /\ exists ff_q_mdr_sourcen. u = ff_q_mdr_sourcen * S ((S (mdr_i_source)) * v) + (mdr_a_source)))) -> (exists mdr_gap_transport. mdr_gap_transport + (l) = (m)) -> (forall mdr_j_old. (exists mdr_gap_oldj. mdr_gap_oldj + S (mdr_j_old) = (k)) -> exists mdr_i_old mdr_up_old mdr_us_old mdr_un_old mdr_ut_old mdr_p_old mdr_n_old. ((exists mdr_gap_oldi. mdr_gap_oldi + S (mdr_i_old) = (l)) /\ ((exists mdr_z_oldr. ((exists mdr_a_oldrc mdr_b_oldrc mdr_c_oldrc mdr_e_oldrc mdr_f_oldrc. ((mdr_a_oldrc = ((q) + (mdr_up_old)) * S ((q) + (mdr_up_old)) + ((mdr_up_old) + (mdr_up_old))) /\ ((mdr_b_oldrc = ((mdr_us_old) + (mdr_un_old)) * S ((mdr_us_old) + (mdr_un_old)) + ((mdr_un_old) + (mdr_un_old))) /\ ((mdr_c_oldrc = ((mdr_a_oldrc) + (mdr_b_oldrc)) * S ((mdr_a_oldrc) + (mdr_b_oldrc)) + ((mdr_b_oldrc) + (mdr_b_oldrc))) /\ ((mdr_e_oldrc = ((mdr_p_old) + (mdr_n_old)) * S ((mdr_p_old) + (mdr_n_old)) + ((mdr_n_old) + (mdr_n_old))) /\ ((mdr_f_oldrc = ((mdr_ut_old) + (mdr_e_oldrc)) * S ((mdr_ut_old) + (mdr_e_oldrc)) + ((mdr_e_oldrc) + (mdr_e_oldrc))) /\ ((mdr_z_oldr) = ((mdr_c_oldrc) + (mdr_f_oldrc)) * S ((mdr_c_oldrc) + (mdr_f_oldrc)) + ((mdr_f_oldrc) + (mdr_f_oldrc))))))))) /\ (((exists ff_h_mdr_oldrb. ff_h_mdr_oldrb + S (mdr_z_oldr) = S ((S (mdr_i_old)) * c)) /\ exists ff_q_mdr_oldrb. b = ff_q_mdr_oldrb * S ((S (mdr_i_old)) * c) + (mdr_z_oldr))))) /\ ((((forall ff_index_mdm_prefix_mdr_oldm_positive. (exists ff_gap_mdm_lt_mdr_oldm_positive_index_bound. ff_gap_mdm_lt_mdr_oldm_positive_index_bound + S (ff_index_mdm_prefix_mdr_oldm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_oldm_positive ff_column_mdm_prefix_mdr_oldm_positive ff_value_mdm_prefix_mdr_oldm_positive. (ff_index_mdm_prefix_mdr_oldm_positive = (q) * ff_row_mdm_prefix_mdr_oldm_positive + ff_column_mdm_prefix_mdr_oldm_positive /\ ((exists ff_gap_mdm_lt_mdr_oldm_positive_column_bound. ff_gap_mdm_lt_mdr_oldm_positive_column_bound + S (ff_column_mdm_prefix_mdr_oldm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_oldm_positive_cell ff_column_mdm_cell_mdr_oldm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_oldm_positive_cell_row_before. ff_gap_mdm_lt_mdr_oldm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_oldm_positive) = (0)) /\ ff_row_mdm_cell_mdr_oldm_positive_cell = ff_row_mdm_prefix_mdr_oldm_positive) \/ ((exists ff_gap_mdm_le_mdr_oldm_positive_cell_row_after. ff_gap_mdm_le_mdr_oldm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_oldm_positive)) /\ ff_row_mdm_cell_mdr_oldm_positive_cell = S ff_row_mdm_prefix_mdr_oldm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_oldm_positive_cell_column_before. ff_gap_mdm_lt_mdr_oldm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_oldm_positive) = (mdr_j_old)) /\ ff_column_mdm_cell_mdr_oldm_positive_cell = ff_column_mdm_prefix_mdr_oldm_positive) \/ ((exists ff_gap_mdm_le_mdr_oldm_positive_cell_column_after. ff_gap_mdm_le_mdr_oldm_positive_cell_column_after + (mdr_j_old) = (ff_column_mdm_prefix_mdr_oldm_positive)) /\ ff_column_mdm_cell_mdr_oldm_positive_cell = S ff_column_mdm_prefix_mdr_oldm_positive))) /\ (((exists ff_h_mdm_mdr_oldm_positive_cell_source. ff_h_mdm_mdr_oldm_positive_cell_source + S (ff_value_mdm_prefix_mdr_oldm_positive) = S ((S ((ff_row_mdm_cell_mdr_oldm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_oldm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_oldm_positive_cell_source. pb = ff_q_mdm_mdr_oldm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_oldm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_oldm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_oldm_positive)))))) /\ (((exists ff_h_mdm_mdr_oldm_positive_target. ff_h_mdm_mdr_oldm_positive_target + S (ff_value_mdm_prefix_mdr_oldm_positive) = S ((S (ff_index_mdm_prefix_mdr_oldm_positive)) * mdr_us_old)) /\ exists ff_q_mdm_mdr_oldm_positive_target. mdr_up_old = ff_q_mdm_mdr_oldm_positive_target * S ((S (ff_index_mdm_prefix_mdr_oldm_positive)) * mdr_us_old) + (ff_value_mdm_prefix_mdr_oldm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_oldm_negative. (exists ff_gap_mdm_lt_mdr_oldm_negative_index_bound. ff_gap_mdm_lt_mdr_oldm_negative_index_bound + S (ff_index_mdm_prefix_mdr_oldm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_oldm_negative ff_column_mdm_prefix_mdr_oldm_negative ff_value_mdm_prefix_mdr_oldm_negative. (ff_index_mdm_prefix_mdr_oldm_negative = (q) * ff_row_mdm_prefix_mdr_oldm_negative + ff_column_mdm_prefix_mdr_oldm_negative /\ ((exists ff_gap_mdm_lt_mdr_oldm_negative_column_bound. ff_gap_mdm_lt_mdr_oldm_negative_column_bound + S (ff_column_mdm_prefix_mdr_oldm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_oldm_negative_cell ff_column_mdm_cell_mdr_oldm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_oldm_negative_cell_row_before. ff_gap_mdm_lt_mdr_oldm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_oldm_negative) = (0)) /\ ff_row_mdm_cell_mdr_oldm_negative_cell = ff_row_mdm_prefix_mdr_oldm_negative) \/ ((exists ff_gap_mdm_le_mdr_oldm_negative_cell_row_after. ff_gap_mdm_le_mdr_oldm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_oldm_negative)) /\ ff_row_mdm_cell_mdr_oldm_negative_cell = S ff_row_mdm_prefix_mdr_oldm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_oldm_negative_cell_column_before. ff_gap_mdm_lt_mdr_oldm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_oldm_negative) = (mdr_j_old)) /\ ff_column_mdm_cell_mdr_oldm_negative_cell = ff_column_mdm_prefix_mdr_oldm_negative) \/ ((exists ff_gap_mdm_le_mdr_oldm_negative_cell_column_after. ff_gap_mdm_le_mdr_oldm_negative_cell_column_after + (mdr_j_old) = (ff_column_mdm_prefix_mdr_oldm_negative)) /\ ff_column_mdm_cell_mdr_oldm_negative_cell = S ff_column_mdm_prefix_mdr_oldm_negative))) /\ (((exists ff_h_mdm_mdr_oldm_negative_cell_source. ff_h_mdm_mdr_oldm_negative_cell_source + S (ff_value_mdm_prefix_mdr_oldm_negative) = S ((S ((ff_row_mdm_cell_mdr_oldm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_oldm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_oldm_negative_cell_source. nb = ff_q_mdm_mdr_oldm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_oldm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_oldm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_oldm_negative)))))) /\ (((exists ff_h_mdm_mdr_oldm_negative_target. ff_h_mdm_mdr_oldm_negative_target + S (ff_value_mdm_prefix_mdr_oldm_negative) = S ((S (ff_index_mdm_prefix_mdr_oldm_negative)) * mdr_ut_old)) /\ exists ff_q_mdm_mdr_oldm_negative_target. mdr_un_old = ff_q_mdm_mdr_oldm_negative_target * S ((S (ff_index_mdm_prefix_mdr_oldm_negative)) * mdr_ut_old) + (ff_value_mdm_prefix_mdr_oldm_negative))))))))) /\ ((((exists ff_h_mdr_oldp. ff_h_mdr_oldp + S (mdr_p_old) = S ((S (mdr_j_old)) * ec)) /\ exists ff_q_mdr_oldp. eb = ff_q_mdr_oldp * S ((S (mdr_j_old)) * ec) + (mdr_p_old))) /\ (((exists ff_h_mdr_oldn. ff_h_mdr_oldn + S (mdr_n_old) = S ((S (mdr_j_old)) * fc)) /\ exists ff_q_mdr_oldn. fb = ff_q_mdr_oldn * S ((S (mdr_j_old)) * fc) + (mdr_n_old)))))))) -> (forall mdr_j_new. (exists mdr_gap_newj. mdr_gap_newj + S (mdr_j_new) = (k)) -> exists mdr_i_new mdr_up_new mdr_us_new mdr_un_new mdr_ut_new mdr_p_new mdr_n_new. ((exists mdr_gap_newi. mdr_gap_newi + S (mdr_i_new) = (m)) /\ ((exists mdr_z_newr. ((exists mdr_a_newrc mdr_b_newrc mdr_c_newrc mdr_e_newrc mdr_f_newrc. ((mdr_a_newrc = ((q) + (mdr_up_new)) * S ((q) + (mdr_up_new)) + ((mdr_up_new) + (mdr_up_new))) /\ ((mdr_b_newrc = ((mdr_us_new) + (mdr_un_new)) * S ((mdr_us_new) + (mdr_un_new)) + ((mdr_un_new) + (mdr_un_new))) /\ ((mdr_c_newrc = ((mdr_a_newrc) + (mdr_b_newrc)) * S ((mdr_a_newrc) + (mdr_b_newrc)) + ((mdr_b_newrc) + (mdr_b_newrc))) /\ ((mdr_e_newrc = ((mdr_p_new) + (mdr_n_new)) * S ((mdr_p_new) + (mdr_n_new)) + ((mdr_n_new) + (mdr_n_new))) /\ ((mdr_f_newrc = ((mdr_ut_new) + (mdr_e_newrc)) * S ((mdr_ut_new) + (mdr_e_newrc)) + ((mdr_e_newrc) + (mdr_e_newrc))) /\ ((mdr_z_newr) = ((mdr_c_newrc) + (mdr_f_newrc)) * S ((mdr_c_newrc) + (mdr_f_newrc)) + ((mdr_f_newrc) + (mdr_f_newrc))))))))) /\ (((exists ff_h_mdr_newrb. ff_h_mdr_newrb + S (mdr_z_newr) = S ((S (mdr_i_new)) * v)) /\ exists ff_q_mdr_newrb. u = ff_q_mdr_newrb * S ((S (mdr_i_new)) * v) + (mdr_z_newr))))) /\ ((((forall ff_index_mdm_prefix_mdr_newm_positive. (exists ff_gap_mdm_lt_mdr_newm_positive_index_bound. ff_gap_mdm_lt_mdr_newm_positive_index_bound + S (ff_index_mdm_prefix_mdr_newm_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_newm_positive ff_column_mdm_prefix_mdr_newm_positive ff_value_mdm_prefix_mdr_newm_positive. (ff_index_mdm_prefix_mdr_newm_positive = (q) * ff_row_mdm_prefix_mdr_newm_positive + ff_column_mdm_prefix_mdr_newm_positive /\ ((exists ff_gap_mdm_lt_mdr_newm_positive_column_bound. ff_gap_mdm_lt_mdr_newm_positive_column_bound + S (ff_column_mdm_prefix_mdr_newm_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_newm_positive_cell ff_column_mdm_cell_mdr_newm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_newm_positive_cell_row_before. ff_gap_mdm_lt_mdr_newm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_newm_positive) = (0)) /\ ff_row_mdm_cell_mdr_newm_positive_cell = ff_row_mdm_prefix_mdr_newm_positive) \/ ((exists ff_gap_mdm_le_mdr_newm_positive_cell_row_after. ff_gap_mdm_le_mdr_newm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_newm_positive)) /\ ff_row_mdm_cell_mdr_newm_positive_cell = S ff_row_mdm_prefix_mdr_newm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_newm_positive_cell_column_before. ff_gap_mdm_lt_mdr_newm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_newm_positive) = (mdr_j_new)) /\ ff_column_mdm_cell_mdr_newm_positive_cell = ff_column_mdm_prefix_mdr_newm_positive) \/ ((exists ff_gap_mdm_le_mdr_newm_positive_cell_column_after. ff_gap_mdm_le_mdr_newm_positive_cell_column_after + (mdr_j_new) = (ff_column_mdm_prefix_mdr_newm_positive)) /\ ff_column_mdm_cell_mdr_newm_positive_cell = S ff_column_mdm_prefix_mdr_newm_positive))) /\ (((exists ff_h_mdm_mdr_newm_positive_cell_source. ff_h_mdm_mdr_newm_positive_cell_source + S (ff_value_mdm_prefix_mdr_newm_positive) = S ((S ((ff_row_mdm_cell_mdr_newm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_newm_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_newm_positive_cell_source. pb = ff_q_mdm_mdr_newm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_newm_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_newm_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_newm_positive)))))) /\ (((exists ff_h_mdm_mdr_newm_positive_target. ff_h_mdm_mdr_newm_positive_target + S (ff_value_mdm_prefix_mdr_newm_positive) = S ((S (ff_index_mdm_prefix_mdr_newm_positive)) * mdr_us_new)) /\ exists ff_q_mdm_mdr_newm_positive_target. mdr_up_new = ff_q_mdm_mdr_newm_positive_target * S ((S (ff_index_mdm_prefix_mdr_newm_positive)) * mdr_us_new) + (ff_value_mdm_prefix_mdr_newm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_newm_negative. (exists ff_gap_mdm_lt_mdr_newm_negative_index_bound. ff_gap_mdm_lt_mdr_newm_negative_index_bound + S (ff_index_mdm_prefix_mdr_newm_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_newm_negative ff_column_mdm_prefix_mdr_newm_negative ff_value_mdm_prefix_mdr_newm_negative. (ff_index_mdm_prefix_mdr_newm_negative = (q) * ff_row_mdm_prefix_mdr_newm_negative + ff_column_mdm_prefix_mdr_newm_negative /\ ((exists ff_gap_mdm_lt_mdr_newm_negative_column_bound. ff_gap_mdm_lt_mdr_newm_negative_column_bound + S (ff_column_mdm_prefix_mdr_newm_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_newm_negative_cell ff_column_mdm_cell_mdr_newm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_newm_negative_cell_row_before. ff_gap_mdm_lt_mdr_newm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_newm_negative) = (0)) /\ ff_row_mdm_cell_mdr_newm_negative_cell = ff_row_mdm_prefix_mdr_newm_negative) \/ ((exists ff_gap_mdm_le_mdr_newm_negative_cell_row_after. ff_gap_mdm_le_mdr_newm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_newm_negative)) /\ ff_row_mdm_cell_mdr_newm_negative_cell = S ff_row_mdm_prefix_mdr_newm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_newm_negative_cell_column_before. ff_gap_mdm_lt_mdr_newm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_newm_negative) = (mdr_j_new)) /\ ff_column_mdm_cell_mdr_newm_negative_cell = ff_column_mdm_prefix_mdr_newm_negative) \/ ((exists ff_gap_mdm_le_mdr_newm_negative_cell_column_after. ff_gap_mdm_le_mdr_newm_negative_cell_column_after + (mdr_j_new) = (ff_column_mdm_prefix_mdr_newm_negative)) /\ ff_column_mdm_cell_mdr_newm_negative_cell = S ff_column_mdm_prefix_mdr_newm_negative))) /\ (((exists ff_h_mdm_mdr_newm_negative_cell_source. ff_h_mdm_mdr_newm_negative_cell_source + S (ff_value_mdm_prefix_mdr_newm_negative) = S ((S ((ff_row_mdm_cell_mdr_newm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_newm_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_newm_negative_cell_source. nb = ff_q_mdm_mdr_newm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_newm_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_newm_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_newm_negative)))))) /\ (((exists ff_h_mdm_mdr_newm_negative_target. ff_h_mdm_mdr_newm_negative_target + S (ff_value_mdm_prefix_mdr_newm_negative) = S ((S (ff_index_mdm_prefix_mdr_newm_negative)) * mdr_ut_new)) /\ exists ff_q_mdm_mdr_newm_negative_target. mdr_un_new = ff_q_mdm_mdr_newm_negative_target * S ((S (ff_index_mdm_prefix_mdr_newm_negative)) * mdr_ut_new) + (ff_value_mdm_prefix_mdr_newm_negative))))))))) /\ ((((exists ff_h_mdr_newp. ff_h_mdr_newp + S (mdr_p_new) = S ((S (mdr_j_new)) * ec)) /\ exists ff_q_mdr_newp. eb = ff_q_mdr_newp * S ((S (mdr_j_new)) * ec) + (mdr_p_new))) /\ (((exists ff_h_mdr_newn. ff_h_mdr_newn + S (mdr_n_new) = S ((S (mdr_j_new)) * fc)) /\ exists ff_q_mdr_newn. fb = ff_q_mdr_newn * S ((S (mdr_j_new)) * fc) + (mdr_n_new))))))))

Constructive proof overview

Generated structural guide

Every actual smaller-matrix child remains present when its evaluation DAG is extended.

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

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

Proof neighborhood

Direct dependencies

lt_of_lt_of_le Stable theorem; checked-use authorized DL0005 matrix_recursive_record_transport

Direct dependents

DL0009 matrix_recursive_step_transport 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

73 script commands · 16 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 (1)
matrix recursive record 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 u
  4. L4
    intro v
  5. L5
    intro l
  6. L6
    intro m
  7. L7
    intro pb
  8. L8
    intro pc
  9. L9
    intro nb
  10. L10
    intro nc
02Fix variables and assumptionsL11–20

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

  1. L11
    intro q
  2. L12
    intro eb
  3. L13
    intro ec
  4. L14
    intro fb
  5. L15
    intro fc
  6. L16
    intro k
  7. L17
    intro hprefix
  8. L18
    intro hlm
  9. L19
    intro hchildren
  10. L20
    intro j
03Fix variables and assumptionsL21–21

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

  1. L21
    intro hj
04Establish hentryL22–25

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

  1. L22
    have hentry : ∃ i. ∃ up. ∃ us. ∃ un. ∃ ut. ∃ a. ∃ z. Lt(i,l) ∧ (SignedDeterminantNodeAt(b,c,i,q,up,us,un,ut,a,z) ∧ (SignedMatrixMinor(pb,pc,nb,nc,S q,0,j,q,up,us,un,ut) ∧ (BetaAt(eb,ec,j,a) ∧ BetaAt(fb,fc,j,z))))Definitions: SignedMatrixMinorSignedDeterminantNodeAtLtBetaAt
  2. L23
    specialize hchildren (j)
  3. L24
    apply hchildren
  4. L25
    exact hj
05Separate the logical casesL26–35

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

  1. L26
    cases hentry
  2. L27
    cases hentry_witness
  3. L28
    cases hentry_witness_witness
  4. L29
    cases hentry_witness_witness_witness
  5. L30
    cases hentry_witness_witness_witness_witness
  6. L31
    cases hentry_witness_witness_witness_witness_witness
  7. L32
    cases hentry_witness_witness_witness_witness_witness_witness
  8. L33
    cases hentry_witness_witness_witness_witness_witness_witness_witness
  9. L34
    cases hentry_witness_witness_witness_witness_witness_witness_witness_right
  10. L35
    cases hentry_witness_witness_witness_witness_witness_witness_witness_right_right
06Separate the logical casesL36–36

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

  1. L36
    cases hentry_witness_witness_witness_witness_witness_witness_witness_right_right_right
07Construct an explicit witnessL37–43

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

  1. L37
    exists x
  2. L38
    exists x1
  3. L39
    exists x2
  4. L40
    exists x3
  5. L41
    exists x4
  6. L42
    exists x5
  7. L43
    exists x6
08Separate the logical casesL44–44

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

  1. L44
    split
09Use earlier factsL45–50

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

  1. L45
    specialize lt_of_lt_of_le (x)
  2. L46
    specialize lt_of_lt_of_le (l)
  3. L47
    specialize lt_of_lt_of_le (m)
  4. L48
    apply lt_of_lt_of_le
  5. L49
    exact hentry_witness_witness_witness_witness_witness_witness_witness_left
  6. L50
    exact hlm
10Separate the logical casesL51–51

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

  1. L51
    split
11Use earlier factsL52–61

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

  1. L52
    specialize matrix_recursive_record_transport (b)
  2. L53
    specialize matrix_recursive_record_transport (c)
  3. L54
    specialize matrix_recursive_record_transport (u)
  4. L55
    specialize matrix_recursive_record_transport (v)
  5. L56
    specialize matrix_recursive_record_transport (l)
  6. L57
    specialize matrix_recursive_record_transport (x)
  7. L58
    specialize matrix_recursive_record_transport (q)
  8. L59
    specialize matrix_recursive_record_transport (x1)
  9. L60
    specialize matrix_recursive_record_transport (x2)
  10. L61
    specialize matrix_recursive_record_transport (x3)
12Use earlier factsL62–68

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

  1. L62
    specialize matrix_recursive_record_transport (x4)
  2. L63
    specialize matrix_recursive_record_transport (x5)
  3. L64
    specialize matrix_recursive_record_transport (x6)
  4. L65
    apply matrix_recursive_record_transport
  5. L66
    exact hprefix
  6. L67
    exact hentry_witness_witness_witness_witness_witness_witness_witness_left
  7. L68
    exact hentry_witness_witness_witness_witness_witness_witness_witness_right_left
13Separate the logical casesL69–69

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

  1. L69
    split
14Use earlier factsL70–70

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

  1. L70
    exact hentry_witness_witness_witness_witness_witness_witness_witness_right_right_left
15Separate the logical casesL71–71

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

  1. L71
    split
16Use earlier factsL72–73

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

  1. L72
    exact hentry_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  2. L73
    exact hentry_witness_witness_witness_witness_witness_witness_witness_right_right_right_right

Library-wide reading audit

Original exact command ledger · 73 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro u
  4. 0004intro v
  5. 0005intro l
  6. 0006intro m
  7. 0007intro pb
  8. 0008intro pc
  9. 0009intro nb
  10. 0010intro nc
  11. 0011intro q
  12. 0012intro eb
  13. 0013intro ec
  14. 0014intro fb
  15. 0015intro fc
  16. 0016intro k
  17. 0017intro hprefix
  18. 0018intro hlm
  19. 0019intro hchildren
  20. 0020intro j
  21. 0021intro hj
  22. 0022have hentry : exists i up us un ut a z. ((exists mdr_gap_at_i. mdr_gap_at_i + S (i) = (l)) /\ ((exists mdr_z_at_r. ((exists mdr_a_at_rc mdr_b_at_rc mdr_c_at_rc mdr_e_at_rc mdr_f_at_rc. ((mdr_a_at_rc = ((q) + (up)) * S ((q) + (up)) + ((up) + (up))) /\ ((mdr_b_at_rc = ((us) + (un)) * S ((us) + (un)) + ((un) + (un))) /\ ((mdr_c_at_rc = ((mdr_a_at_rc) + (mdr_b_at_rc)) * S ((mdr_a_at_rc) + (mdr_b_at_rc)) + ((mdr_b_at_rc) + (mdr_b_at_rc))) /\ ((mdr_e_at_rc = ((a) + (z)) * S ((a) + (z)) + ((z) + (z))) /\ ((mdr_f_at_rc = ((ut) + (mdr_e_at_rc)) * S ((ut) + (mdr_e_at_rc)) + ((mdr_e_at_rc) + (mdr_e_at_rc))) /\ ((mdr_z_at_r) = ((mdr_c_at_rc) + (mdr_f_at_rc)) * S ((mdr_c_at_rc) + (mdr_f_at_rc)) + ((mdr_f_at_rc) + (mdr_f_at_rc))))))))) /\ (((exists ff_h_mdr_at_rb. ff_h_mdr_at_rb + S (mdr_z_at_r) = S ((S (i)) * c)) /\ exists ff_q_mdr_at_rb. b = ff_q_mdr_at_rb * S ((S (i)) * c) + (mdr_z_at_r))))) /\ ((((forall ff_index_mdm_prefix_mdr_at_m_positive. (exists ff_gap_mdm_lt_mdr_at_m_positive_index_bound. ff_gap_mdm_lt_mdr_at_m_positive_index_bound + S (ff_index_mdm_prefix_mdr_at_m_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_at_m_positive ff_column_mdm_prefix_mdr_at_m_positive ff_value_mdm_prefix_mdr_at_m_positive. (ff_index_mdm_prefix_mdr_at_m_positive = (q) * ff_row_mdm_prefix_mdr_at_m_positive + ff_column_mdm_prefix_mdr_at_m_positive /\ ((exists ff_gap_mdm_lt_mdr_at_m_positive_column_bound. ff_gap_mdm_lt_mdr_at_m_positive_column_bound + S (ff_column_mdm_prefix_mdr_at_m_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_at_m_positive_cell ff_column_mdm_cell_mdr_at_m_positive_cell. (((((exists ff_gap_mdm_lt_mdr_at_m_positive_cell_row_before. ff_gap_mdm_lt_mdr_at_m_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_at_m_positive) = (0)) /\ ff_row_mdm_cell_mdr_at_m_positive_cell = ff_row_mdm_prefix_mdr_at_m_positive) \/ ((exists ff_gap_mdm_le_mdr_at_m_positive_cell_row_after. ff_gap_mdm_le_mdr_at_m_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_at_m_positive)) /\ ff_row_mdm_cell_mdr_at_m_positive_cell = S ff_row_mdm_prefix_mdr_at_m_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_at_m_positive_cell_column_before. ff_gap_mdm_lt_mdr_at_m_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_at_m_positive) = (j)) /\ ff_column_mdm_cell_mdr_at_m_positive_cell = ff_column_mdm_prefix_mdr_at_m_positive) \/ ((exists ff_gap_mdm_le_mdr_at_m_positive_cell_column_after. ff_gap_mdm_le_mdr_at_m_positive_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_at_m_positive)) /\ ff_column_mdm_cell_mdr_at_m_positive_cell = S ff_column_mdm_prefix_mdr_at_m_positive))) /\ (((exists ff_h_mdm_mdr_at_m_positive_cell_source. ff_h_mdm_mdr_at_m_positive_cell_source + S (ff_value_mdm_prefix_mdr_at_m_positive) = S ((S ((ff_row_mdm_cell_mdr_at_m_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_at_m_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_at_m_positive_cell_source. pb = ff_q_mdm_mdr_at_m_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_at_m_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_at_m_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_at_m_positive)))))) /\ (((exists ff_h_mdm_mdr_at_m_positive_target. ff_h_mdm_mdr_at_m_positive_target + S (ff_value_mdm_prefix_mdr_at_m_positive) = S ((S (ff_index_mdm_prefix_mdr_at_m_positive)) * us)) /\ exists ff_q_mdm_mdr_at_m_positive_target. up = ff_q_mdm_mdr_at_m_positive_target * S ((S (ff_index_mdm_prefix_mdr_at_m_positive)) * us) + (ff_value_mdm_prefix_mdr_at_m_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_at_m_negative. (exists ff_gap_mdm_lt_mdr_at_m_negative_index_bound. ff_gap_mdm_lt_mdr_at_m_negative_index_bound + S (ff_index_mdm_prefix_mdr_at_m_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_at_m_negative ff_column_mdm_prefix_mdr_at_m_negative ff_value_mdm_prefix_mdr_at_m_negative. (ff_index_mdm_prefix_mdr_at_m_negative = (q) * ff_row_mdm_prefix_mdr_at_m_negative + ff_column_mdm_prefix_mdr_at_m_negative /\ ((exists ff_gap_mdm_lt_mdr_at_m_negative_column_bound. ff_gap_mdm_lt_mdr_at_m_negative_column_bound + S (ff_column_mdm_prefix_mdr_at_m_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_at_m_negative_cell ff_column_mdm_cell_mdr_at_m_negative_cell. (((((exists ff_gap_mdm_lt_mdr_at_m_negative_cell_row_before. ff_gap_mdm_lt_mdr_at_m_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_at_m_negative) = (0)) /\ ff_row_mdm_cell_mdr_at_m_negative_cell = ff_row_mdm_prefix_mdr_at_m_negative) \/ ((exists ff_gap_mdm_le_mdr_at_m_negative_cell_row_after. ff_gap_mdm_le_mdr_at_m_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_at_m_negative)) /\ ff_row_mdm_cell_mdr_at_m_negative_cell = S ff_row_mdm_prefix_mdr_at_m_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_at_m_negative_cell_column_before. ff_gap_mdm_lt_mdr_at_m_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_at_m_negative) = (j)) /\ ff_column_mdm_cell_mdr_at_m_negative_cell = ff_column_mdm_prefix_mdr_at_m_negative) \/ ((exists ff_gap_mdm_le_mdr_at_m_negative_cell_column_after. ff_gap_mdm_le_mdr_at_m_negative_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_at_m_negative)) /\ ff_column_mdm_cell_mdr_at_m_negative_cell = S ff_column_mdm_prefix_mdr_at_m_negative))) /\ (((exists ff_h_mdm_mdr_at_m_negative_cell_source. ff_h_mdm_mdr_at_m_negative_cell_source + S (ff_value_mdm_prefix_mdr_at_m_negative) = S ((S ((ff_row_mdm_cell_mdr_at_m_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_at_m_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_at_m_negative_cell_source. nb = ff_q_mdm_mdr_at_m_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_at_m_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_at_m_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_at_m_negative)))))) /\ (((exists ff_h_mdm_mdr_at_m_negative_target. ff_h_mdm_mdr_at_m_negative_target + S (ff_value_mdm_prefix_mdr_at_m_negative) = S ((S (ff_index_mdm_prefix_mdr_at_m_negative)) * ut)) /\ exists ff_q_mdm_mdr_at_m_negative_target. un = ff_q_mdm_mdr_at_m_negative_target * S ((S (ff_index_mdm_prefix_mdr_at_m_negative)) * ut) + (ff_value_mdm_prefix_mdr_at_m_negative))))))))) /\ ((((exists ff_h_mdr_at_p. ff_h_mdr_at_p + S (a) = S ((S (j)) * ec)) /\ exists ff_q_mdr_at_p. eb = ff_q_mdr_at_p * S ((S (j)) * ec) + (a))) /\ (((exists ff_h_mdr_at_n. ff_h_mdr_at_n + S (z) = S ((S (j)) * fc)) /\ exists ff_q_mdr_at_n. fb = ff_q_mdr_at_n * S ((S (j)) * fc) + (z)))))))
  23. 0023specialize hchildren (j)
  24. 0024apply hchildren
  25. 0025exact hj
  26. 0026cases hentry
  27. 0027cases hentry_witness
  28. 0028cases hentry_witness_witness
  29. 0029cases hentry_witness_witness_witness
  30. 0030cases hentry_witness_witness_witness_witness
  31. 0031cases hentry_witness_witness_witness_witness_witness
  32. 0032cases hentry_witness_witness_witness_witness_witness_witness
  33. 0033cases hentry_witness_witness_witness_witness_witness_witness_witness
  34. 0034cases hentry_witness_witness_witness_witness_witness_witness_witness_right
  35. 0035cases hentry_witness_witness_witness_witness_witness_witness_witness_right_right
  36. 0036cases hentry_witness_witness_witness_witness_witness_witness_witness_right_right_right
  37. 0037exists x
  38. 0038exists x1
  39. 0039exists x2
  40. 0040exists x3
  41. 0041exists x4
  42. 0042exists x5
  43. 0043exists x6
  44. 0044split
  45. 0045specialize lt_of_lt_of_le (x)
  46. 0046specialize lt_of_lt_of_le (l)
  47. 0047specialize lt_of_lt_of_le (m)
  48. 0048apply lt_of_lt_of_le
  49. 0049exact hentry_witness_witness_witness_witness_witness_witness_witness_left
  50. 0050exact hlm
  51. 0051split
  52. 0052specialize matrix_recursive_record_transport (b)
  53. 0053specialize matrix_recursive_record_transport (c)
  54. 0054specialize matrix_recursive_record_transport (u)
  55. 0055specialize matrix_recursive_record_transport (v)
  56. 0056specialize matrix_recursive_record_transport (l)
  57. 0057specialize matrix_recursive_record_transport (x)
  58. 0058specialize matrix_recursive_record_transport (q)
  59. 0059specialize matrix_recursive_record_transport (x1)
  60. 0060specialize matrix_recursive_record_transport (x2)
  61. 0061specialize matrix_recursive_record_transport (x3)
  62. 0062specialize matrix_recursive_record_transport (x4)
  63. 0063specialize matrix_recursive_record_transport (x5)
  64. 0064specialize matrix_recursive_record_transport (x6)
  65. 0065apply matrix_recursive_record_transport
  66. 0066exact hprefix
  67. 0067exact hentry_witness_witness_witness_witness_witness_witness_witness_left
  68. 0068exact hentry_witness_witness_witness_witness_witness_witness_witness_right_left
  69. 0069split
  70. 0070exact hentry_witness_witness_witness_witness_witness_witness_witness_right_right_left
  71. 0071split
  72. 0072exact hentry_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  73. 0073exact hentry_witness_witness_witness_witness_witness_witness_witness_right_right_right_right