DL003B

matrix_rank_bounded_prefix_decidable

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

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

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.

This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ l. ∀ B. (∀ 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))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Le(a,b) · 1Lt(a,b) · 10BetaAt(b,c,i,x) · 5

Actual proof prerequisites

matrix_rank_bounded_prefix_emptymatrix_rank_bounded_prefix_drop_lastmatrix_rank_bounded_prefix_extendbeta_at_exists · checked external prerequisitele_or_lt · checked external prerequisitele_refl · checked external prerequisitematrix_rank_bounded_prefix_valuelt_not_le · checked external prerequisite
Original expanded first-order 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)))

Complete tactic proof in conservative notation

All 63 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (4)
matrix rank bounded prefix emptymatrix rank bounded prefix valuematrix rank bounded prefix extendmatrix rank bounded prefix drop last
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: Lt(x,l)BetaAt(b,c,x,y)Lt(y,B)Original native command in the exact edition
  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 : ∃ a. BetaAt(b,c,l,a)Definitions: BetaAt(b,c,l,a)Original native command in the exact edition
  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 : Le(B,x) ∨ Lt(x,B)Definitions: Le(B,x)Lt(x,B)Original native command in the exact edition
  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 : Lt(x,B)Definitions: Lt(x,B)Original native command in the exact edition
  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 defined 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 : (∀ 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))
  12. 0012specialize IH (B)
  13. 0013apply IH
  14. 0014cases hprevious
  15. 0015have hlast : ∃ a. BetaAt(b,c,l,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 : Le(B,x) ∨ Lt(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 : Lt(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