DL0046

matrix_rank_signed_selected_square_exists

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

Construct both genuine natural-component streams of an arbitrary signed selected square matrix.

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 pb pc nb nc w rb rc cb cc q. exists ub uc vb vc. (((forall mdr_i_signed_square_existspositive. (exists mdr_gap_signed_square_existspositivebound. mdr_gap_signed_square_existspositivebound + S (mdr_i_signed_square_existspositive) = ((q) * (q))) -> exists mdr_a_signed_square_existspositive. (((exists mdr_r_signed_square_existspositivepoint mdr_s_signed_square_existspositivepoint mdr_u_signed_square_existspositivepoint mdr_v_signed_square_existspositivepoint. ((mdr_i_signed_square_existspositive = (q) * mdr_r_signed_square_existspositivepoint + mdr_s_signed_square_existspositivepoint) /\ ((exists mdr_gap_signed_square_existspositivepointcolumn. mdr_gap_signed_square_existspositivepointcolumn + S (mdr_s_signed_square_existspositivepoint) = (q)) /\ ((((exists ff_h_mdr_signed_square_existspositivepointrow_index. ff_h_mdr_signed_square_existspositivepointrow_index + S (mdr_u_signed_square_existspositivepoint) = S ((S (mdr_r_signed_square_existspositivepoint)) * rc)) /\ exists ff_q_mdr_signed_square_existspositivepointrow_index. rb = ff_q_mdr_signed_square_existspositivepointrow_index * S ((S (mdr_r_signed_square_existspositivepoint)) * rc) + (mdr_u_signed_square_existspositivepoint))) /\ ((((exists ff_h_mdr_signed_square_existspositivepointcolumn_index. ff_h_mdr_signed_square_existspositivepointcolumn_index + S (mdr_v_signed_square_existspositivepoint) = S ((S (mdr_s_signed_square_existspositivepoint)) * cc)) /\ exists ff_q_mdr_signed_square_existspositivepointcolumn_index. cb = ff_q_mdr_signed_square_existspositivepointcolumn_index * S ((S (mdr_s_signed_square_existspositivepoint)) * cc) + (mdr_v_signed_square_existspositivepoint))) /\ (((exists ff_h_mdr_signed_square_existspositivepointsource. ff_h_mdr_signed_square_existspositivepointsource + S (mdr_a_signed_square_existspositive) = S ((S ((mdr_u_signed_square_existspositivepoint) * (w) + (mdr_v_signed_square_existspositivepoint))) * pc)) /\ exists ff_q_mdr_signed_square_existspositivepointsource. pb = ff_q_mdr_signed_square_existspositivepointsource * S ((S ((mdr_u_signed_square_existspositivepoint) * (w) + (mdr_v_signed_square_existspositivepoint))) * pc) + (mdr_a_signed_square_existspositive)))))))) /\ (((exists ff_h_mdr_signed_square_existspositiveoutput. ff_h_mdr_signed_square_existspositiveoutput + S (mdr_a_signed_square_existspositive) = S ((S (mdr_i_signed_square_existspositive)) * uc)) /\ exists ff_q_mdr_signed_square_existspositiveoutput. ub = ff_q_mdr_signed_square_existspositiveoutput * S ((S (mdr_i_signed_square_existspositive)) * uc) + (mdr_a_signed_square_existspositive)))))) /\ (forall mdr_i_signed_square_existsnegative. (exists mdr_gap_signed_square_existsnegativebound. mdr_gap_signed_square_existsnegativebound + S (mdr_i_signed_square_existsnegative) = ((q) * (q))) -> exists mdr_a_signed_square_existsnegative. (((exists mdr_r_signed_square_existsnegativepoint mdr_s_signed_square_existsnegativepoint mdr_u_signed_square_existsnegativepoint mdr_v_signed_square_existsnegativepoint. ((mdr_i_signed_square_existsnegative = (q) * mdr_r_signed_square_existsnegativepoint + mdr_s_signed_square_existsnegativepoint) /\ ((exists mdr_gap_signed_square_existsnegativepointcolumn. mdr_gap_signed_square_existsnegativepointcolumn + S (mdr_s_signed_square_existsnegativepoint) = (q)) /\ ((((exists ff_h_mdr_signed_square_existsnegativepointrow_index. ff_h_mdr_signed_square_existsnegativepointrow_index + S (mdr_u_signed_square_existsnegativepoint) = S ((S (mdr_r_signed_square_existsnegativepoint)) * rc)) /\ exists ff_q_mdr_signed_square_existsnegativepointrow_index. rb = ff_q_mdr_signed_square_existsnegativepointrow_index * S ((S (mdr_r_signed_square_existsnegativepoint)) * rc) + (mdr_u_signed_square_existsnegativepoint))) /\ ((((exists ff_h_mdr_signed_square_existsnegativepointcolumn_index. ff_h_mdr_signed_square_existsnegativepointcolumn_index + S (mdr_v_signed_square_existsnegativepoint) = S ((S (mdr_s_signed_square_existsnegativepoint)) * cc)) /\ exists ff_q_mdr_signed_square_existsnegativepointcolumn_index. cb = ff_q_mdr_signed_square_existsnegativepointcolumn_index * S ((S (mdr_s_signed_square_existsnegativepoint)) * cc) + (mdr_v_signed_square_existsnegativepoint))) /\ (((exists ff_h_mdr_signed_square_existsnegativepointsource. ff_h_mdr_signed_square_existsnegativepointsource + S (mdr_a_signed_square_existsnegative) = S ((S ((mdr_u_signed_square_existsnegativepoint) * (w) + (mdr_v_signed_square_existsnegativepoint))) * nc)) /\ exists ff_q_mdr_signed_square_existsnegativepointsource. nb = ff_q_mdr_signed_square_existsnegativepointsource * S ((S ((mdr_u_signed_square_existsnegativepoint) * (w) + (mdr_v_signed_square_existsnegativepoint))) * nc) + (mdr_a_signed_square_existsnegative)))))))) /\ (((exists ff_h_mdr_signed_square_existsnegativeoutput. ff_h_mdr_signed_square_existsnegativeoutput + S (mdr_a_signed_square_existsnegative) = S ((S (mdr_i_signed_square_existsnegative)) * vc)) /\ exists ff_q_mdr_signed_square_existsnegativeoutput. vb = ff_q_mdr_signed_square_existsnegativeoutput * S ((S (mdr_i_signed_square_existsnegative)) * vc) + (mdr_a_signed_square_existsnegative))))))))

