DL003B

matrix_rank_bounded_prefix_decidable

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

Actual finite prefix value bounds are decidable by HA induction and comparison of each decoded entry, without an unbounded-existential decision axiom.

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_bounded_yes. (exists fom_gap_mrf_bounded_yes_index_bound. fom_gap_mrf_bounded_yes_index_bound + S (fom_index_mrf_bounded_yes) = l) -> exists fom_value_mrf_bounded_yes. ((((exists fom_beta_height_mrf_bounded_yes_entry. fom_beta_height_mrf_bounded_yes_entry + S (fom_value_mrf_bounded_yes) = S ((S (fom_index_mrf_bounded_yes)) * c)) /\ exists fom_beta_quotient_mrf_bounded_yes_entry. b = fom_beta_quotient_mrf_bounded_yes_entry * S ((S (fom_index_mrf_bounded_yes)) * c) + (fom_value_mrf_bounded_yes))) /\ (exists fom_gap_mrf_bounded_yes_value_bound. fom_gap_mrf_bounded_yes_value_bound + S (fom_value_mrf_bounded_yes) = B))) \/ ~(forall fom_index_mrf_bounded_no. (exists fom_gap_mrf_bounded_no_index_bound. fom_gap_mrf_bounded_no_index_bound + S (fom_index_mrf_bounded_no) = l) -> exists fom_value_mrf_bounded_no. ((((exists fom_beta_height_mrf_bounded_no_entry. fom_beta_height_mrf_bounded_no_entry + S (fom_value_mrf_bounded_no) = S ((S (fom_index_mrf_bounded_no)) * c)) /\ exists fom_beta_quotient_mrf_bounded_no_entry. b = fom_beta_quotient_mrf_bounded_no_entry * S ((S (fom_index_mrf_bounded_no)) * c) + (fom_value_mrf_bounded_no))) /\ (exists fom_gap_mrf_bounded_no_value_bound. fom_gap_mrf_bounded_no_value_bound + S (fom_value_mrf_bounded_no) = B)))

Constructive proof overview

Generated structural guide

Actual finite prefix value bounds are decidable by HA induction and comparison of each decoded entry, without an unbounded-existential decision axiom.

The unchanged tactic script uses 8 declared prerequisites and contains 63 exact native proof lines.

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

Proof neighborhood

Direct dependencies

DL0038 matrix_rank_bounded_prefix_empty DL0039 matrix_rank_bounded_prefix_drop_last DL003A matrix_rank_bounded_prefix_extend beta_at_exists Stable theorem; checked-use authorized le_or_lt Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized DL002D matrix_rank_bounded_prefix_value lt_not_le Stable theorem; checked-use authorized

Direct dependents

DL003D matrix_rank_selector_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

63 script commands · 19 reading checkpoints · 4 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 (4)
matrix rank bounded prefix emptymatrix rank bounded prefix drop lastmatrix rank bounded prefix extendmatrix rank bounded prefix value

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

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on lL3–4

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction l
  2. L4
    intro B
03Separate the logical casesL5–5

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

  1. L5
    left
04Use earlier factsL6–9

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

  1. L6
    specialize matrix_rank_bounded_prefix_empty (b)
  2. L7
    specialize matrix_rank_bounded_prefix_empty (c)
  3. L8
    specialize matrix_rank_bounded_prefix_empty (B)
  4. L9
    apply matrix_rank_bounded_prefix_empty
05Fix variables and assumptionsL10–10

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

  1. L10
    intro B
