DL002F

matrix_rank_beta_moduli_common_multiple

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

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. ∀ c. ∀ T. (∀ x. (∃ y. S x + S y = S S (k · c)) → ∃ y. T = S x · y) → ∀ x. Lt(x,k) → ∃ y. T = S (S x · c) · y

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

Definition DAG

Lt(a,b) · 1

Actual proof prerequisites

matrix_rank_common_multiple_dividessucc_le_succ · checked external prerequisitemul_le_mul_right · checked external prerequisite
Original expanded first-order 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))

Complete tactic proof in conservative notation

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

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.

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 (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 defined 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