Constructive proof overview

Generated structural guide

Construct both genuine natural-component streams of an arbitrary signed selected square matrix.

The unchanged tactic script uses 1 declared prerequisite and contains 41 exact native proof lines.

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

Proof neighborhood

Direct dependencies

DL0045 matrix_rank_selected_square_exists

Direct dependents

DL0049 matrix_rank_selected_determinant_exists

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

41 script commands · 8 reading checkpoints · 2 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 square exists

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 pb
  2. L2
    intro pc
  3. L3
    intro nb
  4. L4
    intro nc
  5. L5
    intro w
  6. L6
    intro rb
  7. L7
    intro rc
  8. L8
    intro cb
  9. L9
    intro cc
  10. L10
    intro q
02Establish hpositiveL11–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix rank selected square exists.

  1. L11
    have hpositive : ∃ u. ∃ v. ∀ mdr_i_positive_exists. Lt(mdr_i_positive_exists,q · q) → ∃ x. (∃ y. ∃ z. ∃ n. ∃ m. mdr_i_positive_exists = q · y + z ∧ (Lt(z,q) ∧ (BetaAt(rb,rc,y,n) ∧ (BetaAt(cb,cc,z,m) ∧ BetaAt(pb,pc,n · w + m,x))))) ∧ BetaAt(u,v,mdr_i_positive_exists,x)Definitions: LtBetaAt
  2. L12
    specialize matrix_rank_selected_square_exists (pb)
  3. L13
    specialize matrix_rank_selected_square_exists (pc)
  4. L14
    specialize matrix_rank_selected_square_exists (w)
  5. L15
    specialize matrix_rank_selected_square_exists (rb)
  6. L16
    specialize matrix_rank_selected_square_exists (rc)
  7. L17
    specialize matrix_rank_selected_square_exists (cb)
  8. L18
    specialize matrix_rank_selected_square_exists (cc)
  9. L19
    specialize matrix_rank_selected_square_exists (q)
  10. L20
    apply matrix_rank_selected_square_exists
03Separate the logical casesL21–22

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

  1. L21
    cases hpositive
  2. L22
    cases hpositive_witness
