DL00B0

matrix_lattice_identity_selected_natural

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

Selecting every actual row and column with the identity beta prefix yields exactly the original natural matrix code, by genuine row-major index arithmetic.

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 d ib ic. ~(d = 0) -> (forall mdr_i_natural_identity. (exists mdr_gap_natural_identitybound. mdr_gap_natural_identitybound + S (mdr_i_natural_identity) = (d)) -> (((exists ff_h_mdr_natural_identityentry. ff_h_mdr_natural_identityentry + S (mdr_i_natural_identity) = S ((S (mdr_i_natural_identity)) * ic)) /\ exists ff_q_mdr_natural_identityentry. ib = ff_q_mdr_natural_identityentry * S ((S (mdr_i_natural_identity)) * ic) + (mdr_i_natural_identity)))) -> (forall mdr_i_identity_selected_natural. (exists mdr_gap_identity_selected_naturalbound. mdr_gap_identity_selected_naturalbound + S (mdr_i_identity_selected_natural) = (d * d)) -> exists mdr_a_identity_selected_natural. (((exists mdr_r_identity_selected_naturalpoint mdr_s_identity_selected_naturalpoint mdr_u_identity_selected_naturalpoint mdr_v_identity_selected_naturalpoint. ((mdr_i_identity_selected_natural = (d) * mdr_r_identity_selected_naturalpoint + mdr_s_identity_selected_naturalpoint) /\ ((exists mdr_gap_identity_selected_naturalpointcolumn. mdr_gap_identity_selected_naturalpointcolumn + S (mdr_s_identity_selected_naturalpoint) = (d)) /\ ((((exists ff_h_mdr_identity_selected_naturalpointrow_index. ff_h_mdr_identity_selected_naturalpointrow_index + S (mdr_u_identity_selected_naturalpoint) = S ((S (mdr_r_identity_selected_naturalpoint)) * ic)) /\ exists ff_q_mdr_identity_selected_naturalpointrow_index. ib = ff_q_mdr_identity_selected_naturalpointrow_index * S ((S (mdr_r_identity_selected_naturalpoint)) * ic) + (mdr_u_identity_selected_naturalpoint))) /\ ((((exists ff_h_mdr_identity_selected_naturalpointcolumn_index. ff_h_mdr_identity_selected_naturalpointcolumn_index + S (mdr_v_identity_selected_naturalpoint) = S ((S (mdr_s_identity_selected_naturalpoint)) * ic)) /\ exists ff_q_mdr_identity_selected_naturalpointcolumn_index. ib = ff_q_mdr_identity_selected_naturalpointcolumn_index * S ((S (mdr_s_identity_selected_naturalpoint)) * ic) + (mdr_v_identity_selected_naturalpoint))) /\ (((exists ff_h_mdr_identity_selected_naturalpointsource. ff_h_mdr_identity_selected_naturalpointsource + S (mdr_a_identity_selected_natural) = S ((S ((mdr_u_identity_selected_naturalpoint) * (d) + (mdr_v_identity_selected_naturalpoint))) * c)) /\ exists ff_q_mdr_identity_selected_naturalpointsource. b = ff_q_mdr_identity_selected_naturalpointsource * S ((S ((mdr_u_identity_selected_naturalpoint) * (d) + (mdr_v_identity_selected_naturalpoint))) * c) + (mdr_a_identity_selected_natural)))))))) /\ (((exists ff_h_mdr_identity_selected_naturaloutput. ff_h_mdr_identity_selected_naturaloutput + S (mdr_a_identity_selected_natural) = S ((S (mdr_i_identity_selected_natural)) * c)) /\ exists ff_q_mdr_identity_selected_naturaloutput. b = ff_q_mdr_identity_selected_naturaloutput * S ((S (mdr_i_identity_selected_natural)) * c) + (mdr_a_identity_selected_natural))))))

Constructive proof overview

Generated structural guide

Selecting every actual row and column with the identity beta prefix yields exactly the original natural matrix code, by genuine row-major index arithmetic.

The unchanged tactic script uses 4 declared prerequisites and contains 60 exact native proof lines.

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

Proof neighborhood

Direct dependencies

division_remainder_exists Stable theorem; checked-use authorized DL001B matrix_recursive_quotient_row_bound beta_at_exists Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized

Direct dependents

DL00B1 matrix_lattice_identity_selected_signed

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

60 script commands · 19 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 recursive quotient row bound
01Fix variables and assumptionsL1–9

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro ib
  5. L5
    intro ic
  6. L6
    intro hd
  7. L7
    intro hidentity
  8. L8
    intro i
  9. L9
    intro hi
02Establish hcoordinatesL10–14

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

  1. L10
    have hcoordinates : exists r s. i = d * r + s /\ (exists mdr_gap_identity_column. mdr_gap_identity_column + S (s) = (d))
  2. L11
    specialize division_remainder_exists (d)
  3. L12
    specialize division_remainder_exists (i)
  4. L13
    apply division_remainder_exists
  5. L14
    exact hd
03Separate the logical casesL15–17

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

  1. L15
    cases hcoordinates
  2. L16
    cases hcoordinates_witness
  3. L17
    cases hcoordinates_witness_witness
