DL003D

matrix_rank_selector_decidable

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

A genuine finite matrix-selector relation, including every index bound and pairwise distinctness condition, is decidable.

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 B. (((forall fom_index_mrf_selector_yesbound. (exists fom_gap_mrf_selector_yesbound_index_bound. fom_gap_mrf_selector_yesbound_index_bound + S (fom_index_mrf_selector_yesbound) = l) -> exists fom_value_mrf_selector_yesbound. ((((exists fom_beta_height_mrf_selector_yesbound_entry. fom_beta_height_mrf_selector_yesbound_entry + S (fom_value_mrf_selector_yesbound) = S ((S (fom_index_mrf_selector_yesbound)) * c)) /\ exists fom_beta_quotient_mrf_selector_yesbound_entry. b = fom_beta_quotient_mrf_selector_yesbound_entry * S ((S (fom_index_mrf_selector_yesbound)) * c) + (fom_value_mrf_selector_yesbound))) /\ (exists fom_gap_mrf_selector_yesbound_value_bound. fom_gap_mrf_selector_yesbound_value_bound + S (fom_value_mrf_selector_yesbound) = B))) /\ (forall mdr_i_selector_yesdistinct mdr_j_selector_yesdistinct mdr_a_selector_yesdistinct. (exists mdr_gap_selector_yesdistincti. mdr_gap_selector_yesdistincti + S (mdr_i_selector_yesdistinct) = (l)) -> (exists mdr_gap_selector_yesdistinctj. mdr_gap_selector_yesdistinctj + S (mdr_j_selector_yesdistinct) = (l)) -> (((exists ff_h_mdr_selector_yesdistinctfirst. ff_h_mdr_selector_yesdistinctfirst + S (mdr_a_selector_yesdistinct) = S ((S (mdr_i_selector_yesdistinct)) * c)) /\ exists ff_q_mdr_selector_yesdistinctfirst. b = ff_q_mdr_selector_yesdistinctfirst * S ((S (mdr_i_selector_yesdistinct)) * c) + (mdr_a_selector_yesdistinct))) -> (((exists ff_h_mdr_selector_yesdistinctsecond. ff_h_mdr_selector_yesdistinctsecond + S (mdr_a_selector_yesdistinct) = S ((S (mdr_j_selector_yesdistinct)) * c)) /\ exists ff_q_mdr_selector_yesdistinctsecond. b = ff_q_mdr_selector_yesdistinctsecond * S ((S (mdr_j_selector_yesdistinct)) * c) + (mdr_a_selector_yesdistinct))) -> mdr_i_selector_yesdistinct = mdr_j_selector_yesdistinct))) \/ ~(((forall fom_index_mrf_selector_nobound. (exists fom_gap_mrf_selector_nobound_index_bound. fom_gap_mrf_selector_nobound_index_bound + S (fom_index_mrf_selector_nobound) = l) -> exists fom_value_mrf_selector_nobound. ((((exists fom_beta_height_mrf_selector_nobound_entry. fom_beta_height_mrf_selector_nobound_entry + S (fom_value_mrf_selector_nobound) = S ((S (fom_index_mrf_selector_nobound)) * c)) /\ exists fom_beta_quotient_mrf_selector_nobound_entry. b = fom_beta_quotient_mrf_selector_nobound_entry * S ((S (fom_index_mrf_selector_nobound)) * c) + (fom_value_mrf_selector_nobound))) /\ (exists fom_gap_mrf_selector_nobound_value_bound. fom_gap_mrf_selector_nobound_value_bound + S (fom_value_mrf_selector_nobound) = B))) /\ (forall mdr_i_selector_nodistinct mdr_j_selector_nodistinct mdr_a_selector_nodistinct. (exists mdr_gap_selector_nodistincti. mdr_gap_selector_nodistincti + S (mdr_i_selector_nodistinct) = (l)) -> (exists mdr_gap_selector_nodistinctj. mdr_gap_selector_nodistinctj + S (mdr_j_selector_nodistinct) = (l)) -> (((exists ff_h_mdr_selector_nodistinctfirst. ff_h_mdr_selector_nodistinctfirst + S (mdr_a_selector_nodistinct) = S ((S (mdr_i_selector_nodistinct)) * c)) /\ exists ff_q_mdr_selector_nodistinctfirst. b = ff_q_mdr_selector_nodistinctfirst * S ((S (mdr_i_selector_nodistinct)) * c) + (mdr_a_selector_nodistinct))) -> (((exists ff_h_mdr_selector_nodistinctsecond. ff_h_mdr_selector_nodistinctsecond + S (mdr_a_selector_nodistinct) = S ((S (mdr_j_selector_nodistinct)) * c)) /\ exists ff_q_mdr_selector_nodistinctsecond. b = ff_q_mdr_selector_nodistinctsecond * S ((S (mdr_j_selector_nodistinct)) * c) + (mdr_a_selector_nodistinct))) -> mdr_i_selector_nodistinct = mdr_j_selector_nodistinct)))

