DL0031

matrix_rank_bounded_recode_in_fixed_box

Reducing a genuine CRT recoding modulo a fixed common multiple gives a strictly bounded code with every finite source value preserved.

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

∀ k. ∀ B. ∀ c. ∀ T. ∀ b. ∀ e. Le(B,c) → (∀ x. (∃ y. S x + S y = S k) → ∃ y. c = S x · y) → ¬T = 0 → (∀ x. Lt(x,k) → ∃ y. T = S (S x · c) · y) → (∀ x. Lt(x,k) → ∃ y. BetaAt(b,e,x,y) ∧ Lt(y,B)) → ∃ x. Lt(x,T) ∧ (∀ y. ∀ z. Lt(y,k) → BetaAt(b,e,y,z) → BetaAt(x,c,y,z))

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

Definition DAG

Le(a,b) · 2Lt(a,b) · 8BetaAt(b,c,i,x) · 4

Actual proof prerequisites

matrix_rank_recode_congruences_existsdivision_remainder_exists · checked external prerequisitemul_comm · checked external prerequisiteremainder_decomposition_to_mod_eq · checked external prerequisitematrix_rank_bounded_prefix_valuebase_le_beta_modulus · checked external prerequisitele_trans · checked external prerequisitelt_of_lt_of_le · checked external prerequisitemod_eq_of_mod_eq_multiple · checked external prerequisitemod_eq_symm · checked external prerequisitemod_eq_trans · checked external prerequisitebeta_at_of_mod_eq_bound · checked external prerequisite
Original expanded first-order statement 
forall k B c T b e. (exists mdr_gap_fixed_scale. mdr_gap_fixed_scale + (B) = (c)) -> (forall mdr_t_fixed_common. (exists mdr_h_fixed_common. S mdr_t_fixed_common + S mdr_h_fixed_common = S (k)) -> exists mdr_q_fixed_common. c = S mdr_t_fixed_common * mdr_q_fixed_common) -> ~(T = 0) -> (forall mdr_i_fixed_divides. (exists mdr_gap_fixed_dividesi. mdr_gap_fixed_dividesi + S (mdr_i_fixed_divides) = (k)) -> (exists mdr_q_fixed_dividesd. T = (S ((S (mdr_i_fixed_divides)) * (c))) * mdr_q_fixed_dividesd)) -> (forall fom_index_mrf_fixed_source. (exists fom_gap_mrf_fixed_source_index_bound. fom_gap_mrf_fixed_source_index_bound + S (fom_index_mrf_fixed_source) = k) -> exists fom_value_mrf_fixed_source. ((((exists fom_beta_height_mrf_fixed_source_entry. fom_beta_height_mrf_fixed_source_entry + S (fom_value_mrf_fixed_source) = S ((S (fom_index_mrf_fixed_source)) * e)) /\ exists fom_beta_quotient_mrf_fixed_source_entry. b = fom_beta_quotient_mrf_fixed_source_entry * S ((S (fom_index_mrf_fixed_source)) * e) + (fom_value_mrf_fixed_source))) /\ (exists fom_gap_mrf_fixed_source_value_bound. fom_gap_mrf_fixed_source_value_bound + S (fom_value_mrf_fixed_source) = B))) -> exists z. (((exists mdr_gap_fixed_result_bound. mdr_gap_fixed_result_bound + S (z) = (T)) /\ (forall mdr_i_fixed_result_prefix mdr_a_fixed_result_prefix. (exists mdr_gap_fixed_result_prefixb. mdr_gap_fixed_result_prefixb + S (mdr_i_fixed_result_prefix) = (k)) -> (((exists ff_h_mdr_fixed_result_prefixo. ff_h_mdr_fixed_result_prefixo + S (mdr_a_fixed_result_prefix) = S ((S (mdr_i_fixed_result_prefix)) * e)) /\ exists ff_q_mdr_fixed_result_prefixo. b = ff_q_mdr_fixed_result_prefixo * S ((S (mdr_i_fixed_result_prefix)) * e) + (mdr_a_fixed_result_prefix))) -> (((exists ff_h_mdr_fixed_result_prefixn. ff_h_mdr_fixed_result_prefixn + S (mdr_a_fixed_result_prefix) = S ((S (mdr_i_fixed_result_prefix)) * c)) /\ exists ff_q_mdr_fixed_result_prefixn. z = ff_q_mdr_fixed_result_prefixn * S ((S (mdr_i_fixed_result_prefix)) * c) + (mdr_a_fixed_result_prefix))))))

