DL003C

matrix_rank_selector_transport

Both in-range coordinates and distinctness survive the complete finite selector recoding.

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

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

Definition DAG

FiniteMatrixSelector(b,c,l,B) · 2Lt(a,b) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

matrix_rank_bounded_prefix_transportmatrix_rank_injective_prefix_transport
Original expanded first-order statement 
forall b c u v l B. (forall mdr_i_selector_transport mdr_a_selector_transport. (exists mdr_gap_selector_transportb. mdr_gap_selector_transportb + S (mdr_i_selector_transport) = (l)) -> (((exists ff_h_mdr_selector_transporto. ff_h_mdr_selector_transporto + S (mdr_a_selector_transport) = S ((S (mdr_i_selector_transport)) * c)) /\ exists ff_q_mdr_selector_transporto. b = ff_q_mdr_selector_transporto * S ((S (mdr_i_selector_transport)) * c) + (mdr_a_selector_transport))) -> (((exists ff_h_mdr_selector_transportn. ff_h_mdr_selector_transportn + S (mdr_a_selector_transport) = S ((S (mdr_i_selector_transport)) * v)) /\ exists ff_q_mdr_selector_transportn. u = ff_q_mdr_selector_transportn * S ((S (mdr_i_selector_transport)) * v) + (mdr_a_selector_transport)))) -> (((forall fom_index_mrf_selector_sourcebound. (exists fom_gap_mrf_selector_sourcebound_index_bound. fom_gap_mrf_selector_sourcebound_index_bound + S (fom_index_mrf_selector_sourcebound) = l) -> exists fom_value_mrf_selector_sourcebound. ((((exists fom_beta_height_mrf_selector_sourcebound_entry. fom_beta_height_mrf_selector_sourcebound_entry + S (fom_value_mrf_selector_sourcebound) = S ((S (fom_index_mrf_selector_sourcebound)) * c)) /\ exists fom_beta_quotient_mrf_selector_sourcebound_entry. b = fom_beta_quotient_mrf_selector_sourcebound_entry * S ((S (fom_index_mrf_selector_sourcebound)) * c) + (fom_value_mrf_selector_sourcebound))) /\ (exists fom_gap_mrf_selector_sourcebound_value_bound. fom_gap_mrf_selector_sourcebound_value_bound + S (fom_value_mrf_selector_sourcebound) = B))) /\ (forall mdr_i_selector_sourcedistinct mdr_j_selector_sourcedistinct mdr_a_selector_sourcedistinct. (exists mdr_gap_selector_sourcedistincti. mdr_gap_selector_sourcedistincti + S (mdr_i_selector_sourcedistinct) = (l)) -> (exists mdr_gap_selector_sourcedistinctj. mdr_gap_selector_sourcedistinctj + S (mdr_j_selector_sourcedistinct) = (l)) -> (((exists ff_h_mdr_selector_sourcedistinctfirst. ff_h_mdr_selector_sourcedistinctfirst + S (mdr_a_selector_sourcedistinct) = S ((S (mdr_i_selector_sourcedistinct)) * c)) /\ exists ff_q_mdr_selector_sourcedistinctfirst. b = ff_q_mdr_selector_sourcedistinctfirst * S ((S (mdr_i_selector_sourcedistinct)) * c) + (mdr_a_selector_sourcedistinct))) -> (((exists ff_h_mdr_selector_sourcedistinctsecond. ff_h_mdr_selector_sourcedistinctsecond + S (mdr_a_selector_sourcedistinct) = S ((S (mdr_j_selector_sourcedistinct)) * c)) /\ exists ff_q_mdr_selector_sourcedistinctsecond. b = ff_q_mdr_selector_sourcedistinctsecond * S ((S (mdr_j_selector_sourcedistinct)) * c) + (mdr_a_selector_sourcedistinct))) -> mdr_i_selector_sourcedistinct = mdr_j_selector_sourcedistinct))) -> (((forall fom_index_mrf_selector_targetbound. (exists fom_gap_mrf_selector_targetbound_index_bound. fom_gap_mrf_selector_targetbound_index_bound + S (fom_index_mrf_selector_targetbound) = l) -> exists fom_value_mrf_selector_targetbound. ((((exists fom_beta_height_mrf_selector_targetbound_entry. fom_beta_height_mrf_selector_targetbound_entry + S (fom_value_mrf_selector_targetbound) = S ((S (fom_index_mrf_selector_targetbound)) * v)) /\ exists fom_beta_quotient_mrf_selector_targetbound_entry. u = fom_beta_quotient_mrf_selector_targetbound_entry * S ((S (fom_index_mrf_selector_targetbound)) * v) + (fom_value_mrf_selector_targetbound))) /\ (exists fom_gap_mrf_selector_targetbound_value_bound. fom_gap_mrf_selector_targetbound_value_bound + S (fom_value_mrf_selector_targetbound) = B))) /\ (forall mdr_i_selector_targetdistinct mdr_j_selector_targetdistinct mdr_a_selector_targetdistinct. (exists mdr_gap_selector_targetdistincti. mdr_gap_selector_targetdistincti + S (mdr_i_selector_targetdistinct) = (l)) -> (exists mdr_gap_selector_targetdistinctj. mdr_gap_selector_targetdistinctj + S (mdr_j_selector_targetdistinct) = (l)) -> (((exists ff_h_mdr_selector_targetdistinctfirst. ff_h_mdr_selector_targetdistinctfirst + S (mdr_a_selector_targetdistinct) = S ((S (mdr_i_selector_targetdistinct)) * v)) /\ exists ff_q_mdr_selector_targetdistinctfirst. u = ff_q_mdr_selector_targetdistinctfirst * S ((S (mdr_i_selector_targetdistinct)) * v) + (mdr_a_selector_targetdistinct))) -> (((exists ff_h_mdr_selector_targetdistinctsecond. ff_h_mdr_selector_targetdistinctsecond + S (mdr_a_selector_targetdistinct) = S ((S (mdr_j_selector_targetdistinct)) * v)) /\ exists ff_q_mdr_selector_targetdistinctsecond. u = ff_q_mdr_selector_targetdistinctsecond * S ((S (mdr_j_selector_targetdistinct)) * v) + (mdr_a_selector_targetdistinct))) -> mdr_i_selector_targetdistinct = mdr_j_selector_targetdistinct)))