Constructive proof overview

Generated structural guide

A genuine finite matrix-selector relation, including every index bound and pairwise distinctness condition, is decidable.

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

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

Proof neighborhood

Direct dependencies

DL003B matrix_rank_bounded_prefix_decidable DL0037 matrix_rank_injective_prefix_decidable

Direct dependents

DL0050 matrix_rank_nonzero_selected_minor_decidable

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

31 script commands · 14 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.

Named ingredients (2)
matrix rank bounded prefix decidablematrix rank injective prefix decidable

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

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 B
02Establish hboundL5–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix rank bounded prefix decidable.

  1. L5
    have hbound : (∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,B)) ∨ ¬(∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,B))Definitions: LtBetaAt
  2. L6
    specialize matrix_rank_bounded_prefix_decidable (b)
  3. L7
    specialize matrix_rank_bounded_prefix_decidable (c)
  4. L8
    specialize matrix_rank_bounded_prefix_decidable (l)
  5. L9
    specialize matrix_rank_bounded_prefix_decidable (B)
  6. L10
    apply matrix_rank_bounded_prefix_decidable
03Separate the logical casesL11–11

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

  1. L11
    cases hbound
04Establish hinjectiveL12–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix rank injective prefix decidable.

  1. L12
    have hinjective : (∀ x. ∀ y. ∀ z. Lt(x,l) → Lt(y,l) → BetaAt(b,c,x,z) → BetaAt(b,c,y,z) → x = y) ∨ ¬(∀ x. ∀ y. ∀ z. Lt(x,l) → Lt(y,l) → BetaAt(b,c,x,z) → BetaAt(b,c,y,z) → x = y)Definitions: LtBetaAt
  2. L13
    specialize matrix_rank_injective_prefix_decidable (b)
  3. L14
    specialize matrix_rank_injective_prefix_decidable (c)
  4. L15
    specialize matrix_rank_injective_prefix_decidable (l)
  5. L16
    apply matrix_rank_injective_prefix_decidable
05Separate the logical casesL17–19

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

  1. L17
    cases hinjective
  2. L18
    left
  3. L19
    split
06Use earlier factsL20–21

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

  1. L20
    exact hbound_left
  2. L21
    exact hinjective_left
07Separate the logical casesL22–22

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

  1. L22
    right
08Fix variables and assumptionsL23–23

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

  1. L23
    intro hselector
09Separate the logical casesL24–24

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

  1. L24
    cases hselector
10Use earlier factsL25–26

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

  1. L25
    apply hinjective_right
  2. L26
    exact hselector_right
11Separate the logical casesL27–27

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

  1. L27
    right
12Fix variables and assumptionsL28–28

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

  1. L28
    intro hselector
13Separate the logical casesL29–29

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

  1. L29
    cases hselector
14Use earlier factsL30–31

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

  1. L30
    apply hbound_right
  2. L31
    exact hselector_left

Library-wide reading audit