06Establish hpreviousL11–13

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

  1. L11
    have hprevious : (∀ 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. L12
    specialize IH (B)
  3. L13
    apply IH
07Separate the logical casesL14–14

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

  1. L14
    cases hprevious
08Establish hlastL15–19

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

  1. L15
    have hlast : exists a. ((exists ff_h_mdr_decision_last. ff_h_mdr_decision_last + S (a) = S ((S (l)) * c)) /\ exists ff_q_mdr_decision_last. b = ff_q_mdr_decision_last * S ((S (l)) * c) + (a))
  2. L16
    specialize beta_at_exists (b)
  3. L17
    specialize beta_at_exists (c)
  4. L18
    specialize beta_at_exists (l)
  5. L19
    apply beta_at_exists
09Separate the logical casesL20–20

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

  1. L20
    cases hlast
10Establish horderL21–24

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

  1. L21
    have horder : (exists mdr_gap_last_too_large. mdr_gap_last_too_large + (B) = (x)) \/ (exists mdr_gap_last_small. mdr_gap_last_small + S (x) = (B))
  2. L22
    specialize le_or_lt (B)
  3. L23
    specialize le_or_lt (x)
  4. L24
    apply le_or_lt
11Separate the logical casesL25–26

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

  1. L25
    cases horder
  2. L26
    right
12Fix variables and assumptionsL27–27

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

  1. L27
    intro hfull
13Establish hcontradictionL28–37

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

  1. L28
    have hcontradiction : exists mdr_gap_contradiction_bound. mdr_gap_contradiction_bound + S (x) = (B)
  2. L29
    specialize matrix_rank_bounded_prefix_value (b)
  3. L30
    specialize matrix_rank_bounded_prefix_value (c)
  4. L31
    specialize matrix_rank_bounded_prefix_value (S l)
  5. L32
    specialize matrix_rank_bounded_prefix_value (B)
  6. L33
    specialize matrix_rank_bounded_prefix_value (l)
  7. L34
    specialize matrix_rank_bounded_prefix_value (x)
  8. L35
    apply matrix_rank_bounded_prefix_value
  9. L36
    exact hfull
  10. L37
    specialize le_refl (S l)
14Use earlier factsL38–44

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

  1. L38
    apply le_refl
  2. L39
    exact hlast_witness
  3. L40
    specialize lt_not_le (x)
  4. L41
    specialize lt_not_le (B)
  5. L42
    apply lt_not_le
  6. L43
    exact hcontradiction
  7. L44
    exact horder_left
15Separate the logical casesL45–45

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

  1. L45
    left
16Use earlier factsL46–54

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

  1. L46
    specialize matrix_rank_bounded_prefix_extend (b)
  2. L47
    specialize matrix_rank_bounded_prefix_extend (c)
  3. L48
    specialize matrix_rank_bounded_prefix_extend (l)
  4. L49
    specialize matrix_rank_bounded_prefix_extend (B)
  5. L50
    specialize matrix_rank_bounded_prefix_extend (x)
  6. L51
    apply matrix_rank_bounded_prefix_extend
  7. L52
    exact hprevious_left
  8. L53
    exact hlast_witness
  9. L54
    exact horder_right
17Separate the logical casesL55–55

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

  1. L55
    right
18Fix variables and assumptionsL56–56

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

  1. L56
    intro hfull
19Use earlier factsL57–63

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

  1. L57
    apply hprevious_right
  2. L58
    specialize matrix_rank_bounded_prefix_drop_last (b)
  3. L59
    specialize matrix_rank_bounded_prefix_drop_last (c)
  4. L60
    specialize matrix_rank_bounded_prefix_drop_last (l)
  5. L61
    specialize matrix_rank_bounded_prefix_drop_last (B)
  6. L62
    apply matrix_rank_bounded_prefix_drop_last
  7. L63
    exact hfull

Library-wide reading audit

Original exact command ledger · 63 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro B
  5. 0005left
  6. 0006specialize matrix_rank_bounded_prefix_empty (b)
  7. 0007specialize matrix_rank_bounded_prefix_empty (c)
  8. 0008specialize matrix_rank_bounded_prefix_empty (B)
  9. 0009apply matrix_rank_bounded_prefix_empty
  10. 0010intro B
  11. 0011have hprevious : (forall fom_index_mrf_decision_previous. (exists fom_gap_mrf_decision_previous_index_bound. fom_gap_mrf_decision_previous_index_bound + S (fom_index_mrf_decision_previous) = l) -> exists fom_value_mrf_decision_previous. ((((exists fom_beta_height_mrf_decision_previous_entry. fom_beta_height_mrf_decision_previous_entry + S (fom_value_mrf_decision_previous) = S ((S (fom_index_mrf_decision_previous)) * c)) /\ exists fom_beta_quotient_mrf_decision_previous_entry. b = fom_beta_quotient_mrf_decision_previous_entry * S ((S (fom_index_mrf_decision_previous)) * c) + (fom_value_mrf_decision_previous))) /\ (exists fom_gap_mrf_decision_previous_value_bound. fom_gap_mrf_decision_previous_value_bound + S (fom_value_mrf_decision_previous) = B))) \/ ~(forall fom_index_mrf_decision_absent. (exists fom_gap_mrf_decision_absent_index_bound. fom_gap_mrf_decision_absent_index_bound + S (fom_index_mrf_decision_absent) = l) -> exists fom_value_mrf_decision_absent. ((((exists fom_beta_height_mrf_decision_absent_entry. fom_beta_height_mrf_decision_absent_entry + S (fom_value_mrf_decision_absent) = S ((S (fom_index_mrf_decision_absent)) * c)) /\ exists fom_beta_quotient_mrf_decision_absent_entry. b = fom_beta_quotient_mrf_decision_absent_entry * S ((S (fom_index_mrf_decision_absent)) * c) + (fom_value_mrf_decision_absent))) /\ (exists fom_gap_mrf_decision_absent_value_bound. fom_gap_mrf_decision_absent_value_bound + S (fom_value_mrf_decision_absent) = B)))
  12. 0012specialize IH (B)
  13. 0013apply IH
  14. 0014cases hprevious
  15. 0015have hlast : exists a. ((exists ff_h_mdr_decision_last. ff_h_mdr_decision_last + S (a) = S ((S (l)) * c)) /\ exists ff_q_mdr_decision_last. b = ff_q_mdr_decision_last * S ((S (l)) * c) + (a))
  16. 0016specialize beta_at_exists (b)
  17. 0017specialize beta_at_exists (c)
  18. 0018specialize beta_at_exists (l)
  19. 0019apply beta_at_exists
  20. 0020cases hlast
  21. 0021have horder : (exists mdr_gap_last_too_large. mdr_gap_last_too_large + (B) = (x)) \/ (exists mdr_gap_last_small. mdr_gap_last_small + S (x) = (B))
  22. 0022specialize le_or_lt (B)
  23. 0023specialize le_or_lt (x)
  24. 0024apply le_or_lt
  25. 0025cases horder
  26. 0026right
  27. 0027intro hfull
  28. 0028have hcontradiction : exists mdr_gap_contradiction_bound. mdr_gap_contradiction_bound + S (x) = (B)
  29. 0029specialize matrix_rank_bounded_prefix_value (b)
  30. 0030specialize matrix_rank_bounded_prefix_value (c)
  31. 0031specialize matrix_rank_bounded_prefix_value (S l)
  32. 0032specialize matrix_rank_bounded_prefix_value (B)
  33. 0033specialize matrix_rank_bounded_prefix_value (l)
  34. 0034specialize matrix_rank_bounded_prefix_value (x)
  35. 0035apply matrix_rank_bounded_prefix_value
  36. 0036exact hfull
  37. 0037specialize le_refl (S l)
  38. 0038apply le_refl
  39. 0039exact hlast_witness
  40. 0040specialize lt_not_le (x)
  41. 0041specialize lt_not_le (B)
  42. 0042apply lt_not_le
  43. 0043exact hcontradiction
  44. 0044exact horder_left
  45. 0045left
  46. 0046specialize matrix_rank_bounded_prefix_extend (b)
  47. 0047specialize matrix_rank_bounded_prefix_extend (c)
  48. 0048specialize matrix_rank_bounded_prefix_extend (l)
  49. 0049specialize matrix_rank_bounded_prefix_extend (B)
  50. 0050specialize matrix_rank_bounded_prefix_extend (x)
  51. 0051apply matrix_rank_bounded_prefix_extend
  52. 0052exact hprevious_left
  53. 0053exact hlast_witness
  54. 0054exact horder_right
  55. 0055right
  56. 0056intro hfull
  57. 0057apply hprevious_right
  58. 0058specialize matrix_rank_bounded_prefix_drop_last (b)
  59. 0059specialize matrix_rank_bounded_prefix_drop_last (c)
  60. 0060specialize matrix_rank_bounded_prefix_drop_last (l)
  61. 0061specialize matrix_rank_bounded_prefix_drop_last (B)
  62. 0062apply matrix_rank_bounded_prefix_drop_last
  63. 0063exact hfull