Complete tactic proof in conservative notation

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

27 script commands · 4 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 (2)
matrix rank bounded prefix transportmatrix rank injective prefix transport
01Fix variables and assumptionsL1–8

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 B
  7. L7
    intro hprefix
  8. L8
    intro hselector
02Separate the logical casesL9–10

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

  1. L9
    cases hselector
  2. L10
    split
03Use earlier factsL11–20

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

  1. L11
    specialize matrix_rank_bounded_prefix_transport (b)
  2. L12
    specialize matrix_rank_bounded_prefix_transport (c)
  3. L13
    specialize matrix_rank_bounded_prefix_transport (u)
  4. L14
    specialize matrix_rank_bounded_prefix_transport (v)
  5. L15
    specialize matrix_rank_bounded_prefix_transport (l)
  6. L16
    specialize matrix_rank_bounded_prefix_transport (B)
  7. L17
    apply matrix_rank_bounded_prefix_transport
  8. L18
    exact hprefix
  9. L19
    exact hselector_left
  10. L20
    specialize matrix_rank_injective_prefix_transport (b)
04Use earlier factsL21–27

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

  1. L21
    specialize matrix_rank_injective_prefix_transport (c)
  2. L22
    specialize matrix_rank_injective_prefix_transport (u)
  3. L23
    specialize matrix_rank_injective_prefix_transport (v)
  4. L24
    specialize matrix_rank_injective_prefix_transport (l)
  5. L25
    apply matrix_rank_injective_prefix_transport
  6. L26
    exact hprefix
  7. L27
    exact hselector_right

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro u
  4. 0004intro v
  5. 0005intro l
  6. 0006intro B
  7. 0007intro hprefix
  8. 0008intro hselector
  9. 0009cases hselector
  10. 0010split
  11. 0011specialize matrix_rank_bounded_prefix_transport (b)
  12. 0012specialize matrix_rank_bounded_prefix_transport (c)
  13. 0013specialize matrix_rank_bounded_prefix_transport (u)
  14. 0014specialize matrix_rank_bounded_prefix_transport (v)
  15. 0015specialize matrix_rank_bounded_prefix_transport (l)
  16. 0016specialize matrix_rank_bounded_prefix_transport (B)
  17. 0017apply matrix_rank_bounded_prefix_transport
  18. 0018exact hprefix
  19. 0019exact hselector_left
  20. 0020specialize matrix_rank_injective_prefix_transport (b)
  21. 0021specialize matrix_rank_injective_prefix_transport (c)
  22. 0022specialize matrix_rank_injective_prefix_transport (u)
  23. 0023specialize matrix_rank_injective_prefix_transport (v)
  24. 0024specialize matrix_rank_injective_prefix_transport (l)
  25. 0025apply matrix_rank_injective_prefix_transport
  26. 0026exact hprefix
  27. 0027exact hselector_right