Original exact command ledger · 31 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro B
  5. 0005have hbound : (forall fom_index_mrf_select_bound_yes. (exists fom_gap_mrf_select_bound_yes_index_bound. fom_gap_mrf_select_bound_yes_index_bound + S (fom_index_mrf_select_bound_yes) = l) -> exists fom_value_mrf_select_bound_yes. ((((exists fom_beta_height_mrf_select_bound_yes_entry. fom_beta_height_mrf_select_bound_yes_entry + S (fom_value_mrf_select_bound_yes) = S ((S (fom_index_mrf_select_bound_yes)) * c)) /\ exists fom_beta_quotient_mrf_select_bound_yes_entry. b = fom_beta_quotient_mrf_select_bound_yes_entry * S ((S (fom_index_mrf_select_bound_yes)) * c) + (fom_value_mrf_select_bound_yes))) /\ (exists fom_gap_mrf_select_bound_yes_value_bound. fom_gap_mrf_select_bound_yes_value_bound + S (fom_value_mrf_select_bound_yes) = B))) \/ ~(forall fom_index_mrf_select_bound_no. (exists fom_gap_mrf_select_bound_no_index_bound. fom_gap_mrf_select_bound_no_index_bound + S (fom_index_mrf_select_bound_no) = l) -> exists fom_value_mrf_select_bound_no. ((((exists fom_beta_height_mrf_select_bound_no_entry. fom_beta_height_mrf_select_bound_no_entry + S (fom_value_mrf_select_bound_no) = S ((S (fom_index_mrf_select_bound_no)) * c)) /\ exists fom_beta_quotient_mrf_select_bound_no_entry. b = fom_beta_quotient_mrf_select_bound_no_entry * S ((S (fom_index_mrf_select_bound_no)) * c) + (fom_value_mrf_select_bound_no))) /\ (exists fom_gap_mrf_select_bound_no_value_bound. fom_gap_mrf_select_bound_no_value_bound + S (fom_value_mrf_select_bound_no) = B)))
  6. 0006specialize matrix_rank_bounded_prefix_decidable (b)
  7. 0007specialize matrix_rank_bounded_prefix_decidable (c)
  8. 0008specialize matrix_rank_bounded_prefix_decidable (l)
  9. 0009specialize matrix_rank_bounded_prefix_decidable (B)
  10. 0010apply matrix_rank_bounded_prefix_decidable
  11. 0011cases hbound
  12. 0012have hinjective : (forall mdr_i_select_inj_yes mdr_j_select_inj_yes mdr_a_select_inj_yes. (exists mdr_gap_select_inj_yesi. mdr_gap_select_inj_yesi + S (mdr_i_select_inj_yes) = (l)) -> (exists mdr_gap_select_inj_yesj. mdr_gap_select_inj_yesj + S (mdr_j_select_inj_yes) = (l)) -> (((exists ff_h_mdr_select_inj_yesfirst. ff_h_mdr_select_inj_yesfirst + S (mdr_a_select_inj_yes) = S ((S (mdr_i_select_inj_yes)) * c)) /\ exists ff_q_mdr_select_inj_yesfirst. b = ff_q_mdr_select_inj_yesfirst * S ((S (mdr_i_select_inj_yes)) * c) + (mdr_a_select_inj_yes))) -> (((exists ff_h_mdr_select_inj_yessecond. ff_h_mdr_select_inj_yessecond + S (mdr_a_select_inj_yes) = S ((S (mdr_j_select_inj_yes)) * c)) /\ exists ff_q_mdr_select_inj_yessecond. b = ff_q_mdr_select_inj_yessecond * S ((S (mdr_j_select_inj_yes)) * c) + (mdr_a_select_inj_yes))) -> mdr_i_select_inj_yes = mdr_j_select_inj_yes) \/ ~(forall mdr_i_select_inj_no mdr_j_select_inj_no mdr_a_select_inj_no. (exists mdr_gap_select_inj_noi. mdr_gap_select_inj_noi + S (mdr_i_select_inj_no) = (l)) -> (exists mdr_gap_select_inj_noj. mdr_gap_select_inj_noj + S (mdr_j_select_inj_no) = (l)) -> (((exists ff_h_mdr_select_inj_nofirst. ff_h_mdr_select_inj_nofirst + S (mdr_a_select_inj_no) = S ((S (mdr_i_select_inj_no)) * c)) /\ exists ff_q_mdr_select_inj_nofirst. b = ff_q_mdr_select_inj_nofirst * S ((S (mdr_i_select_inj_no)) * c) + (mdr_a_select_inj_no))) -> (((exists ff_h_mdr_select_inj_nosecond. ff_h_mdr_select_inj_nosecond + S (mdr_a_select_inj_no) = S ((S (mdr_j_select_inj_no)) * c)) /\ exists ff_q_mdr_select_inj_nosecond. b = ff_q_mdr_select_inj_nosecond * S ((S (mdr_j_select_inj_no)) * c) + (mdr_a_select_inj_no))) -> mdr_i_select_inj_no = mdr_j_select_inj_no)
  13. 0013specialize matrix_rank_injective_prefix_decidable (b)
  14. 0014specialize matrix_rank_injective_prefix_decidable (c)
  15. 0015specialize matrix_rank_injective_prefix_decidable (l)
  16. 0016apply matrix_rank_injective_prefix_decidable
  17. 0017cases hinjective
  18. 0018left
  19. 0019split
  20. 0020exact hbound_left
  21. 0021exact hinjective_left
  22. 0022right
  23. 0023intro hselector
  24. 0024cases hselector
  25. 0025apply hinjective_right
  26. 0026exact hselector_right
  27. 0027right
  28. 0028intro hselector
  29. 0029cases hselector
  30. 0030apply hbound_right
  31. 0031exact hselector_left