DL002F

matrix_rank_beta_moduli_common_multiple

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

One fixed positive common multiple is divisible by all beta moduli in a finite selector prefix.

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 k c T. (forall mdr_t_moduli_source. (exists mdr_h_moduli_source. S mdr_t_moduli_source + S mdr_h_moduli_source = S (S (k * c))) -> exists mdr_q_moduli_source. T = S mdr_t_moduli_source * mdr_q_moduli_source) -> (forall mdr_i_moduli_result. (exists mdr_gap_moduli_resulti. mdr_gap_moduli_resulti + S (mdr_i_moduli_result) = (k)) -> (exists mdr_q_moduli_resultd. T = (S ((S (mdr_i_moduli_result)) * (c))) * mdr_q_moduli_resultd))

Constructive proof overview

Generated structural guide

One fixed positive common multiple is divisible by all beta moduli in a finite selector prefix.

The unchanged tactic script uses 3 declared prerequisites and contains 19 exact native proof lines.

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

Proof neighborhood

Direct dependencies

DL002E matrix_rank_common_multiple_divides succ_le_succ Stable theorem; checked-use authorized mul_le_mul_right Stable theorem; checked-use authorized

Direct dependents

DL0032 matrix_rank_uniform_beta_prefix_box_exists

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

19 script commands · 3 reading checkpoints · 0 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 rank common multiple divides
01Fix variables and assumptionsL1–6

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

  1. L1
    intro k
  2. L2
    intro c
  3. L3
    intro T
  4. L4
    intro hcommon
  5. L5
    intro i
  6. L6
    intro hi
02Use earlier factsL7–16

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

  1. L7
    specialize matrix_rank_common_multiple_divides (T)
  2. L8
    specialize matrix_rank_common_multiple_divides (S (k * c))
  3. L9
    specialize matrix_rank_common_multiple_divides ((S i) * c)
  4. L10
    apply matrix_rank_common_multiple_divides
  5. L11
    exact hcommon
  6. L12
    specialize succ_le_succ ((S i) * c)
  7. L13
    specialize succ_le_succ (k * c)
  8. L14
    apply succ_le_succ
  9. L15
    specialize mul_le_mul_right (S i)
  10. L16
    specialize mul_le_mul_right (k)
03Use earlier factsL17–19

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

  1. L17
    specialize mul_le_mul_right (c)
  2. L18
    apply mul_le_mul_right
  3. L19
    exact hi

Library-wide reading audit

Original exact command ledger · 19 lines
  1. 0001intro k
  2. 0002intro c
  3. 0003intro T
  4. 0004intro hcommon
  5. 0005intro i
  6. 0006intro hi
  7. 0007specialize matrix_rank_common_multiple_divides (T)
  8. 0008specialize matrix_rank_common_multiple_divides (S (k * c))
  9. 0009specialize matrix_rank_common_multiple_divides ((S i) * c)
  10. 0010apply matrix_rank_common_multiple_divides
  11. 0011exact hcommon
  12. 0012specialize succ_le_succ ((S i) * c)
  13. 0013specialize succ_le_succ (k * c)
  14. 0014apply succ_le_succ
  15. 0015specialize mul_le_mul_right (S i)
  16. 0016specialize mul_le_mul_right (k)
  17. 0017specialize mul_le_mul_right (c)
  18. 0018apply mul_le_mul_right
  19. 0019exact hi