DL0036

matrix_rank_injective_prefix_transport

A recoded finite selector remains genuinely injective; code equality is not assumed.

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. ∀ u. ∀ v. ∀ l. (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(u,v,x,y)) → (∀ x. ∀ y. ∀ z. Lt(x,l) → Lt(y,l) → BetaAt(b,c,x,z) → BetaAt(b,c,y,z) → x = y) → ∀ x. ∀ y. ∀ z. Lt(x,l) → Lt(y,l) → BetaAt(u,v,x,z) → BetaAt(u,v,y,z) → x = y

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

Definition DAG

Lt(a,b) · 6BetaAt(b,c,i,x) · 8

Actual proof prerequisites

matrix_rank_prefix_equality_symmetric
Original expanded first-order statement 
forall b c u v l. (forall mdr_i_injective_transport mdr_a_injective_transport. (exists mdr_gap_injective_transportb. mdr_gap_injective_transportb + S (mdr_i_injective_transport) = (l)) -> (((exists ff_h_mdr_injective_transporto. ff_h_mdr_injective_transporto + S (mdr_a_injective_transport) = S ((S (mdr_i_injective_transport)) * c)) /\ exists ff_q_mdr_injective_transporto. b = ff_q_mdr_injective_transporto * S ((S (mdr_i_injective_transport)) * c) + (mdr_a_injective_transport))) -> (((exists ff_h_mdr_injective_transportn. ff_h_mdr_injective_transportn + S (mdr_a_injective_transport) = S ((S (mdr_i_injective_transport)) * v)) /\ exists ff_q_mdr_injective_transportn. u = ff_q_mdr_injective_transportn * S ((S (mdr_i_injective_transport)) * v) + (mdr_a_injective_transport)))) -> (forall mdr_i_injective_source mdr_j_injective_source mdr_a_injective_source. (exists mdr_gap_injective_sourcei. mdr_gap_injective_sourcei + S (mdr_i_injective_source) = (l)) -> (exists mdr_gap_injective_sourcej. mdr_gap_injective_sourcej + S (mdr_j_injective_source) = (l)) -> (((exists ff_h_mdr_injective_sourcefirst. ff_h_mdr_injective_sourcefirst + S (mdr_a_injective_source) = S ((S (mdr_i_injective_source)) * c)) /\ exists ff_q_mdr_injective_sourcefirst. b = ff_q_mdr_injective_sourcefirst * S ((S (mdr_i_injective_source)) * c) + (mdr_a_injective_source))) -> (((exists ff_h_mdr_injective_sourcesecond. ff_h_mdr_injective_sourcesecond + S (mdr_a_injective_source) = S ((S (mdr_j_injective_source)) * c)) /\ exists ff_q_mdr_injective_sourcesecond. b = ff_q_mdr_injective_sourcesecond * S ((S (mdr_j_injective_source)) * c) + (mdr_a_injective_source))) -> mdr_i_injective_source = mdr_j_injective_source) -> (forall mdr_i_injective_target mdr_j_injective_target mdr_a_injective_target. (exists mdr_gap_injective_targeti. mdr_gap_injective_targeti + S (mdr_i_injective_target) = (l)) -> (exists mdr_gap_injective_targetj. mdr_gap_injective_targetj + S (mdr_j_injective_target) = (l)) -> (((exists ff_h_mdr_injective_targetfirst. ff_h_mdr_injective_targetfirst + S (mdr_a_injective_target) = S ((S (mdr_i_injective_target)) * v)) /\ exists ff_q_mdr_injective_targetfirst. u = ff_q_mdr_injective_targetfirst * S ((S (mdr_i_injective_target)) * v) + (mdr_a_injective_target))) -> (((exists ff_h_mdr_injective_targetsecond. ff_h_mdr_injective_targetsecond + S (mdr_a_injective_target) = S ((S (mdr_j_injective_target)) * v)) /\ exists ff_q_mdr_injective_targetsecond. u = ff_q_mdr_injective_targetsecond * S ((S (mdr_j_injective_target)) * v) + (mdr_a_injective_target))) -> mdr_i_injective_target = mdr_j_injective_target)