04Establish hnegativeL23–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix rank selected square exists.

  1. L23
    have hnegative : ∃ u. ∃ v. ∀ mdr_i_negative_exists. Lt(mdr_i_negative_exists,q · q) → ∃ x. (∃ y. ∃ z. ∃ n. ∃ m. mdr_i_negative_exists = q · y + z ∧ (Lt(z,q) ∧ (BetaAt(rb,rc,y,n) ∧ (BetaAt(cb,cc,z,m) ∧ BetaAt(nb,nc,n · w + m,x))))) ∧ BetaAt(u,v,mdr_i_negative_exists,x)Definitions: LtBetaAt
  2. L24
    specialize matrix_rank_selected_square_exists (nb)
  3. L25
    specialize matrix_rank_selected_square_exists (nc)
  4. L26
    specialize matrix_rank_selected_square_exists (w)
  5. L27
    specialize matrix_rank_selected_square_exists (rb)
  6. L28
    specialize matrix_rank_selected_square_exists (rc)
  7. L29
    specialize matrix_rank_selected_square_exists (cb)
  8. L30
    specialize matrix_rank_selected_square_exists (cc)
  9. L31
    specialize matrix_rank_selected_square_exists (q)
  10. L32
    apply matrix_rank_selected_square_exists
05Separate the logical casesL33–34

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

  1. L33
    cases hnegative
  2. L34
    cases hnegative_witness
06Construct an explicit witnessL35–38

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

  1. L35
    exists x
  2. L36
    exists x1
  3. L37
    exists x2
  4. L38
    exists x3
07Separate the logical casesL39–39

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

  1. L39
    split
08Use earlier factsL40–41

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

  1. L40
    exact hpositive_witness_witness
  2. L41
    exact hnegative_witness_witness

Library-wide reading audit

