DL0047

matrix_rank_selected_prefix_functional

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

Any two codes of the same actual selected square agree on every finite entry.

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 b c w rb rc cb cc q ub uc vb vc. (forall mdr_i_first_prefix. (exists mdr_gap_first_prefixbound. mdr_gap_first_prefixbound + S (mdr_i_first_prefix) = (q * q)) -> exists mdr_a_first_prefix. (((exists mdr_r_first_prefixpoint mdr_s_first_prefixpoint mdr_u_first_prefixpoint mdr_v_first_prefixpoint. ((mdr_i_first_prefix = (q) * mdr_r_first_prefixpoint + mdr_s_first_prefixpoint) /\ ((exists mdr_gap_first_prefixpointcolumn. mdr_gap_first_prefixpointcolumn + S (mdr_s_first_prefixpoint) = (q)) /\ ((((exists ff_h_mdr_first_prefixpointrow_index. ff_h_mdr_first_prefixpointrow_index + S (mdr_u_first_prefixpoint) = S ((S (mdr_r_first_prefixpoint)) * rc)) /\ exists ff_q_mdr_first_prefixpointrow_index. rb = ff_q_mdr_first_prefixpointrow_index * S ((S (mdr_r_first_prefixpoint)) * rc) + (mdr_u_first_prefixpoint))) /\ ((((exists ff_h_mdr_first_prefixpointcolumn_index. ff_h_mdr_first_prefixpointcolumn_index + S (mdr_v_first_prefixpoint) = S ((S (mdr_s_first_prefixpoint)) * cc)) /\ exists ff_q_mdr_first_prefixpointcolumn_index. cb = ff_q_mdr_first_prefixpointcolumn_index * S ((S (mdr_s_first_prefixpoint)) * cc) + (mdr_v_first_prefixpoint))) /\ (((exists ff_h_mdr_first_prefixpointsource. ff_h_mdr_first_prefixpointsource + S (mdr_a_first_prefix) = S ((S ((mdr_u_first_prefixpoint) * (w) + (mdr_v_first_prefixpoint))) * c)) /\ exists ff_q_mdr_first_prefixpointsource. b = ff_q_mdr_first_prefixpointsource * S ((S ((mdr_u_first_prefixpoint) * (w) + (mdr_v_first_prefixpoint))) * c) + (mdr_a_first_prefix)))))))) /\ (((exists ff_h_mdr_first_prefixoutput. ff_h_mdr_first_prefixoutput + S (mdr_a_first_prefix) = S ((S (mdr_i_first_prefix)) * uc)) /\ exists ff_q_mdr_first_prefixoutput. ub = ff_q_mdr_first_prefixoutput * S ((S (mdr_i_first_prefix)) * uc) + (mdr_a_first_prefix)))))) -> (forall mdr_i_second_prefix. (exists mdr_gap_second_prefixbound. mdr_gap_second_prefixbound + S (mdr_i_second_prefix) = (q * q)) -> exists mdr_a_second_prefix. (((exists mdr_r_second_prefixpoint mdr_s_second_prefixpoint mdr_u_second_prefixpoint mdr_v_second_prefixpoint. ((mdr_i_second_prefix = (q) * mdr_r_second_prefixpoint + mdr_s_second_prefixpoint) /\ ((exists mdr_gap_second_prefixpointcolumn. mdr_gap_second_prefixpointcolumn + S (mdr_s_second_prefixpoint) = (q)) /\ ((((exists ff_h_mdr_second_prefixpointrow_index. ff_h_mdr_second_prefixpointrow_index + S (mdr_u_second_prefixpoint) = S ((S (mdr_r_second_prefixpoint)) * rc)) /\ exists ff_q_mdr_second_prefixpointrow_index. rb = ff_q_mdr_second_prefixpointrow_index * S ((S (mdr_r_second_prefixpoint)) * rc) + (mdr_u_second_prefixpoint))) /\ ((((exists ff_h_mdr_second_prefixpointcolumn_index. ff_h_mdr_second_prefixpointcolumn_index + S (mdr_v_second_prefixpoint) = S ((S (mdr_s_second_prefixpoint)) * cc)) /\ exists ff_q_mdr_second_prefixpointcolumn_index. cb = ff_q_mdr_second_prefixpointcolumn_index * S ((S (mdr_s_second_prefixpoint)) * cc) + (mdr_v_second_prefixpoint))) /\ (((exists ff_h_mdr_second_prefixpointsource. ff_h_mdr_second_prefixpointsource + S (mdr_a_second_prefix) = S ((S ((mdr_u_second_prefixpoint) * (w) + (mdr_v_second_prefixpoint))) * c)) /\ exists ff_q_mdr_second_prefixpointsource. b = ff_q_mdr_second_prefixpointsource * S ((S ((mdr_u_second_prefixpoint) * (w) + (mdr_v_second_prefixpoint))) * c) + (mdr_a_second_prefix)))))))) /\ (((exists ff_h_mdr_second_prefixoutput. ff_h_mdr_second_prefixoutput + S (mdr_a_second_prefix) = S ((S (mdr_i_second_prefix)) * vc)) /\ exists ff_q_mdr_second_prefixoutput. vb = ff_q_mdr_second_prefixoutput * S ((S (mdr_i_second_prefix)) * vc) + (mdr_a_second_prefix)))))) -> (forall mdr_i_prefix_unique mdr_a_prefix_unique. (exists mdr_gap_prefix_uniqueb. mdr_gap_prefix_uniqueb + S (mdr_i_prefix_unique) = (q * q)) -> (((exists ff_h_mdr_prefix_uniqueo. ff_h_mdr_prefix_uniqueo + S (mdr_a_prefix_unique) = S ((S (mdr_i_prefix_unique)) * uc)) /\ exists ff_q_mdr_prefix_uniqueo. ub = ff_q_mdr_prefix_uniqueo * S ((S (mdr_i_prefix_unique)) * uc) + (mdr_a_prefix_unique))) -> (((exists ff_h_mdr_prefix_uniquen. ff_h_mdr_prefix_uniquen + S (mdr_a_prefix_unique) = S ((S (mdr_i_prefix_unique)) * vc)) /\ exists ff_q_mdr_prefix_uniquen. vb = ff_q_mdr_prefix_uniquen * S ((S (mdr_i_prefix_unique)) * vc) + (mdr_a_prefix_unique))))