Complete tactic proof in conservative notation

All 98 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

98 script commands · 19 reading checkpoints · 6 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 (2)
matrix rank recode congruences existsmatrix rank bounded prefix value
01Fix variables and assumptionsL1–10

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

  1. L1
    intro k
  2. L2
    intro B
  3. L3
    intro c
  4. L4
    intro T
  5. L5
    intro b
  6. L6
    intro e
  7. L7
    intro hscale
  8. L8
    intro hcommon
  9. L9
    intro hT
  10. L10
    intro hmoduli
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hbounded
03Establish hcodesL12–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix rank recode congruences exists.

  1. L12
    have hcodes : ∃ z. ∀ x. ∀ y. Lt(x,k) → BetaAt(b,e,x,y) → ∃ n. ∃ m. z + S (S x · c) · n = y + S (S x · c) · mDefinitions: Lt(x,k)BetaAt(b,e,x,y)Original native command in the exact edition
  2. L13
    specialize matrix_rank_recode_congruences_exists (k)
  3. L14
    specialize matrix_rank_recode_congruences_exists (c)
  4. L15
    specialize matrix_rank_recode_congruences_exists (b)
  5. L16
    specialize matrix_rank_recode_congruences_exists (e)
  6. L17
    apply matrix_rank_recode_congruences_exists
  7. L18
    exact hcommon
04Separate the logical casesL19–19

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

  1. L19
    cases hcodes
05Establish hdivisionL20–24

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

  1. L20
    have hdivision : ∃ q. ∃ r. x = T · q + r ∧ Lt(r,T)Definitions: Lt(r,T)Original native command in the exact edition
  2. L21
    specialize division_remainder_exists (T)
  3. L22
    specialize division_remainder_exists (x)
  4. L23
    apply division_remainder_exists
  5. L24
    exact hT
06Separate the logical casesL25–27

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

  1. L25
    cases hdivision
  2. L26
    cases hdivision_witness
  3. L27
    cases hdivision_witness_witness
07Establish hcommuteL28–30

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

  1. L28
    have hcommute : T * x1 = x1 * T
  2. L29
    apply mul_comm
  3. L30
    rewrite hcommute at hdivision_witness_witness_left
08Establish hremainderL31–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply remainder decomposition to mod eq.

  1. L31
    have hremainder : exists mdr_u_fixed_remainder mdr_v_fixed_remainder. (x) + (T) * mdr_u_fixed_remainder = (x2) + (T) * mdr_v_fixed_remainder
  2. L32
    specialize remainder_decomposition_to_mod_eq (T)
  3. L33
    specialize remainder_decomposition_to_mod_eq (x)
  4. L34
    specialize remainder_decomposition_to_mod_eq (x1)
  5. L35
    specialize remainder_decomposition_to_mod_eq (x2)
  6. L36
    apply remainder_decomposition_to_mod_eq
  7. L37
    exact hdivision_witness_witness_left
09Construct an explicit witnessL38–38

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

  1. L38
    exists x2
10Separate the logical casesL39–39

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

  1. L39
    split
11Use earlier factsL40–40

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

  1. L40
    exact hdivision_witness_witness_right
12Fix variables and assumptionsL41–44

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

  1. L41
    intro i
  2. L42
    intro a
  3. L43
    intro hi
  4. L44
    intro ha
13Establish hvalueL45–54

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

  1. L45
    have hvalue : Lt(a,B)Definitions: Lt(a,B)Original native command in the exact edition
  2. L46
    specialize matrix_rank_bounded_prefix_value (b)
  3. L47
    specialize matrix_rank_bounded_prefix_value (e)
  4. L48
    specialize matrix_rank_bounded_prefix_value (k)
  5. L49
    specialize matrix_rank_bounded_prefix_value (B)
  6. L50
    specialize matrix_rank_bounded_prefix_value (i)
  7. L51
    specialize matrix_rank_bounded_prefix_value (a)
  8. L52
    apply matrix_rank_bounded_prefix_value
  9. L53
    exact hbounded
  10. L54
    exact hi
