DL0032

matrix_rank_uniform_beta_prefix_box_exists

Unconditionally construct one fixed scale and one positive finite code bound representing every bounded prefix of the requested length.

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. UniformBetaPrefixBox(c,T,k,B)

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

Definition DAG

UniformBetaPrefixBox(c,T,l,B) · 1Le(a,b) · 1

Actual proof prerequisites

bounded_common_multiple_exists · checked external prerequisitescaled_bounded_common_multiple · checked external prerequisitele_scaled_nonzero · checked external prerequisitematrix_rank_beta_moduli_common_multiplematrix_rank_bounded_recode_in_fixed_box
Original expanded first-order statement 
forall k B. exists c T. (((~(T = 0)) /\ (forall mdr_b_uniform_box mdr_e_uniform_box. (forall fom_index_mrf_uniform_boxsource. (exists fom_gap_mrf_uniform_boxsource_index_bound. fom_gap_mrf_uniform_boxsource_index_bound + S (fom_index_mrf_uniform_boxsource) = k) -> exists fom_value_mrf_uniform_boxsource. ((((exists fom_beta_height_mrf_uniform_boxsource_entry. fom_beta_height_mrf_uniform_boxsource_entry + S (fom_value_mrf_uniform_boxsource) = S ((S (fom_index_mrf_uniform_boxsource)) * mdr_e_uniform_box)) /\ exists fom_beta_quotient_mrf_uniform_boxsource_entry. mdr_b_uniform_box = fom_beta_quotient_mrf_uniform_boxsource_entry * S ((S (fom_index_mrf_uniform_boxsource)) * mdr_e_uniform_box) + (fom_value_mrf_uniform_boxsource))) /\ (exists fom_gap_mrf_uniform_boxsource_value_bound. fom_gap_mrf_uniform_boxsource_value_bound + S (fom_value_mrf_uniform_boxsource) = B))) -> exists mdr_z_uniform_box. (((exists mdr_gap_uniform_boxbound. mdr_gap_uniform_boxbound + S (mdr_z_uniform_box) = (T)) /\ (forall mdr_i_uniform_boxprefix mdr_a_uniform_boxprefix. (exists mdr_gap_uniform_boxprefixb. mdr_gap_uniform_boxprefixb + S (mdr_i_uniform_boxprefix) = (k)) -> (((exists ff_h_mdr_uniform_boxprefixo. ff_h_mdr_uniform_boxprefixo + S (mdr_a_uniform_boxprefix) = S ((S (mdr_i_uniform_boxprefix)) * mdr_e_uniform_box)) /\ exists ff_q_mdr_uniform_boxprefixo. mdr_b_uniform_box = ff_q_mdr_uniform_boxprefixo * S ((S (mdr_i_uniform_boxprefix)) * mdr_e_uniform_box) + (mdr_a_uniform_boxprefix))) -> (((exists ff_h_mdr_uniform_boxprefixn. ff_h_mdr_uniform_boxprefixn + S (mdr_a_uniform_boxprefix) = S ((S (mdr_i_uniform_boxprefix)) * c)) /\ exists ff_q_mdr_uniform_boxprefixn. mdr_z_uniform_box = ff_q_mdr_uniform_boxprefixn * S ((S (mdr_i_uniform_boxprefix)) * c) + (mdr_a_uniform_boxprefix)))))))))

Complete tactic proof in conservative notation

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

46 script commands · 13 reading checkpoints · 4 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 recode in fixed boxmatrix rank beta moduli common multiple
01Fix variables and assumptionsL1–2

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

  1. L1
    intro k
  2. L2
    intro B
02Establish hCL3–5

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

  1. L3
    have hC : exists C. ((~(C = 0)) /\ (forall mdr_t_uniform_common. (exists mdr_h_uniform_common. S mdr_t_uniform_common + S mdr_h_uniform_common = S (k)) -> exists mdr_q_uniform_common. C = S mdr_t_uniform_common * mdr_q_uniform_common))
  2. L4
    specialize bounded_common_multiple_exists (k)
  3. L5
    apply bounded_common_multiple_exists
03Separate the logical casesL6–7

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

  1. L6
    cases hC
  2. L7
    cases hC_witness
04Establish hscalecommonL8–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply scaled bounded common multiple.

  1. L8
    have hscalecommon : forall mdr_t_scaled_common. (exists mdr_h_scaled_common. S mdr_t_scaled_common + S mdr_h_scaled_common = S (k)) -> exists mdr_q_scaled_common. x * B = S mdr_t_scaled_common * mdr_q_scaled_common
  2. L9
    specialize scaled_bounded_common_multiple (k)
  3. L10
    specialize scaled_bounded_common_multiple (x)
  4. L11
    specialize scaled_bounded_common_multiple (B)
  5. L12
    apply scaled_bounded_common_multiple
  6. L13
    exact hC_witness_right
05Establish hscaleL14–18

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

  1. L14
    have hscale : Le(B,x · B)Definitions: Le(B,x · B)Original native command in the exact edition
  2. L15
    specialize le_scaled_nonzero (x)
  3. L16
    specialize le_scaled_nonzero (B)
  4. L17
    apply le_scaled_nonzero
  5. L18
    exact hC_witness_left
