DL0047

matrix_rank_selected_prefix_functional

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

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. ∀ w. ∀ rb. ∀ rc. ∀ cb. ∀ cc. ∀ q. ∀ ub. ∀ uc. ∀ vb. ∀ vc. (∀ x. Lt(x,q · q) → ∃ y. (∃ z. ∃ n. ∃ m. ∃ k. x = q · z + n ∧ (Lt(n,q) ∧ (BetaAt(rb,rc,z,m) ∧ (BetaAt(cb,cc,n,k) ∧ BetaAt(b,c,m · w + k,y))))) ∧ BetaAt(ub,uc,x,y)) → (∀ x. Lt(x,q · q) → ∃ y. (∃ z. ∃ n. ∃ m. ∃ k. x = q · z + n ∧ (Lt(n,q) ∧ (BetaAt(rb,rc,z,m) ∧ (BetaAt(cb,cc,n,k) ∧ BetaAt(b,c,m · w + k,y))))) ∧ BetaAt(vb,vc,x,y)) → ∀ x. ∀ y. Lt(x,q · q) → BetaAt(ub,uc,x,y) → BetaAt(vb,vc,x,y)

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

Definition DAG

Lt(a,b) · 7BetaAt(b,c,i,x) · 18

Actual proof prerequisites

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

Complete tactic proof in conservative notation

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

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.

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 rank selected point functional
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: 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)Original native command in the exact edition
  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: 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)Original native command in the exact edition
  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 defined 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 : ∃ 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)
  20. 0020specialize hfirst (i)
  21. 0021apply hfirst
  22. 0022exact hi
  23. 0023cases hleft
  24. 0024cases hleft_witness
  25. 0025have 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)
  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