14Use earlier factsL55–55

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

  1. L55
    exact ha
15Establish hmodboundL56–65

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

  1. L56
    have hmodbound : Le(B,S (S i · c))Definitions: Le(B,S (S i · c))Original native command in the exact edition
  2. L57
    specialize le_trans (B)
  3. L58
    specialize le_trans (c)
  4. L59
    specialize le_trans (S ((S i) * c))
  5. L60
    apply le_trans
  6. L61
    exact hscale
  7. L62
    specialize base_le_beta_modulus (c)
  8. L63
    specialize base_le_beta_modulus (i)
  9. L64
    apply base_le_beta_modulus
  10. L65
    specialize beta_at_of_mod_eq_bound (x2)
16Use earlier factsL66–75

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

  1. L66
    specialize beta_at_of_mod_eq_bound (c)
  2. L67
    specialize beta_at_of_mod_eq_bound (i)
  3. L68
    specialize beta_at_of_mod_eq_bound (a)
  4. L69
    apply beta_at_of_mod_eq_bound
  5. L70
    specialize lt_of_lt_of_le (a)
  6. L71
    specialize lt_of_lt_of_le (B)
  7. L72
    specialize lt_of_lt_of_le (S ((S i) * c))
  8. L73
    apply lt_of_lt_of_le
  9. L74
    exact hvalue
  10. L75
    exact hmodbound
17Use earlier factsL76–85

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

  1. L76
    specialize mod_eq_trans (S ((S i) * c))
  2. L77
    specialize mod_eq_trans (x2)
  3. L78
    specialize mod_eq_trans (x)
  4. L79
    specialize mod_eq_trans (a)
  5. L80
    apply mod_eq_trans
  6. L81
    specialize mod_eq_symm (S ((S i) * c))
  7. L82
    specialize mod_eq_symm (x)
  8. L83
    specialize mod_eq_symm (x2)
  9. L84
    apply mod_eq_symm
  10. L85
    specialize mod_eq_of_mod_eq_multiple (S ((S i) * c))
18Use earlier factsL86–95

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

  1. L86
    specialize mod_eq_of_mod_eq_multiple (T)
  2. L87
    specialize mod_eq_of_mod_eq_multiple (x)
  3. L88
    specialize mod_eq_of_mod_eq_multiple (x2)
  4. L89
    apply mod_eq_of_mod_eq_multiple
  5. L90
    specialize hmoduli (i)
  6. L91
    apply hmoduli
  7. L92
    exact hi
  8. L93
    exact hremainder
  9. L94
    specialize hcodes_witness (i)
  10. L95
    specialize hcodes_witness (a)
19Use earlier factsL96–98

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

  1. L96
    apply hcodes_witness
  2. L97
    exact hi
  3. L98
    exact ha

Library-wide reading audit

