DL00B0

matrix_lattice_identity_selected_natural

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

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

∀ b. ∀ c. ∀ d. ∀ ib. ∀ ic. ¬d = 0 → IdentityMatrixSelector(ib,ic,d) → ∀ x. Lt(x,d · d) → ∃ y. (∃ z. ∃ n. ∃ m. ∃ k. x = d · z + n ∧ (Lt(n,d) ∧ (BetaAt(ib,ic,z,m) ∧ (BetaAt(ib,ic,n,k) ∧ BetaAt(b,c,m · d + k,y))))) ∧ BetaAt(b,c,x,y)

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

Definition DAG

IdentityMatrixSelector(b,c,l) · 1Lt(a,b) · 4BetaAt(b,c,i,x) · 5

Actual proof prerequisites

division_remainder_exists · checked external prerequisitematrix_recursive_quotient_row_boundbeta_at_exists · checked external prerequisitemul_comm · checked external prerequisite
Original expanded first-order 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))))))

Complete tactic proof in conservative notation

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

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.

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 (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 : ∃ r. ∃ s. i = d · r + s ∧ Lt(s,d)Definitions: Lt(s,d)Original native command in the exact edition
  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
  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 : ∃ a. BetaAt(b,c,i,a)Definitions: BetaAt(b,c,i,a)Original native command in the exact edition
  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 defined 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 : ∃ r. ∃ s. i = d · r + s ∧ Lt(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 : Lt(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 : ∃ a. BetaAt(b,c,i,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