Complete tactic proof in conservative notation

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

38 script commands · 5 reading checkpoints · 1 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 prefix equality symmetric
01Fix variables and assumptionsL1–7

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro u
  4. L4
    intro v
  5. L5
    intro l
  6. L6
    intro hprefix
  7. L7
    intro hinjective
02Establish hreverseL8–17

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

  1. L8
    have hreverse : ∀ mdr_i_reverse_injective. ∀ mdr_a_reverse_injective. Lt(mdr_i_reverse_injective,l) → BetaAt(u,v,mdr_i_reverse_injective,mdr_a_reverse_injective) → BetaAt(b,c,mdr_i_reverse_injective,mdr_a_reverse_injective)Definitions: Lt(mdr_i_reverse_injective,l)BetaAt(u,v,mdr_i_reverse_injective,mdr_a_reverse_injective)BetaAt(b,c,mdr_i_reverse_injective,mdr_a_reverse_injective)Original native command in the exact edition
  2. L9
    specialize matrix_rank_prefix_equality_symmetric (b)
  3. L10
    specialize matrix_rank_prefix_equality_symmetric (c)
  4. L11
    specialize matrix_rank_prefix_equality_symmetric (u)
  5. L12
    specialize matrix_rank_prefix_equality_symmetric (v)
  6. L13
    specialize matrix_rank_prefix_equality_symmetric (l)
  7. L14
    apply matrix_rank_prefix_equality_symmetric
  8. L15
    exact hprefix
  9. L16
    intro i
  10. L17
    intro j
03Fix variables and assumptionsL18–22

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

  1. L18
    intro a
  2. L19
    intro hi
  3. L20
    intro hj
  4. L21
    intro ha
  5. L22
    intro hb
04Use earlier factsL23–32

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

  1. L23
    specialize hinjective (i)
  2. L24
    specialize hinjective (j)
  3. L25
    specialize hinjective (a)
  4. L26
    apply hinjective
  5. L27
    exact hi
  6. L28
    exact hj
  7. L29
    specialize hreverse (i)
  8. L30
    specialize hreverse (a)
  9. L31
    apply hreverse
  10. L32
    exact hi
05Use earlier factsL33–38

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

  1. L33
    exact ha
  2. L34
    specialize hreverse (j)
  3. L35
    specialize hreverse (a)
  4. L36
    apply hreverse
  5. L37
    exact hj
  6. L38
    exact hb

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro u
  4. 0004intro v
  5. 0005intro l
  6. 0006intro hprefix
  7. 0007intro hinjective
  8. 0008have hreverse : ∀ mdr_i_reverse_injective. ∀ mdr_a_reverse_injective. Lt(mdr_i_reverse_injective,l) → BetaAt(u,v,mdr_i_reverse_injective,mdr_a_reverse_injective) → BetaAt(b,c,mdr_i_reverse_injective,mdr_a_reverse_injective)
  9. 0009specialize matrix_rank_prefix_equality_symmetric (b)
  10. 0010specialize matrix_rank_prefix_equality_symmetric (c)
  11. 0011specialize matrix_rank_prefix_equality_symmetric (u)
  12. 0012specialize matrix_rank_prefix_equality_symmetric (v)
  13. 0013specialize matrix_rank_prefix_equality_symmetric (l)
  14. 0014apply matrix_rank_prefix_equality_symmetric
  15. 0015exact hprefix
  16. 0016intro i
  17. 0017intro j
  18. 0018intro a
  19. 0019intro hi
  20. 0020intro hj
  21. 0021intro ha
  22. 0022intro hb
  23. 0023specialize hinjective (i)
  24. 0024specialize hinjective (j)
  25. 0025specialize hinjective (a)
  26. 0026apply hinjective
  27. 0027exact hi
  28. 0028exact hj
  29. 0029specialize hreverse (i)
  30. 0030specialize hreverse (a)
  31. 0031apply hreverse
  32. 0032exact hi
  33. 0033exact ha
  34. 0034specialize hreverse (j)
  35. 0035specialize hreverse (a)
  36. 0036apply hreverse
  37. 0037exact hj
  38. 0038exact hb