Constructive proof overview

Generated structural guide

Any two codes of the same actual selected square agree on every finite entry.

The unchanged tactic script uses 2 declared prerequisites and contains 59 exact native proof lines.

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

Proof neighborhood

Direct dependencies

DL0041 matrix_rank_selected_point_functional beta_at_unique Stable theorem; checked-use authorized

Direct dependents

DL0048 matrix_rank_signed_selected_square_functional

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

59 script commands · 12 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 (1)
matrix rank selected point functional

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro w
  4. L4
    intro rb
  5. L5
    intro rc
  6. L6
    intro cb
  7. L7
    intro cc
  8. L8
    intro q
  9. L9
    intro ub
  10. L10
    intro uc
02Fix variables and assumptionsL11–18

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

  1. L11
    intro vb
  2. L12
    intro vc
  3. L13
    intro hfirst
  4. L14
    intro hsecond
  5. L15
    intro i
  6. L16
    intro a
  7. L17
    intro hi
  8. L18
    intro ha
03Establish hleftL19–22

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

  1. L19
    have hleft : ∃ z. (∃ x. ∃ y. ∃ n. ∃ m. i = q · x + y ∧ (Lt(y,q) ∧ (BetaAt(rb,rc,x,n) ∧ (BetaAt(cb,cc,y,m) ∧ BetaAt(b,c,n · w + m,z))))) ∧ BetaAt(ub,uc,i,z)Definitions: LtBetaAt
  2. L20
    specialize hfirst (i)
  3. L21
    apply hfirst
  4. L22
    exact hi
04Separate the logical casesL23–24

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

  1. L23
    cases hleft
  2. L24
    cases hleft_witness