06Establish hTL19–21

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

  1. L19
    have hT : exists T. ((~(T = 0)) /\ (forall mdr_t_uniform_moduli. (exists mdr_h_uniform_moduli. S mdr_t_uniform_moduli + S mdr_h_uniform_moduli = S (S (k * (x * B)))) -> exists mdr_q_uniform_moduli. T = S mdr_t_uniform_moduli * mdr_q_uniform_moduli))
  2. L20
    specialize bounded_common_multiple_exists (S (k * (x * B)))
  3. L21
    apply bounded_common_multiple_exists
07Separate the logical casesL22–23

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

  1. L22
    cases hT
  2. L23
    cases hT_witness
08Construct an explicit witnessL24–25

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

  1. L24
    exists x * B
  2. L25
    exists x1
09Separate the logical casesL26–26

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

  1. L26
    split
10Use earlier factsL27–27

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

  1. L27
    exact hT_witness_left
11Fix variables and assumptionsL28–30

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

  1. L28
    intro b
  2. L29
    intro e
  3. L30
    intro hbounded
12Use earlier factsL31–40

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

  1. L31
    specialize matrix_rank_bounded_recode_in_fixed_box (k)
  2. L32
    specialize matrix_rank_bounded_recode_in_fixed_box (B)
  3. L33
    specialize matrix_rank_bounded_recode_in_fixed_box (x * B)
  4. L34
    specialize matrix_rank_bounded_recode_in_fixed_box (x1)
  5. L35
    specialize matrix_rank_bounded_recode_in_fixed_box (b)
  6. L36
    specialize matrix_rank_bounded_recode_in_fixed_box (e)
  7. L37
    apply matrix_rank_bounded_recode_in_fixed_box
  8. L38
    exact hscale
  9. L39
    exact hscalecommon
  10. L40
    exact hT_witness_left
13Use earlier factsL41–46

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

  1. L41
    specialize matrix_rank_beta_moduli_common_multiple (k)
  2. L42
    specialize matrix_rank_beta_moduli_common_multiple (x * B)
  3. L43
    specialize matrix_rank_beta_moduli_common_multiple (x1)
  4. L44
    apply matrix_rank_beta_moduli_common_multiple
  5. L45
    exact hT_witness_right
  6. L46
    exact hbounded

Library-wide reading audit

Original defined command ledger · 46 lines
  1. 0001intro k
  2. 0002intro B
  3. 0003have hC : exists C. ((~(C = 0)) /\ (forall mdr_t_uniform_common. (exists mdr_h_uniform_common. S mdr_t_uniform_common + S mdr_h_uniform_common = S (k)) -> exists mdr_q_uniform_common. C = S mdr_t_uniform_common * mdr_q_uniform_common))
  4. 0004specialize bounded_common_multiple_exists (k)
  5. 0005apply bounded_common_multiple_exists
  6. 0006cases hC
  7. 0007cases hC_witness
  8. 0008have hscalecommon : forall mdr_t_scaled_common. (exists mdr_h_scaled_common. S mdr_t_scaled_common + S mdr_h_scaled_common = S (k)) -> exists mdr_q_scaled_common. x * B = S mdr_t_scaled_common * mdr_q_scaled_common
  9. 0009specialize scaled_bounded_common_multiple (k)
  10. 0010specialize scaled_bounded_common_multiple (x)
  11. 0011specialize scaled_bounded_common_multiple (B)
  12. 0012apply scaled_bounded_common_multiple
  13. 0013exact hC_witness_right
  14. 0014have hscale : Le(B,x · B)
  15. 0015specialize le_scaled_nonzero (x)
  16. 0016specialize le_scaled_nonzero (B)
  17. 0017apply le_scaled_nonzero
  18. 0018exact hC_witness_left
  19. 0019have hT : exists T. ((~(T = 0)) /\ (forall mdr_t_uniform_moduli. (exists mdr_h_uniform_moduli. S mdr_t_uniform_moduli + S mdr_h_uniform_moduli = S (S (k * (x * B)))) -> exists mdr_q_uniform_moduli. T = S mdr_t_uniform_moduli * mdr_q_uniform_moduli))
  20. 0020specialize bounded_common_multiple_exists (S (k * (x * B)))
  21. 0021apply bounded_common_multiple_exists
  22. 0022cases hT
  23. 0023cases hT_witness
  24. 0024exists x * B
  25. 0025exists x1
  26. 0026split
  27. 0027exact hT_witness_left
  28. 0028intro b
  29. 0029intro e
  30. 0030intro hbounded
  31. 0031specialize matrix_rank_bounded_recode_in_fixed_box (k)
  32. 0032specialize matrix_rank_bounded_recode_in_fixed_box (B)
  33. 0033specialize matrix_rank_bounded_recode_in_fixed_box (x * B)
  34. 0034specialize matrix_rank_bounded_recode_in_fixed_box (x1)
  35. 0035specialize matrix_rank_bounded_recode_in_fixed_box (b)
  36. 0036specialize matrix_rank_bounded_recode_in_fixed_box (e)
  37. 0037apply matrix_rank_bounded_recode_in_fixed_box
  38. 0038exact hscale
  39. 0039exact hscalecommon
  40. 0040exact hT_witness_left
  41. 0041specialize matrix_rank_beta_moduli_common_multiple (k)
  42. 0042specialize matrix_rank_beta_moduli_common_multiple (x * B)
  43. 0043specialize matrix_rank_beta_moduli_common_multiple (x1)
  44. 0044apply matrix_rank_beta_moduli_common_multiple
  45. 0045exact hT_witness_right
  46. 0046exact hbounded