DL0032

matrix_rank_uniform_beta_prefix_box_exists

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

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

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 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)))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 46 exact native proof lines.

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

Proof neighborhood

Direct dependencies

bounded_common_multiple_exists Stable theorem; checked-use authorized scaled_bounded_common_multiple Stable theorem; checked-use authorized le_scaled_nonzero Stable theorem; checked-use authorized DL002F matrix_rank_beta_moduli_common_multiple DL0031 matrix_rank_bounded_recode_in_fixed_box

Direct dependents

DL0059 matrix_rank_nonzero_minor_decidable

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

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.

Named ingredients (2)
matrix rank beta moduli common multiplematrix rank bounded recode in fixed box
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 : exists mdr_gap_uniform_scale. mdr_gap_uniform_scale + (B) = (x * B)
  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 exact 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 : exists mdr_gap_uniform_scale. mdr_gap_uniform_scale + (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