Original exact command ledger · 41 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro w
  6. 0006intro rb
  7. 0007intro rc
  8. 0008intro cb
  9. 0009intro cc
  10. 0010intro q
  11. 0011have hpositive : exists u v. forall mdr_i_positive_exists. (exists mdr_gap_positive_existsbound. mdr_gap_positive_existsbound + S (mdr_i_positive_exists) = (q * q)) -> exists mdr_a_positive_exists. (((exists mdr_r_positive_existspoint mdr_s_positive_existspoint mdr_u_positive_existspoint mdr_v_positive_existspoint. ((mdr_i_positive_exists = (q) * mdr_r_positive_existspoint + mdr_s_positive_existspoint) /\ ((exists mdr_gap_positive_existspointcolumn. mdr_gap_positive_existspointcolumn + S (mdr_s_positive_existspoint) = (q)) /\ ((((exists ff_h_mdr_positive_existspointrow_index. ff_h_mdr_positive_existspointrow_index + S (mdr_u_positive_existspoint) = S ((S (mdr_r_positive_existspoint)) * rc)) /\ exists ff_q_mdr_positive_existspointrow_index. rb = ff_q_mdr_positive_existspointrow_index * S ((S (mdr_r_positive_existspoint)) * rc) + (mdr_u_positive_existspoint))) /\ ((((exists ff_h_mdr_positive_existspointcolumn_index. ff_h_mdr_positive_existspointcolumn_index + S (mdr_v_positive_existspoint) = S ((S (mdr_s_positive_existspoint)) * cc)) /\ exists ff_q_mdr_positive_existspointcolumn_index. cb = ff_q_mdr_positive_existspointcolumn_index * S ((S (mdr_s_positive_existspoint)) * cc) + (mdr_v_positive_existspoint))) /\ (((exists ff_h_mdr_positive_existspointsource. ff_h_mdr_positive_existspointsource + S (mdr_a_positive_exists) = S ((S ((mdr_u_positive_existspoint) * (w) + (mdr_v_positive_existspoint))) * pc)) /\ exists ff_q_mdr_positive_existspointsource. pb = ff_q_mdr_positive_existspointsource * S ((S ((mdr_u_positive_existspoint) * (w) + (mdr_v_positive_existspoint))) * pc) + (mdr_a_positive_exists)))))))) /\ (((exists ff_h_mdr_positive_existsoutput. ff_h_mdr_positive_existsoutput + S (mdr_a_positive_exists) = S ((S (mdr_i_positive_exists)) * v)) /\ exists ff_q_mdr_positive_existsoutput. u = ff_q_mdr_positive_existsoutput * S ((S (mdr_i_positive_exists)) * v) + (mdr_a_positive_exists)))))
  12. 0012specialize matrix_rank_selected_square_exists (pb)
  13. 0013specialize matrix_rank_selected_square_exists (pc)
  14. 0014specialize matrix_rank_selected_square_exists (w)
  15. 0015specialize matrix_rank_selected_square_exists (rb)
  16. 0016specialize matrix_rank_selected_square_exists (rc)
  17. 0017specialize matrix_rank_selected_square_exists (cb)
  18. 0018specialize matrix_rank_selected_square_exists (cc)
  19. 0019specialize matrix_rank_selected_square_exists (q)
  20. 0020apply matrix_rank_selected_square_exists
  21. 0021cases hpositive
  22. 0022cases hpositive_witness
  23. 0023have hnegative : exists u v. forall mdr_i_negative_exists. (exists mdr_gap_negative_existsbound. mdr_gap_negative_existsbound + S (mdr_i_negative_exists) = (q * q)) -> exists mdr_a_negative_exists. (((exists mdr_r_negative_existspoint mdr_s_negative_existspoint mdr_u_negative_existspoint mdr_v_negative_existspoint. ((mdr_i_negative_exists = (q) * mdr_r_negative_existspoint + mdr_s_negative_existspoint) /\ ((exists mdr_gap_negative_existspointcolumn. mdr_gap_negative_existspointcolumn + S (mdr_s_negative_existspoint) = (q)) /\ ((((exists ff_h_mdr_negative_existspointrow_index. ff_h_mdr_negative_existspointrow_index + S (mdr_u_negative_existspoint) = S ((S (mdr_r_negative_existspoint)) * rc)) /\ exists ff_q_mdr_negative_existspointrow_index. rb = ff_q_mdr_negative_existspointrow_index * S ((S (mdr_r_negative_existspoint)) * rc) + (mdr_u_negative_existspoint))) /\ ((((exists ff_h_mdr_negative_existspointcolumn_index. ff_h_mdr_negative_existspointcolumn_index + S (mdr_v_negative_existspoint) = S ((S (mdr_s_negative_existspoint)) * cc)) /\ exists ff_q_mdr_negative_existspointcolumn_index. cb = ff_q_mdr_negative_existspointcolumn_index * S ((S (mdr_s_negative_existspoint)) * cc) + (mdr_v_negative_existspoint))) /\ (((exists ff_h_mdr_negative_existspointsource. ff_h_mdr_negative_existspointsource + S (mdr_a_negative_exists) = S ((S ((mdr_u_negative_existspoint) * (w) + (mdr_v_negative_existspoint))) * nc)) /\ exists ff_q_mdr_negative_existspointsource. nb = ff_q_mdr_negative_existspointsource * S ((S ((mdr_u_negative_existspoint) * (w) + (mdr_v_negative_existspoint))) * nc) + (mdr_a_negative_exists)))))))) /\ (((exists ff_h_mdr_negative_existsoutput. ff_h_mdr_negative_existsoutput + S (mdr_a_negative_exists) = S ((S (mdr_i_negative_exists)) * v)) /\ exists ff_q_mdr_negative_existsoutput. u = ff_q_mdr_negative_existsoutput * S ((S (mdr_i_negative_exists)) * v) + (mdr_a_negative_exists)))))
  24. 0024specialize matrix_rank_selected_square_exists (nb)
  25. 0025specialize matrix_rank_selected_square_exists (nc)
  26. 0026specialize matrix_rank_selected_square_exists (w)
  27. 0027specialize matrix_rank_selected_square_exists (rb)
  28. 0028specialize matrix_rank_selected_square_exists (rc)
  29. 0029specialize matrix_rank_selected_square_exists (cb)
  30. 0030specialize matrix_rank_selected_square_exists (cc)
  31. 0031specialize matrix_rank_selected_square_exists (q)
  32. 0032apply matrix_rank_selected_square_exists
  33. 0033cases hnegative
  34. 0034cases hnegative_witness
  35. 0035exists x
  36. 0036exists x1
  37. 0037exists x2
  38. 0038exists x3
  39. 0039split
  40. 0040exact hpositive_witness_witness
  41. 0041exact hnegative_witness_witness