05Establish hrightL25–28

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

  1. L25
    have hright : ∃ z. (∃ x. ∃ y. ∃ n. ∃ m. i = q · x + y ∧ (Lt(y,q) ∧ (BetaAt(rb,rc,x,n) ∧ (BetaAt(cb,cc,y,m) ∧ BetaAt(b,c,n · w + m,z))))) ∧ BetaAt(vb,vc,i,z)Definitions: LtBetaAt
  2. L26
    specialize hsecond (i)
  3. L27
    apply hsecond
  4. L28
    exact hi
06Separate the logical casesL29–30

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

  1. L29
    cases hright
  2. L30
    cases hright_witness
07Establish hvaluesL31–40

Establish this local claim before using it. It is not an additional assumption.

  1. L31
    have hvalues : x = x1
  2. L32
    specialize matrix_rank_selected_point_functional (b)
  3. L33
    specialize matrix_rank_selected_point_functional (c)
  4. L34
    specialize matrix_rank_selected_point_functional (w)
  5. L35
    specialize matrix_rank_selected_point_functional (rb)
  6. L36
    specialize matrix_rank_selected_point_functional (rc)
  7. L37
    specialize matrix_rank_selected_point_functional (cb)
  8. L38
    specialize matrix_rank_selected_point_functional (cc)
  9. L39
    specialize matrix_rank_selected_point_functional (q)
  10. L40
    specialize matrix_rank_selected_point_functional (i)
08Use earlier factsL41–45

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

  1. L41
    specialize matrix_rank_selected_point_functional (x)
  2. L42
    specialize matrix_rank_selected_point_functional (x1)
  3. L43
    apply matrix_rank_selected_point_functional
  4. L44
    exact hleft_witness_left
  5. L45
    exact hright_witness_left
09Establish houtputL46–55

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L46
    have houtput : a = x1
  2. L47
    trans x
  3. L48
    specialize beta_at_unique (ub)
  4. L49
    specialize beta_at_unique (uc)
  5. L50
    specialize beta_at_unique (i)
  6. L51
    specialize beta_at_unique (a)
  7. L52
    specialize beta_at_unique (x)
  8. L53
    apply beta_at_unique
  9. L54
    exact ha
  10. L55
    exact hleft_witness_right
10Use earlier factsL56–56

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

  1. L56
    exact hvalues
11Calculate and transport equalitiesL57–58

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L57
    rewrite houtput
  2. L58
    rewrite houtput
12Use earlier factsL59–59

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

  1. L59
    exact hright_witness_right

Library-wide reading audit