04Establish hrowL18–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix recursive quotient row bound.

  1. L18
    have hrow : exists mdr_gap_identity_row. mdr_gap_identity_row + S (x) = (d)
  2. L19
    specialize matrix_recursive_quotient_row_bound (d)
  3. L20
    specialize matrix_recursive_quotient_row_bound (i)
  4. L21
    specialize matrix_recursive_quotient_row_bound (x)
  5. L22
    specialize matrix_recursive_quotient_row_bound (x1)
  6. L23
    apply matrix_recursive_quotient_row_bound
  7. L24
    exact hcoordinates_witness_witness_left
  8. L25
    exact hi
05Establish hvalueL26–30

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

  1. L26
    have hvalue : exists a. ((exists ff_h_mdr_identity_parent_value. ff_h_mdr_identity_parent_value + S (a) = S ((S (i)) * c)) /\ exists ff_q_mdr_identity_parent_value. b = ff_q_mdr_identity_parent_value * S ((S (i)) * c) + (a))
  2. L27
    specialize beta_at_exists (b)
  3. L28
    specialize beta_at_exists (c)
  4. L29
    specialize beta_at_exists (i)
  5. L30
    apply beta_at_exists
06Separate the logical casesL31–31

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

  1. L31
    cases hvalue
07Construct an explicit witnessL32–32

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

  1. L32
    exists x2
08Separate the logical casesL33–33

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

  1. L33
    split
09Construct an explicit witnessL34–37

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

  1. L34
    exists x
  2. L35
    exists x1
  3. L36
    exists x
  4. L37
    exists x1
10Separate the logical casesL38–38

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

  1. L38
    split
11Use earlier factsL39–39

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

  1. L39
    exact hcoordinates_witness_witness_left
12Separate the logical casesL40–40

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

  1. L40
    split
13Use earlier factsL41–41

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

  1. L41
    exact hcoordinates_witness_witness_right
14Separate the logical casesL42–42

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

  1. L42
    split
15Use earlier factsL43–45

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

  1. L43
    specialize hidentity (x)
  2. L44
    apply hidentity
  3. L45
    exact hrow
16Separate the logical casesL46–46

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

  1. L46
    split
17Use earlier factsL47–49

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

  1. L47
    specialize hidentity (x1)
  2. L48
    apply hidentity
  3. L49
    exact hcoordinates_witness_witness_right
18Establish hsourceL50–59

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

  1. L50
    have hsource : x * d + x1 = i
  2. L51
    trans d * x + x1
  3. L52
    congr
  4. L53
    apply mul_comm
  5. L54
    refl
  6. L55
    symm
  7. L56
    exact hcoordinates_witness_witness_left
  8. L57
    rewrite hsource
  9. L58
    rewrite hsource
  10. L59
    exact hvalue_witness
19Use earlier factsL60–60

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

  1. L60
    exact hvalue_witness

Library-wide reading audit

Original exact command ledger · 60 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro ib
  5. 0005intro ic
  6. 0006intro hd
  7. 0007intro hidentity
  8. 0008intro i
  9. 0009intro hi
  10. 0010have hcoordinates : exists r s. i = d * r + s /\ (exists mdr_gap_identity_column. mdr_gap_identity_column + S (s) = (d))
  11. 0011specialize division_remainder_exists (d)
  12. 0012specialize division_remainder_exists (i)
  13. 0013apply division_remainder_exists
  14. 0014exact hd
  15. 0015cases hcoordinates
  16. 0016cases hcoordinates_witness
  17. 0017cases hcoordinates_witness_witness
  18. 0018have hrow : exists mdr_gap_identity_row. mdr_gap_identity_row + S (x) = (d)
  19. 0019specialize matrix_recursive_quotient_row_bound (d)
  20. 0020specialize matrix_recursive_quotient_row_bound (i)
  21. 0021specialize matrix_recursive_quotient_row_bound (x)
  22. 0022specialize matrix_recursive_quotient_row_bound (x1)
  23. 0023apply matrix_recursive_quotient_row_bound
  24. 0024exact hcoordinates_witness_witness_left
  25. 0025exact hi
  26. 0026have hvalue : exists a. ((exists ff_h_mdr_identity_parent_value. ff_h_mdr_identity_parent_value + S (a) = S ((S (i)) * c)) /\ exists ff_q_mdr_identity_parent_value. b = ff_q_mdr_identity_parent_value * S ((S (i)) * c) + (a))
  27. 0027specialize beta_at_exists (b)
  28. 0028specialize beta_at_exists (c)
  29. 0029specialize beta_at_exists (i)
  30. 0030apply beta_at_exists
  31. 0031cases hvalue
  32. 0032exists x2
  33. 0033split
  34. 0034exists x
  35. 0035exists x1
  36. 0036exists x
  37. 0037exists x1
  38. 0038split
  39. 0039exact hcoordinates_witness_witness_left
  40. 0040split
  41. 0041exact hcoordinates_witness_witness_right
  42. 0042split
  43. 0043specialize hidentity (x)
  44. 0044apply hidentity
  45. 0045exact hrow
  46. 0046split
  47. 0047specialize hidentity (x1)
  48. 0048apply hidentity
  49. 0049exact hcoordinates_witness_witness_right
  50. 0050have hsource : x * d + x1 = i
  51. 0051trans d * x + x1
  52. 0052congr
  53. 0053apply mul_comm
  54. 0054refl
  55. 0055symm
  56. 0056exact hcoordinates_witness_witness_left
  57. 0057rewrite hsource
  58. 0058rewrite hsource
  59. 0059exact hvalue_witness
  60. 0060exact hvalue_witness