Original defined command ledger · 98 lines
  1. 0001intro k
  2. 0002intro B
  3. 0003intro c
  4. 0004intro T
  5. 0005intro b
  6. 0006intro e
  7. 0007intro hscale
  8. 0008intro hcommon
  9. 0009intro hT
  10. 0010intro hmoduli
  11. 0011intro hbounded
  12. 0012have hcodes : ∃ z. ∀ x. ∀ y. Lt(x,k) → BetaAt(b,e,x,y) → ∃ n. ∃ m. z + S (S x · c) · n = y + S (S x · c) · m
  13. 0013specialize matrix_rank_recode_congruences_exists (k)
  14. 0014specialize matrix_rank_recode_congruences_exists (c)
  15. 0015specialize matrix_rank_recode_congruences_exists (b)
  16. 0016specialize matrix_rank_recode_congruences_exists (e)
  17. 0017apply matrix_rank_recode_congruences_exists
  18. 0018exact hcommon
  19. 0019cases hcodes
  20. 0020have hdivision : ∃ q. ∃ r. x = T · q + r ∧ Lt(r,T)
  21. 0021specialize division_remainder_exists (T)
  22. 0022specialize division_remainder_exists (x)
  23. 0023apply division_remainder_exists
  24. 0024exact hT
  25. 0025cases hdivision
  26. 0026cases hdivision_witness
  27. 0027cases hdivision_witness_witness
  28. 0028have hcommute : T * x1 = x1 * T
  29. 0029apply mul_comm
  30. 0030rewrite hcommute at hdivision_witness_witness_left
  31. 0031have hremainder : exists mdr_u_fixed_remainder mdr_v_fixed_remainder. (x) + (T) * mdr_u_fixed_remainder = (x2) + (T) * mdr_v_fixed_remainder
  32. 0032specialize remainder_decomposition_to_mod_eq (T)
  33. 0033specialize remainder_decomposition_to_mod_eq (x)
  34. 0034specialize remainder_decomposition_to_mod_eq (x1)
  35. 0035specialize remainder_decomposition_to_mod_eq (x2)
  36. 0036apply remainder_decomposition_to_mod_eq
  37. 0037exact hdivision_witness_witness_left
  38. 0038exists x2
  39. 0039split
  40. 0040exact hdivision_witness_witness_right
  41. 0041intro i
  42. 0042intro a
  43. 0043intro hi
  44. 0044intro ha
  45. 0045have hvalue : Lt(a,B)
  46. 0046specialize matrix_rank_bounded_prefix_value (b)
  47. 0047specialize matrix_rank_bounded_prefix_value (e)
  48. 0048specialize matrix_rank_bounded_prefix_value (k)
  49. 0049specialize matrix_rank_bounded_prefix_value (B)
  50. 0050specialize matrix_rank_bounded_prefix_value (i)
  51. 0051specialize matrix_rank_bounded_prefix_value (a)
  52. 0052apply matrix_rank_bounded_prefix_value
  53. 0053exact hbounded
  54. 0054exact hi
  55. 0055exact ha
  56. 0056have hmodbound : Le(B,S (S i · c))
  57. 0057specialize le_trans (B)
  58. 0058specialize le_trans (c)
  59. 0059specialize le_trans (S ((S i) * c))
  60. 0060apply le_trans
  61. 0061exact hscale
  62. 0062specialize base_le_beta_modulus (c)
  63. 0063specialize base_le_beta_modulus (i)
  64. 0064apply base_le_beta_modulus
  65. 0065specialize beta_at_of_mod_eq_bound (x2)
  66. 0066specialize beta_at_of_mod_eq_bound (c)
  67. 0067specialize beta_at_of_mod_eq_bound (i)
  68. 0068specialize beta_at_of_mod_eq_bound (a)
  69. 0069apply beta_at_of_mod_eq_bound
  70. 0070specialize lt_of_lt_of_le (a)
  71. 0071specialize lt_of_lt_of_le (B)
  72. 0072specialize lt_of_lt_of_le (S ((S i) * c))
  73. 0073apply lt_of_lt_of_le
  74. 0074exact hvalue
  75. 0075exact hmodbound
  76. 0076specialize mod_eq_trans (S ((S i) * c))
  77. 0077specialize mod_eq_trans (x2)
  78. 0078specialize mod_eq_trans (x)
  79. 0079specialize mod_eq_trans (a)
  80. 0080apply mod_eq_trans
  81. 0081specialize mod_eq_symm (S ((S i) * c))
  82. 0082specialize mod_eq_symm (x)
  83. 0083specialize mod_eq_symm (x2)
  84. 0084apply mod_eq_symm
  85. 0085specialize mod_eq_of_mod_eq_multiple (S ((S i) * c))
  86. 0086specialize mod_eq_of_mod_eq_multiple (T)
  87. 0087specialize mod_eq_of_mod_eq_multiple (x)
  88. 0088specialize mod_eq_of_mod_eq_multiple (x2)
  89. 0089apply mod_eq_of_mod_eq_multiple
  90. 0090specialize hmoduli (i)
  91. 0091apply hmoduli
  92. 0092exact hi
  93. 0093exact hremainder
  94. 0094specialize hcodes_witness (i)
  95. 0095specialize hcodes_witness (a)
  96. 0096apply hcodes_witness
  97. 0097exact hi
  98. 0098exact ha