Original exact command ledger · 59 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro w
  4. 0004intro rb
  5. 0005intro rc
  6. 0006intro cb
  7. 0007intro cc
  8. 0008intro q
  9. 0009intro ub
  10. 0010intro uc
  11. 0011intro vb
  12. 0012intro vc
  13. 0013intro hfirst
  14. 0014intro hsecond
  15. 0015intro i
  16. 0016intro a
  17. 0017intro hi
  18. 0018intro ha
  19. 0019have hleft : exists z. ((exists mdr_r_first_cell mdr_s_first_cell mdr_u_first_cell mdr_v_first_cell. ((i = (q) * mdr_r_first_cell + mdr_s_first_cell) /\ ((exists mdr_gap_first_cellcolumn. mdr_gap_first_cellcolumn + S (mdr_s_first_cell) = (q)) /\ ((((exists ff_h_mdr_first_cellrow_index. ff_h_mdr_first_cellrow_index + S (mdr_u_first_cell) = S ((S (mdr_r_first_cell)) * rc)) /\ exists ff_q_mdr_first_cellrow_index. rb = ff_q_mdr_first_cellrow_index * S ((S (mdr_r_first_cell)) * rc) + (mdr_u_first_cell))) /\ ((((exists ff_h_mdr_first_cellcolumn_index. ff_h_mdr_first_cellcolumn_index + S (mdr_v_first_cell) = S ((S (mdr_s_first_cell)) * cc)) /\ exists ff_q_mdr_first_cellcolumn_index. cb = ff_q_mdr_first_cellcolumn_index * S ((S (mdr_s_first_cell)) * cc) + (mdr_v_first_cell))) /\ (((exists ff_h_mdr_first_cellsource. ff_h_mdr_first_cellsource + S (z) = S ((S ((mdr_u_first_cell) * (w) + (mdr_v_first_cell))) * c)) /\ exists ff_q_mdr_first_cellsource. b = ff_q_mdr_first_cellsource * S ((S ((mdr_u_first_cell) * (w) + (mdr_v_first_cell))) * c) + (z)))))))) /\ (((exists ff_h_mdr_first_output. ff_h_mdr_first_output + S (z) = S ((S (i)) * uc)) /\ exists ff_q_mdr_first_output. ub = ff_q_mdr_first_output * S ((S (i)) * uc) + (z))))
  20. 0020specialize hfirst (i)
  21. 0021apply hfirst
  22. 0022exact hi
  23. 0023cases hleft
  24. 0024cases hleft_witness
  25. 0025have hright : exists z. ((exists mdr_r_second_cell mdr_s_second_cell mdr_u_second_cell mdr_v_second_cell. ((i = (q) * mdr_r_second_cell + mdr_s_second_cell) /\ ((exists mdr_gap_second_cellcolumn. mdr_gap_second_cellcolumn + S (mdr_s_second_cell) = (q)) /\ ((((exists ff_h_mdr_second_cellrow_index. ff_h_mdr_second_cellrow_index + S (mdr_u_second_cell) = S ((S (mdr_r_second_cell)) * rc)) /\ exists ff_q_mdr_second_cellrow_index. rb = ff_q_mdr_second_cellrow_index * S ((S (mdr_r_second_cell)) * rc) + (mdr_u_second_cell))) /\ ((((exists ff_h_mdr_second_cellcolumn_index. ff_h_mdr_second_cellcolumn_index + S (mdr_v_second_cell) = S ((S (mdr_s_second_cell)) * cc)) /\ exists ff_q_mdr_second_cellcolumn_index. cb = ff_q_mdr_second_cellcolumn_index * S ((S (mdr_s_second_cell)) * cc) + (mdr_v_second_cell))) /\ (((exists ff_h_mdr_second_cellsource. ff_h_mdr_second_cellsource + S (z) = S ((S ((mdr_u_second_cell) * (w) + (mdr_v_second_cell))) * c)) /\ exists ff_q_mdr_second_cellsource. b = ff_q_mdr_second_cellsource * S ((S ((mdr_u_second_cell) * (w) + (mdr_v_second_cell))) * c) + (z)))))))) /\ (((exists ff_h_mdr_second_output. ff_h_mdr_second_output + S (z) = S ((S (i)) * vc)) /\ exists ff_q_mdr_second_output. vb = ff_q_mdr_second_output * S ((S (i)) * vc) + (z))))
  26. 0026specialize hsecond (i)
  27. 0027apply hsecond
  28. 0028exact hi
  29. 0029cases hright
  30. 0030cases hright_witness
  31. 0031have hvalues : x = x1
  32. 0032specialize matrix_rank_selected_point_functional (b)
  33. 0033specialize matrix_rank_selected_point_functional (c)
  34. 0034specialize matrix_rank_selected_point_functional (w)
  35. 0035specialize matrix_rank_selected_point_functional (rb)
  36. 0036specialize matrix_rank_selected_point_functional (rc)
  37. 0037specialize matrix_rank_selected_point_functional (cb)
  38. 0038specialize matrix_rank_selected_point_functional (cc)
  39. 0039specialize matrix_rank_selected_point_functional (q)
  40. 0040specialize matrix_rank_selected_point_functional (i)
  41. 0041specialize matrix_rank_selected_point_functional (x)
  42. 0042specialize matrix_rank_selected_point_functional (x1)
  43. 0043apply matrix_rank_selected_point_functional
  44. 0044exact hleft_witness_left
  45. 0045exact hright_witness_left
  46. 0046have houtput : a = x1
  47. 0047trans x
  48. 0048specialize beta_at_unique (ub)
  49. 0049specialize beta_at_unique (uc)
  50. 0050specialize beta_at_unique (i)
  51. 0051specialize beta_at_unique (a)
  52. 0052specialize beta_at_unique (x)
  53. 0053apply beta_at_unique
  54. 0054exact ha
  55. 0055exact hleft_witness_right
  56. 0056exact hvalues
  57. 0057rewrite houtput
  58. 0058rewrite houtput
  59. 0059exact hright_witness_right